aag 111 7 5 1 99
2
4
6
8
10
12
14
16 194
18 1
20 10
22 12
24 14
222
26 16 16
28 19 19
30 2 2
32 31 31
34 6 6
36 35 35
38 37 33
40 39 39
42 2 2
44 6 6
46 45 43
48 47 47
50 48 40
52 4 2
54 5 3
56 55 53
58 56 56
60 12 12
62 60 58
64 56 56
66 65 65
68 14 14
70 68 66
72 71 63
74 73 73
76 75 51
78 77 77
80 1 1
82 10 10
84 82 80
86 85 79
88 87 87
90 88 88
92 91 91
94 92 28
96 95 27
98 97 97
100 20 20
102 2 2
104 103 103
106 6 6
108 107 107
110 109 105
112 111 111
114 2 2
116 6 6
118 117 115
120 119 119
122 120 112

... [truncated 922 Bytes]

5-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.011504 [2015-pre-classification], 0.005316 [SYNTCOMP2015-RealSeq], 0.008791 [SYNTCOMP2015-RealPar], 0.0 [SYNTCOMP2016-RealSeq], 0.005784 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 0.005805 [SYNTCOMP2017-RealPar]
REF_SIZE : 103
STATUS : realizable
#.