Sudoku Programmers Forum Index

 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister   ProfileProfile   Log inLog in          Games  Calendar

Log in to check your private messagesLog in to check your private messages   

Ultracolouring
Goto page Previous  1, 2, 3, 4  Next
 
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Solving sudoku
View previous topic :: View next topic  
Author Message
DHallman

Joined: 09 Aug 2005
Posts: 24
:
Location: Inglewood, CA 90302 USA

Items
PostPosted: Fri Sep 09, 2005 11:26 pm    Post subject: Reply with quote

angusj wrote:
There are 3 ways to use Simple Coloring that I'm aware of:

3. Candidates for an entire group also group with cells of the same conjugate color


In each of these examples the candidate in the selected cells can be excluded.


Angus,

I do not understand the significance of A B & C.

From the three cells colored, how do you deduce Green is false?

What is meant by "Candidates for an entire group also group with cells of the same conjugate color"?

Because of my ignorance, please elucidate Sad
Back to top
View user's profile Send private message Send e-mail
angusj
Site Admin
Joined: 18 Jun 2005
Posts: 406
:

Items
PostPosted: Fri Sep 09, 2005 11:42 pm    Post subject: Reply with quote

DHallman wrote:
I do not understand the significance of A B & C.

One cell from that group (column 5) must be 'true' (be the 9), so one of A, B or C must be true. Because 'green' shares a group with each of A,B & C it can't be the 'true' colour (because there can't be two 'true's in a group).


DHallman wrote:
Because of my ignorance, please elucidate Sad

I consider genuine ignorance as not knowing when you don't know (ie you think you know when you don't). You, evidently don't fall into that category. Very Happy
Back to top
View user's profile Send private message Visit poster's website
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Thu Sep 15, 2005 11:41 pm    Post subject: Reply with quote

Theoretically, ultracolouring should now be able to solve any puzzle that trebor's tables can, because it is based on exactly the same deuctive principles.

But there is still a small number of puzzles - like "toughest" that tabling solves but ultracolouring can't. It seemed a simple idea to do a back-to-back test by putting this puzzle into both solvers and compare the detail transcript but it turned out to be harder than expected. It's quite hard to get them into exactly the same starting state and to compare their detailed behaviours. It didn't help that I found that I was using a slightly different version of "toughest".

Here's examples of the differences I've found.

Assuming that we agree "toughest" is
Code:

+-------+-------+-------+
| . . . | . 7 . | 9 4 . |
| . 7 . | . 9 . | . . 5 |
| 3 . . | . . 5 | . 7 . |
+-------+-------+-------+
| . 8 7 | 4 . . | 1 . . |
| 4 6 3 | . . . | . . . |
| . . . | . . 7 | . 8 . |
+-------+-------+-------+
| 8 . . | 7 . . | . . . |
| 7 . . | . . . | . 2 8 |
| . 5 . | 2 6 8 | . . . |
+-------+-------+-------+

and get it to the common state
Code:

1256  12    1258  ¦ 1368  7     1236  ¦ 9     4     1236 
126   7     1248  ¦ 1368  9     12346 ¦ 2368  136   5     
3     1249  12489 ¦ 168   1248  5     ¦ 268   7     126   
------------------+-------------------+-------------------
259   8     7     ¦ 4     235   2369  ¦ 1     3569  2369 
4     6     3     ¦ 1589  1258  129   ¦ 257   59    279   
1259  129   1259  ¦ 3569  235   7     ¦ 23456 8     23469
------------------+-------------------+-------------------
8     12349 12469 ¦ 7     1345  1349  ¦ 456   1569  1469 
7     1349  1469  ¦ 1359  1345  1349  ¦ 456   2     8     
19    5     149   ¦ 2     6     8     ¦ 347   139   13479

Tabling asserts that
Code:

R1C3<>2 (Implied by all possible values of R1C3)

whereas ultracolouring only says
Code:

Verities in r1c3
r1c3=2 implies r1c3<>1
r1c3=5 implies r1c3<>1
r1c3=8 implies r1c3<>1

and is unable to say that r1c3=1 implies r1c3<>1 to complete the verity.

Tabling asserts that
Code:

R3C3<>2 (Implied by all possible values of R3C2)
R7C3<>9 (Implied by all possible values of R3C2)
R8C3<>9 (Implied by all possible values of R3C2)

whereas ultracolouring can say nothing about what r3c2=1, 2, 4 or 9 imply for r3c3, r7c3 or r8c3

The ultracolouring "blind spot" may lie somewhere in this different behaviour. Can Mad Overlord or anyone else explain to me the reasoning behind tabling's r1c3 and r3c2 verities above.

Yes, I have RTFM Smile

Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 12:30 am    Post subject: Reply with quote

I've messed up a couple of postings, so I'm editing them.

One thing to keep in mind when using the Susser to table is that after you table the puzzle using the deducer, if you then UNDO to get the pre-tabling state back, you can still mouse over a square and hit "t" to get the full tabling output for that square.


Last edited by MadOverlord on Fri Sep 16, 2005 12:35 am; edited 1 time in total
Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 12:31 am    Post subject: Reply with quote

Here are the complete tabling results for R1C3; likely the issue is related to the invalid assertions. Note that once I prove R1C3=1 is invalid, I can make verities using only R1C3=2,5,8, and so on.


Code:

Invalid assertion R1C3=1 implies:
  R1C2=2 (invalid assertion: R1C3=1 forces R1C2=2)
  R1C1=5 (R1C3=1 row pins R1C1=5)
  R1C4=8 (R1C3=1 row pins R1C4=8)
  R6C3=5 (R1C3=1 column pins R6C3=5)
  R7C3=2 (R1C3=1 column pins R7C3=2)
  R2C1=6 (R1C3=1 forces R2C1=6)
  R8C3=6 (R1C3=1 column pins R8C3=6)
  R1C3<>2 (R1C3=1 implies R1C3<>2)
  R1C3<>5 (R1C3=1 implies R1C3<>5)
  R1C3<>8 (R1C3=1 implies R1C3<>8)
  R1C1<>1 (R1C3=1 indirectly implies R1C1<>1)
  R1C1<>2 (R1C3=1 indirectly implies R1C1<>2)
  R1C1<>6 (R1C3=1 indirectly implies R1C1<>6)
  R1C2<>1 (R1C3=1 indirectly implies R1C2<>1)
  R1C4<>1 (R1C3=1 indirectly implies R1C4<>1)
  R1C4<>3 (R1C3=1 indirectly implies R1C4<>3)
  R1C4<>6 (R1C3=1 indirectly implies R1C4<>6)
  R1C6<>1 (R1C3=1 indirectly implies R1C6<>1)
  R1C6<>2 (R1C3=1 indirectly implies R1C6<>2)
  R1C9<>1 (R1C3=1 indirectly implies R1C9<>1)
  R1C9<>2 (R1C3=1 indirectly implies R1C9<>2)
  R2C3<>1 (R1C3=1 indirectly implies R2C3<>1)
  R2C3<>2 (R1C3=1 indirectly implies R2C3<>2)
  R3C3<>1 (R1C3=1 indirectly implies R3C3<>1)
  R3C3<>2 (R1C3=1 indirectly implies R3C3<>2)
  R6C3<>1 (R1C3=1 indirectly implies R6C3<>1)
  R6C3<>2 (R1C3=1 indirectly implies R6C3<>2)
  R6C3<>9 (R1C3=1 indirectly implies R6C3<>9)
  R7C3<>1 (R1C3=1 indirectly implies R7C3<>1)
  R7C3<>4 (R1C3=1 indirectly implies R7C3<>4)
  R7C3<>6 (R1C3=1 indirectly implies R7C3<>6)
  R7C3<>9 (R1C3=1 indirectly implies R7C3<>9)
  R8C3<>1 (R1C3=1 indirectly implies R8C3<>1)
  R8C3<>4 (R1C3=1 indirectly implies R8C3<>4)
  R8C3<>9 (R1C3=1 indirectly implies R8C3<>9)
  R9C3<>1 (R1C3=1 indirectly implies R9C3<>1)
  R2C1<>1 (R1C3=1 indirectly implies R2C1<>1)
  R2C1<>2 (R1C3=1 indirectly implies R2C1<>2)
  R3C2<>1 (R1C3=1 indirectly implies R3C2<>1)
  R3C2<>2 (R1C3=1 indirectly implies R3C2<>2)
  R6C2<>2 (R1C3=1 forces R1C2=2; R1C2=2 indirectly implies R6C2<>2)
  R7C2<>2 (R1C3=1 forces R1C2=2; R1C2=2 indirectly implies R7C2<>2)
  R8C7<>6 (R1C3=1 forces R1C2=2; R1C2=2 implies R1C2<>1; R1C2<>1 indirectly implies R7C2<>2; R7C2<>2 block pins R8C3=6; R8C3=6 indirectly implies R8C7<>6)
  R4C1<>5 (R1C3=1 row pins R1C1=5; R1C1=5 indirectly implies R4C1<>5)
  R6C1<>5 (R1C3=1 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5)
  R2C4<>6 (R1C3=1 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C4<>6)
  R2C6<>6 (R1C3=1 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6)
  R2C7<>6 (R1C3=1 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C7<>6)
  R2C8<>6 (R1C3=1 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C8<>6)
  R6C4<>5 (R1C3=1 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5)
  R6C5<>5 (R1C3=1 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C5<>5)
  R6C7<>5 (R1C3=1 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5)
  R2C4<>8 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8)
  R3C4<>8 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R5C4<>8 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8)
  R3C5<>8 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R3C5<>8)
  R5C5=8 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8)
  R5C5<>1 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>1)
  R5C5<>2 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>2)
  R5C5<>5 (R1C3=1 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>5)

