aag 627 29 31 1 567
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 1
62 2
64 4
66 6
68 8
70 10
72 12
74 14
76 16
78 18
80 20
82 22
84 24
86 26
88 28
90 30
92 32
94 34
96 36
98 38
100 40
102 42
104 44
106 46
108 48
110 50
112 52
114 54
116 56
118 58
120 1055
1254
122 48 46
124 25 23
126 124 27
128 126 29
130 128 31
132 35 33
134 132 37
136 134 39
138 136 41
140 138 130
142 4 3
144 142 6
146 144 8
148 146 10
150 148 140
152 14 13
154 152 16
156 154 18
158 156 20
160 158 

... [truncated 7.6 kB]

MP2015-RealPar], 5/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 : 3.61223 [SYNTCOMP2014-RealSeq], 1.95318 [SYNTCOMP2015-RealSeq], 3.11127 [SYNTCOMP2015-RealPar], 2.012 [SYNTCOMP2016-RealSeq], 2.8362 [SYNTCOMP2016-RealPar], 2.016 [SYNTCOMP2017-RealSeq], 2.75619 [SYNTCOMP2017-RealPar]
REF_SIZE : 33313
STATUS : realizable
#.