aag 643 29 31 1 583
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 1087
1286
122 45 43
124 122 47
126 125 48
128 25 23
130 128 27
132 130 29
134 132 31
136 35 33
138 136 37
140 138 39
142 140 41
144 142 134
146 4 3
148 146 6
150 148 9
152 150 10
154 152 144
156 14 13
158 156 16
160 158 

... [truncated 7.8 kB]

TCOMP2015-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 : 1.6201 [SYNTCOMP2014-RealSeq], 1.25692 [SYNTCOMP2015-RealSeq], 2.06141 [SYNTCOMP2015-RealPar], 1.44 [SYNTCOMP2016-RealSeq], 3.21653 [SYNTCOMP2016-RealPar], 1.436 [SYNTCOMP2017-RealSeq], 3.25697 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.