aag 311 28 30 1 253
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 1
60 2
62 4
64 6
66 8
68 10
70 12
72 14
74 16
76 18
78 20
80 22
82 24
84 26
86 28
88 30
90 32
92 34
94 36
96 38
98 40
100 42
102 44
104 46
106 48
108 50
110 52
112 54
114 56
116 429
622
118 36 34
120 4 2
122 120 6
124 122 8
126 124 10
128 126 12
130 128 14
132 130 16
134 132 18
136 134 20
138 136 22
140 138 24
142 140 26
144 142 28
146 144 30
148 147 59
150 149 119
152 5 3
154 152 7
156 95 36
158 94 37
160

... [truncated 3.8 kB]

015-RealPar], 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 10/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 9/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.584036 [SYNTCOMP2014-RealSeq], 0.969556 [SYNTCOMP2015-RealSeq], 0.238998 [SYNTCOMP2015-RealPar], 0.756 [SYNTCOMP2016-RealSeq], 1.03788 [SYNTCOMP2016-RealPar], 0.764 [SYNTCOMP2017-RealSeq], 1.05264 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.