Problem3-Full.smv 35.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
MODULE main
VAR
    state  : {s0, s1, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s2, s20, s21, s22, s23, s24, s25, s3, s4, s5, s6, s7, s8, s9};
    input  : {iA, iB, iC, iD, iE, iF, iG, iH, iI, iJ, null};
    output : {oInv, oO, oP, oQ, oR, oS, oT, oU, oV, oW, oX, oY, oZ, null};
ASSIGN
    init(state)  := s0;
    init(output) := null;
    next(state)  := case
        state = s0 & input = iA : s1;
        state = s0 & input = iB : s0;
        state = s0 & input = iC : s0;
        state = s0 & input = iD : s0;
        state = s0 & input = iE : s3;
        state = s0 & input = iF : s0;
        state = s0 & input = iG : s0;
        state = s0 & input = iH : s0;
        state = s0 & input = iI : s0;
        state = s0 & input = iJ : s0;
        state = s1 & input = iA : s2;
        state = s1 & input = iB : s1;
        state = s1 & input = iC : s1;
        state = s1 & input = iD : s1;
        state = s1 & input = iE : s1;
        state = s1 & input = iF : s1;
        state = s1 & input = iG : s1;
        state = s1 & input = iH : s1;
        state = s1 & input = iI : s1;
        state = s1 & input = iJ : s1;
        state = s10 & input = iA : s11;
        state = s10 & input = iB : s14;
        state = s10 & input = iC : s10;
        state = s10 & input = iD : s10;
        state = s10 & input = iE : s10;
        state = s10 & input = iF : s10;
        state = s10 & input = iG : s10;
        state = s10 & input = iH : s10;
        state = s10 & input = iI : s10;
        state = s10 & input = iJ : s10;
        state = s11 & input = iA : s12;
        state = s11 & input = iB : s11;
        state = s11 & input = iC : s11;
        state = s11 & input = iD : s11;
        state = s11 & input = iE : s11;
        state = s11 & input = iF : s2;
        state = s11 & input = iG : s11;
        state = s11 & input = iH : s11;
        state = s11 & input = iI : s11;
        state = s11 & input = iJ : s13;
        state = s12 & input = iA : s12;
        state = s12 & input = iB : s12;
        state = s12 & input = iC : s9;
        state = s12 & input = iD : s12;
        state = s12 & input = iE : s12;
        state = s12 & input = iF : s12;
        state = s12 & input = iG : s2;
        state = s12 & input = iH : s9;
        state = s12 & input = iI : s12;
        state = s12 & input = iJ : s12;
        state = s13 & input = iA : s13;
        state = s13 & input = iB : s13;
        state = s13 & input = iC : s13;
        state = s13 & input = iD : s13;
        state = s13 & input = iE : s9;
        state = s13 & input = iF : s13;
        state = s13 & input = iG : s1;
        state = s13 & input = iH : s13;
        state = s13 & input = iI : s13;
        state = s13 & input = iJ : s13;
        state = s14 & input = iA : s14;
        state = s14 & input = iB : s4;
        state = s14 & input = iC : s14;
        state = s14 & input = iD : s14;
        state = s14 & input = iE : s14;
        state = s14 & input = iF : s14;
        state = s14 & input = iG : s6;
        state = s14 & input = iH : s14;
        state = s14 & input = iI : s14;
        state = s14 & input = iJ : s14;
        state = s15 & input = iA : s16;
        state = s15 & input = iB : s15;
        state = s15 & input = iC : s15;
        state = s15 & input = iD : s15;
        state = s15 & input = iE : s15;
        state = s15 & input = iF : s15;
        state = s15 & input = iG : s15;
        state = s15 & input = iH : s15;
        state = s15 & input = iI : s15;
        state = s15 & input = iJ : s15;
        state = s16 & input = iA : s16;
        state = s16 & input = iB : s16;
        state = s16 & input = iC : s16;
        state = s16 & input = iD : s16;
        state = s16 & input = iE : s16;
        state = s16 & input = iF : s17;
        state = s16 & input = iG : s16;
        state = s16 & input = iH : s16;
        state = s16 & input = iI : s16;
        state = s16 & input = iJ : s16;
        state = s17 & input = iA : s17;
        state = s17 & input = iB : s17;
        state = s17 & input = iC : s17;
        state = s17 & input = iD : s18;
        state = s17 & input = iE : s17;
        state = s17 & input = iF : s17;
        state = s17 & input = iG : s17;
        state = s17 & input = iH : s17;
        state = s17 & input = iI : s17;
        state = s17 & input = iJ : s17;
        state = s18 & input = iA : s18;
        state = s18 & input = iB : s18;
        state = s18 & input = iC : s18;
        state = s18 & input = iD : s18;
        state = s18 & input = iE : s19;
        state = s18 & input = iF : s18;
        state = s18 & input = iG : s18;
        state = s18 & input = iH : s18;
        state = s18 & input = iI : s18;
        state = s18 & input = iJ : s18;
        state = s19 & input = iA : s19;
        state = s19 & input = iB : s19;
        state = s19 & input = iC : s19;
        state = s19 & input = iD : s19;
        state = s19 & input = iE : s19;
        state = s19 & input = iF : s19;
        state = s19 & input = iG : s19;
        state = s19 & input = iH : s20;
        state = s19 & input = iI : s19;
        state = s19 & input = iJ : s19;
        state = s2 & input = iA : s8;
        state = s2 & input = iB : s2;
        state = s2 & input = iC : s2;
        state = s2 & input = iD : s2;
        state = s2 & input = iE : s2;
        state = s2 & input = iF : s2;
        state = s2 & input = iG : s2;
        state = s2 & input = iH : s2;
        state = s2 & input = iI : s2;
        state = s2 & input = iJ : s2;
        state = s20 & input = iA : s21;
        state = s20 & input = iB : s20;
        state = s20 & input = iC : s20;
        state = s20 & input = iD : s20;
        state = s20 & input = iE : s22;
        state = s20 & input = iF : s20;
        state = s20 & input = iG : s20;
        state = s20 & input = iH : s23;
        state = s20 & input = iI : s20;
        state = s20 & input = iJ : s20;
        state = s21 & input = iA : s21;
        state = s21 & input = iB : s21;
        state = s21 & input = iC : s21;
        state = s21 & input = iD : s21;
        state = s21 & input = iE : s21;
        state = s21 & input = iF : s15;
        state = s21 & input = iG : s21;
        state = s21 & input = iH : s21;
        state = s21 & input = iI : s21;
        state = s21 & input = iJ : s25;
        state = s22 & input = iA : s22;
        state = s22 & input = iB : s22;
        state = s22 & input = iC : s22;
        state = s22 & input = iD : s22;
        state = s22 & input = iE : s22;
        state = s22 & input = iF : s22;
        state = s22 & input = iG : s22;
        state = s22 & input = iH : s16;
        state = s22 & input = iI : s22;
        state = s22 & input = iJ : s22;
        state = s23 & input = iA : s23;
        state = s23 & input = iB : s23;
        state = s23 & input = iC : s23;
        state = s23 & input = iD : s23;
        state = s23 & input = iE : s23;
        state = s23 & input = iF : s23;
        state = s23 & input = iG : s23;
        state = s23 & input = iH : s24;
        state = s23 & input = iI : s23;
        state = s23 & input = iJ : s23;
        state = s24 & input = iA : s24;
        state = s24 & input = iB : s24;
        state = s24 & input = iC : s24;
        state = s24 & input = iD : s24;
        state = s24 & input = iE : s24;
        state = s24 & input = iF : s15;
        state = s24 & input = iG : s24;
        state = s24 & input = iH : s24;
        state = s24 & input = iI : s24;
        state = s24 & input = iJ : s24;
        state = s25 & input = iA : s25;
        state = s25 & input = iB : s25;
        state = s25 & input = iC : s25;
        state = s25 & input = iD : s25;
        state = s25 & input = iE : s25;
        state = s25 & input = iF : s25;
        state = s25 & input = iG : s25;
        state = s25 & input = iH : s8;
        state = s25 & input = iI : s25;
        state = s25 & input = iJ : s25;
        state = s3 & input = iA : s3;
        state = s3 & input = iB : s4;
        state = s3 & input = iC : s3;
        state = s3 & input = iD : s3;
        state = s3 & input = iE : s3;
        state = s3 & input = iF : s3;
        state = s3 & input = iG : s3;
        state = s3 & input = iH : s3;
        state = s3 & input = iI : s3;
        state = s3 & input = iJ : s3;
        state = s4 & input = iA : s4;
        state = s4 & input = iB : s4;
        state = s4 & input = iC : s4;
        state = s4 & input = iD : s4;
        state = s4 & input = iE : s4;
        state = s4 & input = iF : s4;
        state = s4 & input = iG : s4;
        state = s4 & input = iH : s4;
        state = s4 & input = iI : s4;
        state = s4 & input = iJ : s5;
        state = s5 & input = iA : s5;
        state = s5 & input = iB : s5;
        state = s5 & input = iC : s5;
        state = s5 & input = iD : s5;
        state = s5 & input = iE : s5;
        state = s5 & input = iF : s5;
        state = s5 & input = iG : s5;
        state = s5 & input = iH : s5;
        state = s5 & input = iI : s5;
        state = s5 & input = iJ : s6;
        state = s6 & input = iA : s6;
        state = s6 & input = iB : s7;
        state = s6 & input = iC : s6;
        state = s6 & input = iD : s6;
        state = s6 & input = iE : s6;
        state = s6 & input = iF : s6;
        state = s6 & input = iG : s6;
        state = s6 & input = iH : s6;
        state = s6 & input = iI : s6;
        state = s6 & input = iJ : s14;
        state = s7 & input = iA : s7;
        state = s7 & input = iB : s4;
        state = s7 & input = iC : s7;
        state = s7 & input = iD : s7;
        state = s7 & input = iE : s7;
        state = s7 & input = iF : s7;
        state = s7 & input = iG : s7;
        state = s7 & input = iH : s7;
        state = s7 & input = iI : s7;
        state = s7 & input = iJ : s7;
        state = s8 & input = iA : s8;
        state = s8 & input = iB : s8;
        state = s8 & input = iC : s8;
        state = s8 & input = iD : s8;
        state = s8 & input = iE : s8;
        state = s8 & input = iF : s8;
        state = s8 & input = iG : s9;
        state = s8 & input = iH : s8;
        state = s8 & input = iI : s8;
        state = s8 & input = iJ : s15;
        state = s9 & input = iA : s9;
        state = s9 & input = iB : s10;
        state = s9 & input = iC : s9;
        state = s9 & input = iD : s9;
        state = s9 & input = iE : s9;
        state = s9 & input = iF : s9;
        state = s9 & input = iG : s9;
        state = s9 & input = iH : s9;
        state = s9 & input = iI : s9;
        state = s9 & input = iJ : s9;
        input = null : state;
    esac;
    next(output) := case
        state = s0 & input = iA : oR;
        state = s0 & input = iB : oInv;
        state = s0 & input = iC : oInv;
        state = s0 & input = iD : oInv;
        state = s0 & input = iE : oY;
        state = s0 & input = iF : oInv;
        state = s0 & input = iG : oInv;
        state = s0 & input = iH : oInv;
        state = s0 & input = iI : oInv;
        state = s0 & input = iJ : oInv;
        state = s1 & input = iA : oP;
        state = s1 & input = iB : oInv;
        state = s1 & input = iC : oInv;
        state = s1 & input = iD : oInv;
        state = s1 & input = iE : oInv;
        state = s1 & input = iF : oInv;
        state = s1 & input = iG : oInv;
        state = s1 & input = iH : oInv;
        state = s1 & input = iI : oInv;
        state = s1 & input = iJ : oInv;
        state = s10 & input = iA : oX;
        state = s10 & input = iB : oX;
        state = s10 & input = iC : oInv;
        state = s10 & input = iD : oInv;
        state = s10 & input = iE : oInv;
        state = s10 & input = iF : oInv;
        state = s10 & input = iG : oInv;
        state = s10 & input = iH : oInv;
        state = s10 & input = iI : oInv;
        state = s10 & input = iJ : oInv;
        state = s11 & input = iA : oS;
        state = s11 & input = iB : oInv;
        state = s11 & input = iC : oInv;
        state = s11 & input = iD : oInv;
        state = s11 & input = iE : oInv;
        state = s11 & input = iF : oP;
        state = s11 & input = iG : oInv;
        state = s11 & input = iH : oInv;
        state = s11 & input = iI : oInv;
        state = s11 & input = iJ : oO;
        state = s12 & input = iA : oInv;
        state = s12 & input = iB : oInv;
        state = s12 & input = iC : oV;
        state = s12 & input = iD : oInv;
        state = s12 & input = iE : oInv;
        state = s12 & input = iF : oInv;
        state = s12 & input = iG : oP;
        state = s12 & input = iH : oV;
        state = s12 & input = iI : oInv;
        state = s12 & input = iJ : oInv;
        state = s13 & input = iA : oInv;
        state = s13 & input = iB : oInv;
        state = s13 & input = iC : oInv;
        state = s13 & input = iD : oInv;
        state = s13 & input = iE : oV;
        state = s13 & input = iF : oInv;
        state = s13 & input = iG : oR;
        state = s13 & input = iH : oInv;
        state = s13 & input = iI : oInv;
        state = s13 & input = iJ : oInv;
        state = s14 & input = iA : oInv;
        state = s14 & input = iB : oP;
        state = s14 & input = iC : oInv;
        state = s14 & input = iD : oInv;
        state = s14 & input = iE : oInv;
        state = s14 & input = iF : oInv;
        state = s14 & input = iG : oY;
        state = s14 & input = iH : oInv;
        state = s14 & input = iI : oInv;
        state = s14 & input = iJ : oInv;
        state = s15 & input = iA : oU;
        state = s15 & input = iB : oInv;
        state = s15 & input = iC : oInv;
        state = s15 & input = iD : oInv;
        state = s15 & input = iE : oInv;
        state = s15 & input = iF : oInv;
        state = s15 & input = iG : oInv;
        state = s15 & input = iH : oInv;
        state = s15 & input = iI : oInv;
        state = s15 & input = iJ : oInv;
        state = s16 & input = iA : oInv;
        state = s16 & input = iB : oInv;
        state = s16 & input = iC : oInv;
        state = s16 & input = iD : oInv;
        state = s16 & input = iE : oInv;
        state = s16 & input = iF : oP;
        state = s16 & input = iG : oInv;
        state = s16 & input = iH : oInv;
        state = s16 & input = iI : oInv;
        state = s16 & input = iJ : oInv;
        state = s17 & input = iA : oInv;
        state = s17 & input = iB : oInv;
        state = s17 & input = iC : oInv;
        state = s17 & input = iD : oV;
        state = s17 & input = iE : oInv;
        state = s17 & input = iF : oInv;
        state = s17 & input = iG : oInv;
        state = s17 & input = iH : oInv;
        state = s17 & input = iI : oInv;
        state = s17 & input = iJ : oInv;
        state = s18 & input = iA : oInv;
        state = s18 & input = iB : oInv;
        state = s18 & input = iC : oInv;
        state = s18 & input = iD : oInv;
        state = s18 & input = iE : oW;
        state = s18 & input = iF : oInv;
        state = s18 & input = iG : oInv;
        state = s18 & input = iH : oInv;
        state = s18 & input = iI : oInv;
        state = s18 & input = iJ : oInv;
        state = s19 & input = iA : oInv;
        state = s19 & input = iB : oInv;
        state = s19 & input = iC : oInv;
        state = s19 & input = iD : oInv;
        state = s19 & input = iE : oInv;
        state = s19 & input = iF : oInv;
        state = s19 & input = iG : oInv;
        state = s19 & input = iH : oV;
        state = s19 & input = iI : oInv;
        state = s19 & input = iJ : oInv;
        state = s2 & input = iA : oU;
        state = s2 & input = iB : oInv;
        state = s2 & input = iC : oInv;
        state = s2 & input = iD : oInv;
        state = s2 & input = iE : oInv;
        state = s2 & input = iF : oInv;
        state = s2 & input = iG : oInv;
        state = s2 & input = iH : oInv;
        state = s2 & input = iI : oInv;
        state = s2 & input = iJ : oInv;
        state = s20 & input = iA : oS;
        state = s20 & input = iB : oInv;
        state = s20 & input = iC : oInv;
        state = s20 & input = iD : oInv;
        state = s20 & input = iE : oQ;
        state = s20 & input = iF : oInv;
        state = s20 & input = iG : oInv;
        state = s20 & input = iH : oW;
        state = s20 & input = iI : oInv;
        state = s20 & input = iJ : oInv;
        state = s21 & input = iA : oInv;
        state = s21 & input = iB : oInv;
        state = s21 & input = iC : oInv;
        state = s21 & input = iD : oInv;
        state = s21 & input = iE : oInv;
        state = s21 & input = iF : oX;
        state = s21 & input = iG : oInv;
        state = s21 & input = iH : oInv;
        state = s21 & input = iI : oInv;
        state = s21 & input = iJ : oS;
        state = s22 & input = iA : oInv;
        state = s22 & input = iB : oInv;
        state = s22 & input = iC : oInv;
        state = s22 & input = iD : oInv;
        state = s22 & input = iE : oInv;
        state = s22 & input = iF : oInv;
        state = s22 & input = iG : oInv;
        state = s22 & input = iH : oX;
        state = s22 & input = iI : oInv;
        state = s22 & input = iJ : oInv;
        state = s23 & input = iA : oInv;
        state = s23 & input = iB : oInv;
        state = s23 & input = iC : oInv;
        state = s23 & input = iD : oInv;
        state = s23 & input = iE : oInv;
        state = s23 & input = iF : oInv;
        state = s23 & input = iG : oInv;
        state = s23 & input = iH : oY;
        state = s23 & input = iI : oInv;
        state = s23 & input = iJ : oInv;
        state = s24 & input = iA : oInv;
        state = s24 & input = iB : oInv;
        state = s24 & input = iC : oInv;
        state = s24 & input = iD : oInv;
        state = s24 & input = iE : oInv;
        state = s24 & input = iF : oX;
        state = s24 & input = iG : oInv;
        state = s24 & input = iH : oInv;
        state = s24 & input = iI : oInv;
        state = s24 & input = iJ : oInv;
        state = s25 & input = iA : oInv;
        state = s25 & input = iB : oInv;
        state = s25 & input = iC : oInv;
        state = s25 & input = iD : oInv;
        state = s25 & input = iE : oInv;
        state = s25 & input = iF : oInv;
        state = s25 & input = iG : oInv;
        state = s25 & input = iH : oX;
        state = s25 & input = iI : oInv;
        state = s25 & input = iJ : oInv;
        state = s3 & input = iA : oInv;
        state = s3 & input = iB : oW;
        state = s3 & input = iC : oInv;
        state = s3 & input = iD : oInv;
        state = s3 & input = iE : oInv;
        state = s3 & input = iF : oInv;
        state = s3 & input = iG : oInv;
        state = s3 & input = iH : oInv;
        state = s3 & input = iI : oInv;
        state = s3 & input = iJ : oInv;
        state = s4 & input = iA : oInv;
        state = s4 & input = iB : oInv;
        state = s4 & input = iC : oInv;
        state = s4 & input = iD : oInv;
        state = s4 & input = iE : oInv;
        state = s4 & input = iF : oInv;
        state = s4 & input = iG : oInv;
        state = s4 & input = iH : oInv;
        state = s4 & input = iI : oInv;
        state = s4 & input = iJ : oO;
        state = s5 & input = iA : oInv;
        state = s5 & input = iB : oInv;
        state = s5 & input = iC : oInv;
        state = s5 & input = iD : oInv;
        state = s5 & input = iE : oInv;
        state = s5 & input = iF : oInv;
        state = s5 & input = iG : oInv;
        state = s5 & input = iH : oInv;
        state = s5 & input = iI : oInv;
        state = s5 & input = iJ : oY;
        state = s6 & input = iA : oInv;
        state = s6 & input = iB : oP;
        state = s6 & input = iC : oInv;
        state = s6 & input = iD : oInv;
        state = s6 & input = iE : oInv;
        state = s6 & input = iF : oInv;
        state = s6 & input = iG : oInv;
        state = s6 & input = iH : oInv;
        state = s6 & input = iI : oInv;
        state = s6 & input = iJ : oO;
        state = s7 & input = iA : oInv;
        state = s7 & input = iB : oY;
        state = s7 & input = iC : oInv;
        state = s7 & input = iD : oInv;
        state = s7 & input = iE : oInv;
        state = s7 & input = iF : oInv;
        state = s7 & input = iG : oInv;
        state = s7 & input = iH : oInv;
        state = s7 & input = iI : oInv;
        state = s7 & input = iJ : oInv;
        state = s8 & input = iA : oInv;
        state = s8 & input = iB : oInv;
        state = s8 & input = iC : oInv;
        state = s8 & input = iD : oInv;
        state = s8 & input = iE : oInv;
        state = s8 & input = iF : oInv;
        state = s8 & input = iG : oV;
        state = s8 & input = iH : oInv;
        state = s8 & input = iI : oInv;
        state = s8 & input = iJ : oQ;
        state = s9 & input = iA : oInv;
        state = s9 & input = iB : oV;
        state = s9 & input = iC : oInv;
        state = s9 & input = iD : oInv;
        state = s9 & input = iE : oInv;
        state = s9 & input = iF : oInv;
        state = s9 & input = iG : oInv;
        state = s9 & input = iH : oInv;
        state = s9 & input = iI : oInv;
        state = s9 & input = iJ : oInv;
        input = null : null;
    esac;
