The New Sudoku Players' Forum

[999_Springs]

So just out of boredom I decided to post the 9.0 rated puzzle from the maximum number of clues thread onto some other forum. Somewhat unexpectedly I got a reply which had a document attached to it that looked like this:
(Sorry I can't get tabs to align in posts - that's very annoying.)

Code: Select all

134a   6   2   |   14b   7   8   |   134c   9   5     
8   14d   9   |   3   14e   5   |   6   2f   7       

5   7   134g   |   6   9   2h   |   134i   8   134j       
-   -   -   +   -   -   -   +   -   -   -   
123k   9   5   |   7   8   4   |   123l   6   123m   

7   1234n   6   |   12o   123p   9   |   8   5   1234q   

1234r   8   134s   |   5   123t   6   |   7   134u   9     

-   -   -   +   -   -   -   +   -   -   -     

1234v   5   7   |   9   6   13w   |   1234x   134y   8

9   13z   8   |   24;   24/   7   |   5   13,   6

6   1234.   134'   |   8   5   13[   |   9   7   1234]

a = 134, b = 14, c = 134, d = 14, e = 14, f = 2, g = 134, h = 2, o = 12, ; = 24, / = 24, w = 13, [ = 13



democrat:
dA: b = 1, o = 2, ; = 4
dB: b = 4, o = 1, ; = 2
dC: b = 4, o = 2, ; = 1

independent:
iA: e = 1, / = 4, pt = 23
iB: e = 2, / = 4, pt = 13
iC: e = 4, / = 2, pt = 13
iD: e = 4, / = 1, pt = 23

republican:
rA: h = 1, w[ = 23
rB: h = 2, w[ = 13


square 2:         dA   dB   dC   iA   iB   iC   iD   rA   rB
2A: b = 1, h = 2, e = 4      *               *   *      *
2B: b = 4, h = 1, e = 2         *   *      *         *
2C: b = 4, h = 2, e = 1         *   *   *               *
                                 
square 5:                                 
5A: o = 1, p = 2, t = 3         *      *         *   *   *
5B: o = 1, p = 3, t = 2         *      *         *   *   *
5C: o = 2, p = 1, t = 3      *      *      *   *      *   *
5D: o = 2, p = 3, t = 1      *      *      *   *      *   *
                                   
square 8:                                 
8A: ; = 1, / = 4, w = 2, [ = 3         *   *   *         *
8B: ; = 1, / = 4, w = 3, [ = 2         *   *   *         *
8C: ; = 2, / = 4, w = 1, [ = 3      *      *   *            *
8D: ; = 2, / = 4, w = 3, [ = 1      *      *   *            *
8E: ; = 4, / = 1, w = 2, [ = 3   *                  *   *   
8F: ; = 4, / = 1, w = 3, [ = 2   *                  *   *
8G: ; = 4, / = 2, w = 1, [ = 3   *               *         *
8H: ; = 4, / = 2, w = 3, [ = 1   *               *         *

column 2:
c2A:   2A5C8G   dAiCrB
c2B:   2A5C8H   dAiCrB
c2C:   2A5D8G   dAiCrB
c2D:   2A5D8H   dAiCrB
c2E:   2C5A8C   dBiArB
c2F:   2C5A8D   dBiArB
c2G:   2C5B8C   dBiArB
c2H:   2C5B8D   dBiArB

top:
tA: a = 1, b = 4, c = 3
tB: a = 3, b = 1, c = 4
tC: a = 3, b = 4, c = 1
tD: a = 4, b = 1, c = 3

mid:
mA: d = 1, e = 2, f = 4
mB: d = 1, e = 4, f = 2
mC: d = 4, e = 1, f = 2
mD: d = 4, e = 2, f = 1

--at this point, i and j are essentially interchangeable--

low:
lA: g = 1, h = 2, ij = 34
lB: g = 3, h = 1, ij = 24
lC: g = 3, h = 2, ij = 14
lD: g = 4, h = 1, ij = 23
lE: g = 4, h = 2, ij = 13

square 1:                     lA   lB   lC   lD   lE
1A: a = 1, d = 4, g = 3      tA            mC mD      *   *
1B: a = 3, d = 1, g = 4         tB tC   mA mB               *   *
1C: a = 3, d = 4, g = 1         tB tC         mC mD   *
1D: a = 4, d = 1, g = 3               tD   mA mB         *   *

square 2:
2A: b = 1, h = 2, e = 4         tB    tD      mB      *      *      *
2B: b = 4, h = 1, e = 2      tA    tC   mA    mD      *      *
2C: b = 4, h = 2, e = 1      tA    tC         mC   *      *      *

square 3:
3A: c = 1, f = 2, i = 3, j = 4         tC      mB mC   *
3B: c = 1, f = 2, i = 4, j = 3         tC      mB mC   *
3C: c = 1, f = 4, i = 2, j = 3         tC   mA               *
3D: c = 1, f = 4, i = 3, j = 2         tC      mA               *
3E: c = 3, f = 1, i = 2, j = 4   tA       tD       mD      *
3F: c = 3, f = 1, i = 4, j = 2   tA       tD       mD      *
3G: c = 3, f = 2, i = 1, j = 4   tA       tD      mB mC         *
3H: c = 3, f = 2, i = 4, j = 1   tA       tD      mB mC         *
3K: c = 4, f = 1, i = 2, j = 3      tB          mD            *
3L: c = 4, f = 1, i = 3, j = 2      tB          mD            *
3M: c = 4, f = 2, i = 1, j = 3      tB         mB mC               *
3N: c = 4, f = 2, i = 3, j = 1      tB         mB mC               *


row1:
r1A: 1A2B3E   tAmDlB
r1B: 1A2B3F   tAmDlB
r1C: 1A2C3G   tAmClC
r1D: 1A2C3H   tAmClC
r1E: 1B2A3M   tAmBlE
r1F: 1B2A3N   tAmBlE
r1G: 1B2B3C   tCmAlD
r1H: 1B2B3D   tCmAlD
r1I: 1C2C3A   tCmClA
r1J: 1C2C3B   tCmClA
r1K: 1D2A3G   tDmBlC
r1L: 1D2A3H   tDmBlC

column 2:
c2A:   2A5C8G   dAiCrB
c2B:   2A5C8H   dAiCrB
c2C:   2A5D8G   dAiCrB
c2D:   2A5D8H   dAiCrB
c2E:   2C5A8C   dBiArB
c2F:   2C5A8D   dBiArB
c2G:   2C5B8C   dBiArB
c2H:   2C5B8D   dBiArB

middle 'T':
mtA:   1A    2C    3(G, H)   5(A, B)   8(C, D)
a = 1, b = 4, c = 3, d = 4, e = 1, f = 2, g = 3, h = 2, o = 1, ; = 2, / = 4, ij = 14, pt = 23, w[ = 13
1   6   2   |   4   7   8   |   3   9   5     
8   4   9   |   3   1   5   |   6   2   7       

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

7   2   6   |   1   3   9   |   8   5   4   

4   8   1   |   5   2   6   |   7   3   9     

-   -   -   +   -   -   -   +   -   -   -     

2   5   7   |   9   6   1   |   3   4   8

9   3   8   |   2   4   7   |   5   1   6

6   1   4   |   8   5   3   |   9   7   23
mtB:   1B   2A   3(M, N) 5(C, D) 8(G, H)
a = 3, b = 1, c = 4, d = 1, e = 4, f = 2, g = 4, h = 2, o = 2, ; = 4, / = 2, ij = 13, pt = 13, w[ = 13
3   6   2   |   1   7   8   |   4   9   5     
8   1   9   |   3   4   5   |   6   2   7       

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

7   4   6   |   2   3   9   |   8   5   1   

2   8   3   |   5   1   6   |   7   4   9     

-   -   -   +   -   -   -   +   -   -   -     

4   5   7   |   9   6   1   |   2   3   8

9   3   8   |   4   2   7   |   5   1   6

6   2   1   |   8   5   3   |   9   7   4
mtC:   1C   2C   3(A, B) 5(A, B) 8(C, D)
a = 3, b = 4, c = 1, d = 4, e = 1, f = 2, g = 1, h = 2, o = 1, ; = 2, / = 4, ij = 34, pt = 23, w[ = 13
134a   6   2   |   14b   7   8   |   134c   9   5     
8   14d   9   |   3   14e   5   |   6   2f   7       

5   7   134g   |   6   9   2h   |   134i   8   134j       
-   -   -   +   -   -   -   +   -   -   -   
123k   9   5   |   7   8   4   |   123l   6   123m   

7   1234n   6   |   12o   123p   9   |   8   5   1234q   

1234r   8   134s   |   5   123t   6   |   7   134u   9     

-   -   -   +   -   -   -   +   -   -   -     

1234v   5   7   |   9   6   13w   |   1234x   134y   8

9   13z   8   |   24;   24/   7   |   5   13,   6

6   1234.   134'   |   8   5   13[   |   9   7   1234]
mtD:   1D   2A   3(G, H)   5(C, D) 8(G, H)
a = 4, b = 1, c = 3, d = 1, e = 4, f = 2, g = 3, h = 2, o = 2, ; = 4, / = 2, ij = 14, pt = 13, w[ = 13
134a   6   2   |   14b   7   8   |   134c   9   5     
8   14d   9   |   3   14e   5   |   6   2f   7       

5   7   134g   |   6   9   2h   |   134i   8   134j       
-   -   -   +   -   -   -   +   -   -   -   
123k   9   5   |   7   8   4   |   123l   6   123m   

7   1234n   6   |   12o   123p   9   |   8   5   1234q   

1234r   8   134s   |   5   123t   6   |   7   134u   9     

-   -   -   +   -   -   -   +   -   -   -     

1234v   5   7   |   9   6   13w   |   1234x   134y   8

9   13z   8   |   24;   24/   7   |   5   13,   6

6   1234.   134'   |   8   5   13[   |   9   7   1234]


So I replied back and asked for explanation and I got this:

It's a method I devised to find a solution. Here's how it works:

First, we number the large squares 1 - 9 like so:
1|2|3
-+-+-
4|5|6
-+-+-
7|8|9

then row 1 is 1 2 and 3, row 2 is 4, 5, and 6, column 1 is 1, 4, and 7, column 2 is 2, 5, and 8.

The idea is to list the possible cases for each square, then list the possible cases for each row and column in terms of the possible cases for each square. Now, if the cases are letters, let's say row 1 has possibilities as follows:

r1A = 1A2A3B
r1B = 1A2A3C
r1C = 1B2C3D

and column 1 has possibilities as follows:

c1A = 1A4C7C
c1B = 1C4A7A

then the left 'r' shape has two possiblities:

lrA = c1A * r1A = 1A2A3B4C7C
lrB = c1A * r1B = 1A2A3C4C7C

and we can then plug in the case numbers and see what happens to the puzzle. It's likely that many of the cases will lead immediately to contradictions, and one might even lead to a solution. Alternatively, we can enumerate column 2 and compare it with lrA and lrB, but this is usually slower.

I got the 2f and 2h after enumerating cases and eliminating impossible ones. It's worth mentioning that they were only incidental to solving the puzzle; the real work happened at the bottom.

So let's analyze the solution. Step 1:

Code: Select all

democrat:
dA: b = 1, o = 2, ; = 4
dB: b = 4, o = 1, ; = 2
dC: b = 4, o = 2, ; = 1

independent:
iA: e = 1, / = 4, pt = 23
iB: e = 2, / = 4, pt = 13
iC: e = 4, / = 2, pt = 13
iD: e = 4, / = 1, pt = 23

republican:
rA: h = 1, w[ = 23
rB: h = 2, w[ = 13


We're starting with the middle column. It's not hard to see that it'll be the easiest one.

democrat is the fourth column; it's so named because it's on the left side. independent is the fifth column, and republican is the sixth. dA, dB, and dC are all the ways democrat can look. iA, iB, iC, and iD are all the ways independent can look. We don't care which of p and t is which, since they're in the same square -- so when we enumerate square cases, it won't help us eliminate p and t combinations.

So let's enumerate square cases:

Code: Select all

square 2:            dA   dB   dC   iA   iB   iC   iD   rA   rB
2A: b = 1, h = 2, e = 4      *               *   *      *
2B: b = 4, h = 1, e = 2         *   *      *         *
2C: b = 4, h = 2, e = 1         *   *   *               *
                                 
square 5:                                 
5A: o = 1, p = 2, t = 3         *      *         *   *   *
5B: o = 1, p = 3, t = 2         *      *         *   *   *
5C: o = 2, p = 1, t = 3      *      *      *   *      *   *
5D: o = 2, p = 3, t = 1      *      *      *   *      *   *
                                   
square 8:                                 
8A: ; = 1, / = 4, w = 2, [ = 3         *   *   *         *
8B: ; = 1, / = 4, w = 3, [ = 2         *   *   *         *
8C: ; = 2, / = 4, w = 1, [ = 3      *      *   *            *
8D: ; = 2, / = 4, w = 3, [ = 1      *      *   *            *
8E: ; = 4, / = 1, w = 2, [ = 3   *                  *   *   
8F: ; = 4, / = 1, w = 3, [ = 2   *                  *   *
8G: ; = 4, / = 2, w = 1, [ = 3   *               *         *
8H: ; = 4, / = 2, w = 3, [ = 1   *               *         *


Now, each case has three associated sets of column cases: they correspond to possibilities for democrat, independent, and republican for the square case. For two cases to occur together in a case for the whole of column 2, they must share a democrat case, an independent case, and a republican case. So, for example, 2A can't occur with 5B since they don't share any democrat cases. We've effectively reduced an exclusive problem, finding sets that don't intersect, to an inclusive one -- finding sets that do. The layout of the stars is a visual aid that makes it easier to tell which combinations are possible and which ones aren't. After combining cases, we're left with just eight possibilities for column 2.

Code: Select all

column 2:
c2A:   2A5C8G   dAiCrB
c2B:   2A5C8H   dAiCrB
c2C:   2A5D8G   dAiCrB
c2D:   2A5D8H   dAiCrB
c2E:   2C5A8C   dBiArB
c2F:   2C5A8D   dBiArB
c2G:   2C5B8C   dBiArB
c2H:   2C5B8D   dBiArB


We're actually going to be solving row 1 in a similar manner. I'm going to ignore the details and just give you the cases, of which there are twelve.

Code: Select all

row1:
r1A: 1A2B3E   tAmDlB
r1B: 1A2B3F   tAmDlB
r1C: 1A2C3G   tAmClC
r1D: 1A2C3H   tAmClC
r1E: 1B2A3M   tAmBlE
r1F: 1B2A3N   tAmBlE
r1G: 1B2B3C   tCmAlD
r1H: 1B2B3D   tCmAlD
r1I: 1C2C3A   tCmClA
r1J: 1C2C3B   tCmClA
r1K: 1D2A3G   tDmBlC
r1L: 1D2A3H   tDmBlC


Now that we've got a row and a column, we can try to combine them. Since square 2 can only have one case at a time, the 2-case from the row case must match the 2-case from the column case. However, this will give us a ridiculous number of cases to enumerate -- 32 to be exact. It's time for us to cheat, and remember that pt, w[, and ij are interchangeable -- at least for now, which means that 5C is equivalent to 5D, 3A is equivalent to 3B, 8G = 8H, and so on, reducing the number of cases for the rows and columns:

Code: Select all

column 2:
c2A:   2A 5(C, D) 8(G, H)
c2B: 2C 5(A, B) 8(G, H)

row 1:
r1A: 1A2B3(E, F)   
r1C: 1A2C3(G, H)   
r1E: 1B2A3(M, N)
r1G: 1B2B3(C, D)
r1I: 1C2C3(A, B)
r1K: 1D2A3(G, H)


so combining cases, we find just four cases for the middle 't' shape:

Code: Select all

middle 'T':
mtA:   1A    2C    3(G, H)   5(A, B)   8(C, D)
a = 1, b = 4, c = 3, d = 4, e = 1, f = 2, g = 3, h = 2, o = 1, ; = 2, / = 4, ij = 14, pt = 23, w[ = 13
1   6   2   |   4   7   8   |   3   9   5     
8   4   9   |   3   1   5   |   6   2   7       

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

7   2   6   |   1   3   9   |   8   5   4   

4   8   1   |   5   2   6   |   7   3   9     

-   -   -   +   -   -   -   +   -   -   -     

2   5   7   |   9   6   1   |   3   4   8

9   3   8   |   2   4   7   |   5   1   6

6   1   4   |   8   5   3   |   9   7   23
mtB:   1B   2A   3(M, N) 5(C, D) 8(G, H)
a = 3, b = 1, c = 4, d = 1, e = 4, f = 2, g = 4, h = 2, o = 2, ; = 4, / = 2, ij = 13, pt = 13, w[ = 13
3   6   2   |   1   7   8   |   4   9   5     
8   1   9   |   3   4   5   |   6   2   7       

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

7   4   6   |   2   3   9   |   8   5   1   

2   8   3   |   5   1   6   |   7   4   9     

-   -   -   +   -   -   -   +   -   -   -     

4   5   7   |   9   6   1   |   2   3   8

9   3   8   |   4   2   7   |   5   1   6

6   2   1   |   8   5   3   |   9   7   4
mtC:   1C   2C   3(A, B) 5(A, B) 8(C, D)
a = 3, b = 4, c = 1, d = 4, e = 1, f = 2, g = 1, h = 2, o = 1, ; = 2, / = 4, ij = 34, pt = 23, w[ = 13
134a   6   2   |   14b   7   8   |   134c   9   5     
8   14d   9   |   3   14e   5   |   6   2f   7       

5   7   134g   |   6   9   2h   |   134i   8   134j       
-   -   -   +   -   -   -   +   -   -   -   
123k   9   5   |   7   8   4   |   123l   6   123m   

7   1234n   6   |   12o   123p   9   |   8   5   1234q   

1234r   8   134s   |   5   123t   6   |   7   134u   9     

-   -   -   +   -   -   -   +   -   -   -     

1234v   5   7   |   9   6   13w   |   1234x   134y   8

9   13z   8   |   24;   24/   7   |   5   13,   6

6   1234.   134'   |   8   5   13[   |   9   7   1234]
mtD:   1D   2A   3(G, H)   5(C, D) 8(G, H)
a = 4, b = 1, c = 3, d = 1, e = 4, f = 2, g = 3, h = 2, o = 2, ; = 4, / = 2, ij = 14, pt = 13, w[ = 13
134a   6   2   |   14b   7   8   |   134c   9   5     
8   14d   9   |   3   14e   5   |   6   2f   7       

5   7   134g   |   6   9   2h   |   134i   8   134j       
-   -   -   +   -   -   -   +   -   -   -   
123k   9   5   |   7   8   4   |   123l   6   123m   

7   1234n   6   |   12o   123p   9   |   8   5   1234q   

1234r   8   134s   |   5   123t   6   |   7   134u   9     

-   -   -   +   -   -   -   +   -   -   -     

1234v   5   7   |   9   6   13w   |   1234x   134y   8

9   13z   8   |   24;   24/   7   |   5   13,   6

6   1234.   134'   |   8   5   13[   |   9   7   1234]


For each case, we enumerate variables (using the square cases as guides), then plug them in and simplify. mtA is an obvious combination, and, lo and behold, mtB solves the puzzle.

Also, I can totally use the royal 'we', because I'm the King of England.

Solving time: 2h34m

To say the least I find this completely baffling. I don't know what you will make of it.

[StrmCkr]

to me this reads as if they are doing manual trial and error, of permutations of rows in whole,
compared to each other row.

removing reducdant checks based on limitations of grid.

[eleven]

So just out of boredom I decided to post the 9.0 rated puzzle from the maximum number of clues thread ...

I dont know, what you posted, but what i can see here as pencilmarks is rated 7.2.
Though it is not easy, you could write a short and clear solution - without needing His Majesties elaborate, but insufficient and incomprehensible explanations. Even if his way to solve is correct, it seems to be very laborious.

[999_Springs]

Thanks for the responses - I'll try to understand what he is going on about.
StrmCkr: is what you're describing basically the same as aligned pair exclusion with entire rows/columns instead of cells? That seems very laborious indeed.

I dont know, what you posted, but what i can see here as pencilmarks is rated 7.2.

Well,

I got the 2f and 2h after enumerating cases and eliminating impossible ones.

In other words the results of all four "cases" have r3c6=r2c8=2 in common. They weren't part of the original puzzle.

Oh, and no, I don't play sudoku regularly. It's too much goddamned work.

[StrmCkr]

much worse... im afraid.

its basically assembling the possible outcomes of each row.

listing them all out.

assinging them a case name
for example

R1 can be
123456789
321456789
etc:


then take R1 Case a compare it to R2 Case A check subgrid for contradiction if none goto
r3 case A check the three rows vrs grid check for contradictios or erros.

if a sub check finds an error go back a step delete selected case.
repeate untill
only 1 case per row remains.

very long and tedious indeed.

[999_Springs]

Slightly off-topic:

999: do you have a simpler method?

I attacked the puzzle myself using some more... normal... methods to see what I could come up with. My last step before the singles tail was this:

Code: Select all

13   6    2   |14  7    8   |134  9    5
8    14   9   |3   124  5   |6    12   7
5    7    134 |6   9    12  |134  8    123
--------------+-------------+--------------
123  9    5   |7   8    4   |13   6    123
7    134  6   |12  13   9   |8    5    1234
1234 8    13  |5   123  6   |7    1234 9
--------------+-------------+--------------
134  5    7   |9   6    13  |2    134  8
9    123  8   |124 24   7   |5    13   6
6    123  134 |8   5    123 |9    7    134


ALS XY-Wing Rule:
ALS A = 124r2c28
ALS B = 124r1c4r2c5
ALS C = 134r5c25
2 restricted common to A, B
4 restricted common to B, C
1 common to B, C
r5c4<>1 ???

The problem is that 1r5c4 doesn't see all the 1 candidates in B and C, but if you follow the als-chain it definitely works. How do you rewrite this without any... uh... contentious issues in the als-chain?

[ronk]

r5c4<>1 ???

The problem is that 1r5c4 doesn't see all the 1 candidates in B and C, but if you follow the als-chain it definitely works. How do you rewrite this without any... uh... contentious issues in the als-chain?

An ALS xy-wing won't work. Write it as an ALS chain comprised of 4 ALSs, with two of them being the bivalues r1c4 and r2c2.

[eleven]

There are other experts in ALS notations here.

I dont need one, this elimination i probably would find using a method by aran:
Looking at r5c25 we either have a pair 13 or r5c2=4. The latter implies r2c2<>4, r2c5=4 and r1c4=1.
So one of r5c25 and r1c4 must be 1.

I know, that many people would (deprecatingly) call this a t&e method. Yes it is, like all ALS finding methods

[Luke]

There are other experts in ALS notations here.

I dont need one, this elimination i probably would find using a method by aran:
Looking at r5c25 we either have a pair 13 or r5c2=4. The latter implies r2c2<>4, r2c5=4 and r1c4=1.
So one of r5c25 and r1c4 must be 1.

I know, that many people would (deprecatingly) call this a t&e method. Yes it is, like all ALS finding methods

I was just working out the following chain as you posted that:

Code: Select all

13   6    2   |14  7    8   |134  9    5
8    14   9   |3   124  5   |6    12   7
5    7    134 |6   9    12  |134  8    123
--------------+-------------+--------------
123  9    5   |7   8    4   |13   6    123
7    134  6   |12  13   9   |8    5    1234
1234 8    13  |5   123  6   |7    1234 9
--------------+-------------+--------------
134  5    7   |9   6    13  |2    134  8
9    123  8   |124 24   7   |5    13   6
6    123  134 |8   5    123 |9    7    134

13r5c25=4r5c2-(4=1)r2c2-(1=2)r2c8-(2=41)r2c5-(4=1)r1c4 =>r5c4<>1

The red high-light references the prior strong inference on the 1. This doesn't seem like trial and error, to me anyway.

Added: Shorter and better, eleven's way:
13r5c25=4r5c2-4r2c2=4r2c5-(4=1)r1c4 =>r5c4<>1

[ttt]

13r5c25=4r5c2-(4=1)r2c2-(1=2)r2c8-(2=41)r2c5-(4=1)r1c4 =>r5c4<>1
The red high-light references the prior strong inference on the 1. This doesn't seem like trial and error, to me anyway.

Added: Shorter and better, eleven's way:
13r5c25=4r5c2-4r2c2=4r2c5-(4=1)r1c4 =>r5c4<>1

Yes, I was waiting for that...

ttt