aag 868 25 21 1 822
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 409
54 477
56 549
58 617
60 689
62 757
64 829
66 897
68 969
70 1037
72 1109
74 1177
76 1249
78 1317
80 1389
82 1457
84 1529
86 1597
88 1669
90 1737
92 134
337
94 53 1
96 55 1
98 57 1
100 59 1
102 61 1
104 63 1
106 65 1
108 67 1
110 69 1
112 71 1
114 73 1
116 75 1
118 77 1
120 79 1
122 81 1
124 83 1
126 85 1
128 87 1
130 89 1
132 91 1
134 1 1
136 94 1
138 97 137
140 139 1
142 99 141
144 143 1
146 101 145
148 147 1
1

... [truncated 10.0 kB]

a[1][1]<0>
l7 a[1][2]<0>
l8 a[1][3]<0>
l9 a[1][4]<0>
l10 a[2][0]<0>
l11 a[2][1]<0>
l12 a[2][2]<0>
l13 a[2][3]<0>
l14 a[2][4]<0>
l15 a[3][0]<0>
l16 a[3][1]<0>
l17 a[3][2]<0>
l18 a[3][3]<0>
l19 a[3][4]<0>
l20 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 4/4 [2017-pre-classification], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
REF_SIZE : 837
SOLVED_IN : 0.668 [SYNTCOMP2017-RealSeq], 0.460489 [SYNTCOMP2017-RealPar]
STATUS : realizable
#.