Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart8 / Flowchart8.smt2 @ eb639349

History | View | Annotate | Download (91.6 KB)

1
(declare-datatypes () ((flowchart8_flowchart8__type POINTFlowchart8_Flowchart8 POINT__TO__FLOWCHART8_A_1 FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1 FLOWCHART8_A_IDL)));
2

    
3
; Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action
4
(declare-var Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent_1 Int)
5
(declare-var Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent Int)
6
(declare-rel Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action (Int Int))
7
(rule (=> 
8
  (= Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent (+ Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent_1 1))
9
  (Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent_1 Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action.cent)
10
))
11

    
12
; Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action
13
(declare-var Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.cent_1 Int)
14
(declare-var Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec_1 Int)
15
(declare-var Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.cent Int)
16
(declare-var Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec Int)
17
(declare-rel Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action (Int Int Int Int))
18
(rule (=> 
19
  (and (= Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec (+ Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec_1 1))
20
       (= Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.cent 0)
21
       )
22
  (Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.cent_1 Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec_1 Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.cent Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action.sec)
23
))
24

    
25
; Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action
26
(declare-var Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.sec_1 Int)
27
(declare-var Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min_1 Int)
28
(declare-var Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.sec Int)
29
(declare-var Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min Int)
30
(declare-rel Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action (Int Int Int Int))
31
(rule (=> 
32
  (and (= Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.sec 0)
33
       (= Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min (+ Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min_1 1))
34
       )
35
  (Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.sec_1 Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min_1 Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.sec Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action.min)
36
))
37

    
38
; Flowchart8_A_en
39
(declare-var Flowchart8_A_en.idFlowchart8_Flowchart8_1 Int)
40
(declare-var Flowchart8_A_en.isInner Bool)
41
(declare-var Flowchart8_A_en.idFlowchart8_Flowchart8 Int)
42
(declare-rel Flowchart8_A_en (Int Bool Int))
43
(rule (=> 
44
  (= Flowchart8_A_en.idFlowchart8_Flowchart8 844)
45
  (Flowchart8_A_en Flowchart8_A_en.idFlowchart8_Flowchart8_1 Flowchart8_A_en.isInner Flowchart8_A_en.idFlowchart8_Flowchart8)
46
))
47

    
48
; flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until
49
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_1 Int)
50
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_1 Int)
51
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_1 Int)
52
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_1 Int)
53
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__restart_in Bool)
54
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
55
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_out Int)
56
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_out Int)
57
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_out Int)
58
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_out Int)
59
(declare-rel flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until (Int Int Int Int Bool flowchart8_flowchart8__type Int Int Int Int))
60
(rule (=> 
61
  (and (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_1)
62
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_1)
63
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_1)
64
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8)
65
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__restart_in true)
66
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_1)
67
       )
68
  (flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_1 flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_1 flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_1 flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_1 flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__restart_in flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.cent_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.min_out flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until.sec_out)
69
))
70

    
71
; flowchart8_flowchart8__FLOWCHART8_A_IDL_unless
72
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_in Bool)
73
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
74
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_act Bool)
75
(declare-var flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__type)
76
(declare-rel flowchart8_flowchart8__FLOWCHART8_A_IDL_unless (Bool flowchart8_flowchart8__type Bool flowchart8_flowchart8__type))
77
(rule (=> 
78
  (and (= flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_in)
79
       (= flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_in)
80
       )
81
  (flowchart8_flowchart8__FLOWCHART8_A_IDL_unless flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_in flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__FLOWCHART8_A_IDL_unless.flowchart8_flowchart8__state_act)
82
))
83

    
84
; flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until
85
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1 Int)
86
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_1 Int)
87
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1 Int)
88
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1 Int)
89
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__restart_in Bool)
90
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
91
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_out Int)
92
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_out Int)
93
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_out Int)
94
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_out Int)
95
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 Bool)
96
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 Bool)
97
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_3 Int)
98
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_4 Int)
99
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_5 Int)
100
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_6 Int)
101
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 Bool)
102
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_8 Int)
103
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_9 Int)
104
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent Int)
105
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2 Int)
106
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_3 Int)
107
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_4 Int)
108
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_5 Int)
109
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_6 Int)
110
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8 Int)
111
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min Int)
112
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_2 Int)
113
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec Int)
114
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2 Int)
115
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_3 Int)
116
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_4 Int)
117
(declare-rel flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until (Int Int Int Int Bool flowchart8_flowchart8__type Int Int Int Int))
118
(rule (=> 
119
  (and (Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action 
120
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_1
121
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_4)
122
       (Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action 
123
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_4
124
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1
125
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_3
126
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_4)
127
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_4 2))
128
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
129
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_4 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_4))
130
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
131
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_4 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1))
132
       )
