Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Flowchart7 / Flowchart7.smt2 @ eb639349

History | View | Annotate | Download (71.5 KB)

1
(declare-datatypes () ((flowchart7_flowchart7__type POINTFlowchart7_Flowchart7 POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1)));
2

    
3
; Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action
4
(declare-var Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.cent_1 Int)
5
(declare-var Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec_1 Int)
6
(declare-var Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.cent Int)
7
(declare-var Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec Int)
8
(declare-rel Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action (Int Int Int Int))
9
(rule (=> 
10
  (and (= Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec (+ Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec_1 1))
11
       (= Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.cent 0)
12
       )
13
  (Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.cent_1 Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec_1 Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.cent Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action.sec)
14
))
15

    
16
; Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action
17
(declare-var Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.sec_1 Int)
18
(declare-var Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min_1 Int)
19
(declare-var Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.sec Int)
20
(declare-var Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min Int)
21
(declare-rel Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action (Int Int Int Int))
22
(rule (=> 
23
  (and (= Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.sec 0)
24
       (= Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min (+ Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min_1 1))
25
       )
26
  (Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.sec_1 Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min_1 Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.sec Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action.min)
27
))
28

    
29
; POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action
30
(declare-var POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent_1 Int)
31
(declare-var POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent Int)
32
(declare-rel POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action (Int Int))
33
(rule (=> 
34
  (= POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent (+ POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent_1 1))
35
  (POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent_1 POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action.cent)
36
))
37

    
38
; flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until
39
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_1 Int)
40
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_1 Int)
41
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_1 Int)
42
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_1 Int)
43
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__restart_in Bool)
44
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__state_in flowchart7_flowchart7__type)
45
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_out Int)
46
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_out Int)
47
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_out Int)
48
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_out Int)
49
(declare-rel flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until (Int Int Int Int Bool flowchart7_flowchart7__type Int Int Int Int))
50
(rule (=> 
51
  (and (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_1)
52
       (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_1)
53
       (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_1)
54
       (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__state_in POINTFlowchart7_Flowchart7)
55
       (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__restart_in false)
56
       (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_1)
57
       )
58
  (flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_1 flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_1 flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_1 flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_1 flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__restart_in flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.flowchart7_flowchart7__state_in flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.cent_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.idFlowchart7_Flowchart7_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.min_out flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until.sec_out)
59
))
60

    
61
; flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless
62
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_in Bool)
63
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_in flowchart7_flowchart7__type)
64
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.idFlowchart7_Flowchart7_1 Int)
65
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.TIC Bool)
66
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_act Bool)
67
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_act flowchart7_flowchart7__type)
68
(declare-var flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.__flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless_1 Bool)
69
(declare-rel flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless (Bool flowchart7_flowchart7__type Int Bool Bool flowchart7_flowchart7__type))
70
(rule (=> 
71
  (and (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.__flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless_1 (and (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.idFlowchart7_Flowchart7_1 0) flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.TIC))
72
       (and (or (not (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.__flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless_1 false))
73
               (and (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_act flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_in)
74
                    (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_act flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_in)
75
                    ))
76
            (or (not (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.__flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless_1 true))
77
               (and (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_act POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1)
78
                    (= flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_act true)
79
                    ))
80
       )
81
       )
82
  (flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_in flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_in flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.idFlowchart7_Flowchart7_1 flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.TIC flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__restart_act flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless.flowchart7_flowchart7__state_act)
83
))
84

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

    
237
; flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless
238
(declare-var flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_in Bool)
239
(declare-var flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_in flowchart7_flowchart7__type)
240
(declare-var flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_act Bool)
241
(declare-var flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_act flowchart7_flowchart7__type)
242
(declare-rel flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless (Bool flowchart7_flowchart7__type Bool flowchart7_flowchart7__type))
243
(rule (=> 
244
  (and (= flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_act flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_in)
245
       (= flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_act flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_in)
246
       )
247
  (flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_in flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_in flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__restart_act flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless.flowchart7_flowchart7__state_act)
248
))
249

    
250
; Flowchart7_Flowchart7_node
251
(declare-var Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7_1 Int)
252
(declare-var Flowchart7_Flowchart7_node.TIC Bool)
253
(declare-var Flowchart7_Flowchart7_node.cent_1 Int)
254
(declare-var Flowchart7_Flowchart7_node.sec_1 Int)
255
(declare-var Flowchart7_Flowchart7_node.min_1 Int)
256
(declare-var Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7 Int)
257
(declare-var Flowchart7_Flowchart7_node.cent Int)
258
(declare-var Flowchart7_Flowchart7_node.sec Int)
259
(declare-var Flowchart7_Flowchart7_node.min Int)
260
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c Bool)
261
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c flowchart7_flowchart7__type)
262
(declare-var Flowchart7_Flowchart7_node.ni_4._arrow._first_c Bool)
263
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Bool)
264
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m flowchart7_flowchart7__type)
265
(declare-var Flowchart7_Flowchart7_node.ni_4._arrow._first_m Bool)
266
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x Bool)
267
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x flowchart7_flowchart7__type)
268
(declare-var Flowchart7_Flowchart7_node.ni_4._arrow._first_x Bool)
269
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_1 Bool)
270
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_10 Int)
271
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_11 Bool)
272
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_12 flowchart7_flowchart7__type)
273
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_13 Int)
274
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_14 Int)
275
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_15 Int)
276
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_16 Int)
277
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_17 Bool)
278
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_2 flowchart7_flowchart7__type)
279
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_3 Bool)
280
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_4 flowchart7_flowchart7__type)
281
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_5 Bool)
282
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_6 flowchart7_flowchart7__type)
283
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_7 Int)
284
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_8 Int)
285
(declare-var Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_9 Int)
286
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_restart_in Bool)
287
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_state_in flowchart7_flowchart7__type)
288
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_act Bool)
289
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_in Bool)
290
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_act flowchart7_flowchart7__type)
291
(declare-var Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in flowchart7_flowchart7__type)
292
(declare-rel Flowchart7_Flowchart7_node_reset (Bool flowchart7_flowchart7__type Bool Bool flowchart7_flowchart7__type Bool))
293
(declare-rel Flowchart7_Flowchart7_node_step (Int Bool Int Int Int Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool flowchart7_flowchart7__type Bool))
294

    
295
(rule (=> 
296
  (and 
297
       (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c)
298
       (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c)
299
       (= Flowchart7_Flowchart7_node.ni_4._arrow._first_m true)
300
  )
301
  (Flowchart7_Flowchart7_node_reset Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
302
                                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
303
                                    Flowchart7_Flowchart7_node.ni_4._arrow._first_c
304
                                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
305
                                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
306
                                    Flowchart7_Flowchart7_node.ni_4._arrow._first_m)
307
))
308

    
309
(rule (=> 
310
  (and (= Flowchart7_Flowchart7_node.ni_4._arrow._first_m Flowchart7_Flowchart7_node.ni_4._arrow._first_c)
311
       (and (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_17 (ite Flowchart7_Flowchart7_node.ni_4._arrow._first_m true false))
312
            (= Flowchart7_Flowchart7_node.ni_4._arrow._first_x false))
313
       (and (or (not (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_17 false))
314
               (and (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c)
315
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c)
316
                    ))
317
            (or (not (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_17 true))
318
               (and (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in POINTFlowchart7_Flowchart7)
319
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_in false)
320
                    ))
321
       )
322
       (and (or (not (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in POINTFlowchart7_Flowchart7))
323
               (and (flowchart7_flowchart7__POINTFlowchart7_Flowchart7_unless 
324
                    Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_in
325
                    Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in
326
                    Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7_1
327
                    Flowchart7_Flowchart7_node.TIC
328
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_3
329
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_4)
330
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_act Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_4)
331
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_act Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_3)
332
                    ))
