aag 312 28 30 1 254
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 431
624
118 35 33
120 119 36
122 4 2
124 122 6
126 124 8
128 126 10
130 128 12
132 130 14
134 132 16
136 134 18
138 136 20
140 138 22
142 140 24
144 142 26
146 144 28
148 146 30
150 149 59
152 151 121
154 5 3
156 154 7
158 95 36
16

... [truncated 3.9 kB]

15-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 : 1.42809 [SYNTCOMP2014-RealSeq], 0.710143 [SYNTCOMP2015-RealSeq], 0.231451 [SYNTCOMP2015-RealPar], 0.732 [SYNTCOMP2016-RealSeq], 0.949798 [SYNTCOMP2016-RealPar], 0.664 [SYNTCOMP2017-RealSeq], 0.956262 [SYNTCOMP2017-RealPar]
REF_SIZE : 718
STATUS : realizable
#.