p cnf 111 386
-1 23 0
-23 24 0
-2 -23 25 0
-25 26 0
-3 -25 27 0
-27 28 0
-4 -27 29 0
-29 30 0
-5 -29 31 0
-31 32 0
-6 -31 0
-2 24 0
-24 33 0
-3 -24 26 0
-26 34 0
-4 -26 28 0
-28 35 0
-5 -28 30 0
-30 36 0
-6 -30 32 0
-32 37 0
-7 -32 0
-3 33 0
-33 38 0
-4 -33 34 0
-34 39 0
-5 -34 35 0
-35 40 0
-6 -35 36 0
-36 41 0
-7 -36 37 0
-37 42 0
-8 -37 0
-4 38 0
-38 43 0
-5 -38 39 0
-39 44 0
-6 -39 40 0
-40 45 0
-7 -40 41 0
-41 46 0
-8 -41 42 0
-42 47 0
-9 -42 0
-5 43 0
-43 48 0
-6 -43 44 0
-44 49 0
-7 -44 45 0
-45 50 0
-8 -45 46 0
-46 51 0
-9 -46 47 0
-47 52 0
-10 -47 0
-6 48 0
-48 53 0
-7 -48 49 0
-49 54 0
-8 -49 50 0
-50 55 0
-9 -50 51 0
-51 56 0
-10 -51 52 0
-52 57 0
-11 -52 0
-7 53 0
-53 58 0
-8 -53 54 0
-54 59 0
-9 -54 55 0
-55 60 0
-10 -55 56 0
-56 61 0
-11 -56 57 0
-57 62 0
-12 -57 0
-8 58 0
-58 63 0
-9 -58 59 0
-59 64 0
-10 -59 60 0
-60 65 0
-11 -60 61 0
-61 66 0
-12 -61 62 0
-62 67 0
-13 -62 0
-9 63 0
-63 68 0
-10 -63 64 0
-64 69 0
-11 -64 65 0
-65 70 0
-12 -65 66 0
-66 71 0
-13 -66 67 0
-67 72 0
-14 -67 0
-10 68 0
-68 73 0
-11 -68 69 0
-69 74 0
-12 -69 70 0
-70 75 0
-13 -70 71 0
-71 76 0
-14 -71 72 0
-72 77 0
-15 -72 0
-11 73 0
-73 78 0
-12 -73 74 0
-74 79 0
-13 -74 75 0
-75 80 0
-14 -75 76 0
-76 81 0
-15 -76 77 0
-77 82 0
-16 -77 0
-12 78 0
-78 83 0
-13 -78 79 0
-79 84 0
-14 -79 80 0
-80 85 0
-15 -80 81 0
-81 86 0
-16 -81 82 0
-82 87 0
-17 -82 0
-13 83 0
-83 88 0
-14 -83 84 0
-84 89 0
-15 -84 85 0
-85 90 0
-16 -85 86 0
-86 91 0
-17 -86 87 0
-87 92 0
-18 -87 0
-14 88 0
-88 93 0
-15 -88 89 0
-89 94 0
-16 -89 90 0
-90 95 0
-17 -90 91 0
-91 96 0
-18 -91 92 0
-92 97 0
-19 -92 0
-15 93 0
-93 98 0
-16 -93 94 0
-94 99 0
-17 -94 95 0
-95 100 0
-18 -95 96 0
-96 101 0
-19 -96 97 0
-97 102 0
-20 -97 0
-16 98 0
-98 103 0
-17 -98 99 0
-99 104 0
-18 -99 100 0
-100 105 0
-19 -100 101 0
-101 106 0
-20 -101 102 0
-102 107 0
-21 -102 0
-17 103 0
-18 -103 104 0
-19 -104 105 0
-20 -105 106 0
-21 -106 107 0
-22 -107 0
-108 1 0
-108 -12 0
-108 2 0
-108 11 0
-109 1 0
-109 -2 0
-109 11 0
-109 12 0
-110 12 0
-110 -1 0
-110 17 0
-110 18 0
-111 12 0
-111 -17 0
-111 1 0
-111 18 0
108 109 110 111 0
2 5 6 7 10 11 13 14 15 19 20 22 0
2 3 6 7 8 11 13 15 16 20 21 22 0
1 3 6 7 8 11 12 14 15 16 20 21 0
1 3 4 7 8 9 12 14 16 17 21 22 0
1 2 4 7 8 9 13 15 16 17 21 22 0
2 4 5 8 9 10 12 13 15 17 18 22 0
2 3 5 8 9 10 12 14 16 17 18 22 0
3 5 6 9 10 11 12 13 14 16 18 19 0
3 4 6 9 10 11 12 13 15 17 18 19 0
1 4 6 7 10 11 13 14 15 17 19 20 0
1 4 5 7 10 11 13 14 16 18 19 20 0
1 2 5 7 8 11 14 15 16 18 20 21 0
1 2 5 6 8 11 14 15 17 19 20 21 0
1 2 3 6 8 9 15 16 17 19 21 22 0
1 2 3 6 7 9 15 16 18 20 21 22 0
2 3 4 7 9 10 12 16 17 18 20 22 0
2 3 4 7 8 10 12 16 17 19 21 22 0
3 4 5 8 10 11 12 13 17 18 19 21 0
3 4 5 8 9 11 12 13 17 18 20 22 0
1 4 5 6 9 11 13 14 18 19 20 22 0
1 4 5 6 9 10 12 13 14 18 19 21 0
1 2 5 6 7 10 12 14 15 19 20 21 0
2 5 6 7 9 11 13 14 15 21 22 0
2 4 6 7 8 11 13 14 20 21 22 0
1 3 6 7 8 10 12 14 15 16 22 0
1 3 5 7 8 9 12 14 15 21 22 0
2 4 7 8 9 11 12 13 15 16 17 0
2 4 6 8 9 10 12 13 15 16 22 0
1 3 5 8 9 10 13 14 16 17 18 0
3 5 7 9 10 11 12 13 14 16 17 0
2 4 6 9 10 11 14 15 17 18 19 0
1 4 6 8 10 11 13 14 15 17 18 0
1 3 5 7 10 11 15 16 18 19 20 0
1 2 5 7 9 11 14 15 16 18 19 0
1 2 4 6 8 11 16 17 19 20 21 0
1 2 3 6 8 10 15 16 17 19 20 0
1 2 3 5 7 9 17 18 20 21 22 0
2 3 4 7 9 11 16 17 18 20 21 0
2 3 4 6 8 10 12 18 19 21 22 0
1 3 4 5 8 10 17 18 19 21 22 0
3 4 5 7 9 11 12 13 19 20 22 0
2 4 5 6 9 11 12 18 19 20 22 0
1 4 5 6 8 10 12 13 14 20 21 0
1 3 5 6 7 10 12 13 19 20 21 0
2 5 6 7 9 11 13 14 15 16 22 0
2 4 6 7 8 11 13 19 20 21 22 0
1 3 6 7 8 10 12 14 15 16 17 0
1 3 5 7 8 9 12 14 20 21 22 0
2 4 7 8 9 11 13 15 16 17 18 0
2 4 6 8 9 10 12 13 15 21 22 0
1 3 5 8 9 10 14 16 17 18 19 0
3 5 7 9 10 11 12 13 14 16 22 0
2 4 6 9 10 11 15 17 18 19 20 0
1 4 6 8 10 11 12 13 14 15 17 0
1 3 5 7 10 11 16 18 19 20 21 0
1 2 5 7 9 11 13 14 15 16 18 0
1 2 4 6 8 11 17 19 20 21 22 0
1 2 3 6 8 10 14 15 16 17 19 0
1 2 3 5 7 9 12 18 20 21 22 0
2 3 4 7 9 11 15 16 17 18 20 0
2 3 4 6 8 10 12 13 19 21 22 0
1 3 4 5 8 10 16 17 18 19 21 0
3 4 5 7 9 11 12 13 14 20 22 0
2 4 5 6 9 11 17 18 19 20 22 0
1 4 5 6 8 10 12 13 14 15 21 0
1 3 5 6 7 10 12 18 19 20 21 0
3 5 7 9 13 19 20 21 0
4 6 8 10 14 15 16 22 0
4 6 8 10 14 20 21 22 0
5 7 9 11 12 15 16 17 0
5 7 9 11 12 15 21 22 0
1 6 8 10 13 16 17 18 0
1 6 8 10 12 13 16 22 0
2 7 9 11 14 17 18 19 0
2 7 9 11 12 13 14 17 0
1 3 8 10 15 18 19 20 0
1 3 8 10 13 14 15 18 0
2 4 9 11 16 19 20 21 0
2 4 9 11 14 15 16 19 0
1 3 5 10 17 20 21 22 0
1 3 5 10 15 16 17 20 0
2 4 6 11 12 18 21 22 0
2 4 6 11 16 17 18 21 0
1 3 5 7 12 13 19 22 0
1 3 5 7 17 18 19 22 0
2 4 6 8 12 13 14 20 0
2 4 6 8 12 18 19 20 0
3 5 7 9 13 14 15 21 0
2 4 6 7 9 11 13 14 21 22 0
1 3 5 7 8 10 12 14 15 22 0
2 4 6 8 9 11 12 13 15 16 0
1 3 5 7 9 10 13 14 16 17 0
2 4 6 8 10 11 14 15 17 18 0
1 3 5 7 9 11 15 16 18 19 0
1 2 4 6 8 10 16 17 19 20 0
2 3 5 7 9 11 17 18 20 21 0
1 3 4 6 8 10 18 19 21 22 0
2 4 5 7 9 11 12 19 20 22 0
1 3 5 6 8 10 12 13 20 21 0
2 3 6 7 9 11 13 15 16 19 22 0
2 4 6 7 10 11 13 16 19 20 22 0
1 3 4 7 8 10 12 14 16 17 20 0
1 3 5 7 8 11 12 14 17 20 21 0
2 4 5 8 9 11 13 15 17 18 21 0
1 2 4 6 8 9 13 15 18 21 22 0
1 3 5 6 9 10 14 16 18 19 22 0
2 3 5 7 9 10 12 14 16 19 22 0
2 4 6 7 10 11 12 15 17 19 20 0
3 4 6 8 10 11 12 13 15 17 20 0
1 3 5 7 8 11 13 16 18 20 21 0
1 4 5 7 9 11 13 14 16 18 21 0
1 2 4 6 8 9 14 17 19 21 22 0
1 2 5 6 8 10 14 15 17 19 22 0
2 3 5 7 9 10 12 15 18 20 22 0
2 3 6 7 9 11 12 15 16 18 20 0
3 4 6 8 10 11 12 13 16 19 21 0
1 3 4 7 8 10 13 16 17 19 21 0
1 4 5 7 9 11 13 14 17 20 22 0
2 4 5 8 9 11 14 17 18 20 22 0
1 2 5 6 8 10 12 14 15 18 21 0
1 3 5 6 9 10 12 15 18 19 21 0
2 5 7 10 11 13 14 15 16 19 20 0
2 3 6 8 11 15 16 19 20 21 22 0
1 3 6 8 11 14 15 16 17 20 21 0
1 3 4 7 9 12 16 17 20 21 22 0
1 2 4 7 9 15 16 17 18 21 22 0
2 4 5 8 10 12 13 17 18 21 22 0
2 3 5 8 10 12 16 17 18 19 22 0
3 5 6 9 11 12 13 14 18 19 22 0
3 4 6 9 11 12 13 17 18 19 20 0
1 4 6 7 10 12 13 14 15 19 20 0
1 4 5 7 10 13 14 18 19 20 21 0
2 5 7 8 11 13 14 15 16 20 21 0
2 5 6 8 11 14 15 19 20 21 22 0
1 3 6 8 9 14 15 16 17 21 22 0
1 3 6 7 9 12 15 16 20 21 22 0
2 4 7 9 10 12 15 16 17 18 22 0
2 4 7 8 10 12 13 16 17 21 22 0
3 5 8 10 11 12 13 16 17 18 19 0
3 5 8 9 11 12 13 14 17 18 22 0
1 4 6 9 11 13 14 17 18 19 20 0
1 4 6 9 10 12 13 14 15 18 19 0
1 2 5 7 10 14 15 18 19 20 21 0
3 6 8 13 15 16 17 18 20 0
5 7 10 15 17 18 19 20 22 0
4 7 9 14 16 17 18 19 21 0
6 8 11 12 16 18 19 20 21 0
5 8 10 15 17 18 19 20 22 0
1 7 9 13 17 19 20 21 22 0
6 9 11 12 16 18 19 20 21 0
2 8 10 12 14 18 20 21 22 0
1 7 10 13 17 19 20 21 22 0
3 9 11 12 13 15 19 21 22 0
2 8 11 12 14 18 20 21 22 0
1 4 10 12 13 14 16 20 22 0
1 3 9 12 13 15 19 21 22 0
2 5 11 12 13 14 15 17 21 0
2 4 10 12 13 14 16 20 22 0
1 3 6 13 14 15 16 18 22 0
3 5 11 12 13 14 15 17 21 0
2 4 7 12 14 15 16 17 19 0
1 4 6 13 14 15 16 18 22 0
3 5 8 13 15 16 17 18 20 0
2 5 7 12 14 15 16 17 19 0
4 6 9 14 16 17 18 19 21 0
3 4 7 10 13 16 17 18 19 20 22 0
3 6 9 10 13 15 16 17 18 19 22 0
4 5 8 11 12 14 17 18 19 20 21 0
4 7 10 11 12 14 16 17 18 19 20 0
1 5 6 9 13 15 18 19 20 21 22 0
1 5 8 11 13 15 17 18 19 20 21 0
2 6 7 10 12 14 16 19 20 21 22 0
1 2 6 9 14 16 18 19 20 21 22 0
3 7 8 11 12 13 15 17 20 21 22 0
2 3 7 10 12 15 17 19 20 21 22 0
1 4 8 9 12 13 14 16 18 21 22 0
3 4 8 11 12 13 16 18 20 21 22 0
2 5 9 10 12 13 14 15 17 19 22 0
1 4 5 9 12 13 14 17 19 21 22 0
3 6 10 11 12 13 14 15 16 18 20 0
2 5 6 10 12 13 14 15 18 20 22 0
1 4 7 11 13 14 15 16 17 19 21 0
3 6 7 11 12 13 14 15 16 19 21 0
1 2 5 8 14 15 16 17 18 20 22 0
1 4 7 8 13 14 15 16 17 20 22 0
2 3 6 9 12 15 16 17 18 19 21 0
2 5 8 9 12 14 15 16 17 18 21 0