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

... [truncated 5.8 kB]

2015-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 : 0.788049 [SYNTCOMP2014-RealSeq], 0.753519 [SYNTCOMP2015-RealSeq], 0.654663 [SYNTCOMP2015-RealPar], 0.608 [SYNTCOMP2016-RealSeq], 0.819223 [SYNTCOMP2016-RealPar], 0.576 [SYNTCOMP2017-RealSeq], 0.8063 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.