INVAR !(input = null & output = null)
    & !(input != null & output != null)
Joshua Moerman's avatar
Joshua Moerman committed
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
LTLSPEC (! (TRUE U (input = iC)) | (! (output = oQ) U ((input = iC) | (((output = oS) & ! (output = oQ)) & X (! (output = oQ) U (output = oY))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oZ) U (((input = iJ) & ! (output = oZ)) & X (! (output = oZ) U (output = oP)))))
LTLSPEC ((output = oZ) V (! (output = oO) | (output = oZ)))
LTLSPEC (! (TRUE U (output = oZ)) | ((! (input = iI) | (! (output = oZ) U ((((output = oO) & ! (output = oZ)) & ! (output = oP)) & X ((! (output = oZ) & ! (output = oP)) U (output = oW))))) U (output = oZ)))
LTLSPEC (! (TRUE U (input = iD)) | ((! (input = iE) | (! (input = iD) U ((output = oR) & ! (input = iD)))) U (input = iD)))
LTLSPEC (FALSE V (! (output = oO) | (((input = iG) & (! X (! (input = iJ) U (input = iI)) | X (! (input = iJ) U ((input = iI) & (TRUE U (output = oV)))))) U ((input = iJ) | (FALSE V ((input = iG) & (! X (! (input = iJ) U (input = iI)) | X (! (input = iJ) U ((input = iI) & (TRUE U (output = oV)))))))))))
LTLSPEC (FALSE V (! (input = iB) | (TRUE U ((output = oQ) & X (TRUE U (output = oY))))))
LTLSPEC (! (TRUE U (output = oS)) | ((! (input = iF) | (! (output = oS) U (((output = oT) & ! (output = oS)) & X (! (output = oS) U (output = oP))))) U (output = oS)))
LTLSPEC (FALSE V (! (input = iB) | (TRUE U (((output = oY) & ! (output = oW)) & X (! (output = oW) U (output = oZ))))))
LTLSPEC (FALSE V (! (input = iE) | ((! (input = iI) | (! (input = iC) U (((output = oP) & ! (input = iC)) & X (! (input = iC) U (output = oW))))) U ((input = iC) | (FALSE V (! (input = iI) | ((output = oP) & X (TRUE U (output = oW)))))))))
LTLSPEC (! (TRUE U (output = oO)) | (! (output = oO) U (((output = oZ) & ! (output = oO)) & X (! (output = oO) U (output = oP)))))
LTLSPEC ((input = iF) V (! (output = oU) | (input = iF)))
LTLSPEC (! (TRUE U (input = iH)) | (! (output = oW) U ((input = iH) | (((input = iJ) & ! (output = oW)) & X (! (output = oW) U (output = oZ))))))
LTLSPEC (! (TRUE U (output = oS)) | (! (output = oS) U (((input = iD) & ! (output = oS)) & X (! (output = oS) U (input = iA)))))
LTLSPEC (FALSE V (! (input = iF) | (TRUE U (((output = oQ) & ! (output = oU)) & X (! (output = oU) U (output = oR))))))
LTLSPEC (! (TRUE U (output = oQ)) | ((! (input = iD) | (! (output = oQ) U ((output = oS) & ! (output = oQ)))) U (output = oQ)))
LTLSPEC (FALSE V (! (input = iB) | ((! (input = iA) | (! (input = iD) U ((((output = oV) & ! (input = iD)) & ! (output = oQ)) & X ((! (input = iD) & ! (output = oQ)) U (output = oP))))) U ((input = iD) | (FALSE V (! (input = iA) | (((output = oV) & ! (output = oQ)) & X (! (output = oQ) U (output = oP)))))))))
LTLSPEC (! (TRUE U (output = oZ)) | ((! (input = iE) | (! (output = oZ) U ((output = oU) & ! (output = oZ)))) U (output = oZ)))
LTLSPEC (FALSE V (! (((input = iE) & ! (output = oR)) & (TRUE U (output = oR))) | (! (output = oY) U ((output = oO) | (output = oR)))))
LTLSPEC (FALSE V (! (input = iE) | (TRUE U ((output = oX) & X (TRUE U (output = oY))))))
LTLSPEC (FALSE V (! (input = iG) | (FALSE V (! (input = iJ) | ((output = oT) & X (TRUE U (output = oX)))))))
LTLSPEC (FALSE V (! ((input = iB) & (TRUE U (input = iD))) | ((! (input = iA) | (! (input = iD) U (((output = oP) & ! (input = iD)) & X (! (input = iD) U (output = oZ))))) U (input = iD))))
LTLSPEC (! (TRUE U ((output = oR) & X (TRUE U (output = oV)))) | (! (output = oR) U (output = oS)))
LTLSPEC (FALSE V (! (output = oY) | (((input = iD) & (! X (! (output = oQ) U (input = iG)) | X (! (output = oQ) U ((input = iG) & (TRUE U (output = oX)))))) U ((output = oQ) | (FALSE V ((input = iD) & (! X (! (output = oQ) U (input = iG)) | X (! (output = oQ) U ((input = iG) & (TRUE U (output = oX)))))))))))
LTLSPEC ((output = oX) V (! (output = oV) | (output = oX)))
LTLSPEC (FALSE V (! (output = oV) | ((! (((output = oX) & ! (output = oW)) & X (! (output = oW) U ((output = oS) & ! (output = oW)))) U ((output = oW) | (output = oR))) | (FALSE V ! ((output = oX) & X (TRUE U (output = oS)))))))
LTLSPEC (FALSE V (! ((input = iG) & (TRUE U (output = oS))) | ((! (input = iA) | (! (output = oS) U ((((output = oW) & ! (output = oS)) & ! (output = oT)) & X ((! (output = oS) & ! (output = oT)) U (output = oQ))))) U (output = oS))))
LTLSPEC (FALSE V (! ((output = oT) & (TRUE U (input = iF))) | (! (output = oY) U ((input = iF) | (((output = oP) & ! (output = oY)) & X (! (output = oY) U (input = iG)))))))
LTLSPEC (! (TRUE U (output = oO)) | (! (((output = oX) & ! (output = oO)) & X (! (output = oO) U ((output = oR) & ! (output = oO)))) U ((output = oO) | (output = oP))))
LTLSPEC (FALSE V (! (((output = oQ) & ! (input = iC)) & (TRUE U (input = iC))) | ((! (input = iG) | (! (input = iC) U ((output = oP) & ! (input = iC)))) U (input = iC))))
LTLSPEC (FALSE V (! (input = iF) | (TRUE U (((output = oU) & ! (output = oZ)) & X (! (output = oZ) U (output = oT))))))
LTLSPEC (! (TRUE U (output = oO)) | ((! (input = iC) | (! (output = oO) U (((output = oW) & ! (output = oO)) & X (! (output = oO) U (output = oT))))) U (output = oO)))
LTLSPEC (FALSE V (! (((input = iA) & ! (output = oR)) & (TRUE U (output = oR))) | (! (output = oS) U ((input = iD) | (output = oR)))))
LTLSPEC (! (TRUE U (output = oO)) | (! (output = oR) U ((input = iC) | (output = oO))))
LTLSPEC ((FALSE V ! (output = oQ)) | (! (output = oQ) U ((output = oQ) & (! (TRUE U (output = oS)) | (! (output = oS) U (((output = oR) & ! (output = oS)) & X (! (output = oS) U (input = iG))))))))
LTLSPEC (FALSE V (! ((input = iD) & (TRUE U (output = oW))) | (((input = iC) & (! X (! (output = oW) U (input = iE)) | X (! (output = oW) U ((input = iE) & (TRUE U (output = oZ)))))) U (output = oW))))
LTLSPEC (! (TRUE U (output = oO)) | (! (output = oO) U (((output = oT) & ! (output = oO)) & X (! (output = oO) U (output = oW)))))
LTLSPEC (! (TRUE U (input = iI)) | ((! (input = iD) | (! (input = iI) U ((output = oQ) & ! (input = iI)))) U (input = iI)))
LTLSPEC (FALSE V (! (output = oY) | (FALSE V ((input = iC) & (! X (TRUE U (input = iD)) | X (! (input = iD) U ((input = iD) & (TRUE U (output = oR)))))))))
LTLSPEC ((FALSE V ! (output = oX)) | (TRUE U ((output = oX) & ((output = oW) V (! (output = oO) | (output = oW))))))
LTLSPEC (FALSE V (! (input = iJ) | (TRUE U (((output = oO) & ! (output = oX)) & X (! (output = oX) U (output = oU))))))
LTLSPEC (FALSE V (! (input = iG) | (TRUE U (output = oR))))
LTLSPEC (FALSE V (! (input = iJ) | (((input = iD) & (! X (! (output = oQ) U (input = iA)) | X (! (output = oQ) U ((input = iA) & (TRUE U (output = oS)))))) U ((output = oQ) | (FALSE V ((input = iD) & (! X (! (output = oQ) U (input = iA)) | X (! (output = oQ) U ((input = iA) & (TRUE U (output = oS)))))))))))
LTLSPEC (FALSE V ((input = iD) & (! ! (output = oU) | (((input = iB) | (output = oU)) V (! (output = oR) | ((input = iB) | (output = oU)))))))
LTLSPEC (FALSE V (! ((input = iI) & (TRUE U (output = oO))) | (! (((output = oS) & ! (output = oO)) & X (! (output = oO) U ((output = oY) & ! (output = oO)))) U ((output = oO) | (input = iB)))))
LTLSPEC (FALSE V (! (output = oR) | (FALSE V (! (input = iJ) | (((output = oZ) & ! (output = oV)) & X (! (output = oV) U (output = oX)))))))
LTLSPEC (! (TRUE U (input = iA)) | ((! (input = iJ) | (! (input = iA) U (((output = oR) & ! (input = iA)) & X (! (input = iA) U (output = oZ))))) U (input = iA)))
LTLSPEC (FALSE V (! (((output = oS) & ! (output = oY)) & (TRUE U (output = oY))) | (! (output = oX) U ((input = iI) | (output = oY)))))
LTLSPEC (FALSE V (! (output = oY) | (! (TRUE U (output = oS)) | (! (output = oS) U ((output = oX) | (((output = oW) & ! (output = oS)) & X (! (output = oS) U (output = oO))))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oU) U ((input = iD) | (output = oZ))))
LTLSPEC ((FALSE V ! (input = iE)) | (! (input = iE) U ((input = iE) & (! (TRUE U (output = oV)) | (! (output = oV) U (((output = oS) & ! (output = oV)) & X (! (output = oV) U (input = iD))))))))
LTLSPEC (FALSE V ((input = iB) & (! ! (output = oX) | ((output = oX) V ((! (input = iA) | (! (output = oX) U ((output = oQ) & ! (output = oX)))) | (output = oX))))))
LTLSPEC (FALSE V (! (input = iH) | (! (TRUE U (output = oY)) | (! (output = oY) U ((output = oV) | (((output = oS) & ! (output = oY)) & X (! (output = oY) U (output = oR))))))))
LTLSPEC (! (TRUE U (output = oU)) | (! (output = oU) U (((output = oW) & ! (output = oU)) & X (! (output = oU) U (input = iJ)))))
LTLSPEC (! (TRUE U (output = oO)) | ((! (input = iE) | (! (output = oO) U (((output = oR) & ! (output = oO)) & X (! (output = oO) U (output = oT))))) U (output = oO)))
LTLSPEC (! (TRUE U (input = iD)) | (! (output = oP) U ((input = iD) | (((input = iC) & ! (output = oP)) & X (! (output = oP) U (output = oU))))))
LTLSPEC (FALSE V ((input = iE) & (! ! (input = iD) | (((output = oT) | (input = iD)) V (! (output = oZ) | ((output = oT) | (input = iD)))))))
LTLSPEC (FALSE V (! ((input = iJ) & (TRUE U (output = oR))) | ((! (input = iC) | (! (output = oR) U ((((output = oT) & ! (output = oR)) & ! (output = oS)) & X ((! (output = oR) & ! (output = oS)) U (output = oW))))) U (output = oR))))
LTLSPEC (FALSE V ((input = iJ) & (! ! (input = iH) | (((input = iI) | (input = iH)) V (! (output = oP) | ((input = iI) | (input = iH)))))))
LTLSPEC (FALSE V (! ((input = iI) & (TRUE U (output = oO))) | (! (output = oT) U ((output = oO) | (((output = oQ) & ! (output = oT)) & X (! (output = oT) U (output = oZ)))))))
LTLSPEC (FALSE V (! ((output = oO) & (TRUE U (output = oY))) | (((input = iJ) & (! X (! (output = oY) U (input = iE)) | X (! (output = oY) U ((input = iE) & (TRUE U (output = oS)))))) U (output = oY))))
LTLSPEC (! (TRUE U (input = iG)) | (((input = iH) & (! X (! (input = iG) U (input = iJ)) | X (! (input = iG) U ((input = iJ) & (TRUE U (output = oQ)))))) U (input = iG)))
LTLSPEC (! (TRUE U (input = iI)) | (! (output = oZ) U ((output = oQ) | (input = iI))))
LTLSPEC (FALSE V (! (input = iD) | (FALSE V (! (input = iH) | (TRUE U (output = oX))))))
LTLSPEC (! (TRUE U (output = oS)) | (! (output = oS) U (((output = oT) & ! (output = oS)) & X (! (output = oS) U (input = iE)))))
LTLSPEC (FALSE V (! (input = iI) | (FALSE V ((input = iG) & (! X (TRUE U (input = iA)) | X (! (input = iA) U ((input = iA) & (TRUE U (output = oS)))))))))
LTLSPEC (FALSE V (! (output = oR) | ((! (input = iB) | (! (output = oS) U ((((output = oY) & ! (output = oS)) & ! (output = oP)) & X ((! (output = oS) & ! (output = oP)) U (output = oX))))) U ((output = oS) | (FALSE V (! (input = iB) | (((output = oY) & ! (output = oP)) & X (! (output = oP) U (output = oX)))))))))
LTLSPEC (FALSE V (! (input = iH) | ((! (input = iF) | (! (output = oY) U (((output = oS) & ! (output = oY)) & X (! (output = oY) U (output = oX))))) U ((output = oY) | (FALSE V (! (input = iF) | ((output = oS) & X (TRUE U (output = oX)))))))))
LTLSPEC (FALSE V (! (input = iC) | (TRUE U (output = oT))))
LTLSPEC (FALSE V (! (output = oY) | (! (TRUE U (output = oP)) | (! (output = oP) U ((output = oT) | (((input = iD) & ! (output = oP)) & X (! (output = oP) U (output = oX))))))))
LTLSPEC (FALSE V (! (output = oU) | (! (TRUE U (output = oT)) | (! (output = oT) U ((input = iA) | (((input = iJ) & ! (output = oT)) & X (! (output = oT) U (input = iB))))))))
LTLSPEC (FALSE V (! (input = iH) | (FALSE V (! (input = iB) | ((output = oQ) & X (TRUE U (output = oS)))))))
LTLSPEC (! (TRUE U (output = oU)) | (! (((output = oY) & ! (output = oU)) & X (! (output = oU) U ((output = oV) & ! (output = oU)))) U ((output = oU) | (input = iC))))
LTLSPEC (FALSE V (! ((output = oS) & (TRUE U (output = oW))) | ((! (input = iG) | (! (output = oW) U ((((output = oR) & ! (output = oW)) & ! (output = oT)) & X ((! (output = oW) & ! (output = oT)) U (output = oP))))) U (output = oW))))
LTLSPEC (FALSE V (! (input = iH) | (TRUE U ((output = oR) & X (TRUE U (output = oQ))))))
LTLSPEC ((FALSE V ! (output = oV)) | (TRUE U ((output = oV) & ((output = oO) V (! (output = oU) | (output = oO))))))
LTLSPEC (! (TRUE U (output = oO)) | ((! (input = iH) | (! (output = oO) U (((output = oW) & ! (output = oO)) & X (! (output = oO) U (output = oZ))))) U (output = oO)))
LTLSPEC (FALSE V ((input = iA) & (! ! (input = iJ) | (((output = oZ) | (input = iJ)) V (! (output = oP) | ((output = oZ) | (input = iJ)))))))
LTLSPEC (FALSE V (! (input = iH) | (TRUE U (output = oY))))
LTLSPEC ((FALSE V ! (output = oX)) | (! (output = oX) U ((output = oX) & (! (TRUE U (output = oW)) | (! (output = oW) U (((output = oS) & ! (output = oW)) & X (! (output = oW) U (input = iF))))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oV) U ((output = oZ) | (((input = iD) & ! (output = oV)) & X (! (output = oV) U (output = oO))))))
LTLSPEC (FALSE V (! (output = oU) | ((! (input = iD) | (! (input = iI) U ((((output = oO) & ! (input = iI)) & ! (output = oW)) & X ((! (input = iI) & ! (output = oW)) U (output = oR))))) U ((input = iI) | (FALSE V (! (input = iD) | (((output = oO) & ! (output = oW)) & X (! (output = oW) U (output = oR)))))))))
LTLSPEC ((FALSE V ! (output = oX)) | (! (output = oX) U ((output = oX) & (! (TRUE U ((output = oO) & X (TRUE U (output = oV)))) | (! (output = oO) U (output = oT))))))
LTLSPEC (! (TRUE U (output = oO)) | ((! (input = iF) | (! (output = oO) U ((output = oW) & ! (output = oO)))) U (output = oO)))
LTLSPEC (! (TRUE U (input = iG)) | (! (output = oR) U ((input = iB) | (input = iG))))
LTLSPEC (! (TRUE U (input = iI)) | (! (output = oY) U ((input = iI) | (((output = oU) & ! (output = oY)) & X (! (output = oY) U (input = iJ))))))
LTLSPEC (! (TRUE U (input = iH)) | ((! (input = iE) | (! (input = iH) U ((output = oS) & ! (input = iH)))) U (input = iH)))
LTLSPEC (FALSE V (! (output = oQ) | (FALSE V ((input = iJ) & (! X (TRUE U (input = iA)) | X (! (input = iA) U ((input = iA) & (TRUE U (output = oP)))))))))
LTLSPEC (FALSE V ((output = oR) & (! ! (output = oU) | ((output = oU) V ((! (input = iJ) | (! (output = oU) U ((output = oT) & ! (output = oU)))) | (output = oU))))))
LTLSPEC (FALSE V ((output = oW) & (! ! (output = oP) | (((output = oX) | (output = oP)) V (! (output = oY) | ((output = oX) | (output = oP)))))))
LTLSPEC ((FALSE V ! (output = oZ)) | (! (output = oZ) U ((output = oZ) & (! (TRUE U ((output = oV) & X (TRUE U (output = oX)))) | (! (output = oV) U (input = iH))))))
LTLSPEC (FALSE V (! (output = oP) | (FALSE V ((input = iH) & (! X (TRUE U (input = iB)) | X (! (input = iB) U ((input = iB) & (TRUE U (output = oS)))))))))
LTLSPEC (FALSE V (! (input = iE) | (FALSE V ((input = iF) & (! X (TRUE U (input = iG)) | X (! (input = iG) U ((input = iG) & (TRUE U (output = oV)))))))))
LTLSPEC ((FALSE V ! (input = iE)) | (TRUE U ((input = iE) & ((input = iI) V (! (output = oQ) | (input = iI))))))
LTLSPEC (FALSE V (! (input = iD) | (TRUE U (output = oR))))
LTLSPEC ((output = oV) V (! (output = oR) | (output = oV)))
LTLSPEC (! (TRUE U (output = oX)) | (! (output = oX) U (((output = oO) & ! (output = oX)) & X (! (output = oX) U (input = iA)))))
LTLSPEC (FALSE V (! (((input = iH) & ! (output = oS)) & (TRUE U (output = oS))) | ((! (input = iD) | (! (output = oS) U ((output = oT) & ! (output = oS)))) U (output = oS))))
LTLSPEC (FALSE V (! (output = oV) | (FALSE V ((input = iA) & (! X (TRUE U (input = iG)) | X (! (input = iG) U ((input = iG) & (TRUE U (output = oX)))))))))
LTLSPEC (! (TRUE U (output = oV)) | ((! (input = iG) | (! (output = oV) U (((output = oX) & ! (output = oV)) & X (! (output = oV) U (output = oT))))) U (output = oV)))