Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / all files / microwave39.smt2 @ b8dc00eb

History | View | Annotate | Download (92.3 KB)

1
; top
2
(declare-var top.KP_START Bool)
3
(declare-var top.KP_CLEAR Bool)
4
(declare-var top.KP_0 Bool)
5
(declare-var top.KP_1 Bool)
6
(declare-var top.KP_2 Bool)
7
(declare-var top.KP_3 Bool)
8
(declare-var top.KP_4 Bool)
9
(declare-var top.KP_5 Bool)
10
(declare-var top.KP_6 Bool)
11
(declare-var top.KP_7 Bool)
12
(declare-var top.KP_8 Bool)
13
(declare-var top.KP_9 Bool)
14
(declare-var top.DOOR_CLOSED Bool)
15
(declare-var top.OK Bool)
16
(declare-var top.__top_13_c Bool)
17
(declare-var top.__top_15_c Bool)
18
(declare-var top.__top_17_c Bool)
19
(declare-var top.__top_19_c Bool)
20
(declare-var top.__top_2_c Int)
21
(declare-var top.__top_21_c Bool)
22
(declare-var top.__top_23_c Bool)
23
(declare-var top.__top_25_c Bool)
24
(declare-var top.__top_27_c Bool)
25
(declare-var top.__top_29_c Bool)
26
(declare-var top.__top_31_c Bool)
27
(declare-var top.__top_36_c Int)
28
(declare-var top.__top_37_c Int)
29
(declare-var top.__top_38_c Int)
30
(declare-var top.__top_39_c Int)
31
(declare-var top.__top_6_c Bool)
32
(declare-var top.__top_66_c Int)
33
(declare-var top.__top_67_c Int)
34
(declare-var top.__top_68_c Int)
35
(declare-var top.__top_69_c Bool)
36
(declare-var top.__top_7_c Bool)
37
(declare-var top.__top_70_c Bool)
38
(declare-var top.__top_74_c Bool)
39
(declare-var top.__top_76_c Int)
40
(declare-var top.__top_77_c Int)
41
(declare-var top.__top_78_c Int)
42
(declare-var top.__top_79_c Int)
43
(declare-var top.__top_80_c Int)
44
(declare-var top.__top_81_c Bool)
45
(declare-var top.__top_82_c Bool)
46
(declare-var top.__top_83_c Bool)
47
(declare-var top.__top_84_c Bool)
48
(declare-var top.__top_85_c Bool)
49
(declare-var top.__top_86_c Bool)
50
(declare-var top.__top_87_c Bool)
51
(declare-var top.__top_88_c Bool)
52
(declare-var top.__top_89_c Bool)
53
(declare-var top.__top_9_c Int)
54
(declare-var top.__top_90_c Bool)
55
(declare-var top.__top_92_c Bool)
56
(declare-var top.__top_93_c Int)
57
(declare-var top.ni_0._arrow._first_c Bool)
58
(declare-var top.__top_13_m Bool)
59
(declare-var top.__top_15_m Bool)
60
(declare-var top.__top_17_m Bool)
61
(declare-var top.__top_19_m Bool)
62
(declare-var top.__top_2_m Int)
63
(declare-var top.__top_21_m Bool)
64
(declare-var top.__top_23_m Bool)
65
(declare-var top.__top_25_m Bool)
66
(declare-var top.__top_27_m Bool)
67
(declare-var top.__top_29_m Bool)
68
(declare-var top.__top_31_m Bool)
69
(declare-var top.__top_36_m Int)
70
(declare-var top.__top_37_m Int)
71
(declare-var top.__top_38_m Int)
72
(declare-var top.__top_39_m Int)
73
(declare-var top.__top_6_m Bool)
74
(declare-var top.__top_66_m Int)
75
(declare-var top.__top_67_m Int)
76
(declare-var top.__top_68_m Int)
77
(declare-var top.__top_69_m Bool)
78
(declare-var top.__top_7_m Bool)
79
(declare-var top.__top_70_m Bool)
80
(declare-var top.__top_74_m Bool)
81
(declare-var top.__top_76_m Int)
82
(declare-var top.__top_77_m Int)
83
(declare-var top.__top_78_m Int)
84
(declare-var top.__top_79_m Int)
85
(declare-var top.__top_80_m Int)
86
(declare-var top.__top_81_m Bool)
87
(declare-var top.__top_82_m Bool)
88
(declare-var top.__top_83_m Bool)
89
(declare-var top.__top_84_m Bool)
90
(declare-var top.__top_85_m Bool)
91
(declare-var top.__top_86_m Bool)
92
(declare-var top.__top_87_m Bool)
93
(declare-var top.__top_88_m Bool)
94
(declare-var top.__top_89_m Bool)
95
(declare-var top.__top_9_m Int)
96
(declare-var top.__top_90_m Bool)
97
(declare-var top.__top_92_m Bool)
98
(declare-var top.__top_93_m Int)
99
(declare-var top.ni_0._arrow._first_m Bool)
100
(declare-var top.__top_13_x Bool)
101
(declare-var top.__top_15_x Bool)
102
(declare-var top.__top_17_x Bool)
103
(declare-var top.__top_19_x Bool)
104
(declare-var top.__top_2_x Int)
105
(declare-var top.__top_21_x Bool)
106
(declare-var top.__top_23_x Bool)
107
(declare-var top.__top_25_x Bool)
108
(declare-var top.__top_27_x Bool)
109
(declare-var top.__top_29_x Bool)
110
(declare-var top.__top_31_x Bool)
111
(declare-var top.__top_36_x Int)
112
(declare-var top.__top_37_x Int)
113
(declare-var top.__top_38_x Int)
114
(declare-var top.__top_39_x Int)
115
(declare-var top.__top_6_x Bool)
116
(declare-var top.__top_66_x Int)
117
(declare-var top.__top_67_x Int)
118
(declare-var top.__top_68_x Int)
119
(declare-var top.__top_69_x Bool)
120
(declare-var top.__top_7_x Bool)
121
(declare-var top.__top_70_x Bool)
122
(declare-var top.__top_74_x Bool)
123
(declare-var top.__top_76_x Int)
124
(declare-var top.__top_77_x Int)
125
(declare-var top.__top_78_x Int)
126
(declare-var top.__top_79_x Int)
127
(declare-var top.__top_80_x Int)
128
(declare-var top.__top_81_x Bool)
129
(declare-var top.__top_82_x Bool)
130
(declare-var top.__top_83_x Bool)
131
(declare-var top.__top_84_x Bool)
132
(declare-var top.__top_85_x Bool)
133
(declare-var top.__top_86_x Bool)
134
(declare-var top.__top_87_x Bool)
135
(declare-var top.__top_88_x Bool)
136
(declare-var top.__top_89_x Bool)
137
(declare-var top.__top_9_x Int)
138
(declare-var top.__top_90_x Bool)
139
(declare-var top.__top_92_x Bool)
140
(declare-var top.__top_93_x Int)
141
(declare-var top.ni_0._arrow._first_x Bool)
142
(declare-var top.CLEAR_PRESSED Bool)
143
(declare-var top.COOKING Bool)
144
(declare-var top.KP_01 Bool)
145
(declare-var top.KP_11 Bool)
146
(declare-var top.KP_21 Bool)
147
(declare-var top.KP_31 Bool)
148
(declare-var top.KP_41 Bool)
149
(declare-var top.KP_51 Bool)
150
(declare-var top.KP_61 Bool)
151
(declare-var top.KP_71 Bool)
152
(declare-var top.KP_81 Bool)
153
(declare-var top.KP_91 Bool)
154
(declare-var top.LEFT_DIGIT Int)
155
(declare-var top.MIDDLE_DIGIT Int)
156
(declare-var top.MWI_FcnMaxI_In1 Int)
157
(declare-var top.MWI_FcnMaxI_In11 Int)
158
(declare-var top.MWI_FcnMaxI_In12 Int)
159
(declare-var top.MWI_FcnMaxI_In13 Int)
160
(declare-var top.MWI_FcnMaxI_In15 Int)
161
(declare-var top.MWI_FcnMaxI_In16 Int)
162
(declare-var top.RIGHT_DIGIT Int)
163
(declare-var top.SETUP Bool)
164
(declare-var top.START_PRESSED Bool)
165
(declare-var top.STEPS_TO_COOK Int)
166
(declare-var top.SUSPENDED Bool)
167
(declare-var top.__top_1 Bool)
168
(declare-var top.__top_10 Int)
169
(declare-var top.__top_100 Bool)
170
(declare-var top.__top_101 Bool)
171
(declare-var top.__top_102 Bool)
172
(declare-var top.__top_103 Bool)
173
(declare-var top.__top_104 Bool)
174
(declare-var top.__top_105 Bool)
175
(declare-var top.__top_11 Bool)
176
(declare-var top.__top_12 Bool)
177
(declare-var top.__top_14 Bool)
178
(declare-var top.__top_16 Bool)
179
(declare-var top.__top_18 Bool)
180
(declare-var top.__top_20 Bool)
181
(declare-var top.__top_22 Bool)
182
(declare-var top.__top_24 Bool)
183
(declare-var top.__top_26 Bool)
184
(declare-var top.__top_28 Bool)
185
(declare-var top.__top_3 Bool)
186
(declare-var top.__top_30 Bool)
187
(declare-var top.__top_32 Bool)
188
(declare-var top.__top_33 Int)
189
(declare-var top.__top_34 Bool)
190
(declare-var top.__top_35 Bool)
191
(declare-var top.__top_4 Bool)
192
(declare-var top.__top_40 Bool)
193
(declare-var top.__top_41 Bool)
194
(declare-var top.__top_42 Bool)
195
(declare-var top.__top_43 Bool)
196
(declare-var top.__top_44 Bool)
197
(declare-var top.__top_45 Bool)
198
(declare-var top.__top_46 Bool)
199
(declare-var top.__top_47 Bool)
200
(declare-var top.__top_48 Bool)
201
(declare-var top.__top_49 Bool)
202
(declare-var top.__top_5 Bool)
203
(declare-var top.__top_50 Bool)
204
(declare-var top.__top_51 Bool)
205
(declare-var top.__top_52 Bool)
206
(declare-var top.__top_53 Bool)
207
(declare-var top.__top_54 Bool)
208
(declare-var top.__top_55 Bool)
209
(declare-var top.__top_56 Bool)
210
(declare-var top.__top_57 Bool)
211
(declare-var top.__top_58 Bool)
212
(declare-var top.__top_59 Bool)
213
(declare-var top.__top_60 Bool)
214
(declare-var top.__top_61 Int)
215
(declare-var top.__top_62 Bool)
216
(declare-var top.__top_63 Bool)
217
(declare-var top.__top_64 Bool)
218
(declare-var top.__top_65 Bool)
219
(declare-var top.__top_71 Bool)
220
(declare-var top.__top_72 Bool)
221
(declare-var top.__top_73 Bool)
222
(declare-var top.__top_75 Bool)
223
(declare-var top.__top_8 Bool)
224
(declare-var top.__top_91 Bool)
225
(declare-var top.__top_94 Bool)
226
(declare-var top.__top_95 Bool)
227
(declare-var top.__top_96 Bool)
228
(declare-var top.__top_97 Bool)
229
(declare-var top.__top_98 Bool)
230
(declare-var top.__top_99 Bool)
231
(declare-var top.chart_microwave_mode_logic____wakeup___ Bool)
232
(declare-var top.chart_microwave_mode_logic_begin_state_outports_mode Int)
233
(declare-var top.chart_microwave_mode_logic_begin_state_outports_steps_remaining Int)
234
(declare-var top.chart_microwave_mode_logic_begin_state_states___root Int)
235
(declare-var top.chart_microwave_mode_logic_clear_off Int)
236
(declare-var top.chart_microwave_mode_logic_door_closed Int)
237
(declare-var top.chart_microwave_mode_logic_final_state_states___root Int)
238
(declare-var top.chart_microwave_mode_logic_mode Int)
239
(declare-var top.chart_microwave_mode_logic_rlt_evtInitStep Bool)
240
(declare-var top.chart_microwave_mode_logic_start Int)
241
(declare-var top.chart_microwave_mode_logic_steps_remaining Int)
242
(declare-var top.enable Bool)
243
(declare-var top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY Int)
244
(declare-var top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY Int)
245
(declare-var top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY Int)
246
(declare-var top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT Int)
247
(declare-var top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT Int)
248
(declare-var top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER Int)
249
(declare-var top.microwave_microwave_mode_logic_mode Int)
250
(declare-var top.p37 Bool)
251
(declare-var top.rlt__Arrow Int)
252
(declare-var top.rlt__Arrow1 Int)
253
(declare-var top.rlt__Arrow2 Int)
254
(declare-var top.rlt__Arrow3 Int)
255
(declare-var top.rlt__Arrow4 Int)
256
(declare-var top.rlt__Arrow5 Int)
257
(declare-var top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock Bool)
258
(declare-var top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step Bool)
259
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_fired_0 Bool)
260
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 Bool)
261
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 Bool)
262
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root Int)
263
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode Int)
264
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root Int)
265
(declare-var top.rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root Int)
266
(declare-var top.rlt_enter_microwave_mode_logic_rlt_state_2_states___root Int)
267
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_complete_1 Bool)
268
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_complete_2 Bool)
269
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 Bool)
270
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 Bool)
271
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 Bool)
272
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 Bool)
273
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 Bool)
274
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root Int)
275
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode Int)
276
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root Int)
277
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root Int)
278
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root Int)
279
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode Int)
280
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root Int)
281
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode Int)
282
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root Int)
283
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining Int)
284
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root Int)
285
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root Int)
286
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode Int)
287
(declare-var top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root Int)
288
(declare-var top.rlt_eval_microwave_mode_logic_rlt_fired_0 Bool)
289
(declare-var top.rlt_eval_microwave_mode_logic_rlt_fired_1 Bool)
290
(declare-var top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining Int)
291
(declare-var top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root Int)
292
(declare-var top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode Int)
293
(declare-var top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root Int)
294
(declare-rel top_reset (Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Int Int Int Int Bool Int Int Int Bool Bool Bool Bool Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Int Bool Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Int Int Int Int Bool Int Int Int Bool Bool Bool Bool Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Int Bool))
295
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Int Int Int Int Bool Int Int Int Bool Bool Bool Bool Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Int Bool Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Int Int Int Int Bool Int Int Int Bool Bool Bool Bool Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Int Bool))
296

    
297
(rule (=> 
298
  (and 
299
       (= top.__top_13_m top.__top_13_c)
300
       (= top.__top_15_m top.__top_15_c)
301
       (= top.__top_17_m top.__top_17_c)
302
       (= top.__top_19_m top.__top_19_c)
303
       (= top.__top_2_m top.__top_2_c)
304
       (= top.__top_21_m top.__top_21_c)
305
       (= top.__top_23_m top.__top_23_c)
306
       (= top.__top_25_m top.__top_25_c)
307
       (= top.__top_27_m top.__top_27_c)
308
       (= top.__top_29_m top.__top_29_c)
309
       (= top.__top_31_m top.__top_31_c)
310
       (= top.__top_36_m top.__top_36_c)
311
       (= top.__top_37_m top.__top_37_c)
312
       (= top.__top_38_m top.__top_38_c)
313
       (= top.__top_39_m top.__top_39_c)
314
       (= top.__top_6_m top.__top_6_c)
315
       (= top.__top_66_m top.__top_66_c)
316
       (= top.__top_67_m top.__top_67_c)
317
       (= top.__top_68_m top.__top_68_c)
318
       (= top.__top_69_m top.__top_69_c)
319
       (= top.__top_7_m top.__top_7_c)
320
       (= top.__top_70_m top.__top_70_c)
321
       (= top.__top_74_m top.__top_74_c)
322
       (= top.__top_76_m top.__top_76_c)
323
       (= top.__top_77_m top.__top_77_c)
324
       (= top.__top_78_m top.__top_78_c)
325
       (= top.__top_79_m top.__top_79_c)
326
       (= top.__top_80_m top.__top_80_c)
327
       (= top.__top_81_m top.__top_81_c)
328
       (= top.__top_82_m top.__top_82_c)
329
       (= top.__top_83_m top.__top_83_c)
330
       (= top.__top_84_m top.__top_84_c)
331
       (= top.__top_85_m top.__top_85_c)
332
       (= top.__top_86_m top.__top_86_c)
333
       (= top.__top_87_m top.__top_87_c)
334
       (= top.__top_88_m top.__top_88_c)
335
       (= top.__top_89_m top.__top_89_c)
336
       (= top.__top_9_m top.__top_9_c)
337
       (= top.__top_90_m top.__top_90_c)
338
       (= top.__top_92_m top.__top_92_c)
339
       (= top.__top_93_m top.__top_93_c)
340
       (= top.ni_0._arrow._first_m true)
341
  )
342
  (top_reset top.__top_13_c
343
             top.__top_15_c
344
             top.__top_17_c
345
             top.__top_19_c
346
             top.__top_2_c
347
             top.__top_21_c
348
             top.__top_23_c
349
             top.__top_25_c
350
             top.__top_27_c
351
             top.__top_29_c
352
             top.__top_31_c
353
             top.__top_36_c
354
             top.__top_37_c
355
             top.__top_38_c
356
             top.__top_39_c
357
             top.__top_6_c
358
             top.__top_66_c
359
             top.__top_67_c
360
             top.__top_68_c
361
             top.__top_69_c
362
             top.__top_7_c
363
             top.__top_70_c
364
             top.__top_74_c
365
             top.__top_76_c
366
             top.__top_77_c
367
             top.__top_78_c
368
             top.__top_79_c
369
             top.__top_80_c
370
             top.__top_81_c
371
             top.__top_82_c
372
             top.__top_83_c
373
             top.__top_84_c
374
             top.__top_85_c
375
             top.__top_86_c
376
             top.__top_87_c
377
             top.__top_88_c
378
             top.__top_89_c
379
             top.__top_9_c
380
             top.__top_90_c
381
             top.__top_92_c
382
             top.__top_93_c
383
             top.ni_0._arrow._first_c
384
             top.__top_13_m
385
             top.__top_15_m
386
             top.__top_17_m
387
             top.__top_19_m
388
             top.__top_2_m
389
             top.__top_21_m
390
             top.__top_23_m
391
             top.__top_25_m
392
             top.__top_27_m
393
             top.__top_29_m
394
             top.__top_31_m
395
             top.__top_36_m
396
             top.__top_37_m
397
             top.__top_38_m
398
             top.__top_39_m
399
             top.__top_6_m
400
             top.__top_66_m
401
             top.__top_67_m
402
             top.__top_68_m
403
             top.__top_69_m
404
             top.__top_7_m
405
             top.__top_70_m
406
             top.__top_74_m
407
             top.__top_76_m
408
             top.__top_77_m
409
             top.__top_78_m
410
             top.__top_79_m
411
             top.__top_80_m
412
             top.__top_81_m
413
             top.__top_82_m
414
             top.__top_83_m
415
             top.__top_84_m
416
             top.__top_85_m
417
             top.__top_86_m
418
             top.__top_87_m
419
             top.__top_88_m
420
             top.__top_89_m
421
             top.__top_9_m
422
             top.__top_90_m
423
             top.__top_92_m
424
             top.__top_93_m
425
             top.ni_0._arrow._first_m)
426
))
427

    
428
(rule (=> 
429
  (and (= top.ni_0._arrow._first_m top.ni_0._arrow._first_c)(and (= top.__top_1 (ite top.ni_0._arrow._first_m true false))
430
                                                                 (= top.ni_0._arrow._first_x false))
431
       (and (or (not (= top.__top_1 true))
432
               (= top.chart_microwave_mode_logic_begin_state_states___root 0))
433
            (or (not (= top.__top_1 false))
434
               (= top.chart_microwave_mode_logic_begin_state_states___root top.__top_68_c))
435
       )
436
       (= top.rlt_eval_microwave_mode_logic_rlt_fired_0 (= top.chart_microwave_mode_logic_begin_state_states___root 4))
437
       (= top.__top_3 (= 1 top.__top_2_c))
438
       (and (or (not (= top.__top_1 true))
439
               (= top.enable true))
440
            (or (not (= top.__top_1 false))
441
               (and (or (not (= top.__top_3 true))
442
                       (= top.enable true))
443
                    (or (not (= top.__top_3 false))
444
                       (= top.enable false))
445
               ))
446
       )
447
       (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock top.enable)
448
       (= top.__top_5 (not top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock))
449
       (and (or (not (= top.__top_1 true))
450
               (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step true))
451
            (or (not (= top.__top_1 false))
452
               (and (or (not (= top.__top_5 true))
453
                       (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step true))
454
                    (or (not (= top.__top_5 false))
455
                       (and (or (not (= top.__top_6_c true))
456
                               (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step false))
457
                            (or (not (= top.__top_6_c false))
458
                               (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step top.__top_7_c))
459
                       ))
460
               ))
461
       )
462
       (= top.KP_91 top.KP_9)
463
       (= top.__top_32 (and top.KP_91 (not top.__top_31_c)))
464
       (= top.KP_81 top.KP_8)
465
       (= top.__top_30 (and top.KP_81 (not top.__top_29_c)))
466
       (= top.KP_71 top.KP_7)
467
       (= top.__top_28 (and top.KP_71 (not top.__top_27_c)))
468
       (= top.KP_61 top.KP_6)
469
       (= top.__top_26 (and top.KP_61 (not top.__top_25_c)))
470
       (= top.KP_51 top.KP_5)
471
       (= top.__top_24 (and top.KP_51 (not top.__top_23_c)))
472
       (= top.KP_41 top.KP_4)
473
       (= top.__top_22 (and top.KP_41 (not top.__top_21_c)))
474
       (= top.KP_31 top.KP_3)
475
       (= top.__top_20 (and top.KP_31 (not top.__top_19_c)))
476
       (= top.KP_21 top.KP_2)
477
       (= top.__top_18 (and top.KP_21 (not top.__top_17_c)))
478
       (= top.KP_11 top.KP_1)
479
       (= top.__top_16 (and top.KP_11 (not top.__top_15_c)))
480
       (= top.KP_01 top.KP_0)
481
       (= top.__top_14 (and top.KP_01 (not top.__top_13_c)))
482
       (and (or (not (= top.__top_14 true))
483
               (= top.__top_33 0))
484
            (or (not (= top.__top_14 false))
485
               (and (or (not (= top.__top_16 true))
486
                       (= top.__top_33 1))
487
                    (or (not (= top.__top_16 false))
488
                       (and (or (not (= top.__top_18 true))
489
                               (= top.__top_33 2))
490
                            (or (not (= top.__top_18 false))
491
                               (and (or (not (= top.__top_20 true))
492
                                       (= top.__top_33 3))
493
                                    (or (not (= top.__top_20 false))
494
                                       (and (or (not (= top.__top_22 true))
495
                                               (= top.__top_33 4))
496
                                            (or (not (= top.__top_22 false))
497
                                               (and (or (not (= top.__top_24 true))
498
                                                       (= top.__top_33 5))
499
                                                    (or (not (= top.__top_24 false))
500
                                                       (and (or (not (= top.__top_26 true))
501
                                                               (= top.__top_33 6))
502
                                                            (or (not (= top.__top_26 false))
503
                                                               (and (or (not (= top.__top_28 true))
504
                                                                    (= top.__top_33 7))
505
                                                                    (or (not (= top.__top_28 false))
506
                                                                    (and 
507
                                                                    (or (not (= top.__top_30 true))
508
                                                                    (= top.__top_33 8))
509
                                                                    (or (not (= top.__top_30 false))
510
                                                                    (and 
511
                                                                    (or (not (= top.__top_32 true))
512
                                                                    (= top.__top_33 9))
513
                                                                    (or (not (= top.__top_32 false))
514
                                                                    (= top.__top_33 10))
515
                                                                    ))
516
                                                                    ))
517
                                                               ))
518
                                                       ))
519
                                               ))
520
                                       ))
521
                               ))
522
                       ))
523
               ))
524
       )
525
       (= top.__top_34 (<= top.__top_33 9))
526
       (and (or (not (= top.__top_34 true))
527
               (= top.__top_35 true))
528
            (or (not (= top.__top_34 false))
529
               (= top.__top_35 false))
530
       )
531
       (and (or (not (= top.KP_01 true))
532
               (= top.__top_10 0))
533
            (or (not (= top.KP_01 false))
534
               (and (or (not (= top.KP_11 true))
535
                       (= top.__top_10 1))
536
                    (or (not (= top.KP_11 false))
537
                       (and (or (not (= top.KP_21 true))
538
                               (= top.__top_10 2))
539
                            (or (not (= top.KP_21 false))
540
                               (and (or (not (= top.KP_31 true))
541
                                       (= top.__top_10 3))
542
                                    (or (not (= top.KP_31 false))
543
                                       (and (or (not (= top.KP_41 true))
544
                                               (= top.__top_10 4))
545
                                            (or (not (= top.KP_41 false))
546
                                               (and (or (not (= top.KP_51 true))
547
                                                       (= top.__top_10 5))
548
                                                    (or (not (= top.KP_51 false))
549
                                                       (and (or (not (= top.KP_61 true))
550
                                                               (= top.__top_10 6))
551
                                                            (or (not (= top.KP_61 false))
552
                                                               (and (or (not (= top.KP_71 true))
553
                                                                    (= top.__top_10 7))
554
                                                                    (or (not (= top.KP_71 false))
555
                                                                    (and 
556
                                                                    (or (not (= top.KP_81 true))
557
                                                                    (= top.__top_10 8))
558
                                                                    (or (not (= top.KP_81 false))
559
                                                                    (and 
560
                                                                    (or (not (= top.KP_91 true))
561
                                                                    (= top.__top_10 9))
562
                                                                    (or (not (= top.KP_91 false))
563
                                                                    (= top.__top_10 10))
564
                                                                    ))
565
                                                                    ))
566
                                                               ))
567
                                                       ))
568
                                               ))
569
                                       ))
570
                               ))
571
                       ))
572
               ))
573
       )
574
       (= top.__top_11 (<= top.__top_10 9))
575
       (and (or (not (= top.__top_11 true))
576
               (= top.__top_12 true))
577
            (or (not (= top.__top_11 false))
578
               (= top.__top_12 false))
579
       )
580
       (and (or (not (= top.__top_1 false))
581
               (and (and (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock false))
582
                            (and (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY top.__top_36_c)
583
                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY top.__top_37_c)
584
                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY top.__top_38_c)
585
                                 ))
586
                         (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock true))
587
                            (and (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step false))
588
                                    (and (or (not (= top.KP_CLEAR false))
589
                                            (and (or (not (= top.__top_35 false))
590
                                                    (and (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY top.__top_36_c)
591
                                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY top.__top_37_c)
592
                                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY top.__top_38_c)
593
                                                         ))
594
                                                 (or (not (= top.__top_35 true))
595
                                                    (and (and (or (not (= top.__top_14 true))
596
                                                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
597
                                                              (or (not (= top.__top_14 false))
598
                                                                 (and 
599
                                                                 (or (not (= top.__top_16 true))
600
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 1))
601
                                                                 (or (not (= top.__top_16 false))
602
                                                                    (and 
603
                                                                    (or (not (= top.__top_18 true))
604
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 2))
605
                                                                    (or (not (= top.__top_18 false))
606
                                                                    (and 
607
                                                                    (or (not (= top.__top_20 true))
608
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 3))
609
                                                                    (or (not (= top.__top_20 false))
610
                                                                    (and 
611
                                                                    (or (not (= top.__top_22 true))
612
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 4))
613
                                                                    (or (not (= top.__top_22 false))
614
                                                                    (and 
615
                                                                    (or (not (= top.__top_24 true))
616
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 5))
617
                                                                    (or (not (= top.__top_24 false))
618
                                                                    (and 
619
                                                                    (or (not (= top.__top_26 true))
620
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 6))
621
                                                                    (or (not (= top.__top_26 false))
622
                                                                    (and 
623
                                                                    (or (not (= top.__top_28 true))
624
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 7))
625
                                                                    (or (not (= top.__top_28 false))
626
                                                                    (and 
627
                                                                    (or (not (= top.__top_30 true))
628
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 8))
629
                                                                    (or (not (= top.__top_30 false))
630
                                                                    (and 
631
                                                                    (or (not (= top.__top_32 true))
632
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 9))
633
                                                                    (or (not (= top.__top_32 false))
634
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 10))
635
                                                                    ))
636
                                                                    ))
637
                                                                    ))
638
                                                                    ))
639
                                                                    ))
640
                                                                    ))
641
                                                                    ))
642
                                                                    ))