133
       (Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action 
134
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_1
135
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2)
136
       (Flowchart8_Flowchart8Junction849__To__Flowchart8_Flowchart8Junction850_1_Condition_Action 
137
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2
138
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1
139
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_8
140
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_9)
141
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2 2))
142
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 true))
143
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_9))
144
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 false))
145
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1))
146
       )
147
       (Flowchart8_Flowchart8Junction850__To__Flowchart8_Flowchart8Junction851_1_Condition_Action 
148
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2
149
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1
150
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_5
151
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_6)
152
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2 2) (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2 3)))
153
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 false))
154
               (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_3 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_2)
155
                    (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
156
                            (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_4))
157
                         (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
158
                            (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
159
                                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_4))
160
                                 (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
161
                                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1))
162
                            ))
163
                    )
164
                    ))
165
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 true))
166
               (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_3 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_5)
167
                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_3)
168
                    ))
169
       )
170
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec)
171
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 false))
172
               (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_2 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1)
173
                    (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
174
                            (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1))
175
                         (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
176
                            (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
177
                                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1))
178
                                 (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
179
                                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1))
180
                            ))
181
                    )
182
                    ))
183
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 true))
184
               (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_2 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_6)
185
                    (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_2)
186
                    ))
187
       )
188
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min)
189
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 true))
190
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1))
191
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 false))
192
               (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
193
                       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1))
194
                    (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
195
                       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
196
                               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1))
197
                            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
198
                               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1))
199
                       ))
200
               ))
201
       )
202
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8)
203
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8)
204
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__restart_in true)
205
       (Flowchart8_A__To__Flowchart8_Flowchart8Junction849_1_Condition_Action 
206
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_1
207
       flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_6)
208
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
209
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_5 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_3))
210
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
211
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_5 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_4))
212
       )
213
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 true))
214
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_3 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_8))
215
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_7 false))
216
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_3 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_2))
217
       )
218
       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 true))
219
               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_3))
220
            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_1 false))
221
               (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
222
                       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_5))
223
                    (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
224
                       (and (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 true))
225
                               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_5))
226
                            (or (not (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.__flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until_2 false))
227
                               (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_6))
228
                       ))
229
               ))
230
       )
231
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent)
232
       )
233
  (flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_1 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_1 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_1 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_1 flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__restart_in flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.cent_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.min_out flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until.sec_out)
234
))
235

    
236
; flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless
237
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_in Bool)
238
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
239
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_act Bool)
240
(declare-var flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__type)
241
(declare-rel flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless (Bool flowchart8_flowchart8__type Bool flowchart8_flowchart8__type))
242
(rule (=> 
243
  (and (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_in)
244
       (= flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_in)
245
       )
246
  (flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_in flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless.flowchart8_flowchart8__state_act)
247
))
248

    
249
; flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until
250
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_1 Int)
251
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_1 Int)
252
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_1 Int)
253
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_1 Int)
254
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__restart_in Bool)
255
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
256
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_out Int)
257
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_out Int)
258
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_out Int)
259
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_out Int)
260
(declare-rel flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until (Int Int Int Int Bool flowchart8_flowchart8__type Int Int Int Int))
261
(rule (=> 
262
  (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_1)
263
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_1)
264
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_1)
265
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8)
266
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__restart_in false)
267
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_1)
268
       )
269
  (flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_1 flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_1 flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_1 flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_1 flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__restart_in flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.cent_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.min_out flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until.sec_out)
270
))
271

    
272
; flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless
273
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_in Bool)
274
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
275
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.idFlowchart8_Flowchart8_1 Int)
276
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.TIC Bool)
277
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act Bool)
278
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__type)
279
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_1 Bool)
280
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_2 Bool)
281
(declare-var flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_3 Bool)
282
(declare-rel flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless (Bool flowchart8_flowchart8__type Int Bool Bool flowchart8_flowchart8__type))
283
(rule (=> 
284
  (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_3 (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.idFlowchart8_Flowchart8_1 844))
285
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_2 (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.idFlowchart8_Flowchart8_1 844) flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.TIC))
286
       (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_1 (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.idFlowchart8_Flowchart8_1 0))
