aag 208 4 49 1 155
2
4
6
8
10 0
12 367
14 371
16 375
18 379
20 383
22 391
24 0
26 393
28 395
30 397
32 399
34 401
36 405
38 0
40 263
42 267
44 271
46 275
48 279
50 287
52 259
54 54
56 56
58 58
60 60
62 62
64 64
66 0
68 318
70 320
72 322
74 324
76 326
78 333
80 0
82 305
84 307
86 309
88 311
90 313
92 317
94 0
96 288
98 290
100 292
102 294
104 296
106 303
417
108 1 41
110 108 89
112 110 75
114 112 25
116 114 59
118 116 13
120 118 97
122 120 81
124 122 47
126 124 21
128 126 105
130 128 35
132 130 65
134 132 39

... [truncated 2.0 kB]

tch42
l43 latch43
l44 latch44
l45 latch45
l46 latch46
l47 latch47
l48 latch48
o0 error
c
#!SYNTCOMP
SOLVED_BY : 7/8 [SYNTCOMP2014-RealSeq], 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.012 [SYNTCOMP2014-RealSeq], 0.0 [SYNTCOMP2016-RealSeq], 0.006587 [SYNTCOMP2016-RealPar], 0.0 [SYNTCOMP2017-RealSeq], 0.006695 [SYNTCOMP2017-RealPar]
STATUS : unrealizable
REF_SIZE : 0
#.