643
                                                                 ))
644
                                                         )
645
                                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY top.__top_36_c)
646
                                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY top.__top_37_c)
647
                                                         ))
648
                                            ))
649
                                         (or (not (= top.KP_CLEAR true))
650
                                            (and (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0)
651
                                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY 0)
652
                                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY 0)
653
                                                 ))
654
                                    ))
655
                                 (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step true))
656
                                    (and (and (or (not (= top.KP_CLEAR true))
657
                                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
658
                                              (or (not (= top.KP_CLEAR false))
659
                                                 (and (or (not (= top.__top_12 true))
660
                                                         (and (or (not (= top.KP_01 true))
661
                                                                 (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
662
                                                              (or (not (= top.KP_01 false))
663
                                                                 (and 
664
                                                                 (or (not (= top.KP_11 true))
665
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 1))
666
                                                                 (or (not (= top.KP_11 false))
667
                                                                    (and 
668
                                                                    (or (not (= top.KP_21 true))
669
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 2))
670
                                                                    (or (not (= top.KP_21 false))
671
                                                                    (and 
672
                                                                    (or (not (= top.KP_31 true))
673
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 3))
674
                                                                    (or (not (= top.KP_31 false))
675
                                                                    (and 
676
                                                                    (or (not (= top.KP_41 true))
677
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 4))
678
                                                                    (or (not (= top.KP_41 false))
679
                                                                    (and 
680
                                                                    (or (not (= top.KP_51 true))
681
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 5))
682
                                                                    (or (not (= top.KP_51 false))
683
                                                                    (and 
684
                                                                    (or (not (= top.KP_61 true))
685
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 6))
686
                                                                    (or (not (= top.KP_61 false))
687
                                                                    (and 
688
                                                                    (or (not (= top.KP_71 true))
689
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 7))
690
                                                                    (or (not (= top.KP_71 false))
691
                                                                    (and 
692
                                                                    (or (not (= top.KP_81 true))
693
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 8))
694
                                                                    (or (not (= top.KP_81 false))
695
                                                                    (and 
696
                                                                    (or (not (= top.KP_91 true))
697
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 9))
698
                                                                    (or (not (= top.KP_91 false))
699
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 10))
700
                                                                    ))
701
                                                                    ))
702
                                                                    ))
703
                                                                    ))
704
                                                                    ))
705
                                                                    ))
706
                                                                    ))
707
                                                                    ))
708
                                                                 ))