333
            (or (not (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1))
334
               (and (flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_unless 
335
                    Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_in
336
                    Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_in
337
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_1
338
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_2)
339
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_act Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_2)
340
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__restart_act Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_1)
341
                    ))
342
       )
343
       (and (or (not (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_act POINTFlowchart7_Flowchart7))
344
               (and (flowchart7_flowchart7__POINTFlowchart7_Flowchart7_handler_until 
345
                    Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7_1
346
                    Flowchart7_Flowchart7_node.cent_1
347
                    Flowchart7_Flowchart7_node.sec_1
348
                    Flowchart7_Flowchart7_node.min_1
349
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_11
350
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_12
351
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_13
352
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_14
353
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_15
354
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_16)
355
                    (= Flowchart7_Flowchart7_node.sec Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_16)
356
                    (= Flowchart7_Flowchart7_node.min Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_15)
357
                    (= Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7 Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_14)
358
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_state_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_12)
359
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_restart_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_11)
360
                    (= Flowchart7_Flowchart7_node.cent Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_13)
361
                    ))
362
            (or (not (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__state_act POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1))
363
               (and (flowchart7_flowchart7__POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1_handler_until 
364
                    Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7_1
365
                    Flowchart7_Flowchart7_node.cent_1
366
                    Flowchart7_Flowchart7_node.sec_1
367
                    Flowchart7_Flowchart7_node.min_1
368
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_5
369
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_6
370
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_7
371
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_8
372
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_9
373
                    Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_10)
374
                    (= Flowchart7_Flowchart7_node.sec Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_10)
375
                    (= Flowchart7_Flowchart7_node.min Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_9)
376
                    (= Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7 Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_8)
377
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_state_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_6)
378
                    (= Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_restart_in Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_5)
379
                    (= Flowchart7_Flowchart7_node.cent Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_7)
380
                    ))