Invalid assertion R1C3=2 implies:
  R1C2=1 (R1C3=2 forces R1C2=1)
  R1C1=5 (R1C3=2 row pins R1C1=5)
  R1C4=8 (R1C3=2 row pins R1C4=8)
  R6C3=5 (R1C3=2 column pins R6C3=5)
  R2C1=6 (R1C3=2 forces R2C1=6)
  R1C3<>1 (R1C3=2 implies R1C3<>1)
  R1C3<>5 (R1C3=2 implies R1C3<>5)
  R1C3<>8 (R1C3=2 implies R1C3<>8)
  R1C1<>1 (R1C3=2 indirectly implies R1C1<>1)
  R1C1<>2 (R1C3=2 indirectly implies R1C1<>2)
  R1C1<>6 (R1C3=2 indirectly implies R1C1<>6)
  R1C2<>2 (R1C3=2 indirectly implies R1C2<>2)
  R1C4<>1 (R1C3=2 indirectly implies R1C4<>1)
  R1C4<>3 (R1C3=2 indirectly implies R1C4<>3)
  R1C4<>6 (R1C3=2 indirectly implies R1C4<>6)
  R1C6<>1 (R1C3=2 indirectly implies R1C6<>1)
  R1C6<>2 (R1C3=2 indirectly implies R1C6<>2)
  R1C9<>1 (R1C3=2 indirectly implies R1C9<>1)
  R1C9<>2 (R1C3=2 indirectly implies R1C9<>2)
  R2C3<>1 (R1C3=2 indirectly implies R2C3<>1)
  R2C3<>2 (R1C3=2 indirectly implies R2C3<>2)
  R3C3<>1 (R1C3=2 indirectly implies R3C3<>1)
  R3C3<>2 (R1C3=2 indirectly implies R3C3<>2)
  R6C3<>1 (R1C3=2 indirectly implies R6C3<>1)
  R6C3<>2 (R1C3=2 indirectly implies R6C3<>2)
  R6C3<>9 (R1C3=2 indirectly implies R6C3<>9)
  R7C3<>2 (R1C3=2 indirectly implies R7C3<>2)
  R2C1<>1 (R1C3=2 indirectly implies R2C1<>1)
  R2C1<>2 (R1C3=2 indirectly implies R2C1<>2)
  R3C2<>1 (R1C3=2 indirectly implies R3C2<>1)
  R3C2<>2 (R1C3=2 indirectly implies R3C2<>2)
  R6C2<>1 (R1C3=2 forces R1C2=1; R1C2=1 indirectly implies R6C2<>1)
  R7C2<>1 (R1C3=2 forces R1C2=1; R1C2=1 indirectly implies R7C2<>1)
  R8C2<>1 (R1C3=2 forces R1C2=1; R1C2=1 indirectly implies R8C2<>1)
  R4C1<>5 (R1C3=2 row pins R1C1=5; R1C1=5 indirectly implies R4C1<>5)
  R6C1<>5 (R1C3=2 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5)
  R2C4<>6 (R1C3=2 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C4<>6)
  R2C6<>6 (R1C3=2 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6)
  R2C7<>6 (R1C3=2 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C7<>6)
  R2C8<>6 (R1C3=2 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C8<>6)
  R6C4<>5 (R1C3=2 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5)
  R6C5<>5 (R1C3=2 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C5<>5)
  R6C7<>5 (R1C3=2 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5)
  R2C4<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8)
  R3C4<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R5C4<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8)
  R3C5<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R3C5<>8)
  R7C2=2 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2)
  R8C2=3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 block pins R8C2=3)
  R7C2<>3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 indirectly implies R7C2<>3)
  R7C2<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 indirectly implies R7C2<>4)
  R7C2<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 indirectly implies R7C2<>9)
  R8C2<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 indirectly implies R8C2<>4)
  R8C2<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 indirectly implies R8C2<>9)
  R5C5=8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8)
  R5C5<>1 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>1)
  R5C5<>2 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>2)
  R5C5<>5 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>5)
  R3C2=4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4)
  R6C2=9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 forces R6C2=9)
  R3C2<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 indirectly implies R3C2<>9)
  R6C2<>2 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 indirectly implies R6C2<>2)
  R8C4<>3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 block pins R8C2=3; R8C2=3 indirectly implies R8C4<>3)
  R8C5<>3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 block pins R8C2=3; R8C2=3 indirectly implies R8C5<>3)
  R8C6<>3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 block pins R8C2=3; R8C2=3 indirectly implies R8C6<>3)
  R3C3=9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 row pins R3C3=9)
  R3C3<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C3<>4)
  R3C3<>8 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C3<>8)
  R3C5<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4)
  R2C3<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R2C3<>4)
  R6C1<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 forces R6C2=9; R6C2=9 indirectly implies R6C1<>9)
  R6C4<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 forces R6C2=9; R6C2=9 indirectly implies R6C4<>9)
  R6C9<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 forces R6C2=9; R6C2=9 indirectly implies R6C9<>9)
  R4C1<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 forces R6C2=9; R6C2=9 indirectly implies R4C1<>9)
  R7C3<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 row pins R3C3=9; R3C3=9 indirectly implies R7C3<>9)
  R8C3<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 row pins R3C3=9; R3C3=9 indirectly implies R8C3<>9)
  R9C3<>9 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 row pins R3C3=9; R3C3=9 indirectly implies R9C3<>9)
  R2C6=4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 block pins R2C6=4)
  R2C6<>1 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 indirectly implies R2C6<>1)
  R2C6<>2 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 indirectly implies R2C6<>2)
  R2C6<>3 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 indirectly implies R2C6<>3)
  R7C6<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 block pins R2C6=4; R2C6=4 indirectly implies R7C6<>4)
  R8C6<>4 (R1C3=2 indirectly implies R7C3<>2; R7C3<>2 row pins R7C2=2; R7C2=2 column pins R3C2=4; R3C2=4 indirectly implies R3C5<>4; R3C5<>4 block pins R2C6=4; R2C6=4 indirectly implies R8C6<>4)
  R2C7=2 (All other possibilities excluded via pin)
  R3C5=2 (All other possibilities excluded via pin)
  R3C7=8 (All other possibilities excluded via pin)
  R6C1=1 (All other possibilities excluded via pin)
  R4C1=2 (All other possibilities excluded via force)
  R9C1=9 (All other possibilities excluded via force)
  R2C3=8 (All other possibilities excluded via force)
  R5C6=2 (All other possibilities excluded via pin)
  R6C9=2 (All other possibilities excluded via pin)
  R5C4=1 (All other possibilities excluded via pin)
  R6C7=4 (All other possibilities excluded via pin)
  R2C8=1 (All other possibilities excluded via pin)
  R6C4=6 (All other possibilities excluded via pin)
  R3C4=? (All possibilities excluded)