709
                                                         ))
710
                                                      (or (not (= top.__top_12 false))
711
                                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
712
                                                 ))
713
                                         )
714
                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY 0)
715
                                         (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY 0)
716
                                         ))
717
                            ))
718
                    )
719
                    (= top.START_PRESSED (and top.KP_START (not top.__top_74_c)))
720
                    ))
721
            (or (not (= top.__top_1 true))
722
               (and (and (or (not (= top.KP_CLEAR true))
723
                            (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
724
                         (or (not (= top.KP_CLEAR false))
725
                            (and (or (not (= top.__top_12 true))
726
                                    (and (or (not (= top.KP_01 true))
727
                                            (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
728
                                         (or (not (= top.KP_01 false))
729
                                            (and (or (not (= top.KP_11 true))
730
                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 1))
731
                                                 (or (not (= top.KP_11 false))
732
                                                    (and (or (not (= top.KP_21 true))
733
                                                            (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 2))
734
                                                         (or (not (= top.KP_21 false))
735
                                                            (and (or (not (= top.KP_31 true))
736
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 3))
737
                                                                 (or (not (= top.KP_31 false))
738
                                                                    (and 
739
                                                                    (or (not (= top.KP_41 true))
740
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 4))
741
                                                                    (or (not (= top.KP_41 false))
742
                                                                    (and 
743
                                                                    (or (not (= top.KP_51 true))
744
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 5))
745
                                                                    (or (not (= top.KP_51 false))
746
                                                                    (and 
747
                                                                    (or (not (= top.KP_61 true))
748
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 6))
749
                                                                    (or (not (= top.KP_61 false))
750
                                                                    (and 
751
                                                                    (or (not (= top.KP_71 true))
752
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 7))
753
                                                                    (or (not (= top.KP_71 false))
754
                                                                    (and 
755
                                                                    (or (not (= top.KP_81 true))
756
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 8))
757
                                                                    (or (not (= top.KP_81 false))
758
                                                                    (and 
759
                                                                    (or (not (= top.KP_91 true))
760
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 9))
761
                                                                    (or (not (= top.KP_91 false))
762
                                                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 10))
763
                                                                    ))
764
                                                                    ))
765
                                                                    ))
766
                                                                    ))
767
                                                                    ))
768
                                                                    ))
769
                                                            ))
770
                                                    ))
771
                                            ))
772
                                    ))
