aag 476 23 25 1 428
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48 1
50 2
52 4
54 6
56 8
58 10
60 12
62 14
64 16
66 18
68 20
70 22
72 24
74 26
76 28
78 30
80 32
82 34
84 36
86 38
88 40
90 42
92 44
94 46
96 797
952
98 12 10
100 98 14
102 100 16
104 21 19
106 104 23
108 106 25
110 29 27
112 110 31
114 112 33
116 114 108
118 4 3
120 118 6
122 120 8
124 122 116
126 12 11
128 126 14
130 128 16
132 130 124
134 37 35
136 134 132
138 4 2
140 138 6
142 140 8
144 143 136
146 145 49
148 147 103
15

... [truncated 5.5 kB]

-RealPar], 6/7 [SYNTCOMP2016-SyntSeq], 3/4 [SYNTCOMP2016-SyntPar], 10/11 [SYNTCOMP2016-RealSeq], 5/6 [SYNTCOMP2016-RealPar], 9/10 [SYNTCOMP2017-RealSeq], 5/6 [SYNTCOMP2017-RealPar], 5/6 [SYNTCOMP2017-SyntSeq], 3/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.316019 [SYNTCOMP2014-RealSeq], 0.250637 [SYNTCOMP2015-RealSeq], 0.440786 [SYNTCOMP2015-RealPar], 0.452 [SYNTCOMP2016-RealSeq], 0.630905 [SYNTCOMP2016-RealPar], 0.452 [SYNTCOMP2017-RealSeq], 0.620446 [SYNTCOMP2017-RealPar]
REF_SIZE : 3834
STATUS : realizable
#.