Assertion R1C3=5 implies:
  R1C4=8 (R1C3=5 row pins R1C4=8)
  R1C3<>1 (R1C3=5 implies R1C3<>1)
  R1C3<>2 (R1C3=5 implies R1C3<>2)
  R1C3<>8 (R1C3=5 implies R1C3<>8)
  R1C1<>5 (R1C3=5 indirectly implies R1C1<>5)
  R1C4<>1 (R1C3=5 indirectly implies R1C4<>1)
  R1C4<>3 (R1C3=5 indirectly implies R1C4<>3)
  R1C4<>6 (R1C3=5 indirectly implies R1C4<>6)
  R6C3<>5 (R1C3=5 indirectly implies R6C3<>5)
  R2C4<>8 (R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8)
  R3C4<>8 (R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R5C4<>8 (R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8)
  R3C5<>8 (R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R3C5<>8)
  R5C5=8 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8)
  R5C5<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>1)
  R5C5<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>2)
  R5C5<>5 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>5)
  R2C3<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R2C3<>1)
  R2C3<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R2C3<>2)
  R3C2<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R3C2<>1)
  R3C2<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R3C2<>2)
  R3C3<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R3C3<>1)
  R3C3<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1=126(<>5) proves R3C3<>2)
  R2C6<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>1)
  R2C6<>3 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>3)
  R2C6<>6 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>6)
  R3C3<>8 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R3C3<>8)
  R7C3<>9 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R7C3<>9)
  R8C3<>9 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R8C3<>9)
  R3C7=8 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin)
  R2C3=8 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin)
  R2C6=4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin)
  R7C2<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; R6C3<>5 column pins R1C3=5; R1C3=5 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R7C3<>9; R7C3=1246(<>9) proves R7C2<>1)
  R3C7<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R3C7=8 implies R3C7<>2)
  R3C7<>6 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R3C7=8 implies R3C7<>6)
  R2C7<>8 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R3C7=8 indirectly implies R2C7<>8)
  R2C7<>6 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R3C7=8 indirectly implies R2C7<>8; R2C7=23(<>8) proves R2C7<>6)
  R2C3<>4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 implies R2C3<>4)
  R2C6<>2 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 indirectly implies R2C6<>2)
  R7C6<>4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R7C6<>4)
  R8C6<>4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4)
  R3C5<>4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R3C5<>4)
  R7C6<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R7C6<>4; R7C6=39(<>4) proves R7C6<>1)
  R4C6<>9 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R7C6<>4; R7C6=39(<>4) proves R4C6<>9)
  R8C6<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C6<>1)
  R8C4<>3 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C4<>3)
  R8C5<>3 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C5<>3)
  R5C6<>9 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R5C6<>9)
  R8C2<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C2<>1)
  R8C2<>4 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C2<>4)
  R8C4<>9 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C4<>9)
  R8C5<>5 (R1C3=5 indirectly implies R1C1<>5; R1C1<>5 row pins R1C3=5; R1C3=5 indirectly implies R6C3<>5; All other possibilities excluded via pin; R2C3=8 row pins R2C6=4; R2C6=4 indirectly implies R8C6<>4; R8C6=39(<>4) proves R8C5<>5)
  R1C1<>1 (R1C3=5 indirectly implies R1C1<>5; R1C1=26(<>5) proves R1C1<>1)
  R2C4<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>1)
  R2C4<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>6)
  R2C7<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7<>3)
  R2C8<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>3)
  R6C4<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>3)
  R1C6<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>3)
  R1C9=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9=3)
  R1C6<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>1)
  R1C6<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>2)
  R1C1<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1<>6)
  R1C9<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>6)
  R4C6<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>6)
  R3C4<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4<>6)
  R2C1=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1=6)
  R2C1<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>1)
  R2C1<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>2)
  R2C8<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>6)
  R6C4=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4=6)
  R6C4<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>5)
  R6C4<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>9)
  R6C7<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>6)
  R6C9<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>6)
  R6C7<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>2)
  R6C7<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>5)
  R6C9<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>2)
  R6C9<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>9)
  R5C4=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4=9)
  R5C6=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6=1)
  R8C4=5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4=5)
  R1C9<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>1)
  R1C9<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>2)
  R4C9<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>3)
  R6C9<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>3)
  R9C9<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>3)
  R9C9<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>4)
  R9C9<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>9)
  R9C3<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>9)
  R5C9<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>9)
  R5C7<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>5)
  R5C6<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6<>2)
  R4C9<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>2)
  R5C4<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>1)
  R3C3<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3<>4)
  R7C3<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>4)
  R7C2<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>4)
  R6C3<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>9)
  R3C2=4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2=4)
  R3C3=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3=9)
  R3C2<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2<>9)
  R1C6=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6=6)
  R5C8=5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8=5)
  R5C4<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>5)
  R5C8<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8<>9)
  R4C8<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>5)
  R7C8<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>5)
  R8C4<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>1)
  R8C7<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>5)
  R7C5<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>5)
  R7C7<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>4)
  R7C7=5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7=5)
  R7C7<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>6)
  R1C2=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2=1)
  R2C7=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7=2)
  R3C5=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5=2)
  R3C9=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9=6)
  R4C8=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8=6)
  R5C9=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9=2)
  R7C3=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3=6)
  R8C7=6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7=6)
  R6C3=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3=2)
  R3C4=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4=1)
  R4C6=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6=2)
  R9C8=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8=3)
  R9C9=7 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9=7)
  R1C1=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1=2)
  R2C8=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8=1)
  R6C1=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1=1)
  R6C7=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7=3)
  R5C7=7 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7=7)
  R4C9=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9=9)
  R7C2=2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2=2)
  R7C9=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9=1)
  R7C8=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8=9)
  R4C5=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5=3)
  R6C9=4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9=4)
  R6C5=5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5=5)
  R6C2=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2=9)
  R7C6=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6=3)
  R7C5=4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5=4)
  R8C2=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2=3)
  R8C3=4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3=4)
  R8C6=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6=9)
  R9C3=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3=1)
  R9C7=4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7=4)
  R9C1=9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1=9)
  R4C1=5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1=5)
  R8C5=1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5=1)
  R1C2<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2<>2)
  R6C2<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>1)
  R5C7<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>2)
  R3C9<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>2)
  R3C5<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5<>1)
  R4C5<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>2)
  R6C5<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>2)
  R3C9<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>1)
  R4C9<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>6)
  R7C9<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>6)
  R4C8<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>3)
  R4C8<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>9)
  R7C8<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>6)
  R5C9<>7 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>7)
  R9C9<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>1)
  R9C7<>7 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>7)
  R7C3<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>1)
  R7C3<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>2)
  R7C2<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>3)
  R7C2<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>9)
  R8C3<>6 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>6)
  R8C2<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>9)
  R6C2<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>2)
  R8C6<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>3)
  R6C1<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>9)
  R4C1<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>9)
  R9C1<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1<>1)
  R9C8<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>9)
  R6C1<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>2)
  R6C1<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>5)
  R6C3<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>1)
  R8C7<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>4)
  R7C6<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>9)
  R7C5<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>3)
  R4C6<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>3)
  R4C1<>2 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>2)
  R9C8<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>1)
  R9C7<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>3)
  R7C8<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>1)
  R6C7<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>4)
  R6C5<>3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>3)
  R7C9<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>4)
  R7C9<>9 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>9)
  R7C5<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>1)
  R4C5<>5 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>5)
  R8C5<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>4)
  R8C3<>1 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>1)
  R9C3<>4 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>4)
  R2C4=3 (R1C3=5 implies R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4=3)