773
                                 (or (not (= top.__top_12 false))
774
                                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 0))
775
                            ))
776
                    )
777
                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY 0)
778
                    (= top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY 0)
779
                    (= top.START_PRESSED top.KP_START)
780
                    ))
781
       )
782
       (= top.__top_73 (= top.START_PRESSED false))
783
       (and (or (not (= top.__top_73 true))
784
               (= top.chart_microwave_mode_logic_start 0))
785
            (or (not (= top.__top_73 false))
786
               (= top.chart_microwave_mode_logic_start 1))
787
       )
788
       (= top.__top_8 (and top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step (not top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)))
789
       (and (or (not (= top.__top_1 true))
790
               (and (or (not (= top.__top_8 true))
791
                       (= top.STEPS_TO_COOK 0))
792
                    (or (not (= top.__top_8 false))
793
                       (= top.STEPS_TO_COOK (* (+ (+ (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 1) (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY 10)) (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY 60)) 1)))
794
               ))
795
            (or (not (= top.__top_1 false))
796
               (and (or (not (= top.__top_8 true))
797
                       (= top.STEPS_TO_COOK 0))
798
                    (or (not (= top.__top_8 false))
799
                       (and (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock true))
800
                               (= top.STEPS_TO_COOK (* (+ (+ (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY 1) (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY 10)) (* top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY 60)) 1)))
801
                            (or (not (= top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock false))
802
                               (= top.STEPS_TO_COOK top.__top_9_c))
803
                       ))
804
               ))
805
       )
806
       (= top.__top_60 (= (> top.STEPS_TO_COOK 0) false))
807
       (and (or (not (= top.__top_60 true))
808
               (= top.__top_61 0))
809
            (or (not (= top.__top_60 false))
810
               (= top.__top_61 1))
811
       )
812
       (= top.__top_62 (not (= top.__top_61 0)))
813
       (and (or (not (= top.__top_62 true))
814
               (= top.__top_63 true))
815
            (or (not (= top.__top_62 false))
816
               (= top.__top_63 false))
817
       )
818
       (= top.__top_56 (not (= top.chart_microwave_mode_logic_start 0)))
819
       (and (or (not (= top.__top_56 true))
820
               (= top.__top_57 true))
821
            (or (not (= top.__top_56 false))
822
               (= top.__top_57 false))
823
       )
824
       (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 (and top.rlt_eval_microwave_mode_logic_rlt_fired_0 (and (= top.chart_microwave_mode_logic_begin_state_states___root 4) (and top.__top_57 top.__top_63))))
825
       (= top.__top_59 (= top.chart_microwave_mode_logic_begin_state_states___root 4))
826
       (and (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 true))
827
               (and (or (not (= top.__top_59 true))
828
                       (= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root 0))
829
                    (or (not (= top.__top_59 false))
830
                       (= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root top.chart_microwave_mode_logic_begin_state_states___root))
831
               ))
832
            (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 false))
833
               (= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root top.chart_microwave_mode_logic_begin_state_states___root))
834
       )
835
       (= top.__top_45 (not (and (>= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root 1) (<= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root 3))))
836
       (and (or (not (= top.__top_45 true))
837
               (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 1))
838
            (or (not (= top.__top_45 false))
839
               (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root))
840
       )
841
       (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_0 (and (not (and (>= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root 1) (<= top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root 3))) (and (>= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 1) (<= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 3))))
842
       (= top.__top_71 (= top.DOOR_CLOSED false))
843
       (and (or (not (= top.__top_71 true))
844
               (= top.chart_microwave_mode_logic_door_closed 0))
845
            (or (not (= top.__top_71 false))
846
               (= top.chart_microwave_mode_logic_door_closed 1))
847
       )
848
       (= top.__top_43 (not (= top.chart_microwave_mode_logic_door_closed 0)))
849
       (and (or (not (= top.__top_43 true))
850
               (= top.__top_44 true))
851
            (or (not (= top.__top_43 false))
852
               (= top.__top_44 false))
853
       )
854
       (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 (and top.rlt_enter_microwave_mode_logic_ON_rlt_fired_0 (and (and (>= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 1) (<= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 3)) top.__top_44)))
