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

... [truncated 7.4 kB]

015-RealPar], 5/7 [SYNTCOMP2016-SyntSeq], 3/4 [SYNTCOMP2016-SyntPar], 8/11 [SYNTCOMP2016-RealSeq], 5/6 [SYNTCOMP2016-RealPar], 7/10 [SYNTCOMP2017-RealSeq], 5/6 [SYNTCOMP2017-RealPar], 5/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 84.0933 [SYNTCOMP2014-RealSeq], 1134.51 [SYNTCOMP2015-RealSeq], 157.255 [SYNTCOMP2015-RealPar], 1017.51 [SYNTCOMP2016-RealSeq], 2101.69 [SYNTCOMP2016-RealPar], 1003.62 [SYNTCOMP2017-RealSeq], 2049.24 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.