aag 1004 40 0 1 964
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
72
74
76
78
80
2009
82 36 8
84 24 20
86 26 18
88 87 84
90 86 85
92 91 89
94 93 82
96 92 83
98 97 95
100 22 20
102 24 18
104 102 100
106 104 98
108 105 99
110 109 107
112 34 10
114 28 16
116 32 12
118 116 115
120 117 114
122 121 119
124 123 112
126 122 113
128 127 125
130 26 16
132 40 2
134 30 12
136 133 131
138 137 134
140 132 130
142 141 139
144 38 4
146 36 6
148 28 14
150 147 145
152 15

... [truncated 12.9 kB]

2015-RealPar], 6/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 7/11 [SYNTCOMP2016-RealSeq], 4/6 [SYNTCOMP2016-RealPar], 7/10 [SYNTCOMP2017-RealSeq], 4/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.084005 [SYNTCOMP2014-RealSeq], 16.766 [SYNTCOMP2015-RealSeq], 9.67238 [SYNTCOMP2015-RealPar], 16.396 [SYNTCOMP2016-RealSeq], 9.32921 [SYNTCOMP2016-RealPar], 16.556 [SYNTCOMP2017-RealSeq], 9.23471 [SYNTCOMP2017-RealPar]
REF_SIZE : 1741
STATUS : realizable
#.