aag 760 34 36 1 690
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 1277
1520
142 56 54
144 142 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.6 kB]

015-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 : 36.5463 [SYNTCOMP2014-RealSeq], 39.1693 [SYNTCOMP2015-RealSeq], 80.7778 [SYNTCOMP2015-RealPar], 32.348 [SYNTCOMP2016-RealSeq], 69.9447 [SYNTCOMP2016-RealPar], 32.952 [SYNTCOMP2017-RealSeq], 69.3663 [SYNTCOMP2017-RealPar]
REF_SIZE : 86052
STATUS : realizable
#.