aag 2573 64 41 1 2468
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74
76
78
80
82
84
86
88
90
92
94
96
98
100
102
104
106
108
110
112
114
116
118
120
122
124
126
128
130 781
132 891
134 1005
136 1115
138 1229
140 1339
142 1453
144 1563
146 1673
148 1787
150 1897
152 2011
154 2121
156 2235
158 2345
160 2459
162 2573
164 2683
166 2797
168 2907
170 3021
172 3131
174 3245
176 3355
178 3465
180 3579
182 3689
184 3803
186 3913
188 4027
190 4137
192 4251
1

... [truncated 33.5 kB]

 a[3][2]<0>
l27 a[3][3]<0>
l28 a[3][4]<0>
l29 a[3][5]<0>
l30 a[3][6]<0>
l31 a[3][7]<0>
l32 a[4][0]<0>
l33 a[4][1]<0>
l34 a[4][2]<0>
l35 a[4][3]<0>
l36 a[4][4]<0>
l37 a[4][5]<0>
l38 a[4][6]<0>
l39 a[4][7]<0>
l40 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 0/4 [2017-pre-classification], 1/10 [SYNTCOMP2017-RealSeq], 3/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 0/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 3.24 [SYNTCOMP2017-RealSeq], 0.920914 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 0
#.