c Nd85_1296_0 68
c Nd156_564_-1 5
c machine_concret1_a1.state_2_0 58
c Nd180_193_-1 16
c o1_0_0 1
c Nd733_2976_-1 12
c Nd72_805_-1 47
c Nd85_1260_0 63
c Nd145_624_-1 27
c Nd61_829_-1 32
c Nd145_672_-1 44
c Nd145_768_-1 19
c Nd168_745_-1 98
c Nd120_133_0 71
c Nd733_1728_-1 31
c Nd97_1248_0 64
c machine_concret1_a1.state$raw_na$initial$_nb_3_-1 10
c Nd709_3576_-1 2
c machine_concret1_a1.state$raw_na$initial$_nb_2_-1 8
c Nd49_781_-1 17
c Nd685_4320_-1 43
c Nd96_1320_0 80
c Nd156_756_-1 20
c Nd168_600_-1 29
c Nd168_744_-1 21
c machine_concret1_a1.state_1_0 56
c Nd805_985_-1 92
c Nd85_1500_0 76
c Nd180_192_-1 22
c Nd709_2664_-1 46
c machine_concret1_a1.nd_r_i1_0_-1 48
c r_i1_0_0 38
c Nd120_132_0 82
c Nd121_132_0 66
c Nd697_901_-1 96
c Nd108_1116_0 70
c Nd145_696_-1 3
c Nd157_564_-1 41
c machine_concret1_a1.state$raw_na$initial$_nb_4_-1 11
c machine_concret1_a1.state$raw_na$initial$_nb_1_-1 6
c Nd157_888_-1 97
c machine_concret1_a1.state_0_0 54
c Nd169_600_-1 50
c Nd157_612_-1 28
c Nd84_1080_0 84
c Nd85_1452_0 73
c Nd121_133_0 59
c Nd168_552_-1 7
c Nd169_744_-1 35
c Nd108_1164_0 81
c Nd96_1212_0 74
c Nd168_648_-1 15
c machine_concret1_a1.state_4_0 61
c Nd145_973_-1 93
c Nd85_1524_0 79
c Nd108_1068_0 65
c Nd637_3600_-1 26
c Nd145_576_-1 40
c Nd181_193_-1 9
c Nd589_5616_-1 39
c Nd85_1224_0 53
c Nd637_4956_-1 42
c Nd145_720_-1 13
c Nd721_924_-1 95
c Nd108_1020_0 57
c Nd829_996_-1 91
c Nd97_1284_0 69
c machine_concret1_a1.nd_o1_0_-1 18
c machine_concret1_a1.state_3_0 60
c Nd769_948_-1 94
c machine_concret1_a1.state$raw_na$initial$_nb_0_-1 4
c Nd144_816_-1 34
c Nd84_108_0 90
c Nd109_1164_0 88
c Nd96_1284_0 77
c Nd181_192_-1 30
c o2_0_0 25
c machine_concret1_a1.nd_o2_0_-1 33
c Nd144_792_-1 49
c Nd97_1212_0 55
c Nd156_660_-1 14
c Nd84_1176_0 87
c Nd109_1068_0 85
c Nd157_660_-1 45
p cnf 99 261
10 11 9 0
-10 -9 0
-11 -9 0
-8 -9 7 0
8 -7 0
9 -7 0
-6 -7 5 0
6 -5 0
7 -5 0
4 -5 3 0
-4 -3 0
5 -3 0
-10 11 16 0
10 -16 0
-11 -16 0
-8 -16 15 0
8 -15 0
16 -15 0
-6 -15 14 0
6 -14 0
15 -14 0
4 -14 13 0
-4 -13 0
14 -13 0
-10 -11 22 0
10 -22 0
11 -22 0
-8 -22 21 0
8 -21 0
22 -21 0
-6 -21 20 0
6 -20 0
21 -20 0
4 -20 19 0
-4 -19 0
20 -19 0
18 19 17 0
-18 -17 0
-19 -17 0
13 -17 12 0
-13 -12 0
17 -12 0
3 -12 2 0
-3 -2 0
12 -2 0
1 -2 23 0
-1 -23 0
2 -23 0
-1 2 24 0
1 -24 0
-2 -24 0
23 24 0
10 -11 30 0
-10 -30 0
11 -30 0
-8 -30 29 0
8 -29 0
30 -29 0
6 -29 28 0
-6 -28 0
29 -28 0
4 -28 27 0
-4 -27 0
28 -27 0
8 -22 35 0
-8 -35 0
22 -35 0
-4 -35 34 0
4 -34 0
35 -34 0
33 34 32 0
-33 -32 0
-34 -32 0
13 -32 31 0
-13 -31 0
32 -31 0
27 -31 26 0
-27 -26 0
31 -26 0
25 -26 36 0
-25 -36 0
26 -36 0
-25 26 37 0
25 -37 0
-26 -37 0
36 37 0
6 -7 41 0
-6 -41 0
7 -41 0
4 -41 40 0
-4 -40 0
41 -40 0
6 -15 45 0
-6 -45 0
15 -45 0
4 -45 44 0
-4 -44 0
45 -44 0
8 -30 50 0
-8 -50 0
30 -50 0
-4 -50 49 0
4 -49 0
50 -49 0
-48 49 47 0
48 -47 0
-49 -47 0
3 -47 46 0
-3 -46 0
47 -46 0
44 -46 43 0
-44 -43 0
46 -43 0
27 -43 42 0
-27 -42 0
43 -42 0
40 -42 39 0
-40 -39 0
42 -39 0
38 39 51 0
-38 -51 0
-39 -51 0
-38 -39 52 0
38 -52 0
39 -52 0
51 52 0
60 61 59 0
-60 -59 0
-61 -59 0
-58 -59 57 0
58 -57 0
59 -57 0
56 -57 55 0
-56 -55 0
57 -55 0
54 -55 53 0
-54 -53 0
55 -53 0
-53 -40 62 0
53 -62 0
40 -62 0
60 -61 66 0
-60 -66 0
61 -66 0
-58 -66 65 0
58 -65 0
66 -65 0
56 -65 64 0
-56 -64 0
65 -64 0
54 -64 63 0
-54 -63 0
64 -63 0
-63 -27 67 0
63 -67 0
27 -67 0
-60 61 71 0
60 -71 0
-61 -71 0
-58 -71 70 0
58 -70 0
71 -70 0
56 -70 69 0
-56 -69 0
70 -69 0
54 -69 68 0
-54 -68 0
69 -68 0
-68 -44 72 0
68 -72 0
44 -72 0
-56 -57 74 0
56 -74 0
57 -74 0
54 -74 73 0
-54 -73 0
74 -73 0
-73 -3 75 0
73 -75 0
3 -75 0
-56 -70 77 0
56 -77 0
70 -77 0
54 -77 76 0
-54 -76 0
77 -76 0
-76 -13 78 0
76 -78 0
13 -78 0
-60 -61 82 0
60 -82 0
61 -82 0
-58 -82 81 0
58 -81 0
82 -81 0
-56 -81 80 0
56 -80 0
81 -80 0
54 -80 79 0
-54 -79 0
80 -79 0
-79 -19 83 0
79 -83 0
19 -83 0
58 -66 85 0
-58 -85 0
66 -85 0
-54 -85 84 0
54 -84 0
85 -84 0
-84 -49 86 0
84 -86 0
49 -86 0
58 -82 88 0
-58 -88 0
82 -88 0
-54 -88 87 0
54 -87 0
88 -87 0
-87 -34 89 0
87 -89 0
34 -89 0
-54 -58 90 0
54 -90 0
58 -90 0
-8 22 98 0
8 -98 0
-22 -98 0
6 -98 97 0
-6 -97 0
98 -97 0
5 97 96 0
-5 -96 0
-97 -96 0
14 -96 95 0
-14 -95 0
96 -95 0
20 -95 94 0
-20 -94 0
95 -94 0
4 94 93 0
-4 -93 0
-94 -93 0
49 93 92 0
-49 -92 0
-93 -92 0
34 -92 91 0
-34 -91 0
92 -91 0
-90 -91 99 0
90 -99 0
91 -99 0
62 67 72 75 78 83 86 89 99 0
54 0
-56 0
58 0
-60 0
-61 0
-1 0
25 0
38 0