aag 1427 48 0 1 1379
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
82
84
86
88
90
92
94
96
2855
98 39 36
100 38 37
102 101 99
104 40 21
106 41 20
108 107 105
110 40 19
112 41 18
114 113 111
116 41 39
118 40 38
120 119 117
122 120 102
124 122 115
126 109 103
128 127 125
130 47 44
132 46 45
134 133 131
136 49 47
138 48 46
140 139 137
142 140 134
144 48 11
146 49 10
148 147 145
150 48 13
152 49 12
154 153 151
156 155 135
158 149 142
160 159 

... [truncated 18.8 kB]

P2015-RealPar], 1/7 [SYNTCOMP2016-SyntSeq], 2/4 [SYNTCOMP2016-SyntPar], 1/11 [SYNTCOMP2016-RealSeq], 4/6 [SYNTCOMP2016-RealPar], 0/10 [SYNTCOMP2017-RealSeq], 4/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 2/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.140008 [SYNTCOMP2014-RealSeq], 1668.54 [SYNTCOMP2015-RealSeq], 32.2189 [SYNTCOMP2015-RealPar], 1663.74 [SYNTCOMP2016-RealSeq], 30.4217 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 31.4672 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 2539
#.