287
       (and (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_1 false))
288
               (and (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_2 false))
289
                       (and (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_3 false))
290
                               (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_in)
291
                                    (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_in)
292
                                    ))
293
                            (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_3 true))
294
                               (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act FLOWCHART8_A_IDL)
295
                                    (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act true)
296
                                    ))
297
                       ))
298
                    (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_2 true))
299
                       (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1)
300
                            (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act true)
301
                            ))
302
               ))
303
            (or (not (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.__flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless_1 true))
304
               (and (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act POINT__TO__FLOWCHART8_A_1)
305
                    (= flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act true)
306
                    ))
307
       )
308
       )
309
  (flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_in flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.idFlowchart8_Flowchart8_1 flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.TIC flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless.flowchart8_flowchart8__state_act)
310
))
311

    
312
; flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until
313
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_1 Int)
314
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_1 Int)
315
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_1 Int)
316
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_1 Int)
317
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__restart_in Bool)
318
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
319
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_out Int)
320
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_out Int)
321
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_out Int)
322
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_out Int)
323
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_2 Int)
324
(declare-rel flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until (Int Int Int Int Bool flowchart8_flowchart8__type Int Int Int Int))
325
(rule (=> 
326
  (and (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_1)
327
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_1)
328
       (Flowchart8_A_en flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_1
329
                        false
330
                        flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_2)
331
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_2)
332
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8)
333
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__restart_in true)
334
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_1)
335
       )
336
  (flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_1 flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_1 flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_1 flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_1 flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__restart_in flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.flowchart8_flowchart8__state_in flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.cent_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.idFlowchart8_Flowchart8_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.min_out flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until.sec_out)
337
))
338

    
339
; flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless
340
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_in Bool)
341
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
342
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_act Bool)
343
(declare-var flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__type)
344
(declare-rel flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless (Bool flowchart8_flowchart8__type Bool flowchart8_flowchart8__type))
345
(rule (=> 
346
  (and (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_act flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_in)
347
       (= flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_in)
348
       )
349
  (flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_in flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_in flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__restart_act flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless.flowchart8_flowchart8__state_act)
350
))
351

    
352
; Flowchart8_Flowchart8_node
353
(declare-var Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1 Int)
354
(declare-var Flowchart8_Flowchart8_node.TIC Bool)
355
(declare-var Flowchart8_Flowchart8_node.cent_1 Int)
356
(declare-var Flowchart8_Flowchart8_node.sec_1 Int)
357
(declare-var Flowchart8_Flowchart8_node.min_1 Int)
358
(declare-var Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8 Int)
359
(declare-var Flowchart8_Flowchart8_node.cent Int)
360
(declare-var Flowchart8_Flowchart8_node.sec Int)
361
(declare-var Flowchart8_Flowchart8_node.min Int)
362
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c Bool)
363
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c flowchart8_flowchart8__type)
364
(declare-var Flowchart8_Flowchart8_node.ni_4._arrow._first_c Bool)
365
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Bool)
366
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m flowchart8_flowchart8__type)
367
(declare-var Flowchart8_Flowchart8_node.ni_4._arrow._first_m Bool)
368
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x Bool)
369
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x flowchart8_flowchart8__type)
370
(declare-var Flowchart8_Flowchart8_node.ni_4._arrow._first_x Bool)
371
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_1 Bool)
372
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_10 flowchart8_flowchart8__type)
373
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_11 Int)
374
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_12 Int)
375
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_13 Int)
376
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_14 Int)
377
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_15 Bool)
378
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_16 flowchart8_flowchart8__type)
379
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_17 Int)
380
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_18 Int)
381
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_19 Int)
382
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_2 flowchart8_flowchart8__type)
383
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_20 Int)
384
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_21 Bool)
385
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_22 flowchart8_flowchart8__type)
386
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_23 Int)
387
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_24 Int)
388
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_25 Int)
389
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_26 Int)
390
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_27 Bool)
391
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_28 flowchart8_flowchart8__type)
392
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_29 Int)
393
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_3 Bool)
394
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_30 Int)
395
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_31 Int)
396
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_32 Int)
397
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_33 Bool)
398
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_4 flowchart8_flowchart8__type)
399
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_5 Bool)
400
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_6 flowchart8_flowchart8__type)
401
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_7 Bool)
402
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_8 flowchart8_flowchart8__type)
403
(declare-var Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_9 Bool)
404
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in Bool)
405
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in flowchart8_flowchart8__type)
406
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_act Bool)
407
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in Bool)
408
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act flowchart8_flowchart8__type)
409
(declare-var Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in flowchart8_flowchart8__type)
410
(declare-rel Flowchart8_Flowchart8_node_reset (Bool flowchart8_flowchart8__type Bool Bool flowchart8_flowchart8__type Bool))
411
(declare-rel Flowchart8_Flowchart8_node_step (Int Bool Int Int Int Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool flowchart8_flowchart8__type Bool))
412

    
413
(rule (=> 
414
  (and 
415
       (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c)
416
       (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c)
417
       (= Flowchart8_Flowchart8_node.ni_4._arrow._first_m true)
418
  )
419
  (Flowchart8_Flowchart8_node_reset Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
420
                                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
421
                                    Flowchart8_Flowchart8_node.ni_4._arrow._first_c
422
                                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
423
                                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
424
                                    Flowchart8_Flowchart8_node.ni_4._arrow._first_m)
425
))
426

    
427
(rule (=> 
428
  (and (= Flowchart8_Flowchart8_node.ni_4._arrow._first_m Flowchart8_Flowchart8_node.ni_4._arrow._first_c)
429
       (and (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_33 (ite Flowchart8_Flowchart8_node.ni_4._arrow._first_m true false))
430
            (= Flowchart8_Flowchart8_node.ni_4._arrow._first_x false))
431
       (and (or (not (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_33 false))
432
               (and (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c)
433
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c)
434
                    ))
435
            (or (not (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_33 true))
436
               (and (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8)
437
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in false)
438
                    ))
439
       )
440
       (and (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in FLOWCHART8_A_IDL))
441
               (and (flowchart8_flowchart8__FLOWCHART8_A_IDL_unless Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in
442
                                                                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in
443
                                                                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_1
444
                                                                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_2)
445
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_2)
446
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_1)
447
                    ))
