r0_c0 + r0_c1 + r0_c2 + r1_c0 + r1_c2 + r2_c0 + r2_c1 + r2_c2 == 0 r0_c1 + r0_c2 + r0_c3 + r1_c1 + r1_c3 + r2_c1 + r2_c2 + r2_c3 == 1 r0_c3 + r0_c4 + r0_c5 + r1_c3 + r1_c5 + r2_c3 + r2_c4 + r2_c5 == 1 r0_c4 + r0_c5 + r0_c6 + r1_c4 + r1_c6 + r2_c4 + r2_c5 + r2_c6 == 0 r0_c5 + r0_c6 + r0_c7 + r1_c5 + r1_c7 + r2_c5 + r2_c6 + r2_c7 == 0 r0_c6 + r0_c7 + r0_c8 + r1_c6 + r1_c8 + r2_c6 + r2_c7 + r2_c8 == 0 r0_c7 + r0_c8 + r0_c9 + r1_c7 + r1_c9 + r2_c7 + r2_c8 + r2_c9 == 1 r1_c0 + r1_c1 + r1_c2 + r2_c0 + r2_c2 + r3_c0 + r3_c1 + r3_c2 == 0 r1_c1 + r1_c2 + r1_c3 + r2_c1 + r2_c3 + r3_c1 + r3_c2 + r3_c3 == 1 r1_c3 + r1_c4 + r1_c5 + r2_c3 + r2_c5 + r3_c3 + r3_c4 + r3_c5 == 1 r1_c4 + r1_c5 + r1_c6 + r2_c4 + r2_c6 + r3_c4 + r3_c5 + r3_c6 == 0 r1_c5 + r1_c6 + r1_c7 + r2_c5 + r2_c7 + r3_c5 + r3_c6 + r3_c7 == 0 r1_c6 + r1_c7 + r1_c8 + r2_c6 + r2_c8 + r3_c6 + r3_c7 + r3_c8 == 0 r1_c7 + r1_c8 + r1_c9 + r2_c7 + r2_c9 + r3_c7 + r3_c8 + r3_c9 == 1 r1_c8 + r1_c9 + r1_c10 + r2_c8 + r2_c10 + r3_c8 + r3_c9 + r3_c10 == 1 r2_c0 + r2_c1 + r2_c2 + r3_c0 + r3_c2 + r4_c0 + r4_c1 + r4_c2 == 0 r2_c1 + r2_c2 + r2_c3 + r3_c1 + r3_c3 + r4_c1 + r4_c2 + r4_c3 == 1 r2_c2 + r2_c3 + r2_c4 + r3_c2 + r3_c4 + r4_c2 + r4_c3 + r4_c4 == 1 r2_c3 + r2_c4 + r2_c5 + r3_c3 + r3_c5 + r4_c3 + r4_c4 + r4_c5 == 1 r2_c4 + r2_c5 + r2_c6 + r3_c4 + r3_c6 + r4_c4 + r4_c5 + r4_c6 == 0 r2_c5 + r2_c6 + r2_c7 + r3_c5 + r3_c7 + r4_c5 + r4_c6 + r4_c7 == 0 r2_c6 + r2_c7 + r2_c8 + r3_c6 + r3_c8 + r4_c6 + r4_c7 + r4_c8 == 0 r2_c7 + r2_c8 + r2_c9 + r3_c7 + r3_c9 + r4_c7 + r4_c8 + r4_c9 == 0 r2_c8 + r2_c9 + r2_c10 + r3_c8 + r3_c10 + r4_c8 + r4_c9 + r4_c10 == 0 r3_c0 + r3_c1 + r3_c2 + r4_c0 + r4_c2 + r5_c0 + r5_c1 + r5_c2 == 0 r3_c1 + r3_c2 + r3_c3 + r4_c1 + r4_c3 + r5_c1 + r5_c2 + r5_c3 == 0 r3_c2 + r3_c3 + r3_c4 + r4_c2 + r4_c4 + r5_c2 + r5_c3 + r5_c4 == 0 r3_c3 + r3_c4 + r3_c5 + r4_c3 + r4_c5 + r5_c3 + r5_c4 + r5_c5 == 0 r3_c4 + r3_c5 + r3_c6 + r4_c4 + r4_c6 + r5_c4 + r5_c5 + r5_c6 == 0 r3_c5 + r3_c6 + r3_c7 + r4_c5 + r4_c7 + r5_c5 + r5_c6 + r5_c7 == 0 r3_c6 + r3_c7 + r3_c8 + r4_c6 + r4_c8 + r5_c6 + r5_c7 + r5_c8 == 0 r3_c7 + r3_c8 + r3_c9 + r4_c7 + r4_c9 + r5_c7 + r5_c8 + r5_c9 == 0 r3_c8 + r3_c9 + r3_c10 + r4_c8 + r4_c10 + r5_c8 + r5_c9 + r5_c10 == 0 r4_c0 + r4_c1 + r4_c2 + r5_c0 + r5_c2 + r6_c0 + r6_c1 + r6_c2 == 1 r4_c1 + r4_c2 + r4_c3 + r5_c1 + r5_c3 + r6_c1 + r6_c2 + r6_c3 == 1 r4_c2 + r4_c3 + r4_c4 + r5_c2 + r5_c4 + r6_c2 + r6_c3 + r6_c4 == 1 r4_c3 + r4_c4 + r4_c5 + r5_c3 + r5_c5 + r6_c3 + r6_c4 + r6_c5 == 1 r4_c4 + r4_c5 + r4_c6 + r5_c4 + r5_c6 + r6_c4 + r6_c5 + r6_c6 == 1 r4_c5 + r4_c6 + r4_c7 + r5_c5 + r5_c7 + r6_c5 + r6_c6 + r6_c7 == 0 r4_c6 + r4_c7 + r4_c8 + r5_c6 + r5_c8 + r6_c6 + r6_c7 + r6_c8 == 0 r4_c7 + r4_c8 + r4_c9 + r5_c7 + r5_c9 + r6_c7 + r6_c8 + r6_c9 == 1 r4_c8 + r4_c9 + r4_c10 + r5_c8 + r5_c10 + r6_c8 + r6_c9 + r6_c10 == 1 r5_c4 + r5_c5 + r5_c6 + r6_c4 + r6_c6 + r7_c4 + r7_c5 + r7_c6 == 1 r5_c5 + r5_c6 + r5_c7 + r6_c5 + r6_c7 + r7_c5 + r7_c6 + r7_c7 == 0 r5_c6 + r5_c7 + r5_c8 + r6_c6 + r6_c8 + r7_c6 + r7_c7 + r7_c8 == 0 r5_c7 + r5_c8 + r5_c9 + r6_c7 + r6_c9 + r7_c7 + r7_c8 + r7_c9 == 1 r6_c4 + r6_c5 + r6_c6 + r7_c4 + r7_c6 + r8_c4 + r8_c5 + r8_c6 == 3 r6_c5 + r6_c6 + r6_c7 + r7_c5 + r7_c7 + r8_c5 + r8_c6 + r8_c7 == 1 r6_c6 + r6_c7 + r6_c8 + r7_c6 + r7_c8 + r8_c6 + r8_c7 + r8_c8 == 0 r6_c7 + r6_c8 + r6_c9 + r7_c7 + r7_c9 + r8_c7 + r8_c8 + r8_c9 == 1 r7_c5 + r7_c6 + r7_c7 + r8_c5 + r8_c7 + r9_c5 + r9_c6 + r9_c7 == 2 r7_c6 + r7_c7 + r7_c8 + r8_c6 + r8_c8 + r9_c6 + r9_c7 + r9_c8 == 1 r7_c7 + r7_c8 + r7_c9 + r8_c7 + r8_c9 + r9_c7 + r9_c8 + r9_c9 == 1 row=1 col=3, unsat!