855
       (= top.__top_42 (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root 2)))
856
       (and (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 true))
857
               (and (or (not (= top.__top_42 true))
858
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root 2))
859
                    (or (not (= top.__top_42 false))
860
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root))
861
               ))
862
            (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 false))
863
               (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root top.rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root))
864
       )
865
       (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 (and top.rlt_enter_microwave_mode_logic_ON_rlt_fired_0 (and (and (>= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root 1) (<= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root 3)) (not top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1))))
866
       (= top.__top_41 (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root 3)))
867
       (and (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 true))
868
               (and (or (not (= top.__top_41 true))
869
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root 3))
870
                    (or (not (= top.__top_41 false))
871
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root))
872
               ))
873
            (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 false))
874
               (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root))
875
       )
876
       (and (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 true))
877
               (= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root top.rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root))
878
            (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 false))
879
               (= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root top.rlt_eval_microwave_mode_logic_rlt_state_2_states___root))
880
       )
881
       (and (or (not (= top.__top_1 true))
882
               (= top.chart_microwave_mode_logic_begin_state_outports_mode 0))
883
            (or (not (= top.__top_1 false))
884
               (= top.chart_microwave_mode_logic_begin_state_outports_mode top.__top_67_c))
885
       )
886
       (and (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 true))
887
               (and (or (not (= top.__top_42 true))
888
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode 2))
889
                    (or (not (= top.__top_42 false))
890
                       (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode top.chart_microwave_mode_logic_begin_state_outports_mode))
891
               ))
892
            (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_1 false))
893
               (= top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode top.chart_microwave_mode_logic_begin_state_outports_mode))
894
       )
895
       (and (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 true))
896
               (and (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 true))
897
                       (and (or (not (= top.__top_41 true))
898
                               (= top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode 3))
899
                            (or (not (= top.__top_41 false))
900
                               (= top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode))
901
                       ))
902
                    (or (not (= top.rlt_enter_microwave_mode_logic_ON_rlt_fired_2 false))
903
                       (= top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode top.rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode))
904
               ))
905
            (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_1 false))
906
               (= top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode top.chart_microwave_mode_logic_begin_state_outports_mode))
907
       )
908
       (and (or (not (= top.__top_1 true))
909
               (= top.chart_microwave_mode_logic_begin_state_outports_steps_remaining 0))
910
            (or (not (= top.__top_1 false))
911
               (= top.chart_microwave_mode_logic_begin_state_outports_steps_remaining top.__top_66_c))
912
       )
913
       (and (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_0 true))
914
               (= top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining top.STEPS_TO_COOK))
915
            (or (not (= top.rlt_eval_microwave_mode_logic_rlt_fired_0 false))
916
               (= top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining top.chart_microwave_mode_logic_begin_state_outports_steps_remaining))
917
       )
918
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 (and (and (= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 2) (<= top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining 0)) (= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 2)))
919
       (= top.__top_58 (and (>= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 1) (<= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 3)))
920
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 true))
921
               (and (or (not (= top.__top_58 true))
922
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root 0))
923
                    (or (not (= top.__top_58 false))
924
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root))
925
               ))
926
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 false))
927
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root))
928
       )
929
       (= top.__top_54 (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root 4)))
930
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 true))
931
               (and (or (not (= top.__top_54 true))
932
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root 4))
933
                    (or (not (= top.__top_54 false))
934
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root))
935
               ))
936
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 false))
937
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root))
938
       )
939
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root 3) (and (and top.__top_57 top.__top_44) (not top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1))))
940
       (= top.__top_55 (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root 3))
941
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 true))
942
               (and (or (not (= top.__top_55 true))
943
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root 1))
944
                    (or (not (= top.__top_55 false))
945
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root))
946
               ))
947
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 false))
948
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root))
949
       )
950
       (= top.__top_53 (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root 2)))
951
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 true))
952
               (and (or (not (= top.__top_53 true))
953
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root 2))
954
                    (or (not (= top.__top_53 false))
955
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root))
956
               ))
957
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 false))
958
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root))
959
       )
960
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_complete_1 (or top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1))
961
       (and (or (not (= top.__top_1 true))
962
               (= top.CLEAR_PRESSED top.KP_CLEAR))
963
            (or (not (= top.__top_1 false))
964
               (= top.CLEAR_PRESSED (and top.KP_CLEAR (not top.__top_92_c))))
965
       )
966
       (= top.__top_72 (= top.CLEAR_PRESSED false))
967
       (and (or (not (= top.__top_72 true))
968
               (= top.chart_microwave_mode_logic_clear_off 0))
969
            (or (not (= top.__top_72 false))
970
               (= top.chart_microwave_mode_logic_clear_off 1))
971
       )
972
       (= top.__top_48 (not (= top.chart_microwave_mode_logic_clear_off 0)))
973
       (and (or (not (= top.__top_48 true))
974
               (= top.__top_49 true))
975
            (or (not (= top.__top_48 false))
976
               (= top.__top_49 false))
977
       )
978
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 (and (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root 3) (and top.__top_49 (not top.rlt_eval_microwave_mode_logic_ON_rlt_complete_1))) (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root 3) (not top.rlt_eval_microwave_mode_logic_ON_rlt_complete_1))))
979
       (= top.__top_52 (and (>= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root 1) (<= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root 3)))
980
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 true))
981
               (and (or (not (= top.__top_52 true))
982
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root 0))
983
                    (or (not (= top.__top_52 false))
984
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root))
985
               ))
986
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 false))
987
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root))
988
       )
989
       (= top.__top_51 (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root 4)))
990
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 false))
991
               (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root)
992
                    (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining)
993
                    ))
994
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 true))
995
               (and (and (or (not (= top.__top_51 true))
996
                            (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root 4))
997
                         (or (not (= top.__top_51 false))
998
                            (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root))
999
                    )
1000
                    (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining 0)
1001
                    ))
1002
       )
1003
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_complete_2 (or top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 top.rlt_eval_microwave_mode_logic_ON_rlt_complete_1))
1004
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root 2) (and (> top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining 0) (not top.rlt_eval_microwave_mode_logic_ON_rlt_complete_2))))
1005
       (= top.__top_50 (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root 2))
1006
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 true))
1007
               (and (or (not (= top.__top_50 true))
1008
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root 1))
1009
                    (or (not (= top.__top_50 false))
1010
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root))
1011
               ))
1012
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 false))
1013
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root))
1014
       )
1015
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 true))
1016
               (and (or (not (= top.__top_54 true))
1017
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode 1))
1018
                    (or (not (= top.__top_54 false))
1019
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))
1020
               ))
1021
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_1 false))
1022
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))
1023
       )
1024
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 true))
1025
               (and (or (not (= top.__top_53 true))
1026
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode 2))
1027
                    (or (not (= top.__top_53 false))
1028
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode))
1029
               ))
1030
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_2 false))
1031
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode))
1032
       )
1033
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 true))
1034
               (and (or (not (= top.__top_51 true))
1035
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode 1))
1036
                    (or (not (= top.__top_51 false))
1037
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode))
1038
               ))
1039
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_4 false))
1040
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode))
1041
       )
1042
       (= top.__top_46 (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root 2)))
1043
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 true))
1044
               (and (or (not (= top.__top_46 true))
1045
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root 2))
1046
                    (or (not (= top.__top_46 false))
1047
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root))
1048
               ))
1049
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 false))
1050
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root))
1051
       )
1052
       (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 (and (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root 2) (and (or top.__top_49 (not top.__top_44)) (not (or top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 top.rlt_eval_microwave_mode_logic_ON_rlt_complete_2)))))
1053
       (= top.__top_47 (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root 2))
1054
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 true))
1055
               (and (or (not (= top.__top_47 true))
1056
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root 1))
1057
                    (or (not (= top.__top_47 false))
1058
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root))
1059
               ))
1060
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 false))
1061
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root))
1062
       )
1063
       (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 true))
1064
               (and (or (not (= top.__top_46 true))
1065
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode 2))
1066
                    (or (not (= top.__top_46 false))
1067
                       (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode))
1068
               ))
1069
            (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 false))
1070
               (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode))
1071
       )
1072
       (= top.__top_40 (not (= top.chart_microwave_mode_logic_begin_state_states___root 4)))
1073
       (and (or (not (= top.__top_40 true))
1074
               (= top.rlt_enter_microwave_mode_logic_rlt_state_2_states___root 4))
1075
            (or (not (= top.__top_40 false))
1076
               (= top.rlt_enter_microwave_mode_logic_rlt_state_2_states___root top.chart_microwave_mode_logic_begin_state_states___root))
1077
       )
1078
       (and (or (not (= top.__top_1 true))
1079
               (= top.chart_microwave_mode_logic_rlt_evtInitStep true))
1080
            (or (not (= top.__top_1 false))
1081
               (and (or (not (= top.__top_69_c true))
1082
                       (= top.chart_microwave_mode_logic_rlt_evtInitStep false))
1083
                    (or (not (= top.__top_69_c false))
1084
                       (= top.chart_microwave_mode_logic_rlt_evtInitStep top.__top_70_c))
1085
               ))
1086
       )
1087
       (= top.chart_microwave_mode_logic____wakeup___ true)
1088
       (= top.__top_65 (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root 3)))
1089
       (= top.__top_64 (and (not top.rlt_eval_microwave_mode_logic_rlt_fired_1) (and (>= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 1) (<= top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root 3))))
