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

... [truncated 9.6 kB]

P2015-RealPar], 6/7 [SYNTCOMP2016-SyntSeq], 3/4 [SYNTCOMP2016-SyntPar], 9/11 [SYNTCOMP2016-RealSeq], 5/6 [SYNTCOMP2016-RealPar], 8/10 [SYNTCOMP2017-RealSeq], 5/6 [SYNTCOMP2017-RealPar], 5/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 53.4273 [SYNTCOMP2014-RealSeq], 120.438 [SYNTCOMP2015-RealSeq], 141.496 [SYNTCOMP2015-RealPar], 49.296 [SYNTCOMP2016-RealSeq], 75.8368 [SYNTCOMP2016-RealPar], 52.872 [SYNTCOMP2017-RealSeq], 73.6052 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.