448
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1))
449
               (and (flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_unless 
450
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in
451
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in
452
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_3
453
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_4)
454
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_4)
455
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_3)
456
                    ))
457
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in POINTFlowchart8_Flowchart8))
458
               (and (flowchart8_flowchart8__POINTFlowchart8_Flowchart8_unless 
459
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in
460
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in
461
                    Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
462
                    Flowchart8_Flowchart8_node.TIC
463
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_7
464
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_8)
465
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_8)
466
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_7)
467
                    ))
468
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in POINT__TO__FLOWCHART8_A_1))
469
               (and (flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_unless 
470
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_in
471
                    Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_in
472
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_5
473
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_6)
474
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_6)
475
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__restart_act Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_5)
476
                    ))
477
       )
478
       (and (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act FLOWCHART8_A_IDL))
479
               (and (flowchart8_flowchart8__FLOWCHART8_A_IDL_handler_until 
480
                    Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
481
                    Flowchart8_Flowchart8_node.cent_1
482
                    Flowchart8_Flowchart8_node.sec_1
483
                    Flowchart8_Flowchart8_node.min_1
484
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_9
485
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_10
486
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_11
487
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_12
488
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_13
489
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_14)
490
                    (= Flowchart8_Flowchart8_node.sec Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_14)
491
                    (= Flowchart8_Flowchart8_node.min Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_13)
492
                    (= Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8 Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_12)
493
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_10)
494
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_9)
495
                    (= Flowchart8_Flowchart8_node.cent Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_11)
496
                    ))
497
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1))
498
               (and (flowchart8_flowchart8__FLOWCHART8_A__TO__FLOWCHART8_FLOWCHART8JUNCTION849_1_handler_until 
499
                    Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
500
                    Flowchart8_Flowchart8_node.cent_1
501
                    Flowchart8_Flowchart8_node.sec_1
502
                    Flowchart8_Flowchart8_node.min_1
503
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_15
504
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_16
505
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_17
506
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_18
507
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_19
508
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_20)
509
                    (= Flowchart8_Flowchart8_node.sec Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_20)
510
                    (= Flowchart8_Flowchart8_node.min Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_19)
511
                    (= Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8 Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_18)
512
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_16)
513
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_15)
514
                    (= Flowchart8_Flowchart8_node.cent Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_17)