1090
       (and (or (not (= top.chart_microwave_mode_logic____wakeup___ true))
1091
               (and (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep true))
1092
                       (and (or (not (= top.__top_40 true))
1093
                               (= top.chart_microwave_mode_logic_mode 1))
1094
                            (or (not (= top.__top_40 false))
1095
                               (= top.chart_microwave_mode_logic_mode top.chart_microwave_mode_logic_begin_state_outports_mode))
1096
                       ))
1097
                    (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep false))
1098
                       (and (or (not (= top.__top_64 true))
1099
                               (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 true))
1100
                                       (and (or (not (= top.__top_65 true))
1101
                                               (= top.chart_microwave_mode_logic_mode 3))
1102
                                            (or (not (= top.__top_65 false))
1103
                                               (= top.chart_microwave_mode_logic_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode))
1104
                                       ))
1105
                                    (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 false))
1106
                                       (= top.chart_microwave_mode_logic_mode top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode))
1107
                               ))
1108
                            (or (not (= top.__top_64 false))
1109
                               (= top.chart_microwave_mode_logic_mode top.rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode))
1110
                       ))
1111
               ))
1112
            (or (not (= top.chart_microwave_mode_logic____wakeup___ false))
1113
               (= top.chart_microwave_mode_logic_mode top.chart_microwave_mode_logic_begin_state_outports_mode))
1114
       )
1115
       (= top.microwave_microwave_mode_logic_mode top.chart_microwave_mode_logic_mode)
1116
       (= top.__top_4 (= 1 top.microwave_microwave_mode_logic_mode))
1117
       (= top.MWI_FcnMaxI_In13 (- top.__top_39_c 1))
1118
       (= top.__top_105 (> top.MWI_FcnMaxI_In13 0))
1119
       (and (or (not (= top.__top_4 true))
1120
               (= top.SETUP true))
1121
            (or (not (= top.__top_4 false))
1122
               (= top.SETUP false))
1123
       )
1124
       (= top.__top_104 (not (not top.SETUP)))
1125
       (and (or (not (= top.__top_1 true))
1126
               (= top.rlt__Arrow5 639))
1127
            (or (not (= top.__top_1 false))
1128
               (and (or (not (= top.__top_104 true))
1129
                       (and (or (not (= top.__top_105 true))
1130
                               (= top.rlt__Arrow5 top.MWI_FcnMaxI_In13))
1131
                            (or (not (= top.__top_105 false))
1132
                               (= top.rlt__Arrow5 0))
1133
                       ))
1134
                    (or (not (= top.__top_104 false))
1135
                       (= top.rlt__Arrow5 639))
1136
               ))
1137
       )
1138
       (= top.__top_91 (= 3 top.microwave_microwave_mode_logic_mode))
1139
       (= top.MWI_FcnMaxI_In12 (- top.__top_76_c 1))
1140
       (= top.__top_103 (> top.MWI_FcnMaxI_In12 0))
1141
       (and (or (not (= top.__top_91 true))
1142
               (= top.SUSPENDED true))
1143
            (or (not (= top.__top_91 false))
1144
               (= top.SUSPENDED false))
1145
       )
1146
       (= top.__top_102 (not top.SUSPENDED))
1147
       (and (or (not (= top.__top_1 true))
1148
               (= top.rlt__Arrow4 639))
1149
            (or (not (= top.__top_1 false))
1150
               (and (or (not (= top.__top_102 true))
1151
                       (and (or (not (= top.__top_103 true))
1152
                               (= top.rlt__Arrow4 top.MWI_FcnMaxI_In12))
1153
                            (or (not (= top.__top_103 false))
1154
                               (= top.rlt__Arrow4 0))
1155
                       ))
1156
                    (or (not (= top.__top_102 false))
1157
                       (= top.rlt__Arrow4 639))
1158
               ))
1159
       )
1160
       (= top.__top_75 (= 2 top.microwave_microwave_mode_logic_mode))
1161
       (= top.MWI_FcnMaxI_In16 (- top.__top_77_c 1))
1162
       (= top.__top_101 (> top.MWI_FcnMaxI_In16 0))
1163
       (and (or (not (= top.__top_75 true))
1164
               (= top.COOKING true))
1165
            (or (not (= top.__top_75 false))
1166
               (= top.COOKING false))
1167
       )
1168
       (= top.__top_100 (not (not top.COOKING)))
1169
       (and (or (not (= top.__top_1 true))
1170
               (= top.rlt__Arrow3 639))
1171
            (or (not (= top.__top_1 false))
1172
               (and (or (not (= top.__top_100 true))
1173
                       (and (or (not (= top.__top_101 true))
1174
                               (= top.rlt__Arrow3 top.MWI_FcnMaxI_In16))
1175
                            (or (not (= top.__top_101 false))
1176
                               (= top.rlt__Arrow3 0))
1177
                       ))
1178
                    (or (not (= top.__top_100 false))
1179
                       (= top.rlt__Arrow3 639))
1180
               ))
1181
       )
1182
       (= top.MWI_FcnMaxI_In15 (- top.__top_78_c 1))
1183
       (= top.__top_99 (> top.MWI_FcnMaxI_In15 0))
1184
       (= top.__top_98 (not (not top.SUSPENDED)))
1185
       (and (or (not (= top.__top_1 true))
1186
               (= top.rlt__Arrow2 639))
1187
            (or (not (= top.__top_1 false))
1188
               (and (or (not (= top.__top_98 true))
1189
                       (and (or (not (= top.__top_99 true))
1190
                               (= top.rlt__Arrow2 top.MWI_FcnMaxI_In15))
1191
                            (or (not (= top.__top_99 false))
1192
                               (= top.rlt__Arrow2 0))
1193
                       ))
1194
                    (or (not (= top.__top_98 false))
1195
                       (= top.rlt__Arrow2 639))
1196
               ))
1197
       )
1198
       (= top.MWI_FcnMaxI_In11 (- top.__top_79_c 1))
1199
       (= top.__top_97 (> top.MWI_FcnMaxI_In11 0))
1200
       (= top.__top_96 (not top.COOKING))
1201
       (and (or (not (= top.__top_1 true))
1202
               (= top.rlt__Arrow1 639))
1203
            (or (not (= top.__top_1 false))
1204
               (and (or (not (= top.__top_96 true))
1205
                       (and (or (not (= top.__top_97 true))
1206
                               (= top.rlt__Arrow1 top.MWI_FcnMaxI_In11))
1207
                            (or (not (= top.__top_97 false))
1208
                               (= top.rlt__Arrow1 0))
1209
                       ))
1210
                    (or (not (= top.__top_96 false))
1211
                       (= top.rlt__Arrow1 639))
1212
               ))
1213
       )
1214
       (= top.MWI_FcnMaxI_In1 (- top.__top_93_c 1))
1215
       (= top.__top_95 (> top.MWI_FcnMaxI_In1 0))
1216
       (= top.__top_94 (not top.SETUP))
1217
       (and (or (not (= top.__top_1 true))
1218
               (= top.rlt__Arrow 639))
1219
            (or (not (= top.__top_1 false))
1220
               (and (or (not (= top.__top_94 true))
1221
                       (and (or (not (= top.__top_95 true))
1222
                               (= top.rlt__Arrow top.MWI_FcnMaxI_In1))
1223
                            (or (not (= top.__top_95 false))
1224
                               (= top.rlt__Arrow 0))
1225
                       ))
1226
                    (or (not (= top.__top_94 false))
1227
                       (= top.rlt__Arrow 639))
1228
               ))
1229
       )
1230
       (and (or (not (= top.chart_microwave_mode_logic____wakeup___ true))
1231
               (and (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep true))
1232
                       (= top.chart_microwave_mode_logic_steps_remaining top.chart_microwave_mode_logic_begin_state_outports_steps_remaining))
1233
                    (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep false))
1234
                       (and (or (not (= top.__top_64 true))
1235
                               (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 true))
1236
                                       (= top.chart_microwave_mode_logic_steps_remaining (- top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining 1)))
1237
                                    (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_5 false))
1238
                                       (= top.chart_microwave_mode_logic_steps_remaining top.rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining))
1239
                               ))
1240
                            (or (not (= top.__top_64 false))
1241
                               (= top.chart_microwave_mode_logic_steps_remaining top.rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining))
1242
                       ))
1243
               ))
1244
            (or (not (= top.chart_microwave_mode_logic____wakeup___ false))
1245
               (= top.chart_microwave_mode_logic_steps_remaining top.chart_microwave_mode_logic_begin_state_outports_steps_remaining))
1246
       )
1247
       (= top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER (- (- (div top.chart_microwave_mode_logic_steps_remaining 1) (* (div (div top.chart_microwave_mode_logic_steps_remaining 1) 60) 60)) (* (div (- (div top.chart_microwave_mode_logic_steps_remaining 1) (* (div (div top.chart_microwave_mode_logic_steps_remaining 1) 60) 60)) 10) 10)))
1248
       (= top.RIGHT_DIGIT top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__REMAINDER)
1249
       (and (or (not (= top.__top_1 true))
1250
               (= top.p37 true))
1251
            (or (not (= top.__top_1 false))
1252
               (= top.p37 (or (not (and top.enable (not top.KP_CLEAR))) (or (or (or (or (or (or (or (or (or (or (and top.KP_1 (not top.__top_90_c)) (and top.KP_2 (not top.__top_89_c))) (and top.KP_3 (not top.__top_88_c))) (and top.KP_4 (not top.__top_87_c))) (and top.KP_5 (not top.__top_86_c))) (and top.KP_6 (not top.__top_85_c))) (and top.KP_7 (not top.__top_84_c))) (and top.KP_8 (not top.__top_83_c))) (and top.KP_9 (not top.__top_82_c))) (and top.KP_0 (not top.__top_81_c))) (= top.RIGHT_DIGIT top.__top_80_c)))))
1253
       )
