aag 822 47 0 1 775
2
4
6
8
10
12
14
58
60
62
64
128
130
132
134
240
242
244
246
352
354
356
358
422
478
572
666
668
670
672
736
792
886
980
982
984
986
1050
1106
1200
1294
1296
1298
1300
1364
1420
1514
1645
16 15 1
18 7 1
20 12 19
22 21 1
24 3 23
26 3 25
28 8 27
30 9 23
32 29 31
34 8 27
36 9 23
38 35 37
40 14 33
42 15 38
44 41 43
46 4 17
48 5 45
50 47 49
52 10 51
54 11 45
56 53 55
66 65 1
68 63 1
70 12 69
72 71 1
74 59 73
76 59 75
78 59 73
80 59 79
82 64 77
84 65 80
86 83 85
88 60 67
90 61 87
92 89 91
94 12

... [truncated 9.7 kB]

1][2]<0>
i31 controllable_c[2][2]<0>
i32 controllable_c[3][2]<0>
i33 b[0][3]<0>
i34 b[1][3]<0>
i35 b[2][3]<0>
i36 controllable_c[0][3]<0>
i37 controllable_c[1][3]<0>
i38 controllable_c[2][3]<0>
i39 controllable_c[3][3]<0>
i40 b[0][4]<0>
i41 b[1][4]<0>
i42 b[2][4]<0>
i43 controllable_c[0][4]<0>
i44 controllable_c[1][4]<0>
i45 controllable_c[2][4]<0>
i46 controllable_c[3][4]<0>
o0 err<0>
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 5.9417 [2015-pre-classification]
#.