515
                    ))
516
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act POINTFlowchart8_Flowchart8))
517
               (and (flowchart8_flowchart8__POINTFlowchart8_Flowchart8_handler_until 
518
                    Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
519
                    Flowchart8_Flowchart8_node.cent_1
520
                    Flowchart8_Flowchart8_node.sec_1
521
                    Flowchart8_Flowchart8_node.min_1
522
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_27
523
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_28
524
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_29
525
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_30
526
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_31
527
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_32)
528
                    (= Flowchart8_Flowchart8_node.sec Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_32)
529
                    (= Flowchart8_Flowchart8_node.min Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_31)
530
                    (= Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8 Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_30)
531
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_28)
532
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_27)
533
                    (= Flowchart8_Flowchart8_node.cent Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_29)
534
                    ))
535
            (or (not (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__state_act POINT__TO__FLOWCHART8_A_1))
536
               (and (flowchart8_flowchart8__POINT__TO__FLOWCHART8_A_1_handler_until 
537
                    Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
538
                    Flowchart8_Flowchart8_node.cent_1
539
                    Flowchart8_Flowchart8_node.sec_1
540
                    Flowchart8_Flowchart8_node.min_1
541
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_21
542
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_22
543
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_23
544
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_24
545
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_25
546
                    Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_26)
547
                    (= Flowchart8_Flowchart8_node.sec Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_26)
548
                    (= Flowchart8_Flowchart8_node.min Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_25)
549
                    (= Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8 Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_24)
550
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_22)
551
                    (= Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_21)
552
                    (= Flowchart8_Flowchart8_node.cent Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_23)
553
                    ))
554
       )
555
       (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_state_in)
556
       (= Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x Flowchart8_Flowchart8_node.flowchart8_flowchart8__next_restart_in)
557
       )
558
  (Flowchart8_Flowchart8_node_step Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8_1
559
                                   Flowchart8_Flowchart8_node.TIC
560
                                   Flowchart8_Flowchart8_node.cent_1
561
                                   Flowchart8_Flowchart8_node.sec_1
562
                                   Flowchart8_Flowchart8_node.min_1
563
                                   Flowchart8_Flowchart8_node.idFlowchart8_Flowchart8
564
                                   Flowchart8_Flowchart8_node.cent
565
                                   Flowchart8_Flowchart8_node.sec
566
                                   Flowchart8_Flowchart8_node.min
567
                                   Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
568
                                   Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
569
                                   Flowchart8_Flowchart8_node.ni_4._arrow._first_c
570
                                   Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x
571
                                   Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x
572
                                   Flowchart8_Flowchart8_node.ni_4._arrow._first_x)
573
))
574

    
575
; Flowchart8_Flowchart8
576
(declare-var Flowchart8_Flowchart8.TIC Bool)
577
(declare-var Flowchart8_Flowchart8.cent Int)
578
(declare-var Flowchart8_Flowchart8.sec Int)
579
(declare-var Flowchart8_Flowchart8.min Int)
580
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c Int)
581
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c Int)
582
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c Int)
583
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c Int)
584
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c Bool)
585
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c flowchart8_flowchart8__type)
586
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c Bool)
587
(declare-var Flowchart8_Flowchart8.ni_3._arrow._first_c Bool)
588
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m Int)
589
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m Int)
590
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m Int)
591
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m Int)
592
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Bool)
593
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m flowchart8_flowchart8__type)
594
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m Bool)
595
(declare-var Flowchart8_Flowchart8.ni_3._arrow._first_m Bool)
596
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x Int)
597
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x Int)
598
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x Int)
599
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x Int)
600
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x Bool)
601
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x flowchart8_flowchart8__type)
602
(declare-var Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x Bool)
603
(declare-var Flowchart8_Flowchart8.ni_3._arrow._first_x Bool)
604
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_1 Int)
605
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_2 Int)
606
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_3 Int)
607
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_4 Int)
608
(declare-var Flowchart8_Flowchart8.__Flowchart8_Flowchart8_5 Bool)
609
(declare-var Flowchart8_Flowchart8.cent_1 Int)
610
(declare-var Flowchart8_Flowchart8.idFlowchart8_Flowchart8 Int)
611
(declare-var Flowchart8_Flowchart8.idFlowchart8_Flowchart8_1 Int)
612
(declare-var Flowchart8_Flowchart8.min_1 Int)
613
(declare-var Flowchart8_Flowchart8.sec_1 Int)
614
(declare-rel Flowchart8_Flowchart8_reset (Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool))
615
(declare-rel Flowchart8_Flowchart8_step (Bool Int Int Int Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool))
616

    
617
(rule (=> 
618
  (and 
619
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c)
620
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c)
621
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c)
622
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c)
623
       (= Flowchart8_Flowchart8.ni_3._arrow._first_m true)