Continued in next posting...
Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 12:32 am    Post subject: Reply with quote

Code:

Invalid assertion R1C3=8 implies:
  R1C1=5 (R1C3=8 row pins R1C1=5)
  R6C3=5 (R1C3=8 column pins R6C3=5)
  R2C1=6 (R1C3=8 block pins R2C1=6)
  R1C3<>1 (R1C3=8 implies R1C3<>1)
  R1C3<>2 (R1C3=8 implies R1C3<>2)
  R1C3<>5 (R1C3=8 implies R1C3<>5)
  R1C1<>1 (R1C3=8 indirectly implies R1C1<>1)
  R1C1<>2 (R1C3=8 indirectly implies R1C1<>2)
  R1C1<>6 (R1C3=8 indirectly implies R1C1<>6)
  R1C4<>8 (R1C3=8 indirectly implies R1C4<>8)
  R2C3<>8 (R1C3=8 indirectly implies R2C3<>8)
  R3C3<>8 (R1C3=8 indirectly implies R3C3<>8)
  R6C3<>1 (R1C3=8 indirectly implies R6C3<>1)
  R6C3<>2 (R1C3=8 indirectly implies R6C3<>2)
  R6C3<>9 (R1C3=8 indirectly implies R6C3<>9)
  R2C1<>1 (R1C3=8 indirectly implies R2C1<>1)
  R2C1<>2 (R1C3=8 indirectly implies R2C1<>2)
  R4C1<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R4C1<>5)
  R6C1<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5)
  R2C4<>6 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C4<>6)
  R2C6<>6 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6)
  R2C7<>6 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C7<>6)
  R2C8<>6 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C8<>6)
  R6C4<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5)
  R6C5<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C5<>5)
  R6C7<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5)
  R7C3<>9 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R7C3<>9)
  R8C3<>9 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R8C3<>9)
  R2C6<>1 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6; R2C6=24(<>6) proves R2C6<>1)
  R2C6<>3 (R1C3=8 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6; R2C6=24(<>6) proves R2C6<>3)
  R4C6<>9 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R4C6<>9)
  R5C5<>5 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>5)
  R5C5<>1 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>1)
  R5C5<>2 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>2)
  R5C4<>8 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C4<>8)
  R3C5<>8 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C5<>8)
  R3C3<>2 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C3<>2)
  R3C2<>2 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C2<>2)
  R5C5=8 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5=8)
  R6C7<>2 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5; R6C7=346(<>5) proves R6C7<>2)
  R7C2<>1 (R1C3=8 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R7C3<>9; R7C3=1246(<>9) proves R7C2<>1)
  R3C3<>4 (R1C3=8 indirectly implies R2C3<>8; R2C3=124(<>8) proves R3C3<>4)

Assertion R1C3<>1 implies:
  R1C3<>1 (R1C3<>1 implies R1C3<>1)
  R1C3<>2 (R1C3=58(<>1) proves R1C3<>2)
  R5C4<>8 (R1C3=58(<>1) proves R5C4<>8)
  R3C5<>8 (R1C3=58(<>1) proves R3C5<>8)
  R5C5=8 (R1C3=58(<>1) proves R5C5=8)
  R5C5<>1 (R1C3=58(<>1) proves R5C5<>1)
  R5C5<>2 (R1C3=58(<>1) proves R5C5<>2)
  R5C5<>5 (R1C3=58(<>1) proves R5C5<>5)
  R3C2<>2 (R1C3=58(<>1) proves R3C2<>2)
  R3C3<>2 (R1C3=58(<>1) proves R3C3<>2)
  R2C6<>1 (R1C3=58(<>1) proves R2C6<>1)
  R2C6<>3 (R1C3=58(<>1) proves R2C6<>3)
  R2C6<>6 (R1C3=58(<>1) proves R2C6<>6)
  R3C3<>8 (R1C3=58(<>1) proves R3C3<>8)
  R7C3<>9 (R1C3=58(<>1) proves R7C3<>9)
  R8C3<>9 (R1C3=58(<>1) proves R8C3<>9)
  R7C2<>1 (R1C3=58(<>1) proves R7C2<>1)
  R2C7<>6 (R1C3=58(<>1) proves R2C7<>6)
  R4C6<>9 (R1C3=58(<>1) proves R4C6<>9)
  R1C1<>1 (R1C3=58(<>1) proves R1C1<>1)
  R2C6<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C6<>2)
  R2C3<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>4)
  R7C6<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>4)
  R8C6<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>4)
  R3C5<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5<>4)
  R3C3<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3<>1)
  R3C2<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2<>1)
  R7C6<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>1)
  R8C6<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>1)
  R8C4<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>3)
  R8C5<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>3)
  R5C6<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6<>9)
  R8C2<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>1)
  R8C2<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>4)
  R8C4<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>9)
  R8C5<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>5)
  R2C3<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>1)
  R2C3<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>2)
  R2C4<>8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>8)
  R2C7<>8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7<>8)
  R1C3<>8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C3<>8)
  R3C7=8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7=8)
  R3C7<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7<>2)
  R3C7<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7<>6)
  R1C4=8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4=8)
  R1C4<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>1)
  R1C4<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>3)
  R1C4<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>6)
  R3C4<>8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4<>8)
  R1C1<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1<>5)
  R6C3<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>5)
  R1C3=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C3=5)
  R2C4<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>1)
  R2C4<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>6)
  R2C7<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7<>3)
  R2C8<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>3)
  R6C4<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>3)
  R1C6<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>3)
  R1C9=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9=3)
  R2C3=8 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3=8)
  R1C6<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>1)
  R1C6<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>2)
  R1C1<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1<>6)
  R1C9<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>6)
  R4C6<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>6)
  R3C4<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4<>6)
  R2C1=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1=6)
  R2C1<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>1)
  R2C1<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>2)
  R2C8<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>6)
  R6C4=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4=6)
  R6C4<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>5)
  R6C4<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>9)
  R6C7<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>6)
  R6C9<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>6)
  R6C7<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>2)
  R6C7<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>5)
  R6C9<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>2)
  R6C9<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>9)
  R5C4=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4=9)
  R5C6=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6=1)
  R8C4=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4=5)
  R1C9<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>1)
  R1C9<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>2)
  R4C9<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>3)
  R6C9<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>3)
  R9C9<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>3)
  R9C9<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>4)
  R9C9<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>9)
  R9C3<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>9)
  R5C9<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>9)
  R5C7<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>5)
  R5C6<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6<>2)
  R4C9<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>2)
  R5C4<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>1)
  R3C3<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3<>4)
  R7C3<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>4)
  R7C2<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>4)
  R6C3<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>9)
  R3C2=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2=4)
  R3C3=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3=9)
  R3C2<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2<>9)
  R1C6=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6=6)
  R5C8=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8=5)
  R5C4<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>5)
  R5C8<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8<>9)
  R4C8<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>5)
  R7C8<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>5)
  R8C4<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>1)
  R8C7<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>5)
  R7C5<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>5)
  R7C7<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>4)
  R7C7=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7=5)
  R7C7<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>6)
  R1C2=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2=1)
  R2C7=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7=2)
  R3C5=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5=2)
  R3C9=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9=6)
  R4C8=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8=6)
  R5C9=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9=2)
  R7C3=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3=6)
  R8C7=6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7=6)
  R6C3=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3=2)
  R3C4=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4=1)
  R4C6=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6=2)
  R9C8=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8=3)
  R9C9=7 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9=7)
  R1C1=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1=2)
  R2C8=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8=1)
  R6C1=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1=1)
  R6C7=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7=3)
  R5C7=7 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7=7)
  R4C9=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9=9)
  R7C2=2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2=2)
  R7C9=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9=1)
  R7C8=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8=9)
  R4C5=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5=3)
  R6C9=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9=4)
  R6C5=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5=5)
  R6C2=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2=9)
  R7C6=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6=3)
  R7C5=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5=4)
  R8C2=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2=3)
  R8C3=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3=4)
  R8C6=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6=9)
  R9C3=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3=1)
  R9C7=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7=4)
  R9C1=9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1=9)
  R4C1=5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1=5)
  R8C5=1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5=1)
  R1C2<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2<>2)
  R6C2<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>1)
  R5C7<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>2)
  R3C9<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>2)
  R3C5<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5<>1)
  R4C5<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>2)
  R6C5<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>2)
  R3C9<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>1)
  R4C9<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>6)
  R7C9<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>6)
  R4C8<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>3)
  R4C8<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>9)
  R7C8<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>6)
  R5C9<>7 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>7)
  R9C9<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>1)
  R9C7<>7 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>7)
  R7C3<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>1)
  R7C3<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>2)
  R7C2<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>3)
  R7C2<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>9)
  R8C3<>6 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>6)
  R8C2<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>9)
  R6C2<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>2)
  R8C6<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>3)
  R6C1<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>9)
  R4C1<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>9)
  R9C1<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1<>1)
  R9C8<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>9)
  R6C1<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>2)
  R6C1<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>5)
  R6C3<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>1)
  R8C7<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>4)
  R7C6<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>9)
  R7C5<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>3)
  R4C6<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>3)
  R4C1<>2 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>2)
  R9C8<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>1)
  R9C7<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>3)
  R7C8<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>1)
  R6C7<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>4)
  R6C5<>3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>3)
  R7C9<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>4)
  R7C9<>9 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>9)
  R7C5<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>1)
  R4C5<>5 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>5)
  R8C5<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>4)
  R8C3<>1 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>1)
  R9C3<>4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>4)
  R2C4=3 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4=3)
  R2C6=4 (R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R3C3<>8; R3C3=149(<>8) proves R3C3<>2; R3C3=149(<>2) proves R3C2<>2; R3C2=149(<>2) proves R1C3<>2; R1C3=58(<>2) proves R2C7<>6; R2C7=238(<>6) proves R1C3<>2; R1C3=58(<>2) proves R2C6<>1; R2C6=4(<>1) proves R2C6<>2; R2C6=4(<>2) proves R2C3<>4; R2C3<>4 row pins R2C6=4)

Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 12:33 am    Post subject: Reply with quote