1254
       (= top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT (div (- (div top.chart_microwave_mode_logic_steps_remaining 1) (* (div (div top.chart_microwave_mode_logic_steps_remaining 1) 60) 60)) 10))
1255
       (= top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT (div (div top.chart_microwave_mode_logic_steps_remaining 1) 60))
1256
       (and (or (not (= top.chart_microwave_mode_logic____wakeup___ true))
1257
               (and (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep true))
1258
                       (= top.chart_microwave_mode_logic_final_state_states___root top.rlt_enter_microwave_mode_logic_rlt_state_2_states___root))
1259
                    (or (not (= top.chart_microwave_mode_logic_rlt_evtInitStep false))
1260
                       (and (or (not (= top.__top_64 true))
1261
                               (and (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 true))
1262
                                       (and (or (not (= top.__top_65 true))
1263
                                               (= top.chart_microwave_mode_logic_final_state_states___root 3))
1264
                                            (or (not (= top.__top_65 false))
1265
                                               (= top.chart_microwave_mode_logic_final_state_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root))
1266
                                       ))
1267
                                    (or (not (= top.rlt_eval_microwave_mode_logic_ON_rlt_fired_6 false))
1268
                                       (= top.chart_microwave_mode_logic_final_state_states___root top.rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root))
1269
                               ))
1270
                            (or (not (= top.__top_64 false))
1271
                               (= top.chart_microwave_mode_logic_final_state_states___root top.rlt_eval_microwave_mode_logic_rlt_state_3_states___root))
1272
                       ))
1273
               ))
1274
            (or (not (= top.chart_microwave_mode_logic____wakeup___ false))
1275
               (= top.chart_microwave_mode_logic_final_state_states___root top.chart_microwave_mode_logic_begin_state_states___root))
1276
       )
1277
       (= top.__top_93_x top.rlt__Arrow)
1278
       (= top.__top_92_x top.KP_CLEAR)
1279
       (and (or (not (= top.__top_1 true))
1280
               (= top.OK true))
1281
            (or (not (= top.__top_1 false))
1282
               (= top.OK (or (not (and top.enable (not top.KP_CLEAR))) (or (not (and (and top.KP_9 (not top.__top_82_c)) (and (not (and top.KP_8 (not top.__top_83_c))) (and (not (and top.KP_7 (not top.__top_84_c))) (and (not (and top.KP_6 (not top.__top_85_c))) (and (not (and top.KP_5 (not top.__top_86_c))) (and (not (and top.KP_4 (not top.__top_87_c))) (and (not (and top.KP_3 (not top.__top_88_c))) (and (not (and top.KP_2 (not top.__top_89_c))) (and (not (and top.KP_1 (not top.__top_90_c))) (not (and top.KP_0 (not top.__top_81_c))))))))))))) (= top.RIGHT_DIGIT 9)))))
1283
       )
1284
       (= top.__top_90_x top.KP_1)
1285
       (= top.__top_9_x top.STEPS_TO_COOK)
1286
       (= top.__top_89_x top.KP_2)
1287
       (= top.__top_88_x top.KP_3)
1288
       (= top.__top_87_x top.KP_4)
1289
       (= top.__top_86_x top.KP_5)
1290
       (= top.__top_85_x top.KP_6)
1291
       (= top.__top_84_x top.KP_7)
1292
       (= top.__top_83_x top.KP_8)
1293
       (= top.__top_82_x top.KP_9)
1294
       (= top.__top_81_x top.KP_0)
1295
       (= top.__top_80_x top.RIGHT_DIGIT)
1296
       (= top.__top_79_x top.rlt__Arrow1)
1297
       (= top.__top_78_x top.rlt__Arrow2)
1298
       (= top.__top_77_x top.rlt__Arrow3)
1299
       (= top.__top_76_x top.rlt__Arrow4)
1300
       (= top.__top_74_x top.KP_START)
1301
       (= top.__top_70_x top.chart_microwave_mode_logic_rlt_evtInitStep)
1302
       (= top.__top_7_x top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step)
1303
       (= top.__top_69_x top.chart_microwave_mode_logic____wakeup___)
1304
       (= top.__top_68_x top.chart_microwave_mode_logic_final_state_states___root)
1305
       (= top.__top_67_x top.chart_microwave_mode_logic_mode)
1306
       (= top.__top_66_x top.chart_microwave_mode_logic_steps_remaining)
1307
       (= top.__top_6_x top.rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock)
1308
       (= top.__top_39_x top.rlt__Arrow5)
1309
       (= top.__top_38_x top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY)
1310
       (= top.__top_37_x top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY)
1311
       (= top.__top_36_x top.microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY)
1312
       (= top.__top_31_x top.KP_91)
1313
       (= top.__top_29_x top.KP_81)
1314
       (= top.__top_27_x top.KP_71)
1315
       (= top.__top_25_x top.KP_61)
1316
       (= top.__top_23_x top.KP_51)
1317
       (= top.__top_21_x top.KP_41)
1318
       (= top.__top_2_x top.microwave_microwave_mode_logic_mode)
1319
       (= top.__top_19_x top.KP_31)
1320
       (= top.__top_17_x top.KP_21)
1321
       (= top.__top_15_x top.KP_11)
1322
       (= top.__top_13_x top.KP_01)
1323
       (= top.MIDDLE_DIGIT top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_TENS__QUOTIENT)
1324
       (= top.LEFT_DIGIT top.microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT)
1325
       )
1326
  (top_step top.KP_START
1327
            top.KP_CLEAR
1328
            top.KP_0
1329
            top.KP_1
1330
            top.KP_2
1331
            top.KP_3
1332
            top.KP_4
1333
            top.KP_5
1334
            top.KP_6
1335
            top.KP_7
1336
            top.KP_8
1337
            top.KP_9
1338
            top.DOOR_CLOSED
1339
            top.OK
1340
            top.__top_13_c
1341
            top.__top_15_c
1342
            top.__top_17_c
1343
            top.__top_19_c
1344
            top.__top_2_c
1345
            top.__top_21_c
1346
            top.__top_23_c
1347
            top.__top_25_c
1348
            top.__top_27_c
1349
            top.__top_29_c
1350
            top.__top_31_c
1351
            top.__top_36_c
1352
            top.__top_37_c
1353
            top.__top_38_c
1354
            top.__top_39_c
1355
            top.__top_6_c
1356
            top.__top_66_c
1357
            top.__top_67_c
1358
            top.__top_68_c
1359
            top.__top_69_c
1360
            top.__top_7_c
1361
            top.__top_70_c
1362
            top.__top_74_c
1363
            top.__top_76_c
1364
            top.__top_77_c
1365
            top.__top_78_c
1366
            top.__top_79_c
1367
            top.__top_80_c
1368
            top.__top_81_c
1369
            top.__top_82_c
1370
            top.__top_83_c
1371
            top.__top_84_c
1372
            top.__top_85_c
1373
            top.__top_86_c
1374
            top.__top_87_c
1375
            top.__top_88_c
1376
            top.__top_89_c
1377
            top.__top_9_c
1378
            top.__top_90_c
1379
            top.__top_92_c
1380
            top.__top_93_c
1381
            top.ni_0._arrow._first_c
1382
            top.__top_13_x
1383
            top.__top_15_x
1384
            top.__top_17_x
1385
            top.__top_19_x
1386
            top.__top_2_x
1387
            top.__top_21_x
1388
            top.__top_23_x
1389
            top.__top_25_x
1390
            top.__top_27_x
1391
            top.__top_29_x
1392
            top.__top_31_x
1393
            top.__top_36_x
1394
            top.__top_37_x
1395
            top.__top_38_x
1396
            top.__top_39_x
1397
            top.__top_6_x
1398
            top.__top_66_x
1399
            top.__top_67_x
1400
            top.__top_68_x
1401
            top.__top_69_x
1402
            top.__top_7_x
1403
            top.__top_70_x
1404
            top.__top_74_x
1405
            top.__top_76_x
1406
            top.__top_77_x
1407
            top.__top_78_x
1408
            top.__top_79_x
1409
            top.__top_80_x
1410
            top.__top_81_x
1411
            top.__top_82_x
1412
            top.__top_83_x
1413
            top.__top_84_x
1414
            top.__top_85_x
1415
            top.__top_86_x
1416
            top.__top_87_x
1417
            top.__top_88_x
1418
            top.__top_89_x
1419
            top.__top_9_x
1420
            top.__top_90_x
1421
            top.__top_92_x
1422
            top.__top_93_x
1423
            top.ni_0._arrow._first_x)