381
       )
382
       (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_state_in)
383
       (= Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x Flowchart7_Flowchart7_node.flowchart7_flowchart7__next_restart_in)
384
       )
385
  (Flowchart7_Flowchart7_node_step Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7_1
386
                                   Flowchart7_Flowchart7_node.TIC
387
                                   Flowchart7_Flowchart7_node.cent_1
388
                                   Flowchart7_Flowchart7_node.sec_1
389
                                   Flowchart7_Flowchart7_node.min_1
390
                                   Flowchart7_Flowchart7_node.idFlowchart7_Flowchart7
391
                                   Flowchart7_Flowchart7_node.cent
392
                                   Flowchart7_Flowchart7_node.sec
393
                                   Flowchart7_Flowchart7_node.min
394
                                   Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
395
                                   Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
396
                                   Flowchart7_Flowchart7_node.ni_4._arrow._first_c
397
                                   Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x
398
                                   Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x
399
                                   Flowchart7_Flowchart7_node.ni_4._arrow._first_x)
400
))
401

    
402
; Flowchart7_Flowchart7
403
(declare-var Flowchart7_Flowchart7.TIC Bool)
404
(declare-var Flowchart7_Flowchart7.cent Int)
405
(declare-var Flowchart7_Flowchart7.sec Int)
406
(declare-var Flowchart7_Flowchart7.min Int)
407
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c Int)
408
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c Int)
409
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c Int)
410
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c Int)
411
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c Bool)
412
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c flowchart7_flowchart7__type)
413
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c Bool)
414
(declare-var Flowchart7_Flowchart7.ni_3._arrow._first_c Bool)
415
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m Int)
416
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m Int)
417
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m Int)
418
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m Int)
419
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Bool)
420
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m flowchart7_flowchart7__type)
421
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m Bool)
422
(declare-var Flowchart7_Flowchart7.ni_3._arrow._first_m Bool)
423
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x Int)
424
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x Int)
425
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x Int)
426
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x Int)
427
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x Bool)
428
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x flowchart7_flowchart7__type)
429
(declare-var Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x Bool)
430
(declare-var Flowchart7_Flowchart7.ni_3._arrow._first_x Bool)
431
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_1 Int)
432
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_2 Int)
433
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_3 Int)
434
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_4 Int)
435
(declare-var Flowchart7_Flowchart7.__Flowchart7_Flowchart7_5 Bool)
436
(declare-var Flowchart7_Flowchart7.cent_1 Int)
437
(declare-var Flowchart7_Flowchart7.idFlowchart7_Flowchart7 Int)
438
(declare-var Flowchart7_Flowchart7.idFlowchart7_Flowchart7_1 Int)
439
(declare-var Flowchart7_Flowchart7.min_1 Int)
440
(declare-var Flowchart7_Flowchart7.sec_1 Int)
441
(declare-rel Flowchart7_Flowchart7_reset (Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool))
442
(declare-rel Flowchart7_Flowchart7_step (Bool Int Int Int Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool))
443

    
444
(rule (=> 
445
  (and 
446
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c)
447
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c)
448
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c)
449
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c)
450
       (= Flowchart7_Flowchart7.ni_3._arrow._first_m true)