Code:

Assertion R1C3<>2 implies:
  R1C3<>2 (R1C3<>2 implies R1C3<>2)
  R1C3<>1 (R1C3=58(<>2) proves R1C3<>1)
  R5C4<>8 (R1C3=58(<>2) proves R5C4<>8)
  R3C5<>8 (R1C3=58(<>2) proves R3C5<>8)
  R5C5=8 (R1C3=58(<>2) proves R5C5=8)
  R5C5<>1 (R1C3=58(<>2) proves R5C5<>1)
  R5C5<>2 (R1C3=58(<>2) proves R5C5<>2)
  R5C5<>5 (R1C3=58(<>2) proves R5C5<>5)
  R3C2<>2 (R1C3=58(<>2) proves R3C2<>2)
  R3C3<>2 (R1C3=58(<>2) proves R3C3<>2)
  R2C6<>1 (R1C3=58(<>2) proves R2C6<>1)
  R2C6<>3 (R1C3=58(<>2) proves R2C6<>3)
  R2C6<>6 (R1C3=58(<>2) proves R2C6<>6)
  R3C3<>8 (R1C3=58(<>2) proves R3C3<>8)
  R7C3<>9 (R1C3=58(<>2) proves R7C3<>9)
  R8C3<>9 (R1C3=58(<>2) proves R8C3<>9)
  R7C2<>1 (R1C3=58(<>2) proves R7C2<>1)
  R2C7<>6 (R1C3=58(<>2) proves R2C7<>6)
  R4C6<>9 (R1C3=58(<>2) proves R4C6<>9)
  R1C1<>1 (R1C3=58(<>2) proves R1C1<>1)
  R2C6<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C6<>2)
  R2C3<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>4)
  R7C6<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>4)
  R8C6<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>4)
  R3C5<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5<>4)
  R3C3<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3<>1)
  R3C2<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2<>1)
  R7C6<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>1)
  R8C6<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>1)
  R8C4<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>3)
  R8C5<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>3)
  R5C6<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6<>9)
  R8C2<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>1)
  R8C2<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>4)
  R8C4<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>9)
  R8C5<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>5)
  R2C3<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>1)
  R2C3<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3<>2)
  R2C4<>8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>8)
  R2C7<>8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7<>8)
  R1C3<>8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C3<>8)
  R3C7=8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7=8)
  R3C7<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7<>2)
  R3C7<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C7<>6)
  R1C4=8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4=8)
  R1C4<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>1)
  R1C4<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>3)
  R1C4<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C4<>6)
  R3C4<>8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4<>8)
  R1C1<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1<>5)
  R6C3<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>5)
  R1C3=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C3=5)
  R2C4<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>1)
  R2C4<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4<>6)
  R2C7<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7<>3)
  R2C8<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>3)
  R6C4<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>3)
  R1C6<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>3)
  R1C9=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9=3)
  R2C3=8 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C3=8)
  R1C6<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>1)
  R1C6<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6<>2)
  R1C1<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1<>6)
  R1C9<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>6)
  R4C6<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>6)
  R3C4<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4<>6)
  R2C1=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1=6)
  R2C1<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>1)
  R2C1<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C1<>2)
  R2C8<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8<>6)
  R6C4=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4=6)
  R6C4<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>5)
  R6C4<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C4<>9)
  R6C7<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>6)
  R6C9<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>6)
  R6C7<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>2)
  R6C7<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>5)
  R6C9<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>2)
  R6C9<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>9)
  R5C4=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4=9)
  R5C6=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6=1)
  R8C4=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4=5)
  R1C9<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>1)
  R1C9<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C9<>2)
  R4C9<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>3)
  R6C9<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9<>3)
  R9C9<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>3)
  R9C9<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>4)
  R9C9<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>9)
  R9C3<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>9)
  R5C9<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>9)
  R5C7<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>5)
  R5C6<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C6<>2)
  R4C9<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>2)
  R5C4<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>1)
  R3C3<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3<>4)
  R7C3<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>4)
  R7C2<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>4)
  R6C3<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>9)
  R3C2=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2=4)
  R3C3=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C3=9)
  R3C2<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C2<>9)
  R1C6=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C6=6)
  R5C8=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8=5)
  R5C4<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C4<>5)
  R5C8<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C8<>9)
  R4C8<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>5)
  R7C8<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>5)
  R8C4<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C4<>1)
  R8C7<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>5)
  R7C5<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>5)
  R7C7<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>4)
  R7C7=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7=5)
  R7C7<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C7<>6)
  R1C2=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2=1)
  R2C7=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C7=2)
  R3C5=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5=2)
  R3C9=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9=6)
  R4C8=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8=6)
  R5C9=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9=2)
  R7C3=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3=6)
  R8C7=6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7=6)
  R6C3=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3=2)
  R3C4=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C4=1)
  R4C6=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6=2)
  R9C8=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8=3)
  R9C9=7 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9=7)
  R1C1=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C1=2)
  R2C8=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C8=1)
  R6C1=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1=1)
  R6C7=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7=3)
  R5C7=7 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7=7)
  R4C9=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9=9)
  R7C2=2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2=2)
  R7C9=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9=1)
  R7C8=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8=9)
  R4C5=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5=3)
  R6C9=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C9=4)
  R6C5=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5=5)
  R6C2=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2=9)
  R7C6=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6=3)
  R7C5=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5=4)
  R8C2=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2=3)
  R8C3=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3=4)
  R8C6=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6=9)
  R9C3=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3=1)
  R9C7=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7=4)
  R9C1=9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1=9)
  R4C1=5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1=5)
  R8C5=1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5=1)
  R1C2<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R1C2<>2)
  R6C2<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>1)
  R5C7<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C7<>2)
  R3C9<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>2)
  R3C5<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C5<>1)
  R4C5<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>2)
  R6C5<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>2)
  R3C9<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R3C9<>1)
  R4C9<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C9<>6)
  R7C9<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>6)
  R4C8<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>3)
  R4C8<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C8<>9)
  R7C8<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>6)
  R5C9<>7 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R5C9<>7)
  R9C9<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C9<>1)
  R9C7<>7 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>7)
  R7C3<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>1)
  R7C3<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C3<>2)
  R7C2<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>3)
  R7C2<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C2<>9)
  R8C3<>6 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>6)
  R8C2<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C2<>9)
  R6C2<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C2<>2)
  R8C6<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C6<>3)
  R6C1<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>9)
  R4C1<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>9)
  R9C1<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C1<>1)
  R9C8<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>9)
  R6C1<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>2)
  R6C1<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C1<>5)
  R6C3<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C3<>1)
  R8C7<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C7<>4)
  R7C6<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C6<>9)
  R7C5<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>3)
  R4C6<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C6<>3)
  R4C1<>2 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C1<>2)
  R9C8<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C8<>1)
  R9C7<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C7<>3)
  R7C8<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C8<>1)
  R6C7<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C7<>4)
  R6C5<>3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R6C5<>3)
  R7C9<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>4)
  R7C9<>9 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C9<>9)
  R7C5<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R7C5<>1)
  R4C5<>5 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R4C5<>5)
  R8C5<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C5<>4)
  R8C3<>1 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R8C3<>1)
  R9C3<>4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R9C3<>4)
  R2C4=3 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4=3)
  R2C6=4 (R1C3=58(<>2) proves R1C3<>1; R1C3=58(<>1) proves R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R3C3<>8; R3C3=149(<>8) proves R3C3<>2; R3C3=149(<>2) proves R3C2<>2; R3C2=149(<>2) proves R1C3<>2; R1C3=58(<>2) proves R2C7<>6; R2C7=238(<>6) proves R1C3<>2; R1C3=58(<>2) proves R2C6<>1; R2C6=4(<>1) proves R2C6<>2; R2C6=4(<>2) proves R2C3<>4; R2C3<>4 row pins R2C6=4)