1424
))
1425

    
1426
; Collecting semantics for node top
1427

    
1428
(declare-rel MAIN (Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Int Int Int Int Bool Int Int Int Bool Bool Bool Bool Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Int Bool Bool))
1429
; Initial set: Reset(c,m) + One Step(m,x) 
1430
(declare-rel INIT_STATE ())
1431
(rule INIT_STATE)
1432
(rule (=> 
1433
  (and INIT_STATE
1434
       (top_reset top.__top_13_c top.__top_15_c top.__top_17_c top.__top_19_c top.__top_2_c top.__top_21_c top.__top_23_c top.__top_25_c top.__top_27_c top.__top_29_c top.__top_31_c top.__top_36_c top.__top_37_c top.__top_38_c top.__top_39_c top.__top_6_c top.__top_66_c top.__top_67_c top.__top_68_c top.__top_69_c top.__top_7_c top.__top_70_c top.__top_74_c top.__top_76_c top.__top_77_c top.__top_78_c top.__top_79_c top.__top_80_c top.__top_81_c top.__top_82_c top.__top_83_c top.__top_84_c top.__top_85_c top.__top_86_c top.__top_87_c top.__top_88_c top.__top_89_c top.__top_9_c top.__top_90_c top.__top_92_c top.__top_93_c top.ni_0._arrow._first_c top.__top_13_m top.__top_15_m top.__top_17_m top.__top_19_m top.__top_2_m top.__top_21_m top.__top_23_m top.__top_25_m top.__top_27_m top.__top_29_m top.__top_31_m top.__top_36_m top.__top_37_m top.__top_38_m top.__top_39_m top.__top_6_m top.__top_66_m top.__top_67_m top.__top_68_m top.__top_69_m top.__top_7_m top.__top_70_m top.__top_74_m top.__top_76_m top.__top_77_m top.__top_78_m top.__top_79_m top.__top_80_m top.__top_81_m top.__top_82_m top.__top_83_m top.__top_84_m top.__top_85_m top.__top_86_m top.__top_87_m top.__top_88_m top.__top_89_m top.__top_9_m top.__top_90_m top.__top_92_m top.__top_93_m top.ni_0._arrow._first_m)
1435
       (top_step top.KP_START top.KP_CLEAR top.KP_0 top.KP_1 top.KP_2 top.KP_3 top.KP_4 top.KP_5 top.KP_6 top.KP_7 top.KP_8 top.KP_9 top.DOOR_CLOSED top.OK top.__top_13_m top.__top_15_m top.__top_17_m top.__top_19_m top.__top_2_m top.__top_21_m top.__top_23_m top.__top_25_m top.__top_27_m top.__top_29_m top.__top_31_m top.__top_36_m top.__top_37_m top.__top_38_m top.__top_39_m top.__top_6_m top.__top_66_m top.__top_67_m top.__top_68_m top.__top_69_m top.__top_7_m top.__top_70_m top.__top_74_m top.__top_76_m top.__top_77_m top.__top_78_m top.__top_79_m top.__top_80_m top.__top_81_m top.__top_82_m top.__top_83_m top.__top_84_m top.__top_85_m top.__top_86_m top.__top_87_m top.__top_88_m top.__top_89_m top.__top_9_m top.__top_90_m top.__top_92_m top.__top_93_m top.ni_0._arrow._first_m top.__top_13_x top.__top_15_x top.__top_17_x top.__top_19_x top.__top_2_x top.__top_21_x top.__top_23_x top.__top_25_x top.__top_27_x top.__top_29_x top.__top_31_x top.__top_36_x top.__top_37_x top.__top_38_x top.__top_39_x top.__top_6_x top.__top_66_x top.__top_67_x top.__top_68_x top.__top_69_x top.__top_7_x top.__top_70_x top.__top_74_x top.__top_76_x top.__top_77_x top.__top_78_x top.__top_79_x top.__top_80_x top.__top_81_x top.__top_82_x top.__top_83_x top.__top_84_x top.__top_85_x top.__top_86_x top.__top_87_x top.__top_88_x top.__top_89_x top.__top_9_x top.__top_90_x top.__top_92_x top.__top_93_x top.ni_0._arrow._first_x)
1436
  )
1437
  (MAIN top.__top_13_x top.__top_15_x top.__top_17_x top.__top_19_x top.__top_2_x top.__top_21_x top.__top_23_x top.__top_25_x top.__top_27_x top.__top_29_x top.__top_31_x top.__top_36_x top.__top_37_x top.__top_38_x top.__top_39_x top.__top_6_x top.__top_66_x top.__top_67_x top.__top_68_x top.__top_69_x top.__top_7_x top.__top_70_x top.__top_74_x top.__top_76_x top.__top_77_x top.__top_78_x top.__top_79_x top.__top_80_x top.__top_81_x top.__top_82_x top.__top_83_x top.__top_84_x top.__top_85_x top.__top_86_x top.__top_87_x top.__top_88_x top.__top_89_x top.__top_9_x top.__top_90_x top.__top_92_x top.__top_93_x top.ni_0._arrow._first_x top.OK)
1438
))
1439

    
1440
; Inductive def
1441
(declare-var dummytop.OK Bool)
1442
(rule (=> 
1443
  (and (MAIN top.__top_13_c top.__top_15_c top.__top_17_c top.__top_19_c top.__top_2_c top.__top_21_c top.__top_23_c top.__top_25_c top.__top_27_c top.__top_29_c top.__top_31_c top.__top_36_c top.__top_37_c top.__top_38_c top.__top_39_c top.__top_6_c top.__top_66_c top.__top_67_c top.__top_68_c top.__top_69_c top.__top_7_c top.__top_70_c top.__top_74_c top.__top_76_c top.__top_77_c top.__top_78_c top.__top_79_c top.__top_80_c top.__top_81_c top.__top_82_c top.__top_83_c top.__top_84_c top.__top_85_c top.__top_86_c top.__top_87_c top.__top_88_c top.__top_89_c top.__top_9_c top.__top_90_c top.__top_92_c top.__top_93_c top.ni_0._arrow._first_c dummytop.OK)
1444
       (top_step top.KP_START top.KP_CLEAR top.KP_0 top.KP_1 top.KP_2 top.KP_3 top.KP_4 top.KP_5 top.KP_6 top.KP_7 top.KP_8 top.KP_9 top.DOOR_CLOSED top.OK top.__top_13_c top.__top_15_c top.__top_17_c top.__top_19_c top.__top_2_c top.__top_21_c top.__top_23_c top.__top_25_c top.__top_27_c top.__top_29_c top.__top_31_c top.__top_36_c top.__top_37_c top.__top_38_c top.__top_39_c top.__top_6_c top.__top_66_c top.__top_67_c top.__top_68_c top.__top_69_c top.__top_7_c top.__top_70_c top.__top_74_c top.__top_76_c top.__top_77_c top.__top_78_c top.__top_79_c top.__top_80_c top.__top_81_c top.__top_82_c top.__top_83_c top.__top_84_c top.__top_85_c top.__top_86_c top.__top_87_c top.__top_88_c top.__top_89_c top.__top_9_c top.__top_90_c top.__top_92_c top.__top_93_c top.ni_0._arrow._first_c top.__top_13_x top.__top_15_x top.__top_17_x top.__top_19_x top.__top_2_x top.__top_21_x top.__top_23_x top.__top_25_x top.__top_27_x top.__top_29_x top.__top_31_x top.__top_36_x top.__top_37_x top.__top_38_x top.__top_39_x top.__top_6_x top.__top_66_x top.__top_67_x top.__top_68_x top.__top_69_x top.__top_7_x top.__top_70_x top.__top_74_x top.__top_76_x top.__top_77_x top.__top_78_x top.__top_79_x top.__top_80_x top.__top_81_x top.__top_82_x top.__top_83_x top.__top_84_x top.__top_85_x top.__top_86_x top.__top_87_x top.__top_88_x top.__top_89_x top.__top_9_x top.__top_90_x top.__top_92_x top.__top_93_x top.ni_0._arrow._first_x)
1445
  )
1446
  (MAIN top.__top_13_x top.__top_15_x top.__top_17_x top.__top_19_x top.__top_2_x top.__top_21_x top.__top_23_x top.__top_25_x top.__top_27_x top.__top_29_x top.__top_31_x top.__top_36_x top.__top_37_x top.__top_38_x top.__top_39_x top.__top_6_x top.__top_66_x top.__top_67_x top.__top_68_x top.__top_69_x top.__top_7_x top.__top_70_x top.__top_74_x top.__top_76_x top.__top_77_x top.__top_78_x top.__top_79_x top.__top_80_x top.__top_81_x top.__top_82_x top.__top_83_x top.__top_84_x top.__top_85_x top.__top_86_x top.__top_87_x top.__top_88_x top.__top_89_x top.__top_9_x top.__top_90_x top.__top_92_x top.__top_93_x top.ni_0._arrow._first_x top.OK)
1447
))
1448

    
1449
; Property def
1450
(declare-rel ERR ())
1451
(rule (=> 
1452
  (and (not top.OK)
1453
       (MAIN top.__top_13_x top.__top_15_x top.__top_17_x top.__top_19_x top.__top_2_x top.__top_21_x top.__top_23_x top.__top_25_x top.__top_27_x top.__top_29_x top.__top_31_x top.__top_36_x top.__top_37_x top.__top_38_x top.__top_39_x top.__top_6_x top.__top_66_x top.__top_67_x top.__top_68_x top.__top_69_x top.__top_7_x top.__top_70_x top.__top_74_x top.__top_76_x top.__top_77_x top.__top_78_x top.__top_79_x top.__top_80_x top.__top_81_x top.__top_82_x top.__top_83_x top.__top_84_x top.__top_85_x top.__top_86_x top.__top_87_x top.__top_88_x top.__top_89_x top.__top_9_x top.__top_90_x top.__top_92_x top.__top_93_x top.ni_0._arrow._first_x top.OK))
1454
  ERR))
1455
(query ERR)