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

... [truncated 6.9 kB]

P2015-RealPar], 0/7 [SYNTCOMP2016-SyntSeq], 0/4 [SYNTCOMP2016-SyntPar], 2/11 [SYNTCOMP2016-RealSeq], 2/6 [SYNTCOMP2016-RealPar], 2/10 [SYNTCOMP2017-RealSeq], 2/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 0/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 74.9487 [SYNTCOMP2014-RealSeq], 283.99 [SYNTCOMP2015-RealSeq], 96.7641 [SYNTCOMP2015-RealPar], 286.456 [SYNTCOMP2016-RealSeq], 544.813 [SYNTCOMP2016-RealPar], 338.472 [SYNTCOMP2017-RealSeq], 618.07 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.