Back to top
View user's profile Send private message Visit poster's website AIM Address
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 12:36 am    Post subject: Reply with quote

Code:

Invalid assertion R1C3<>5 implies:
  R1C1=5 (R1C3<>5 row pins R1C1=5)
  R6C3=5 (R1C3<>5 column pins R6C3=5)
  R2C1=6 (R1C3<>5 block pins R2C1=6)
  R1C3<>5 (R1C3<>5 implies R1C3<>5)
  R1C1<>1 (R1C3<>5 indirectly implies R1C1<>1)
  R1C1<>2 (R1C3<>5 indirectly implies R1C1<>2)
  R1C1<>6 (R1C3<>5 indirectly implies R1C1<>6)
  R6C3<>1 (R1C3<>5 indirectly implies R6C3<>1)
  R6C3<>2 (R1C3<>5 indirectly implies R6C3<>2)
  R6C3<>9 (R1C3<>5 indirectly implies R6C3<>9)
  R2C1<>1 (R1C3<>5 indirectly implies R2C1<>1)
  R2C1<>2 (R1C3<>5 indirectly implies R2C1<>2)
  R4C1<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R4C1<>5)
  R6C1<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5)
  R2C4<>6 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C4<>6)
  R2C6<>6 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6)
  R2C7<>6 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C7<>6)
  R2C8<>6 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C8<>6)
  R6C4<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5)
  R6C5<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C5<>5)
  R6C7<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5)
  R1C3<>2 (R1C3=18(<>5) proves R1C3<>2)
  R7C3<>9 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R7C3<>9)
  R8C3<>9 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R8C3<>9)
  R2C6<>1 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6; R2C6=24(<>6) proves R2C6<>1)
  R2C6<>3 (R1C3<>5 row pins R1C1=5; R1C1=5 column pins R2C1=6; R2C1=6 indirectly implies R2C6<>6; R2C6=24(<>6) proves R2C6<>3)
  R4C6<>9 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R4C6<>9)
  R5C5<>5 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>5)
  R5C5<>1 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>1)
  R5C5<>2 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5<>2)
  R5C4<>8 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C4<>8)
  R3C5<>8 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C5<>8)
  R3C3<>8 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C3<>8)
  R3C3<>2 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C3<>2)
  R3C2<>2 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R3C2<>2)
  R5C5=8 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C4<>5; R6C4=369(<>5) proves R5C5=8)
  R6C7<>2 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R1C3<>5; R1C3<>5 column pins R6C3=5; R6C3=5 indirectly implies R6C7<>5; R6C7=346(<>5) proves R6C7<>2)
  R7C2<>1 (R1C3<>5 row pins R1C1=5; R1C1=5 indirectly implies R6C1<>5; R6C1=129(<>5) proves R7C3<>9; R7C3=1246(<>9) proves R7C2<>1)
  R1C3<>1 (R1C3=8(<>5) proves R1C3<>1)
  R1C4<>8 (R1C3=8(<>5) proves R1C4<>8)
  R2C3<>8 (R1C3=8(<>5) proves R2C3<>8)
  R3C3<>4 (R1C3=8(<>5) proves R3C3<>4)

