aag 918 47 0 1 871
2
4
6
8
10
12
14
16
18
72
74
76
78
80
156
158
160
162
164
394
396
398
400
402
478
546
748
750
752
754
756
832
900
1102
1104
1106
1108
1110
1186
1254
1456
1458
1460
1462
1464
1540
1608
1837
20 19 1
22 9 1
24 16 23
26 25 1
28 7 27
30 7 29
32 14 31
34 15 27
36 33 35
38 3 37
40 3 39
42 10 41
44 11 37
46 43 45
48 10 41
50 11 37
52 49 51
54 18 47
56 19 52
58 55 57
60 4 21
62 5 59
64 61 63
66 12 65
68 13 59
70 67 69
82 81 1
84 79 1
86 16 85
88 87 1
90 77 89
92 77 91
94 14 93
96 15 89
98 95 97
10

... [truncated 11.0 kB]

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