451
       (Flowchart7_Flowchart7_node_reset Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
452
                                         Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
453
                                         Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
454
                                         Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
455
                                         Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
456
                                         Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m)
457
  )
458
  (Flowchart7_Flowchart7_reset Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c
459
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c
460
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c
461
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c
462
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
463
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
464
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
465
                               Flowchart7_Flowchart7.ni_3._arrow._first_c
466
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m
467
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m
468
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m
469
                               Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m
470
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
471
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
472
                               Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m
473
                               Flowchart7_Flowchart7.ni_3._arrow._first_m)
474
))
475

    
476
(rule (=> 
477
  (and (= Flowchart7_Flowchart7.ni_3._arrow._first_m Flowchart7_Flowchart7.ni_3._arrow._first_c)
478
       (and (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_5 (ite Flowchart7_Flowchart7.ni_3._arrow._first_m true false))
479
            (= Flowchart7_Flowchart7.ni_3._arrow._first_x false))
480
       (and (or (not (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_5 false))
481
               (and (= Flowchart7_Flowchart7.sec_1 Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c)
482
                    (= Flowchart7_Flowchart7.min_1 Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c)
483
                    (= Flowchart7_Flowchart7.idFlowchart7_Flowchart7_1 Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c)
484
                    (= Flowchart7_Flowchart7.cent_1 Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c)
485
                    ))
486
            (or (not (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_5 true))
487
               (and (= Flowchart7_Flowchart7.sec_1 0)
488
                    (= Flowchart7_Flowchart7.min_1 0)
489
                    (= Flowchart7_Flowchart7.idFlowchart7_Flowchart7_1 0)
490
                    (= Flowchart7_Flowchart7.cent_1 0)
491
                    ))
492
       )
493
       (and (= Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c)
494
            (= Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c)
495
            (= Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c)
496
            )
497
       (Flowchart7_Flowchart7_node_step Flowchart7_Flowchart7.idFlowchart7_Flowchart7_1
498
                                        Flowchart7_Flowchart7.TIC
499
                                        Flowchart7_Flowchart7.cent_1
500
                                        Flowchart7_Flowchart7.sec_1
501
                                        Flowchart7_Flowchart7.min_1
502
                                        Flowchart7_Flowchart7.__Flowchart7_Flowchart7_1
503
                                        Flowchart7_Flowchart7.__Flowchart7_Flowchart7_2
504
                                        Flowchart7_Flowchart7.__Flowchart7_Flowchart7_3
505
                                        Flowchart7_Flowchart7.__Flowchart7_Flowchart7_4
506
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
507
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
508
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m
509
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x
510
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x
511
                                        Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x)
512
       (and (or (not (= Flowchart7_Flowchart7.TIC false))
513
               (and (= Flowchart7_Flowchart7.sec Flowchart7_Flowchart7.sec_1)
514
                    (= Flowchart7_Flowchart7.min Flowchart7_Flowchart7.min_1)
515
                    (= Flowchart7_Flowchart7.idFlowchart7_Flowchart7 Flowchart7_Flowchart7.idFlowchart7_Flowchart7_1)
516
                    (= Flowchart7_Flowchart7.cent Flowchart7_Flowchart7.cent_1)
517
                    ))
518
            (or (not (= Flowchart7_Flowchart7.TIC true))
519
               (and (= Flowchart7_Flowchart7.sec Flowchart7_Flowchart7.__Flowchart7_Flowchart7_3)
520
                    (= Flowchart7_Flowchart7.min Flowchart7_Flowchart7.__Flowchart7_Flowchart7_4)
521
                    (= Flowchart7_Flowchart7.idFlowchart7_Flowchart7 Flowchart7_Flowchart7.__Flowchart7_Flowchart7_1)
522
                    (= Flowchart7_Flowchart7.cent Flowchart7_Flowchart7.__Flowchart7_Flowchart7_2)
523
                    ))
524
       )
525
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x Flowchart7_Flowchart7.cent)
526
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x Flowchart7_Flowchart7.sec)
527
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x Flowchart7_Flowchart7.min)
528
       (= Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x Flowchart7_Flowchart7.idFlowchart7_Flowchart7)