Assertion R1C3<>8 implies:
  R1C4=8 (R1C3<>8 row pins R1C4=8)
  R1C3<>8 (R1C3<>8 implies R1C3<>8)
  R1C4<>1 (R1C3<>8 indirectly implies R1C4<>1)
  R1C4<>3 (R1C3<>8 indirectly implies R1C4<>3)
  R1C4<>6 (R1C3<>8 indirectly implies R1C4<>6)
  R2C4<>8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8)
  R3C4<>8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R5C4<>8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8)
  R3C5<>8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C5<>8)
  R5C5=8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8)
  R5C5<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>1)
  R5C5<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>2)
  R5C5<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 indirectly implies R5C5<>5)
  R1C3<>2 (R1C3=15(<>8) proves R1C3<>2)
  R2C3<>1 (R1C3=15(<>8) proves R2C3<>1)
  R2C3<>2 (R1C3=15(<>8) proves R2C3<>2)
  R3C3<>1 (R1C3=15(<>8) proves R3C3<>1)
  R3C3<>2 (R1C3=15(<>8) proves R3C3<>2)
  R3C2<>1 (R1C3=15(<>8) proves R3C2<>1)
  R3C2<>2 (R1C3=15(<>8) proves R3C2<>2)
  R2C6<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>1)
  R2C6<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>3)
  R2C6<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>6)
  R3C3<>8 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R3C3<>8)
  R7C3<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R7C3<>9)
  R8C3<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R8C3<>9)
  R7C2<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R5C4<>8; R5C4<>8 row pins R5C5=8; R5C5=8 indirectly implies R3C5<>8; R3C5=124(<>8) proves R7C3<>9; R7C3=1246(<>9) proves R7C2<>1)
  R3C7=8 (All other possibilities excluded via pin)
  R2C3=8 (All other possibilities excluded via pin)
  R2C6=4 (All other possibilities excluded via pin)
  R1C3<>1 (R1C3=5(<>8) proves R1C3<>1)
  R1C1<>5 (R1C3=5(<>8) proves R1C1<>5)
  R6C3<>5 (R1C3=5(<>8) proves R6C3<>5)
  R3C7<>2 (R1C3=5(<>8) proves R3C7<>2)
  R3C7<>6 (R1C3=5(<>8) proves R3C7<>6)
  R2C7<>8 (R1C3=5(<>8) proves R2C7<>8)
  R2C7<>6 (R1C3=5(<>8) proves R2C7<>6)
  R2C3<>4 (R1C3=5(<>8) proves R2C3<>4)
  R2C6<>2 (R1C3=5(<>8) proves R2C6<>2)
  R7C6<>4 (R1C3=5(<>8) proves R7C6<>4)
  R8C6<>4 (R1C3=5(<>8) proves R8C6<>4)
  R3C5<>4 (R1C3=5(<>8) proves R3C5<>4)
  R7C6<>1 (R1C3=5(<>8) proves R7C6<>1)
  R4C6<>9 (R1C3=5(<>8) proves R4C6<>9)
  R8C6<>1 (R1C3=5(<>8) proves R8C6<>1)
  R8C4<>3 (R1C3=5(<>8) proves R8C4<>3)
  R8C5<>3 (R1C3=5(<>8) proves R8C5<>3)
  R5C6<>9 (R1C3=5(<>8) proves R5C6<>9)
  R8C2<>1 (R1C3=5(<>8) proves R8C2<>1)
  R8C2<>4 (R1C3=5(<>8) proves R8C2<>4)
  R8C4<>9 (R1C3=5(<>8) proves R8C4<>9)
  R8C5<>5 (R1C3=5(<>8) proves R8C5<>5)
  R1C1<>1 (R1C3=5(<>8) proves R1C1<>1)
  R1C3=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R1C3<>8; R1C3=5(<>8) proves R1C1<>5; R1C1<>5 row pins R1C3=5)
  R2C4<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C4<>1)
  R2C4<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C4<>6)
  R2C7<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C7<>3)
  R2C8<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C8<>3)
  R6C4<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C4<>3)
  R1C6<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C6<>3)
  R1C9=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C9=3)
  R1C6<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C6<>1)
  R1C6<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C6<>2)
  R1C1<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C1<>6)
  R1C9<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C9<>6)
  R4C6<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C6<>6)
  R3C4<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C4<>6)
  R2C1=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C1=6)
  R2C1<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C1<>1)
  R2C1<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C1<>2)
  R2C8<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C8<>6)
  R6C4=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C4=6)
  R6C4<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C4<>5)
  R6C4<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C4<>9)
  R6C7<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C7<>6)
  R6C9<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C9<>6)
  R6C7<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C7<>2)
  R6C7<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C7<>5)
  R6C9<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C9<>2)
  R6C9<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C9<>9)
  R5C4=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C4=9)
  R5C6=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C6=1)
  R8C4=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C4=5)
  R1C9<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C9<>1)
  R1C9<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C9<>2)
  R4C9<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C9<>3)
  R6C9<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C9<>3)
  R9C9<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C9<>3)
  R9C9<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C9<>4)
  R9C9<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C9<>9)
  R9C3<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C3<>9)
  R5C9<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C9<>9)
  R5C7<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C7<>5)
  R5C6<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C6<>2)
  R4C9<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C9<>2)
  R5C4<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C4<>1)
  R3C3<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C3<>4)
  R7C3<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C3<>4)
  R7C2<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C2<>4)
  R6C3<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C3<>9)
  R3C2=4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C2=4)
  R3C3=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C3=9)
  R3C2<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C2<>9)
  R1C6=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C6=6)
  R5C8=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C8=5)
  R5C4<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C4<>5)
  R5C8<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C8<>9)
  R4C8<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C8<>5)
  R7C8<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C8<>5)
  R8C4<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C4<>1)
  R8C7<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C7<>5)
  R7C5<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C5<>5)
  R7C7<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C7<>4)
  R7C7=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C7=5)
  R7C7<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C7<>6)
  R1C2=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C2=1)
  R2C7=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C7=2)
  R3C5=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C5=2)
  R3C9=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C9=6)
  R4C8=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C8=6)
  R5C9=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C9=2)
  R7C3=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C3=6)
  R8C7=6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C7=6)
  R6C3=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C3=2)
  R3C4=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C4=1)
  R4C6=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C6=2)
  R9C8=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C8=3)
  R9C9=7 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C9=7)
  R1C1=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C1=2)
  R2C8=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R2C8=1)
  R6C1=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C1=1)
  R6C7=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C7=3)
  R5C7=7 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C7=7)
  R4C9=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C9=9)
  R7C2=2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C2=2)
  R7C9=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C9=1)
  R7C8=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C8=9)
  R4C5=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C5=3)
  R6C9=4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C9=4)
  R6C5=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C5=5)
  R6C2=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C2=9)
  R7C6=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C6=3)
  R7C5=4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C5=4)
  R8C2=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C2=3)
  R8C3=4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C3=4)
  R8C6=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C6=9)
  R9C3=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C3=1)
  R9C7=4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C7=4)
  R9C1=9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C1=9)
  R4C1=5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C1=5)
  R8C5=1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C5=1)
  R1C2<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R1C2<>2)
  R6C2<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C2<>1)
  R5C7<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C7<>2)
  R3C9<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C9<>2)
  R3C5<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C5<>1)
  R4C5<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C5<>2)
  R6C5<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C5<>2)
  R3C9<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R3C9<>1)
  R4C9<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C9<>6)
  R7C9<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C9<>6)
  R4C8<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C8<>3)
  R4C8<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C8<>9)
  R7C8<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C8<>6)
  R5C9<>7 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R5C9<>7)
  R9C9<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C9<>1)
  R9C7<>7 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C7<>7)
  R7C3<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C3<>1)
  R7C3<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C3<>2)
  R7C2<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C2<>3)
  R7C2<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C2<>9)
  R8C3<>6 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C3<>6)
  R8C2<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C2<>9)
  R6C2<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C2<>2)
  R8C6<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C6<>3)
  R6C1<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C1<>9)
  R4C1<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C1<>9)
  R9C1<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C1<>1)
  R9C8<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C8<>9)
  R6C1<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C1<>2)
  R6C1<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C1<>5)
  R6C3<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C3<>1)
  R8C7<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C7<>4)
  R7C6<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C6<>9)
  R7C5<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C5<>3)
  R4C6<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C6<>3)
  R4C1<>2 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C1<>2)
  R9C8<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C8<>1)
  R9C7<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C7<>3)
  R7C8<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C8<>1)
  R6C7<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C7<>4)
  R6C5<>3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R6C5<>3)
  R7C9<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C9<>4)
  R7C9<>9 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C9<>9)
  R7C5<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R7C5<>1)
  R4C5<>5 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R4C5<>5)
  R8C5<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C5<>4)
  R8C3<>1 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R8C3<>1)
  R9C3<>4 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R2C4<>8; R2C4=3(<>8) proves R9C3<>4)
  R2C4=3 (R1C3<>8 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8; R3C4=16(<>8) proves R2C6<>1; R2C6=4(<>1) proves R2C4=3)

The possibilities for R1C3 can be reduced from <1258> to <5>.

All assertions for this square have been completely expanded.
Back to top
View user's profile Send private message Visit poster's website AIM Address
Nick70

Joined: 08 Jun 2005
Posts: 160
:

Items
PostPosted: Fri Sep 16, 2005 9:42 am    Post subject: Reply with quote

Trebor, AMcK says that your tabling generates the following assertion:

Code:
R1C3<>2 (Implied by all possible values of R1C3)

In the transcripts you posted, I don't see R1C3<>2 as a consequence of R1C3=2. Can you explain how it is derived?
Back to top
View user's profile Send private message
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 10:53 am    Post subject: Reply with quote

As I mentioned, one of the features of tabling is that once you know an assertion is invalid, you don't use it when computing verities and veracities. So, since R1C3=2 is known to be invalid, R1C3<>2 only has to appear in the remaining valid positive assertions for R1C3.

In this case, it is a bit circular, since we already know from the invalidation that R1C3<>2 (since R1C3=2 is invalid!)

From a quick glance, the reason R1C3=2 is invalid is that it implies:

R3C4=? (All possibilities excluded)

(in other words, if R1C3=2, there are no legal values for R3C4)
Back to top
View user's profile Send private message Visit poster's website AIM Address
Nick70

Joined: 08 Jun 2005
Posts: 160
:

Items
PostPosted: Fri Sep 16, 2005 1:01 pm    Post subject: Reply with quote

MadOverlord wrote:
In this case, it is a bit circular, since we already know from the invalidation that R1C3<>2 (since R1C3=2 is invalid!)

From a quick glance, the reason R1C3=2 is invalid is that it implies:

R3C4=? (All possibilities excluded)

OK. So the statement
Code:
R1C3<>2 (Implied by all possible values of R1C3)

is misleading. It should be something like

R1C3<>2 (because R1C3=2 excludes all possibilities for R3C4)

this is an extension of the Nishio reasoning, which might seem new on first glance, but it is actually equivalent to multiple forcing chains.
If A,B,C are three statements of which at least one must be true, you are doing:

