aag 2637 65 0 1 2572
2
4
6
8
10
12
14
16
18
20
22
86
88
90
92
94
96
182
184
186
188
190
192
674
676
678
680
682
684
1166
1168
1170
1172
1174
1176
1262
1340
1762
2184
2186
2188
2190
2192
2194
2280
2358
2780
3202
3204
3206
3208
3210
3212
3298
3376
3798
4220
4222
4224
4226
4228
4230
4316
4394
4816
5275
24 23 1
26 11 1
28 20 27
30 29 1
32 9 31
34 9 33
36 18 35
38 19 31
40 37 39
42 7 41
44 7 43
46 16 45
48 17 41
50 47 49
52 3 51
54 3 53
56 12 55
58 13 51
60 57 59
62 12 55
64 13 51
66 63 65
68 22 61
70 23 66
72 6

... [truncated 35.5 kB]

c[3][2]<0>
i47 b[0][3]<0>
i48 b[1][3]<0>
i49 b[2][3]<0>
i50 b[3][3]<0>
i51 b[4][3]<0>
i52 controllable_c[0][3]<0>
i53 controllable_c[1][3]<0>
i54 controllable_c[2][3]<0>
i55 controllable_c[3][3]<0>
i56 b[0][4]<0>
i57 b[1][4]<0>
i58 b[2][4]<0>
i59 b[3][4]<0>
i60 b[4][4]<0>
i61 controllable_c[0][4]<0>
i62 controllable_c[1][4]<0>
i63 controllable_c[2][4]<0>
i64 controllable_c[3][4]<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : unknown
SOLVED_BY : 0/3 [2015-pre-classification]
SOLVED_IN : 0.0 [2015-pre-classification]
#.