624
       (Flowchart8_Flowchart8_node_reset Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
625
                                         Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
626
                                         Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
627
                                         Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
628
                                         Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
629
                                         Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m)
630
  )
631
  (Flowchart8_Flowchart8_reset Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c
632
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c
633
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c
634
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c
635
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
636
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
637
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
638
                               Flowchart8_Flowchart8.ni_3._arrow._first_c
639
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m
640
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m
641
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m
642
                               Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m
643
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
644
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
645
                               Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m
646
                               Flowchart8_Flowchart8.ni_3._arrow._first_m)
647
))
648

    
649
(rule (=> 
650
  (and (= Flowchart8_Flowchart8.ni_3._arrow._first_m Flowchart8_Flowchart8.ni_3._arrow._first_c)
651
       (and (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_5 (ite Flowchart8_Flowchart8.ni_3._arrow._first_m true false))
652
            (= Flowchart8_Flowchart8.ni_3._arrow._first_x false))
653
       (and (or (not (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_5 false))
654
               (and (= Flowchart8_Flowchart8.sec_1 Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c)
655
                    (= Flowchart8_Flowchart8.min_1 Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c)
656
                    (= Flowchart8_Flowchart8.idFlowchart8_Flowchart8_1 Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c)
657
                    (= Flowchart8_Flowchart8.cent_1 Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c)
658
                    ))
659
            (or (not (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_5 true))
660
               (and (= Flowchart8_Flowchart8.sec_1 0)
661
                    (= Flowchart8_Flowchart8.min_1 0)
662
                    (= Flowchart8_Flowchart8.idFlowchart8_Flowchart8_1 0)
663
                    (= Flowchart8_Flowchart8.cent_1 0)
664
                    ))
665
       )
666
       (and (= Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c)
667
            (= Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c)
668
            (= Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c)
669
            )
670
       (Flowchart8_Flowchart8_node_step Flowchart8_Flowchart8.idFlowchart8_Flowchart8_1
671
                                        Flowchart8_Flowchart8.TIC
672
                                        Flowchart8_Flowchart8.cent_1
673
                                        Flowchart8_Flowchart8.sec_1
674
                                        Flowchart8_Flowchart8.min_1
675
                                        Flowchart8_Flowchart8.__Flowchart8_Flowchart8_1
676
                                        Flowchart8_Flowchart8.__Flowchart8_Flowchart8_2
677
                                        Flowchart8_Flowchart8.__Flowchart8_Flowchart8_3
678
                                        Flowchart8_Flowchart8.__Flowchart8_Flowchart8_4
679
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
680
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
681
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m
682
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x
683
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x
684
                                        Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x)
685
       (and (or (not (= Flowchart8_Flowchart8.TIC false))
686
               (and (= Flowchart8_Flowchart8.sec Flowchart8_Flowchart8.sec_1)
687
                    (= Flowchart8_Flowchart8.min Flowchart8_Flowchart8.min_1)
688
                    (= Flowchart8_Flowchart8.idFlowchart8_Flowchart8 Flowchart8_Flowchart8.idFlowchart8_Flowchart8_1)
689
                    (= Flowchart8_Flowchart8.cent Flowchart8_Flowchart8.cent_1)
690
                    ))
691
            (or (not (= Flowchart8_Flowchart8.TIC true))
692
               (and (= Flowchart8_Flowchart8.sec Flowchart8_Flowchart8.__Flowchart8_Flowchart8_3)
693
                    (= Flowchart8_Flowchart8.min Flowchart8_Flowchart8.__Flowchart8_Flowchart8_4)
694
                    (= Flowchart8_Flowchart8.idFlowchart8_Flowchart8 Flowchart8_Flowchart8.__Flowchart8_Flowchart8_1)
695
                    (= Flowchart8_Flowchart8.cent Flowchart8_Flowchart8.__Flowchart8_Flowchart8_2)
696
                    ))
697
       )
698
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x Flowchart8_Flowchart8.cent)
699
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x Flowchart8_Flowchart8.sec)
700
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x Flowchart8_Flowchart8.min)
701
       (= Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x Flowchart8_Flowchart8.idFlowchart8_Flowchart8)
