aag 342 17 19 1 306
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36 1
38 2
40 4
42 6
44 8
46 10
48 12
50 14
52 16
54 18
56 20
58 22
60 24
62 26
64 28
66 30
68 32
70 34
72 573
684
74 10 8
76 74 12
78 17 15
80 78 19
82 23 21
84 82 25
86 84 80
88 4 3
90 88 6
92 90 86
94 10 9
96 94 12
98 96 92
100 4 2
102 100 6
104 103 98
106 105 37
108 107 77
110 40 38
112 111 43
114 40 4
116 38 3
118 116 115
120 41 5
122 40 39
124 123 121
126 124 119
128 126 6
130 129 113
132 110 42
134 127 7
136 135 133
138 136 131
140 46 

... [truncated 3.9 kB]

5-RealPar], 7/7 [SYNTCOMP2016-SyntSeq], 4/4 [SYNTCOMP2016-SyntPar], 10/11 [SYNTCOMP2016-RealSeq], 6/6 [SYNTCOMP2016-RealPar], 9/10 [SYNTCOMP2017-RealSeq], 6/6 [SYNTCOMP2017-RealPar], 6/6 [SYNTCOMP2017-SyntSeq], 4/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 0.076004 [SYNTCOMP2014-RealSeq], 0.051252 [SYNTCOMP2015-RealSeq], 0.093317 [SYNTCOMP2015-RealPar], 0.048 [SYNTCOMP2016-RealSeq], 0.095571 [SYNTCOMP2016-RealPar], 0.048 [SYNTCOMP2017-RealSeq], 0.090256 [SYNTCOMP2017-RealPar]
REF_SIZE : 513
STATUS : realizable
#.