529
       )
530
  (Flowchart7_Flowchart7_step Flowchart7_Flowchart7.TIC
531
                              Flowchart7_Flowchart7.cent
532
                              Flowchart7_Flowchart7.sec
533
                              Flowchart7_Flowchart7.min
534
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c
535
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c
536
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c
537
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c
538
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
539
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
540
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
541
                              Flowchart7_Flowchart7.ni_3._arrow._first_c
542
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x
543
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x
544
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x
545
                              Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x
546
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x
547
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x
548
                              Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x
549
                              Flowchart7_Flowchart7.ni_3._arrow._first_x)
550
))
551

    
552
; Flowchart7
553
(declare-var Flowchart7.TIC_1_1 Real)
554
(declare-var Flowchart7.Out1_1_1 Int)
555
(declare-var Flowchart7.Out2_2_1 Int)
556
(declare-var Flowchart7.Out3_3_1 Int)
557
(declare-var Flowchart7.__Flowchart7_2_c Real)
558
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c Int)
559
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c Int)
560
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c Int)
561
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c Int)
562
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c Bool)
563
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c flowchart7_flowchart7__type)
564
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c Bool)
565
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_c Bool)
566
(declare-var Flowchart7.ni_1._arrow._first_c Bool)
567
(declare-var Flowchart7.__Flowchart7_2_m Real)
568
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m Int)
569
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m Int)
570
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m Int)
571
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m Int)
572
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Bool)
573
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m flowchart7_flowchart7__type)
574
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m Bool)
575
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_m Bool)
576
(declare-var Flowchart7.ni_1._arrow._first_m Bool)
577
(declare-var Flowchart7.__Flowchart7_2_x Real)
578
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x Int)
579
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x Int)
580
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x Int)
581
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x Int)
582
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x Bool)
583
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x flowchart7_flowchart7__type)
584
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x Bool)
585
(declare-var Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_x Bool)
586
(declare-var Flowchart7.ni_1._arrow._first_x Bool)
587
(declare-var Flowchart7.Flowchart7TIC_1_1_event Bool)
588
(declare-var Flowchart7.Flowchart7_1_1 Int)
589
(declare-var Flowchart7.Flowchart7_2_1 Int)
590
(declare-var Flowchart7.Flowchart7_3_1 Int)
591
(declare-var Flowchart7.__Flowchart7_1 Bool)
592
(declare-var Flowchart7.i_virtual_local Real)
593
(declare-rel Flowchart7_reset (Real Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Bool Real Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Bool))
594
(declare-rel Flowchart7_step (Real Int Int Int Real Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Bool Real Int Int Int Int Bool flowchart7_flowchart7__type Bool Bool Bool))
595

    
596
(rule (=> 
597
  (and 
598
       (= Flowchart7.__Flowchart7_2_m Flowchart7.__Flowchart7_2_c)
599
       (= Flowchart7.ni_1._arrow._first_m true)
600
       (Flowchart7_Flowchart7_reset Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c
601
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c
602
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c
603
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c
604
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
605
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
606
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
607
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_c
608
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m
609
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m
610
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m
611
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m
612
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
613
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
614
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m
615
                                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_m)
616
  )
617
  (Flowchart7_reset Flowchart7.__Flowchart7_2_c
618
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c
619
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c
620
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c
621
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c
622
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
623
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
624
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
625
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_c
626
                    Flowchart7.ni_1._arrow._first_c
627
                    Flowchart7.__Flowchart7_2_m
628
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m
629
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m
630
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m
631
                    Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m
632
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
633
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
634
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m
635
                    Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_m
636
                    Flowchart7.ni_1._arrow._first_m)
637
))
638

    
639
(rule (=> 
640
  (and (= Flowchart7.ni_1._arrow._first_m Flowchart7.ni_1._arrow._first_c)
641
       (and (= Flowchart7.__Flowchart7_1 (ite Flowchart7.ni_1._arrow._first_m true false))
642
            (= Flowchart7.ni_1._arrow._first_x false))
643
       (and (or (not (= Flowchart7.__Flowchart7_1 false))
644
               (and (= Flowchart7.i_virtual_local 1.)
645
                    (= Flowchart7.Flowchart7TIC_1_1_event (or (and (> Flowchart7.__Flowchart7_2_c 0.) (<= Flowchart7.TIC_1_1 0.)) (and (<= Flowchart7.__Flowchart7_2_c 0.) (> Flowchart7.TIC_1_1 0.))))
646
                    ))
647
            (or (not (= Flowchart7.__Flowchart7_1 true))
648
               (and (= Flowchart7.i_virtual_local 0.)
649
                    (= Flowchart7.Flowchart7TIC_1_1_event false)
650
                    ))
651
       )
652
       (= Flowchart7.__Flowchart7_2_x Flowchart7.TIC_1_1)
653
       (and (= Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c)
654
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c)
655
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c)
656
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c)
657
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c)
658
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c)
659
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c)
660
            (= Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_m Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_c)