702
       )
703
  (Flowchart8_Flowchart8_step Flowchart8_Flowchart8.TIC
704
                              Flowchart8_Flowchart8.cent
705
                              Flowchart8_Flowchart8.sec
706
                              Flowchart8_Flowchart8.min
707
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c
708
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c
709
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c
710
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c
711
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
712
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
713
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
714
                              Flowchart8_Flowchart8.ni_3._arrow._first_c
715
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x
716
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x
717
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x
718
                              Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x
719
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x
720
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x
721
                              Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x
722
                              Flowchart8_Flowchart8.ni_3._arrow._first_x)
723
))
724

    
725
; Flowchart8
726
(declare-var Flowchart8.In1_1_1 Real)
727
(declare-var Flowchart8.cent_1_1 Int)
728
(declare-var Flowchart8.sec_2_1 Int)
729
(declare-var Flowchart8.Out3_3_1 Int)
730
(declare-var Flowchart8.__Flowchart8_2_c Real)
731
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c Int)
732
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c Int)
733
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c Int)
734
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c Int)
735
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c Bool)
736
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c flowchart8_flowchart8__type)
737
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c Bool)
738
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_c Bool)
739
(declare-var Flowchart8.ni_1._arrow._first_c Bool)
740
(declare-var Flowchart8.__Flowchart8_2_m Real)
741
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m Int)
742
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m Int)
743
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m Int)
744
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m Int)
745
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Bool)
746
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m flowchart8_flowchart8__type)
747
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m Bool)
748
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_m Bool)
749
(declare-var Flowchart8.ni_1._arrow._first_m Bool)
750
(declare-var Flowchart8.__Flowchart8_2_x Real)
751
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x Int)
752
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x Int)
753
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x Int)
754
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x Int)
755
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x Bool)
756
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x flowchart8_flowchart8__type)
757
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x Bool)
758
(declare-var Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_x Bool)
759
(declare-var Flowchart8.ni_1._arrow._first_x Bool)
760
(declare-var Flowchart8.Flowchart8In1_1_1_event Bool)
761
(declare-var Flowchart8.Flowchart8_1_1 Int)
762
(declare-var Flowchart8.Flowchart8_2_1 Int)
763
(declare-var Flowchart8.Flowchart8_3_1 Int)
764
(declare-var Flowchart8.__Flowchart8_1 Bool)
765
(declare-var Flowchart8.i_virtual_local Real)
766
(declare-rel Flowchart8_reset (Real Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Bool Real Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Bool))
767
(declare-rel Flowchart8_step (Real Int Int Int Real Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Bool Real Int Int Int Int Bool flowchart8_flowchart8__type Bool Bool Bool))
768

    
769
(rule (=> 
770
  (and 
771
       (= Flowchart8.__Flowchart8_2_m Flowchart8.__Flowchart8_2_c)
772
       (= Flowchart8.ni_1._arrow._first_m true)
773
       (Flowchart8_Flowchart8_reset Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c
774
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c
775
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c
776
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c
777
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
778
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
779
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
780
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_c
781
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m
782
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m
783
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m
784
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m
785
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
786
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
787
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m
788
                                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_m)
789
  )
790
  (Flowchart8_reset Flowchart8.__Flowchart8_2_c
791
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c
792
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c
793
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c
794
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c
795
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
796
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
797
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
798
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_c
799
                    Flowchart8.ni_1._arrow._first_c
800
                    Flowchart8.__Flowchart8_2_m
801
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m
802
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m
803
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m
804
                    Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m
805
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
806
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
807
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m
808
                    Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_m
809
                    Flowchart8.ni_1._arrow._first_m)
810
))
811

    
812
(rule (=> 
813
  (and (= Flowchart8.ni_1._arrow._first_m Flowchart8.ni_1._arrow._first_c)
814
       (and (= Flowchart8.__Flowchart8_1 (ite Flowchart8.ni_1._arrow._first_m true false))
815
            (= Flowchart8.ni_1._arrow._first_x false))
816
       (and (or (not (= Flowchart8.__Flowchart8_1 true))
817
               (= Flowchart8.Flowchart8In1_1_1_event false))
818
            (or (not (= Flowchart8.__Flowchart8_1 false))
819
               (= Flowchart8.Flowchart8In1_1_1_event (or (and (> Flowchart8.__Flowchart8_2_c 0.) (<= Flowchart8.In1_1_1 0.)) (and (<= Flowchart8.__Flowchart8_2_c 0.) (> Flowchart8.In1_1_1 0.)))))
820
       )
821
       (and (= Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c)
822
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c)
823
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c)
824
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c)
825
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c)
826
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c)
827
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c)
828
            (= Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_m Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_c)
