aag 893 39 41 1 813
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 1
82 2
84 4
86 6
88 8
90 10
92 12
94 14
96 16
98 18
100 20
102 22
104 24
106 26
108 28
110 30
112 32
114 34
116 36
118 38
120 40
122 42
124 44
126 46
128 48
130 50
132 52
134 54
136 56
138 58
140 60
142 62
144 64
146 66
148 68
150 70
152 72
154 74
156 76
158 78
160 1499
1786
162 64 62
164 162 66
166 164 68
168 33 31
170 168 35
172 170 37
174 172 39
176 174 41
178 176 43
180

... [truncated 11.5 kB]

0/4 [SYNTCOMP2015-RealPar], 0/7 [SYNTCOMP2016-SyntSeq], 0/4 [SYNTCOMP2016-SyntPar], 2/11 [SYNTCOMP2016-RealSeq], 1/6 [SYNTCOMP2016-RealPar], 2/10 [SYNTCOMP2017-RealSeq], 0/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 0/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.0 [SYNTCOMP2014-RealSeq], 3257.25 [SYNTCOMP2015-RealSeq], 0.0 [SYNTCOMP2015-RealPar], 2351.28 [SYNTCOMP2016-RealSeq], 3504.52 [SYNTCOMP2016-RealPar], 2586.55 [SYNTCOMP2017-RealSeq], 0.0 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 0
#.