aag 416 30 17 1 369
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 1
64 321
66 349
68 385
70 421
72 457
74 493
76 529
78 565
80 601
82 637
84 673
86 709
88 745
90 781
92 817
94 832
220
96 65 62
98 64 62
100 97 62
102 67 62
104 66 62
106 103 62
108 69 62
110 68 62
112 109 62
114 71 62
116 70 62
118 115 62
120 73 62
122 72 62
124 121 62
126 75 62
128 74 62
130 127 62
132 77 62
134 76 62
136 133 62
138 79 62
140 78 62
142 139 62
144 81 62
146 80 62
148 145 62
150 83 62

... [truncated 6.2 kB]

-RealPar], 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 11/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 10/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.032002 [SYNTCOMP2014-RealSeq], 0.032789 [SYNTCOMP2015-RealSeq], 0.040571 [SYNTCOMP2015-RealPar], 0.024 [SYNTCOMP2016-RealSeq], 0.096147 [SYNTCOMP2016-RealPar], 0.028 [SYNTCOMP2017-RealSeq], 0.072947 [SYNTCOMP2017-RealPar]
REF_SIZE : 384
STATUS : realizable
#.