aag 775 34 36 1 705
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 1307
1550
142 57 55
144 143 58
146 29 27
148 146 31
150 148 33
152 150 35
154 152 37
156 41 39
158 156 43
160 158 45
162 160 47
164 162 49
166 164 154
168 4 3
170 16

... [truncated 9.8 kB]

2015-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 : 28.2898 [SYNTCOMP2014-RealSeq], 15.3235 [SYNTCOMP2015-RealSeq], 17.4412 [SYNTCOMP2015-RealPar], 23.0 [SYNTCOMP2016-RealSeq], 36.3492 [SYNTCOMP2016-RealPar], 19.032 [SYNTCOMP2017-RealSeq], 33.6319 [SYNTCOMP2017-RealPar]
REF_SIZE : 119875
STATUS : realizable
#.