D => ~A
D => ~B
D => ~C
therefore D is false

however you can reverse the above statements and obtain a typical forcing chain:
A => ~D
B => ~D
C => ~D
therefore D is false

Going back to the example being discussed, instead of saying that R1C3=2 => R3C4=? we could just show that any value placed in R3C4 => R1C3<>2.
With simple forcing chains we cannot do either of that, however.
And in your transcript, it isn't obvious how it comes to be either.
The only statements relative to R3C4 are:

Code:
Invalid assertion R1C3=2 implies:
  R3C4<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R3C4=? (All possibilities excluded)

The first is obvious. The second just falls from above without an explicit implication.

What I understand from the transcript is that you are assuming that R1C3=2, and solving the puzzle from there until you reach a contradiction. And then you repeat the process for every possible.
Back to top
View user's profile Send private message
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 5:02 pm    Post subject: Reply with quote

[quote="Nick70"]
OK. So the statement
Code:
R1C3<>2 (Implied by all possible values of R1C3)

is misleading. It should be something like

R1C3<>2 (because R1C3=2 excludes all possibilities for R3C4)
[/code]

It would take a fair amount of busywork in the tabling algorithm to generate that kind of diagnostic; I'll add that to the to-do list. I could probably make it something like:

(Implied by R1C3=<whatever>; R1C3=<invalids> are no longer valid)

Quote:
Going back to the example being discussed, instead of saying that R1C3=2 => R3C4=? we could just show that any value placed in R3C4 => R1C3<>2.


I'm not 100% sure if this is true all the time. It may well be that this turns out to be a verity, but maybe not.

Quote:
And in your transcript, it isn't obvious how it comes to be either.
The only statements relative to R3C4 are:

Code:
Invalid assertion R1C3=2 implies:
  R3C4<>8 (R1C3=2 row pins R1C4=8; R1C4=8 indirectly implies R3C4<>8)
  R3C4=? (All possibilities excluded)

The first is obvious. The second just falls from above without an explicit implication.


I think I see your confusion. The "all possibilities excluded" is an implication that gets added to the assertion when applying all the prior implications to the original puzzle state results in a square that has no possibilities left.

R3C4 starts out at <168>, and it can't be 8, so that leaves <16>. But other positive statements also exclude values; R6C4=6 knocks out the 6, and R5C4=1 knocks out the 1.

Finding such contradictions via this kind of implicit analysis reduces the size of the tables needed to solve a puzzle, but it isn't required. You can turn off contradiction propagation and the puzzle still cracks.

Quote:
What I understand from the transcript is that you are assuming that R1C3=2, and solving the puzzle from there until you reach a contradiction. And then you repeat the process for every possible.


I'm looking for the implications of the various choices, yes, but as I said, contradiction is not required to solve; they just make it easier to find the verities and veracities.

If you haven't read my description of tabling in the Susser manual, it might be helpful. If you have, then let me know where things got confusing.

best
R
Back to top
View user's profile Send private message Visit poster's website AIM Address
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Fri Sep 16, 2005 8:52 pm    Post subject: Reply with quote

MadOverlord wrote:
Invalid assertion R1C3=1 implies:

You're in serious trouble now that Nick70's on your case Smile
Just a couple of questions from me
1) Can you show how you prove that R1C3=1 is an invalid assertion.
2) If you can prove that R1C3=1 is invalid, why don't you just treat it as a contradiction and assert that everything implied by R1C3<>1 is true
Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
MadOverlord

Joined: 01 Jun 2005
Posts: 80
:
Location: Wilmington, NC, USA

Items
PostPosted: Fri Sep 16, 2005 9:48 pm    Post subject: Reply with quote

Quote:

1) Can you show how you prove that R1C3=1 is an invalid assertion.


If you take the initial puzzle state and apply all the implications of R1C3=1 to it, you will find that R3C4 has no legal values left. To do this, you have to apply the "force and pin" implications of any positive moves. You could add these implications to the actual implications list, but it makes the tables huge, so I just infer them during the invalidity check stage.

Note that this puzzle is pathologically difficult; it requires the "aggressive forces and pins" feature of tabling (which prevents the tables from getting immense)

Quote:

2) If you can prove that R1C3=1 is invalid, why don't you just treat it as a contradiction and assert that everything implied by R1C3<>1 is true


Dave Bowman would be the one to give the definitive answer; that may be a nice shortcut we are missing. I do know you can find verities and veracities from the intersection of two negative assertions (whether or not you know they are invalid).
Back to top
View user's profile Send private message Visit poster's website AIM Address
AMcK

Joined: 07 Apr 2005
Posts: 89
:
Location: Cambridge

Items
PostPosted: Fri Sep 16, 2005 10:34 pm    Post subject: Reply with quote

MadOverlord wrote:
If you take the initial puzzle state and apply all the implications of R1C3=1 to it, you will find that R3C4 has no legal values left. To do this, you have to apply the "force and pin" implications of any positive moves.
Hmmm! the implications of R1C3=1 that I calculate are just ...
1c r1c3=1 in r1c3 implies ¬1a r1c1<>1 ¬1b r1c2<>1 ¬1d r1c4<>1 ¬1e r1c6<>1 ¬1f r1c9<>1 ¬1g r2c1<>1 ¬1h r2c3<>1 ¬1l r3c2<>1 ¬1m r3c3<>1 ¬1r r5c5<>1 ¬1v r6c3<>1 ¬1x r7c3<>1 ¬1D r8c3<>1 ¬1I r9c3<>1 ¬2a r1c1<>2 ¬2c r1c3<>2 ¬2d r1c6<>2 ¬2e r1c9<>2 ¬2f r2c1<>2 ¬2g r2c3<>2 ¬2j r3c2<>2 ¬2s r5c5<>2 ¬2x r6c2<>2 ¬2y r6c3<>2 ¬2C r7c2<>2 ¬3a r1c4<>3 ¬4i r7c3<>4 ¬4o r8c3<>4 ¬5b r1c3<>5 ¬5c r4c1<>5 ¬5g r5c5<>5 ¬5j r6c1<>5 ¬5l r6c4<>5 ¬5m r6c5<>5 ¬5n r6c7<>5 ¬6a r1c1<>6 ¬6b r1c4<>6 ¬6f r2c4<>6 ¬6g r2c6<>6 ¬6h r2c7<>6 ¬6i r2c8<>6 ¬6s r7c3<>6 ¬6x r8c7<>6 ¬8a r1c3<>8 ¬8d r2c4<>8 ¬8g r3c4<>8 ¬8h r3c5<>8 ¬8j r5c4<>8 ¬9m r6c3<>9
That doesn't eliminate all possible values of R3C4, even though all the force and pin implications *should* be built into the transitive closure of the implication matrices. It proves r1c3=1 => r3c4<>8 but doesn't say r1c3=1 => r3c4<>1 or r1c3=1 => r3c4<>6. Can you point me to the proofs of these implications.

MadOverlord wrote:
You could add these implications to the actual implications list, but it makes the tables huge, so I just infer them during the invalidity check stage.
Ah! that's the beauty of the matrix representation - the size of each matrix is always NxNx1 where N is the number of possibles in the grid.

If you can assert u=true and have the u=>v and u=>¬v matrices then you just walk along the u row asserting v=true when u=>v and v=false when u=>¬v. The converse can be done for u=false.
Actually, if you don't have the implication matrix closures - only exclusions and conjugations (as in Nick70's advanced coloring subset) and you can know that u=true then you can recursively assert that v=false if excludes(u,v). If you know that u=false then you can recursively assert that v=true if conjugates(u,v). Just one contradiction can often recusrively cascade a complete solution to quite complex puzzles.
Regards
Andrew
Back to top
View user's profile Send private message Send e-mail
Display posts from previous:   
Post new topic   Reply to topic    Sudoku Programmers Forum Index -> Solving sudoku All times are GMT
Goto page Previous  1, 2, 3, 4  Next
Page 3 of 4

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
Sudoku Programmers topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group

Igloo Theme Version 1.0 :: Created By: Andrew Charron