829
            )
830
       (Flowchart8_Flowchart8_step Flowchart8.Flowchart8In1_1_1_event
831
                                   Flowchart8.Flowchart8_1_1
832
                                   Flowchart8.Flowchart8_2_1
833
                                   Flowchart8.Flowchart8_3_1
834
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_m
835
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_m
836
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_m
837
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_m
838
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_m
839
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_m
840
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_m
841
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_m
842
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x
843
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x
844
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x
845
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x
846
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x
847
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x
848
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x
849
                                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_x)
850
       (= Flowchart8.sec_2_1 Flowchart8.Flowchart8_2_1)
851
       (and (or (not (= Flowchart8.__Flowchart8_1 true))
852
               (= Flowchart8.i_virtual_local 0.))
853
            (or (not (= Flowchart8.__Flowchart8_1 false))
854
               (= Flowchart8.i_virtual_local 1.))
855
       )
856
       (= Flowchart8.cent_1_1 Flowchart8.Flowchart8_1_1)
857
       (= Flowchart8.__Flowchart8_2_x Flowchart8.In1_1_1)
858
       (= Flowchart8.Out3_3_1 Flowchart8.Flowchart8_3_1)
859
       )
860
  (Flowchart8_step Flowchart8.In1_1_1
861
                   Flowchart8.cent_1_1
862
                   Flowchart8.sec_2_1
863
                   Flowchart8.Out3_3_1
864
                   Flowchart8.__Flowchart8_2_c
865
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_c
866
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_c
867
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_c
868
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_c
869
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_c
870
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_c
871
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_c
872
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_c
873
                   Flowchart8.ni_1._arrow._first_c
874
                   Flowchart8.__Flowchart8_2_x
875
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_6_x
876
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_7_x
877
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_8_x
878
                   Flowchart8.ni_0.Flowchart8_Flowchart8.__Flowchart8_Flowchart8_9_x
879
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_34_x
880
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.__Flowchart8_Flowchart8_node_35_x
881
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_2.Flowchart8_Flowchart8_node.ni_4._arrow._first_x
882
                   Flowchart8.ni_0.Flowchart8_Flowchart8.ni_3._arrow._first_x
883
                   Flowchart8.ni_1._arrow._first_x)
884
))
885

    
886
; Flowchart8_A_ex
887
(declare-var Flowchart8_A_ex.idFlowchart8_Flowchart8_1 Int)
888
(declare-var Flowchart8_A_ex.isInner Bool)
889
(declare-var Flowchart8_A_ex.idFlowchart8_Flowchart8 Int)
890
(declare-var Flowchart8_A_ex.idFlowchart8_Flowchart8_2 Int)
891
(declare-rel Flowchart8_A_ex (Int Bool Int))
892
(rule (=> 
893
  (and (and (or (not (= (not Flowchart8_A_ex.isInner) true))
894
               (= Flowchart8_A_ex.idFlowchart8_Flowchart8_2 0))
895
            (or (not (= (not Flowchart8_A_ex.isInner) false))
896
               (= Flowchart8_A_ex.idFlowchart8_Flowchart8_2 Flowchart8_A_ex.idFlowchart8_Flowchart8_1))
897
       )
898
       (= Flowchart8_A_ex.idFlowchart8_Flowchart8 Flowchart8_A_ex.idFlowchart8_Flowchart8_1)
899
       )
900
  (Flowchart8_A_ex Flowchart8_A_ex.idFlowchart8_Flowchart8_1 Flowchart8_A_ex.isInner Flowchart8_A_ex.idFlowchart8_Flowchart8)
901
))
902