661
            )
662
       (Flowchart7_Flowchart7_step Flowchart7.Flowchart7TIC_1_1_event
663
                                   Flowchart7.Flowchart7_1_1
664
                                   Flowchart7.Flowchart7_2_1
665
                                   Flowchart7.Flowchart7_3_1
666
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_m
667
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_m
668
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_m
669
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_m
670
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_m
671
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_m
672
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_m
673
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_m
674
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x
675
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x
676
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x
677
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x
678
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x
679
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x
680
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x
681
                                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_x)
682
       (= Flowchart7.Out3_3_1 Flowchart7.Flowchart7_3_1)
683
       (= Flowchart7.Out2_2_1 Flowchart7.Flowchart7_2_1)
684
       (= Flowchart7.Out1_1_1 Flowchart7.Flowchart7_1_1)
685
       )
686
  (Flowchart7_step Flowchart7.TIC_1_1
687
                   Flowchart7.Out1_1_1
688
                   Flowchart7.Out2_2_1
689
                   Flowchart7.Out3_3_1
690
                   Flowchart7.__Flowchart7_2_c
691
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_c
692
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_c
693
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_c
694
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_c
695
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_c
696
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_c
697
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_c
698
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_c
699
                   Flowchart7.ni_1._arrow._first_c
700
                   Flowchart7.__Flowchart7_2_x
701
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_6_x
702
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_7_x
703
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_8_x
704
                   Flowchart7.ni_0.Flowchart7_Flowchart7.__Flowchart7_Flowchart7_9_x
705
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_18_x
706
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.__Flowchart7_Flowchart7_node_19_x
707
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_2.Flowchart7_Flowchart7_node.ni_4._arrow._first_x
708
                   Flowchart7.ni_0.Flowchart7_Flowchart7.ni_3._arrow._first_x
709
                   Flowchart7.ni_1._arrow._first_x)
710
))
711