c Nd253_277_1 79
c o1_0_0 72
c Nd25_36_3 52
c Nd253_277_0 75
c Nd25_36_2 42
c Nd24_36_4 70
c Nd25_36_1 31
c Nd24_36_3 57
c Nd25_36_0 35
c Nd24_36_2 47
c Nd25_37_4 59
c Nd24_36_1 37
c Nd25_37_3 22
c Nd25_37_2 16
c r_i1_0_0 90
c r_i1_0_1 94
c Nd25_37_1 10
c Nd24_37_4 68
c r_i1_0_2 97
c Nd25_37_0 4
c Nd24_37_3 55
c r_i1_0_3 100
c Nd24_37_2 45
c r_i1_0_4 103
c Nd13_84_3 62
c Nd24_37_1 34
c Nd13_84_2 49
c i1_0_-1 91
c machine_concret1.m_state_1_0 6
c Nd13_84_1 39
c machine_concret1.m_state_1_1 12
c Nd13_84_0 28
c Nd12_84_3 66
c Nd12_84_2 53
c machine_concret1.m_state_1_2 18
c Nd12_84_1 43
c machine_concret1.m_state_1_3 24
c Nd12_84_0 32
c machine_concret1.m_state_1_4 61
c machine_concret1.m_state_0_0 5
c o2_0_4 21
c i1_0_0 29
c machine_concret1.m_state_0_1 11
c o2_0_3 15
c i1_0_1 40
c o1_0_4 86
c machine_concret1.m_state_0_2 17
c o2_0_2 9
c i1_0_2 50
c machine_concret1.m_state_0_3 23
c o2_0_1 3
c i1_0_3 63
c o1_0_3 82
c machine_concret1.m_state_0_4 60
c o2_0_0 1
c Nd253_277_3 87
c o1_0_2 78
c Nd25_36_4 65
c Nd253_277_2 83
c o1_0_1 74
p cnf 105 257
1 2 0
-1 -2 0
2 0
5 6 4 0
-5 -4 0
-6 -4 0
3 -4 7 0
-3 -7 0
4 -7 0
-3 4 8 0
3 -8 0
-4 -8 0
7 8 0
11 12 10 0
-11 -10 0
-12 -10 0
9 -10 13 0
-9 -13 0
10 -13 0
-9 10 14 0
9 -14 0
-10 -14 0
13 14 0
17 18 16 0
-17 -16 0
-18 -16 0
15 -16 19 0
-15 -19 0
16 -19 0
-15 16 20 0
15 -20 0
-16 -20 0
19 20 0
23 24 22 0
-23 -22 0
-24 -22 0
21 -22 25 0
-21 -25 0
22 -25 0
-21 22 26 0
21 -26 0
-22 -26 0
25 26 0
-4 27 0
4 -27 0
27 0
29 -4 28 0
-29 -28 0
4 -28 0
-10 -28 30 0
10 -30 0
28 -30 0
11 -12 31 0
-11 -31 0
12 -31 0
-29 -4 32 0
29 -32 0
4 -32 0
-31 -32 33 0
31 -33 0
32 -33 0
-11 12 34 0
11 -34 0
-12 -34 0
5 -6 35 0
-5 -35 0
6 -35 0
-34 -35 36 0
34 -36 0
35 -36 0
-11 -12 37 0
11 -37 0
12 -37 0
-37 -5 38 0
37 -38 0
5 -38 0
30 33 36 38 0
40 -10 39 0
-40 -39 0
10 -39 0
-16 -39 41 0
16 -41 0
39 -41 0
17 -18 42 0
-17 -42 0
18 -42 0
-40 -10 43 0
40 -43 0
10 -43 0
-42 -43 44 0
42 -44 0
43 -44 0
-17 18 45 0
17 -45 0
-18 -45 0
-45 -31 46 0
45 -46 0
31 -46 0
-17 -18 47 0
17 -47 0
18 -47 0
-47 -11 48 0
47 -48 0
11 -48 0
41 44 46 48 0
50 -16 49 0
-50 -49 0
16 -49 0
-22 -49 51 0
22 -51 0
49 -51 0
23 -24 52 0
-23 -52 0
24 -52 0
-50 -16 53 0
50 -53 0
16 -53 0
-52 -53 54 0
52 -54 0
53 -54 0
-23 24 55 0
23 -55 0
-24 -55 0
-55 -42 56 0
55 -56 0
42 -56 0
-23 -24 57 0
23 -57 0
24 -57 0
-57 -17 58 0
57 -58 0
17 -58 0
51 54 56 58 0
60 61 59 0
-60 -59 0
-61 -59 0
63 -22 62 0
-63 -62 0
22 -62 0
-59 -62 64 0
59 -64 0
62 -64 0
60 -61 65 0
-60 -65 0
61 -65 0
-63 -22 66 0
63 -66 0
22 -66 0
-65 -66 67 0
65 -67 0
66 -67 0
-60 61 68 0
60 -68 0
-61 -68 0
-68 -52 69 0
68 -69 0
52 -69 0
-60 -61 70 0
60 -70 0
61 -70 0
-70 -23 71 0
70 -71 0
23 -71 0
64 67 69 71 0
72 73 0
-72 -73 0
73 0
28 35 75 0
-28 -75 0
-35 -75 0
74 75 76 0
-74 -76 0
-75 -76 0
-74 -75 77 0
74 -77 0
75 -77 0
76 77 0
39 31 79 0
-39 -79 0
-31 -79 0
78 79 80 0
-78 -80 0
-79 -80 0
-78 -79 81 0
78 -81 0
79 -81 0
80 81 0
49 42 83 0
-49 -83 0
-42 -83 0
82 83 84 0
-82 -84 0
-83 -84 0
-82 -83 85 0
82 -85 0
83 -85 0
84 85 0
62 52 87 0
-62 -87 0
-52 -87 0
86 87 88 0
-86 -88 0
-87 -88 0
-86 -87 89 0
86 -89 0
87 -89 0
88 89 0
90 91 92 0
-90 -92 0
-91 -92 0
-90 -91 93 0
90 -93 0
91 -93 0
92 93 0
94 29 95 0
-94 -95 0
-29 -95 0
-94 -29 96 0
94 -96 0
29 -96 0
95 96 0
97 40 98 0
-97 -98 0
-40 -98 0
-97 -40 99 0
97 -99 0
40 -99 0
98 99 0
100 50 101 0
-100 -101 0
-50 -101 0
-100 -50 102 0
100 -102 0
50 -102 0
101 102 0
103 63 104 0
-103 -104 0
-63 -104 0
-103 -63 105 0
103 -105 0
63 -105 0
104 105 0
-72 0
-1 0
-90 0
74 0
-3 0
-94 0
78 0
-9 0
-97 0
82 0
-15 0
-100 0
86 0
-21 0
-103 0