aag 324 38 21 1 265
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 1
80 315
82 330
84 348
86 366
88 384
90 402
92 420
94 438
96 456
98 474
100 492
102 510
104 528
106 546
108 564
110 582
112 600
114 618
116 636
118 648
196
120 80 78
122 82 78
124 122 120
126 84 78
128 126 124
130 86 78
132 130 128
134 88 78
136 134 132
138 90 78
140 138 136
142 92 78
144 142 140
146 94 78
148 146 144
150 96 78
152 150 148
154 98 78
156 154 152
158 100 78
160 

... [truncated 5.6 kB]

-RealPar], 6/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 5/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.032002 [SYNTCOMP2014-RealSeq], 0.066557 [SYNTCOMP2015-RealSeq], 0.068677 [SYNTCOMP2015-RealPar], 0.032 [SYNTCOMP2016-RealSeq], 0.071997 [SYNTCOMP2016-RealPar], 0.032 [SYNTCOMP2017-RealSeq], 0.068018 [SYNTCOMP2017-RealPar]
REF_SIZE : 284
STATUS : realizable
#.