blob: 662b398591465b0a8bd192f458c07a6cf642195f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
(benchmark abz5_1400.smt
:source {
These benchmarks are used by the job-shop scheduling community and were
originaly from Andre Henning. They were translated into CVC format by Bruno
Dutertre and Leonardo de Moura. Contact demoura@csl.sri.com for more
information.
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
:status sat
:category { crafted }
:difficulty { 0 }
:logic QF_RDL
:extrafuns ((cvclZero Real))
:extrafuns ((Z Real))
:extrafuns ((t_0_0 Real))
:extrafuns ((t_0_1 Real))
:extrafuns ((t_0_2 Real))
:extrafuns ((t_0_3 Real))
:extrafuns ((t_0_4 Real))
:extrafuns ((t_0_5 Real))
:extrafuns ((t_0_6 Real))
:extrafuns ((t_0_7 Real))
:extrafuns ((t_0_8 Real))
:extrafuns ((t_0_9 Real))
:extrafuns ((t_1_0 Real))
:extrafuns ((t_1_1 Real))
:extrafuns ((t_1_2 Real))
:extrafuns ((t_1_3 Real))
:extrafuns ((t_1_4 Real))
:extrafuns ((t_1_5 Real))
:extrafuns ((t_1_6 Real))
:extrafuns ((t_1_7 Real))
:extrafuns ((t_1_8 Real))
:extrafuns ((t_1_9 Real))
:extrafuns ((t_2_0 Real))
:extrafuns ((t_2_1 Real))
:extrafuns ((t_2_2 Real))
:extrafuns ((t_2_3 Real))
:extrafuns ((t_2_4 Real))
:extrafuns ((t_2_5 Real))
:extrafuns ((t_2_6 Real))
:extrafuns ((t_2_7 Real))
:extrafuns ((t_2_8 Real))
:extrafuns ((t_2_9 Real))
:extrafuns ((t_3_0 Real))
:extrafuns ((t_3_1 Real))
:extrafuns ((t_3_2 Real))
:extrafuns ((t_3_3 Real))
:extrafuns ((t_3_4 Real))
:extrafuns ((t_3_5 Real))
:extrafuns ((t_3_6 Real))
:extrafuns ((t_3_7 Real))
:extrafuns ((t_3_8 Real))
:extrafuns ((t_3_9 Real))
:extrafuns ((t_4_0 Real))
:extrafuns ((t_4_1 Real))
:extrafuns ((t_4_2 Real))
:extrafuns ((t_4_3 Real))
:extrafuns ((t_4_4 Real))
:extrafuns ((t_4_5 Real))
:extrafuns ((t_4_6 Real))
:extrafuns ((t_4_7 Real))
:extrafuns ((t_4_8 Real))
:extrafuns ((t_4_9 Real))
:extrafuns ((t_5_0 Real))
:extrafuns ((t_5_1 Real))
:extrafuns ((t_5_2 Real))
:extrafuns ((t_5_3 Real))
:extrafuns ((t_5_4 Real))
:extrafuns ((t_5_5 Real))
:extrafuns ((t_5_6 Real))
:extrafuns ((t_5_7 Real))
:extrafuns ((t_5_8 Real))
:extrafuns ((t_5_9 Real))
:extrafuns ((t_6_0 Real))
:extrafuns ((t_6_1 Real))
:extrafuns ((t_6_2 Real))
:extrafuns ((t_6_3 Real))
:extrafuns ((t_6_4 Real))
:extrafuns ((t_6_5 Real))
:extrafuns ((t_6_6 Real))
:extrafuns ((t_6_7 Real))
:extrafuns ((t_6_8 Real))
:extrafuns ((t_6_9 Real))
:extrafuns ((t_7_0 Real))
:extrafuns ((t_7_1 Real))
:extrafuns ((t_7_2 Real))
:extrafuns ((t_7_3 Real))
:extrafuns ((t_7_4 Real))
:extrafuns ((t_7_5 Real))
:extrafuns ((t_7_6 Real))
:extrafuns ((t_7_7 Real))
:extrafuns ((t_7_8 Real))
:extrafuns ((t_7_9 Real))
:extrafuns ((t_8_0 Real))
:extrafuns ((t_8_1 Real))
:extrafuns ((t_8_2 Real))
:extrafuns ((t_8_3 Real))
:extrafuns ((t_8_4 Real))
:extrafuns ((t_8_5 Real))
:extrafuns ((t_8_6 Real))
:extrafuns ((t_8_7 Real))
:extrafuns ((t_8_8 Real))
:extrafuns ((t_8_9 Real))
:extrafuns ((t_9_0 Real))
:extrafuns ((t_9_1 Real))
:extrafuns ((t_9_2 Real))
:extrafuns ((t_9_3 Real))
:extrafuns ((t_9_4 Real))
:extrafuns ((t_9_5 Real))
:extrafuns ((t_9_6 Real))
:extrafuns ((t_9_7 Real))
:extrafuns ((t_9_8 Real))
:extrafuns ((t_9_9 Real))
:formula
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (- t_0_4 cvclZero) 0) (>= (- t_0_8 t_0_4) 88)) (>= (- t_0_6 t_0_8) 68)) (>= (- t_0_5 t_0_6) 94)) (>= (- t_0_1 t_0_5) 99)) (>= (- t_0_2 t_0_1) 67)) (>= (- t_0_9 t_0_2) 89)) (>= (- t_0_7 t_0_9) 77)) (>= (- t_0_0 t_0_7) 99)) (>= (- t_0_3 t_0_0) 86)) (>= (- Z t_0_3) 92)) (and (and (and (and (and (and (and (and (and (and (>= (- t_1_5 cvclZero) 0) (>= (- t_1_3 t_1_5) 72)) (>= (- t_1_6 t_1_3) 50)) (>= (- t_1_4 t_1_6) 69)) (>= (- t_1_2 t_1_4) 75)) (>= (- t_1_8 t_1_2) 94)) (>= (- t_1_0 t_1_8) 66)) (>= (- t_1_1 t_1_0) 92)) (>= (- t_1_7 t_1_1) 82)) (>= (- t_1_9 t_1_7) 94)) (>= (- Z t_1_9) 63))) (and (and (and (and (and (and (and (and (and (and (>= (- t_2_9 cvclZero) 0) (>= (- t_2_8 t_2_9) 83)) (>= (- t_2_0 t_2_8) 61)) (>= (- t_2_1 t_2_0) 83)) (>= (- t_2_6 t_2_1) 65)) (>= (- t_2_5 t_2_6) 64)) (>= (- t_2_7 t_2_5) 85)) (>= (- t_2_4 t_2_7) 78)) (>= (- t_2_2 t_2_4) 85)) (>= (- t_2_3 t_2_2) 55)) (>= (- Z t_2_3) 77))) (and (and (and (and (and (and (and (and (and (and (>= (- t_3_7 cvclZero) 0) (>= (- t_3_2 t_3_7) 94)) (>= (- t_3_1 t_3_2) 68)) (>= (- t_3_4 t_3_1) 61)) (>= (- t_3_3 t_3_4) 99)) (>= (- t_3_6 t_3_3) 54)) (>= (- t_3_5 t_3_6) 75)) (>= (- t_3_0 t_3_5) 66)) (>= (- t_3_9 t_3_0) 76)) (>= (- t_3_8 t_3_9) 63)) (>= (- Z t_3_8) 67))) (and (and (and (and (and (and (and (and (and (and (>= (- t_4_3 cvclZero) 0) (>= (- t_4_4 t_4_3) 69)) (>= (- t_4_9 t_4_4) 88)) (>= (- t_4_8 t_4_9) 82)) (>= (- t_4_0 t_4_8) 95)) (>= (- t_4_2 t_4_0) 99)) (>= (- t_4_6 t_4_2) 67)) (>= (- t_4_5 t_4_6) 95)) (>= (- t_4_7 t_4_5) 68)) (>= (- t_4_1 t_4_7) 67)) (>= (- Z t_4_1) 86))) (and (and (and (and (and (and (and (and (and (and (>= (- t_5_1 cvclZero) 0) (>= (- t_5_4 t_5_1) 99)) (>= (- t_5_5 t_5_4) 81)) (>= (- t_5_6 t_5_5) 64)) (>= (- t_5_8 t_5_6) 66)) (>= (- t_5_2 t_5_8) 80)) (>= (- t_5_7 t_5_2) 80)) (>= (- t_5_9 t_5_7) 69)) (>= (- t_5_3 t_5_9) 62)) (>= (- t_5_0 t_5_3) 79)) (>= (- Z t_5_0) 88))) (and (and (and (and (and (and (and (and (and (and (>= (- t_6_7 cvclZero) 0) (>= (- t_6_1 t_6_7) 50)) (>= (- t_6_4 t_6_1) 86)) (>= (- t_6_3 t_6_4) 97)) (>= (- t_6_0 t_6_3) 96)) (>= (- t_6_8 t_6_0) 95)) (>= (- t_6_2 t_6_8) 97)) (>= (- t_6_5 t_6_2) 66)) (>= (- t_6_6 t_6_5) 99)) (>= (- t_6_9 t_6_6) 52)) (>= (- Z t_6_9) 71))) (and (and (and (and (and (and (and (and (and (and (>= (- t_7_4 cvclZero) 0) (>= (- t_7_6 t_7_4) 98)) (>= (- t_7_3 t_7_6) 73)) (>= (- t_7_2 t_7_3) 82)) (>= (- t_7_1 t_7_2) 51)) (>= (- t_7_5 t_7_1) 71)) (>= (- t_7_7 t_7_5) 94)) (>= (- t_7_0 t_7_7) 85)) (>= (- t_7_8 t_7_0) 62)) (>= (- t_7_9 t_7_8) 95)) (>= (- Z t_7_9) 79))) (and (and (and (and (and (and (and (and (and (and (>= (- t_8_0 cvclZero) 0) (>= (- t_8_6 t_8_0) 94)) (>= (- t_8_3 t_8_6) 71)) (>= (- t_8_7 t_8_3) 81)) (>= (- t_8_1 t_8_7) 85)) (>= (- t_8_2 t_8_1) 66)) (>= (- t_8_4 t_8_2) 90)) (>= (- t_8_5 t_8_4) 76)) (>= (- t_8_8 t_8_5) 58)) (>= (- t_8_9 t_8_8) 93)) (>= (- Z t_8_9) 97))) (and (and (and (and (and (and (and (and (and (and (>= (- t_9_3 cvclZero) 0) (>= (- t_9_0 t_9_3) 50)) (>= (- t_9_1 t_9_0) 59)) (>= (- t_9_8 t_9_1) 82)) (>= (- t_9_7 t_9_8) 67)) (>= (- t_9_9 t_9_7) 56)) (>= (- t_9_6 t_9_9) 96)) (>= (- t_9_4 t_9_6) 58)) (>= (- t_9_5 t_9_4) 81)) (>= (- t_9_2 t_9_5) 59)) (>= (- Z t_9_2) 96))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_0 t_1_0) 92) (>= (- t_1_0 t_0_0) 86) )) (or (>= (- t_0_0 t_2_0) 83) (>= (- t_2_0 t_0_0) 86) )) (or (>= (- t_0_0 t_3_0) 76) (>= (- t_3_0 t_0_0) 86) )) (or (>= (- t_0_0 t_4_0) 99) (>= (- t_4_0 t_0_0) 86) )) (or (>= (- t_0_0 t_5_0) 88) (>= (- t_5_0 t_0_0) 86) )) (or (>= (- t_0_0 t_6_0) 95) (>= (- t_6_0 t_0_0) 86) )) (or (>= (- t_0_0 t_7_0) 62) (>= (- t_7_0 t_0_0) 86) )) (or (>= (- t_0_0 t_8_0) 94) (>= (- t_8_0 t_0_0) 86) )) (or (>= (- t_0_0 t_9_0) 59) (>= (- t_9_0 t_0_0) 86) )) (or (>= (- t_1_0 t_2_0) 83) (>= (- t_2_0 t_1_0) 92) )) (or (>= (- t_1_0 t_3_0) 76) (>= (- t_3_0 t_1_0) 92) )) (or (>= (- t_1_0 t_4_0) 99) (>= (- t_4_0 t_1_0) 92) )) (or (>= (- t_1_0 t_5_0) 88) (>= (- t_5_0 t_1_0) 92) )) (or (>= (- t_1_0 t_6_0) 95) (>= (- t_6_0 t_1_0) 92) )) (or (>= (- t_1_0 t_7_0) 62) (>= (- t_7_0 t_1_0) 92) )) (or (>= (- t_1_0 t_8_0) 94) (>= (- t_8_0 t_1_0) 92) )) (or (>= (- t_1_0 t_9_0) 59) (>= (- t_9_0 t_1_0) 92) )) (or (>= (- t_2_0 t_3_0) 76) (>= (- t_3_0 t_2_0) 83) )) (or (>= (- t_2_0 t_4_0) 99) (>= (- t_4_0 t_2_0) 83) )) (or (>= (- t_2_0 t_5_0) 88) (>= (- t_5_0 t_2_0) 83) )) (or (>= (- t_2_0 t_6_0) 95) (>= (- t_6_0 t_2_0) 83) )) (or (>= (- t_2_0 t_7_0) 62) (>= (- t_7_0 t_2_0) 83) )) (or (>= (- t_2_0 t_8_0) 94) (>= (- t_8_0 t_2_0) 83) )) (or (>= (- t_2_0 t_9_0) 59) (>= (- t_9_0 t_2_0) 83) )) (or (>= (- t_3_0 t_4_0) 99) (>= (- t_4_0 t_3_0) 76) )) (or (>= (- t_3_0 t_5_0) 88) (>= (- t_5_0 t_3_0) 76) )) (or (>= (- t_3_0 t_6_0) 95) (>= (- t_6_0 t_3_0) 76) )) (or (>= (- t_3_0 t_7_0) 62) (>= (- t_7_0 t_3_0) 76) )) (or (>= (- t_3_0 t_8_0) 94) (>= (- t_8_0 t_3_0) 76) )) (or (>= (- t_3_0 t_9_0) 59) (>= (- t_9_0 t_3_0) 76) )) (or (>= (- t_4_0 t_5_0) 88) (>= (- t_5_0 t_4_0) 99) )) (or (>= (- t_4_0 t_6_0) 95) (>= (- t_6_0 t_4_0) 99) )) (or (>= (- t_4_0 t_7_0) 62) (>= (- t_7_0 t_4_0) 99) )) (or (>= (- t_4_0 t_8_0) 94) (>= (- t_8_0 t_4_0) 99) )) (or (>= (- t_4_0 t_9_0) 59) (>= (- t_9_0 t_4_0) 99) )) (or (>= (- t_5_0 t_6_0) 95) (>= (- t_6_0 t_5_0) 88) )) (or (>= (- t_5_0 t_7_0) 62) (>= (- t_7_0 t_5_0) 88) )) (or (>= (- t_5_0 t_8_0) 94) (>= (- t_8_0 t_5_0) 88) )) (or (>= (- t_5_0 t_9_0) 59) (>= (- t_9_0 t_5_0) 88) )) (or (>= (- t_6_0 t_7_0) 62) (>= (- t_7_0 t_6_0) 95) )) (or (>= (- t_6_0 t_8_0) 94) (>= (- t_8_0 t_6_0) 95) )) (or (>= (- t_6_0 t_9_0) 59) (>= (- t_9_0 t_6_0) 95) )) (or (>= (- t_7_0 t_8_0) 94) (>= (- t_8_0 t_7_0) 62) )) (or (>= (- t_7_0 t_9_0) 59) (>= (- t_9_0 t_7_0) 62) )) (or (>= (- t_8_0 t_9_0) 59) (>= (- t_9_0 t_8_0) 94) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_1 t_1_1) 82) (>= (- t_1_1 t_0_1) 67) )) (or (>= (- t_0_1 t_2_1) 65) (>= (- t_2_1 t_0_1) 67) )) (or (>= (- t_0_1 t_3_1) 61) (>= (- t_3_1 t_0_1) 67) )) (or (>= (- t_0_1 t_4_1) 86) (>= (- t_4_1 t_0_1) 67) )) (or (>= (- t_0_1 t_5_1) 99) (>= (- t_5_1 t_0_1) 67) )) (or (>= (- t_0_1 t_6_1) 86) (>= (- t_6_1 t_0_1) 67) )) (or (>= (- t_0_1 t_7_1) 71) (>= (- t_7_1 t_0_1) 67) )) (or (>= (- t_0_1 t_8_1) 66) (>= (- t_8_1 t_0_1) 67) )) (or (>= (- t_0_1 t_9_1) 82) (>= (- t_9_1 t_0_1) 67) )) (or (>= (- t_1_1 t_2_1) 65) (>= (- t_2_1 t_1_1) 82) )) (or (>= (- t_1_1 t_3_1) 61) (>= (- t_3_1 t_1_1) 82) )) (or (>= (- t_1_1 t_4_1) 86) (>= (- t_4_1 t_1_1) 82) )) (or (>= (- t_1_1 t_5_1) 99) (>= (- t_5_1 t_1_1) 82) )) (or (>= (- t_1_1 t_6_1) 86) (>= (- t_6_1 t_1_1) 82) )) (or (>= (- t_1_1 t_7_1) 71) (>= (- t_7_1 t_1_1) 82) )) (or (>= (- t_1_1 t_8_1) 66) (>= (- t_8_1 t_1_1) 82) )) (or (>= (- t_1_1 t_9_1) 82) (>= (- t_9_1 t_1_1) 82) )) (or (>= (- t_2_1 t_3_1) 61) (>= (- t_3_1 t_2_1) 65) )) (or (>= (- t_2_1 t_4_1) 86) (>= (- t_4_1 t_2_1) 65) )) (or (>= (- t_2_1 t_5_1) 99) (>= (- t_5_1 t_2_1) 65) )) (or (>= (- t_2_1 t_6_1) 86) (>= (- t_6_1 t_2_1) 65) )) (or (>= (- t_2_1 t_7_1) 71) (>= (- t_7_1 t_2_1) 65) )) (or (>= (- t_2_1 t_8_1) 66) (>= (- t_8_1 t_2_1) 65) )) (or (>= (- t_2_1 t_9_1) 82) (>= (- t_9_1 t_2_1) 65) )) (or (>= (- t_3_1 t_4_1) 86) (>= (- t_4_1 t_3_1) 61) )) (or (>= (- t_3_1 t_5_1) 99) (>= (- t_5_1 t_3_1) 61) )) (or (>= (- t_3_1 t_6_1) 86) (>= (- t_6_1 t_3_1) 61) )) (or (>= (- t_3_1 t_7_1) 71) (>= (- t_7_1 t_3_1) 61) )) (or (>= (- t_3_1 t_8_1) 66) (>= (- t_8_1 t_3_1) 61) )) (or (>= (- t_3_1 t_9_1) 82) (>= (- t_9_1 t_3_1) 61) )) (or (>= (- t_4_1 t_5_1) 99) (>= (- t_5_1 t_4_1) 86) )) (or (>= (- t_4_1 t_6_1) 86) (>= (- t_6_1 t_4_1) 86) )) (or (>= (- t_4_1 t_7_1) 71) (>= (- t_7_1 t_4_1) 86) )) (or (>= (- t_4_1 t_8_1) 66) (>= (- t_8_1 t_4_1) 86) )) (or (>= (- t_4_1 t_9_1) 82) (>= (- t_9_1 t_4_1) 86) )) (or (>= (- t_5_1 t_6_1) 86) (>= (- t_6_1 t_5_1) 99) )) (or (>= (- t_5_1 t_7_1) 71) (>= (- t_7_1 t_5_1) 99) )) (or (>= (- t_5_1 t_8_1) 66) (>= (- t_8_1 t_5_1) 99) )) (or (>= (- t_5_1 t_9_1) 82) (>= (- t_9_1 t_5_1) 99) )) (or (>= (- t_6_1 t_7_1) 71) (>= (- t_7_1 t_6_1) 86) )) (or (>= (- t_6_1 t_8_1) 66) (>= (- t_8_1 t_6_1) 86) )) (or (>= (- t_6_1 t_9_1) 82) (>= (- t_9_1 t_6_1) 86) )) (or (>= (- t_7_1 t_8_1) 66) (>= (- t_8_1 t_7_1) 71) )) (or (>= (- t_7_1 t_9_1) 82) (>= (- t_9_1 t_7_1) 71) )) (or (>= (- t_8_1 t_9_1) 82) (>= (- t_9_1 t_8_1) 66) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_2 t_1_2) 94) (>= (- t_1_2 t_0_2) 89) )) (or (>= (- t_0_2 t_2_2) 55) (>= (- t_2_2 t_0_2) 89) )) (or (>= (- t_0_2 t_3_2) 68) (>= (- t_3_2 t_0_2) 89) )) (or (>= (- t_0_2 t_4_2) 67) (>= (- t_4_2 t_0_2) 89) )) (or (>= (- t_0_2 t_5_2) 80) (>= (- t_5_2 t_0_2) 89) )) (or (>= (- t_0_2 t_6_2) 66) (>= (- t_6_2 t_0_2) 89) )) (or (>= (- t_0_2 t_7_2) 51) (>= (- t_7_2 t_0_2) 89) )) (or (>= (- t_0_2 t_8_2) 90) (>= (- t_8_2 t_0_2) 89) )) (or (>= (- t_0_2 t_9_2) 96) (>= (- t_9_2 t_0_2) 89) )) (or (>= (- t_1_2 t_2_2) 55) (>= (- t_2_2 t_1_2) 94) )) (or (>= (- t_1_2 t_3_2) 68) (>= (- t_3_2 t_1_2) 94) )) (or (>= (- t_1_2 t_4_2) 67) (>= (- t_4_2 t_1_2) 94) )) (or (>= (- t_1_2 t_5_2) 80) (>= (- t_5_2 t_1_2) 94) )) (or (>= (- t_1_2 t_6_2) 66) (>= (- t_6_2 t_1_2) 94) )) (or (>= (- t_1_2 t_7_2) 51) (>= (- t_7_2 t_1_2) 94) )) (or (>= (- t_1_2 t_8_2) 90) (>= (- t_8_2 t_1_2) 94) )) (or (>= (- t_1_2 t_9_2) 96) (>= (- t_9_2 t_1_2) 94) )) (or (>= (- t_2_2 t_3_2) 68) (>= (- t_3_2 t_2_2) 55) )) (or (>= (- t_2_2 t_4_2) 67) (>= (- t_4_2 t_2_2) 55) )) (or (>= (- t_2_2 t_5_2) 80) (>= (- t_5_2 t_2_2) 55) )) (or (>= (- t_2_2 t_6_2) 66) (>= (- t_6_2 t_2_2) 55) )) (or (>= (- t_2_2 t_7_2) 51) (>= (- t_7_2 t_2_2) 55) )) (or (>= (- t_2_2 t_8_2) 90) (>= (- t_8_2 t_2_2) 55) )) (or (>= (- t_2_2 t_9_2) 96) (>= (- t_9_2 t_2_2) 55) )) (or (>= (- t_3_2 t_4_2) 67) (>= (- t_4_2 t_3_2) 68) )) (or (>= (- t_3_2 t_5_2) 80) (>= (- t_5_2 t_3_2) 68) )) (or (>= (- t_3_2 t_6_2) 66) (>= (- t_6_2 t_3_2) 68) )) (or (>= (- t_3_2 t_7_2) 51) (>= (- t_7_2 t_3_2) 68) )) (or (>= (- t_3_2 t_8_2) 90) (>= (- t_8_2 t_3_2) 68) )) (or (>= (- t_3_2 t_9_2) 96) (>= (- t_9_2 t_3_2) 68) )) (or (>= (- t_4_2 t_5_2) 80) (>= (- t_5_2 t_4_2) 67) )) (or (>= (- t_4_2 t_6_2) 66) (>= (- t_6_2 t_4_2) 67) )) (or (>= (- t_4_2 t_7_2) 51) (>= (- t_7_2 t_4_2) 67) )) (or (>= (- t_4_2 t_8_2) 90) (>= (- t_8_2 t_4_2) 67) )) (or (>= (- t_4_2 t_9_2) 96) (>= (- t_9_2 t_4_2) 67) )) (or (>= (- t_5_2 t_6_2) 66) (>= (- t_6_2 t_5_2) 80) )) (or (>= (- t_5_2 t_7_2) 51) (>= (- t_7_2 t_5_2) 80) )) (or (>= (- t_5_2 t_8_2) 90) (>= (- t_8_2 t_5_2) 80) )) (or (>= (- t_5_2 t_9_2) 96) (>= (- t_9_2 t_5_2) 80) )) (or (>= (- t_6_2 t_7_2) 51) (>= (- t_7_2 t_6_2) 66) )) (or (>= (- t_6_2 t_8_2) 90) (>= (- t_8_2 t_6_2) 66) )) (or (>= (- t_6_2 t_9_2) 96) (>= (- t_9_2 t_6_2) 66) )) (or (>= (- t_7_2 t_8_2) 90) (>= (- t_8_2 t_7_2) 51) )) (or (>= (- t_7_2 t_9_2) 96) (>= (- t_9_2 t_7_2) 51) )) (or (>= (- t_8_2 t_9_2) 96) (>= (- t_9_2 t_8_2) 90) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_3 t_1_3) 50) (>= (- t_1_3 t_0_3) 92) )) (or (>= (- t_0_3 t_2_3) 77) (>= (- t_2_3 t_0_3) 92) )) (or (>= (- t_0_3 t_3_3) 54) (>= (- t_3_3 t_0_3) 92) )) (or (>= (- t_0_3 t_4_3) 69) (>= (- t_4_3 t_0_3) 92) )) (or (>= (- t_0_3 t_5_3) 79) (>= (- t_5_3 t_0_3) 92) )) (or (>= (- t_0_3 t_6_3) 96) (>= (- t_6_3 t_0_3) 92) )) (or (>= (- t_0_3 t_7_3) 82) (>= (- t_7_3 t_0_3) 92) )) (or (>= (- t_0_3 t_8_3) 81) (>= (- t_8_3 t_0_3) 92) )) (or (>= (- t_0_3 t_9_3) 50) (>= (- t_9_3 t_0_3) 92) )) (or (>= (- t_1_3 t_2_3) 77) (>= (- t_2_3 t_1_3) 50) )) (or (>= (- t_1_3 t_3_3) 54) (>= (- t_3_3 t_1_3) 50) )) (or (>= (- t_1_3 t_4_3) 69) (>= (- t_4_3 t_1_3) 50) )) (or (>= (- t_1_3 t_5_3) 79) (>= (- t_5_3 t_1_3) 50) )) (or (>= (- t_1_3 t_6_3) 96) (>= (- t_6_3 t_1_3) 50) )) (or (>= (- t_1_3 t_7_3) 82) (>= (- t_7_3 t_1_3) 50) )) (or (>= (- t_1_3 t_8_3) 81) (>= (- t_8_3 t_1_3) 50) )) (or (>= (- t_1_3 t_9_3) 50) (>= (- t_9_3 t_1_3) 50) )) (or (>= (- t_2_3 t_3_3) 54) (>= (- t_3_3 t_2_3) 77) )) (or (>= (- t_2_3 t_4_3) 69) (>= (- t_4_3 t_2_3) 77) )) (or (>= (- t_2_3 t_5_3) 79) (>= (- t_5_3 t_2_3) 77) )) (or (>= (- t_2_3 t_6_3) 96) (>= (- t_6_3 t_2_3) 77) )) (or (>= (- t_2_3 t_7_3) 82) (>= (- t_7_3 t_2_3) 77) )) (or (>= (- t_2_3 t_8_3) 81) (>= (- t_8_3 t_2_3) 77) )) (or (>= (- t_2_3 t_9_3) 50) (>= (- t_9_3 t_2_3) 77) )) (or (>= (- t_3_3 t_4_3) 69) (>= (- t_4_3 t_3_3) 54) )) (or (>= (- t_3_3 t_5_3) 79) (>= (- t_5_3 t_3_3) 54) )) (or (>= (- t_3_3 t_6_3) 96) (>= (- t_6_3 t_3_3) 54) )) (or (>= (- t_3_3 t_7_3) 82) (>= (- t_7_3 t_3_3) 54) )) (or (>= (- t_3_3 t_8_3) 81) (>= (- t_8_3 t_3_3) 54) )) (or (>= (- t_3_3 t_9_3) 50) (>= (- t_9_3 t_3_3) 54) )) (or (>= (- t_4_3 t_5_3) 79) (>= (- t_5_3 t_4_3) 69) )) (or (>= (- t_4_3 t_6_3) 96) (>= (- t_6_3 t_4_3) 69) )) (or (>= (- t_4_3 t_7_3) 82) (>= (- t_7_3 t_4_3) 69) )) (or (>= (- t_4_3 t_8_3) 81) (>= (- t_8_3 t_4_3) 69) )) (or (>= (- t_4_3 t_9_3) 50) (>= (- t_9_3 t_4_3) 69) )) (or (>= (- t_5_3 t_6_3) 96) (>= (- t_6_3 t_5_3) 79) )) (or (>= (- t_5_3 t_7_3) 82) (>= (- t_7_3 t_5_3) 79) )) (or (>= (- t_5_3 t_8_3) 81) (>= (- t_8_3 t_5_3) 79) )) (or (>= (- t_5_3 t_9_3) 50) (>= (- t_9_3 t_5_3) 79) )) (or (>= (- t_6_3 t_7_3) 82) (>= (- t_7_3 t_6_3) 96) )) (or (>= (- t_6_3 t_8_3) 81) (>= (- t_8_3 t_6_3) 96) )) (or (>= (- t_6_3 t_9_3) 50) (>= (- t_9_3 t_6_3) 96) )) (or (>= (- t_7_3 t_8_3) 81) (>= (- t_8_3 t_7_3) 82) )) (or (>= (- t_7_3 t_9_3) 50) (>= (- t_9_3 t_7_3) 82) )) (or (>= (- t_8_3 t_9_3) 50) (>= (- t_9_3 t_8_3) 81) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_4 t_1_4) 75) (>= (- t_1_4 t_0_4) 88) )) (or (>= (- t_0_4 t_2_4) 85) (>= (- t_2_4 t_0_4) 88) )) (or (>= (- t_0_4 t_3_4) 99) (>= (- t_3_4 t_0_4) 88) )) (or (>= (- t_0_4 t_4_4) 88) (>= (- t_4_4 t_0_4) 88) )) (or (>= (- t_0_4 t_5_4) 81) (>= (- t_5_4 t_0_4) 88) )) (or (>= (- t_0_4 t_6_4) 97) (>= (- t_6_4 t_0_4) 88) )) (or (>= (- t_0_4 t_7_4) 98) (>= (- t_7_4 t_0_4) 88) )) (or (>= (- t_0_4 t_8_4) 76) (>= (- t_8_4 t_0_4) 88) )) (or (>= (- t_0_4 t_9_4) 81) (>= (- t_9_4 t_0_4) 88) )) (or (>= (- t_1_4 t_2_4) 85) (>= (- t_2_4 t_1_4) 75) )) (or (>= (- t_1_4 t_3_4) 99) (>= (- t_3_4 t_1_4) 75) )) (or (>= (- t_1_4 t_4_4) 88) (>= (- t_4_4 t_1_4) 75) )) (or (>= (- t_1_4 t_5_4) 81) (>= (- t_5_4 t_1_4) 75) )) (or (>= (- t_1_4 t_6_4) 97) (>= (- t_6_4 t_1_4) 75) )) (or (>= (- t_1_4 t_7_4) 98) (>= (- t_7_4 t_1_4) 75) )) (or (>= (- t_1_4 t_8_4) 76) (>= (- t_8_4 t_1_4) 75) )) (or (>= (- t_1_4 t_9_4) 81) (>= (- t_9_4 t_1_4) 75) )) (or (>= (- t_2_4 t_3_4) 99) (>= (- t_3_4 t_2_4) 85) )) (or (>= (- t_2_4 t_4_4) 88) (>= (- t_4_4 t_2_4) 85) )) (or (>= (- t_2_4 t_5_4) 81) (>= (- t_5_4 t_2_4) 85) )) (or (>= (- t_2_4 t_6_4) 97) (>= (- t_6_4 t_2_4) 85) )) (or (>= (- t_2_4 t_7_4) 98) (>= (- t_7_4 t_2_4) 85) )) (or (>= (- t_2_4 t_8_4) 76) (>= (- t_8_4 t_2_4) 85) )) (or (>= (- t_2_4 t_9_4) 81) (>= (- t_9_4 t_2_4) 85) )) (or (>= (- t_3_4 t_4_4) 88) (>= (- t_4_4 t_3_4) 99) )) (or (>= (- t_3_4 t_5_4) 81) (>= (- t_5_4 t_3_4) 99) )) (or (>= (- t_3_4 t_6_4) 97) (>= (- t_6_4 t_3_4) 99) )) (or (>= (- t_3_4 t_7_4) 98) (>= (- t_7_4 t_3_4) 99) )) (or (>= (- t_3_4 t_8_4) 76) (>= (- t_8_4 t_3_4) 99) )) (or (>= (- t_3_4 t_9_4) 81) (>= (- t_9_4 t_3_4) 99) )) (or (>= (- t_4_4 t_5_4) 81) (>= (- t_5_4 t_4_4) 88) )) (or (>= (- t_4_4 t_6_4) 97) (>= (- t_6_4 t_4_4) 88) )) (or (>= (- t_4_4 t_7_4) 98) (>= (- t_7_4 t_4_4) 88) )) (or (>= (- t_4_4 t_8_4) 76) (>= (- t_8_4 t_4_4) 88) )) (or (>= (- t_4_4 t_9_4) 81) (>= (- t_9_4 t_4_4) 88) )) (or (>= (- t_5_4 t_6_4) 97) (>= (- t_6_4 t_5_4) 81) )) (or (>= (- t_5_4 t_7_4) 98) (>= (- t_7_4 t_5_4) 81) )) (or (>= (- t_5_4 t_8_4) 76) (>= (- t_8_4 t_5_4) 81) )) (or (>= (- t_5_4 t_9_4) 81) (>= (- t_9_4 t_5_4) 81) )) (or (>= (- t_6_4 t_7_4) 98) (>= (- t_7_4 t_6_4) 97) )) (or (>= (- t_6_4 t_8_4) 76) (>= (- t_8_4 t_6_4) 97) )) (or (>= (- t_6_4 t_9_4) 81) (>= (- t_9_4 t_6_4) 97) )) (or (>= (- t_7_4 t_8_4) 76) (>= (- t_8_4 t_7_4) 98) )) (or (>= (- t_7_4 t_9_4) 81) (>= (- t_9_4 t_7_4) 98) )) (or (>= (- t_8_4 t_9_4) 81) (>= (- t_9_4 t_8_4) 76) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_5 t_1_5) 72) (>= (- t_1_5 t_0_5) 99) )) (or (>= (- t_0_5 t_2_5) 85) (>= (- t_2_5 t_0_5) 99) )) (or (>= (- t_0_5 t_3_5) 66) (>= (- t_3_5 t_0_5) 99) )) (or (>= (- t_0_5 t_4_5) 68) (>= (- t_4_5 t_0_5) 99) )) (or (>= (- t_0_5 t_5_5) 64) (>= (- t_5_5 t_0_5) 99) )) (or (>= (- t_0_5 t_6_5) 99) (>= (- t_6_5 t_0_5) 99) )) (or (>= (- t_0_5 t_7_5) 94) (>= (- t_7_5 t_0_5) 99) )) (or (>= (- t_0_5 t_8_5) 58) (>= (- t_8_5 t_0_5) 99) )) (or (>= (- t_0_5 t_9_5) 59) (>= (- t_9_5 t_0_5) 99) )) (or (>= (- t_1_5 t_2_5) 85) (>= (- t_2_5 t_1_5) 72) )) (or (>= (- t_1_5 t_3_5) 66) (>= (- t_3_5 t_1_5) 72) )) (or (>= (- t_1_5 t_4_5) 68) (>= (- t_4_5 t_1_5) 72) )) (or (>= (- t_1_5 t_5_5) 64) (>= (- t_5_5 t_1_5) 72) )) (or (>= (- t_1_5 t_6_5) 99) (>= (- t_6_5 t_1_5) 72) )) (or (>= (- t_1_5 t_7_5) 94) (>= (- t_7_5 t_1_5) 72) )) (or (>= (- t_1_5 t_8_5) 58) (>= (- t_8_5 t_1_5) 72) )) (or (>= (- t_1_5 t_9_5) 59) (>= (- t_9_5 t_1_5) 72) )) (or (>= (- t_2_5 t_3_5) 66) (>= (- t_3_5 t_2_5) 85) )) (or (>= (- t_2_5 t_4_5) 68) (>= (- t_4_5 t_2_5) 85) )) (or (>= (- t_2_5 t_5_5) 64) (>= (- t_5_5 t_2_5) 85) )) (or (>= (- t_2_5 t_6_5) 99) (>= (- t_6_5 t_2_5) 85) )) (or (>= (- t_2_5 t_7_5) 94) (>= (- t_7_5 t_2_5) 85) )) (or (>= (- t_2_5 t_8_5) 58) (>= (- t_8_5 t_2_5) 85) )) (or (>= (- t_2_5 t_9_5) 59) (>= (- t_9_5 t_2_5) 85) )) (or (>= (- t_3_5 t_4_5) 68) (>= (- t_4_5 t_3_5) 66) )) (or (>= (- t_3_5 t_5_5) 64) (>= (- t_5_5 t_3_5) 66) )) (or (>= (- t_3_5 t_6_5) 99) (>= (- t_6_5 t_3_5) 66) )) (or (>= (- t_3_5 t_7_5) 94) (>= (- t_7_5 t_3_5) 66) )) (or (>= (- t_3_5 t_8_5) 58) (>= (- t_8_5 t_3_5) 66) )) (or (>= (- t_3_5 t_9_5) 59) (>= (- t_9_5 t_3_5) 66) )) (or (>= (- t_4_5 t_5_5) 64) (>= (- t_5_5 t_4_5) 68) )) (or (>= (- t_4_5 t_6_5) 99) (>= (- t_6_5 t_4_5) 68) )) (or (>= (- t_4_5 t_7_5) 94) (>= (- t_7_5 t_4_5) 68) )) (or (>= (- t_4_5 t_8_5) 58) (>= (- t_8_5 t_4_5) 68) )) (or (>= (- t_4_5 t_9_5) 59) (>= (- t_9_5 t_4_5) 68) )) (or (>= (- t_5_5 t_6_5) 99) (>= (- t_6_5 t_5_5) 64) )) (or (>= (- t_5_5 t_7_5) 94) (>= (- t_7_5 t_5_5) 64) )) (or (>= (- t_5_5 t_8_5) 58) (>= (- t_8_5 t_5_5) 64) )) (or (>= (- t_5_5 t_9_5) 59) (>= (- t_9_5 t_5_5) 64) )) (or (>= (- t_6_5 t_7_5) 94) (>= (- t_7_5 t_6_5) 99) )) (or (>= (- t_6_5 t_8_5) 58) (>= (- t_8_5 t_6_5) 99) )) (or (>= (- t_6_5 t_9_5) 59) (>= (- t_9_5 t_6_5) 99) )) (or (>= (- t_7_5 t_8_5) 58) (>= (- t_8_5 t_7_5) 94) )) (or (>= (- t_7_5 t_9_5) 59) (>= (- t_9_5 t_7_5) 94) )) (or (>= (- t_8_5 t_9_5) 59) (>= (- t_9_5 t_8_5) 58) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_6 t_1_6) 69) (>= (- t_1_6 t_0_6) 94) )) (or (>= (- t_0_6 t_2_6) 64) (>= (- t_2_6 t_0_6) 94) )) (or (>= (- t_0_6 t_3_6) 75) (>= (- t_3_6 t_0_6) 94) )) (or (>= (- t_0_6 t_4_6) 95) (>= (- t_4_6 t_0_6) 94) )) (or (>= (- t_0_6 t_5_6) 66) (>= (- t_5_6 t_0_6) 94) )) (or (>= (- t_0_6 t_6_6) 52) (>= (- t_6_6 t_0_6) 94) )) (or (>= (- t_0_6 t_7_6) 73) (>= (- t_7_6 t_0_6) 94) )) (or (>= (- t_0_6 t_8_6) 71) (>= (- t_8_6 t_0_6) 94) )) (or (>= (- t_0_6 t_9_6) 58) (>= (- t_9_6 t_0_6) 94) )) (or (>= (- t_1_6 t_2_6) 64) (>= (- t_2_6 t_1_6) 69) )) (or (>= (- t_1_6 t_3_6) 75) (>= (- t_3_6 t_1_6) 69) )) (or (>= (- t_1_6 t_4_6) 95) (>= (- t_4_6 t_1_6) 69) )) (or (>= (- t_1_6 t_5_6) 66) (>= (- t_5_6 t_1_6) 69) )) (or (>= (- t_1_6 t_6_6) 52) (>= (- t_6_6 t_1_6) 69) )) (or (>= (- t_1_6 t_7_6) 73) (>= (- t_7_6 t_1_6) 69) )) (or (>= (- t_1_6 t_8_6) 71) (>= (- t_8_6 t_1_6) 69) )) (or (>= (- t_1_6 t_9_6) 58) (>= (- t_9_6 t_1_6) 69) )) (or (>= (- t_2_6 t_3_6) 75) (>= (- t_3_6 t_2_6) 64) )) (or (>= (- t_2_6 t_4_6) 95) (>= (- t_4_6 t_2_6) 64) )) (or (>= (- t_2_6 t_5_6) 66) (>= (- t_5_6 t_2_6) 64) )) (or (>= (- t_2_6 t_6_6) 52) (>= (- t_6_6 t_2_6) 64) )) (or (>= (- t_2_6 t_7_6) 73) (>= (- t_7_6 t_2_6) 64) )) (or (>= (- t_2_6 t_8_6) 71) (>= (- t_8_6 t_2_6) 64) )) (or (>= (- t_2_6 t_9_6) 58) (>= (- t_9_6 t_2_6) 64) )) (or (>= (- t_3_6 t_4_6) 95) (>= (- t_4_6 t_3_6) 75) )) (or (>= (- t_3_6 t_5_6) 66) (>= (- t_5_6 t_3_6) 75) )) (or (>= (- t_3_6 t_6_6) 52) (>= (- t_6_6 t_3_6) 75) )) (or (>= (- t_3_6 t_7_6) 73) (>= (- t_7_6 t_3_6) 75) )) (or (>= (- t_3_6 t_8_6) 71) (>= (- t_8_6 t_3_6) 75) )) (or (>= (- t_3_6 t_9_6) 58) (>= (- t_9_6 t_3_6) 75) )) (or (>= (- t_4_6 t_5_6) 66) (>= (- t_5_6 t_4_6) 95) )) (or (>= (- t_4_6 t_6_6) 52) (>= (- t_6_6 t_4_6) 95) )) (or (>= (- t_4_6 t_7_6) 73) (>= (- t_7_6 t_4_6) 95) )) (or (>= (- t_4_6 t_8_6) 71) (>= (- t_8_6 t_4_6) 95) )) (or (>= (- t_4_6 t_9_6) 58) (>= (- t_9_6 t_4_6) 95) )) (or (>= (- t_5_6 t_6_6) 52) (>= (- t_6_6 t_5_6) 66) )) (or (>= (- t_5_6 t_7_6) 73) (>= (- t_7_6 t_5_6) 66) )) (or (>= (- t_5_6 t_8_6) 71) (>= (- t_8_6 t_5_6) 66) )) (or (>= (- t_5_6 t_9_6) 58) (>= (- t_9_6 t_5_6) 66) )) (or (>= (- t_6_6 t_7_6) 73) (>= (- t_7_6 t_6_6) 52) )) (or (>= (- t_6_6 t_8_6) 71) (>= (- t_8_6 t_6_6) 52) )) (or (>= (- t_6_6 t_9_6) 58) (>= (- t_9_6 t_6_6) 52) )) (or (>= (- t_7_6 t_8_6) 71) (>= (- t_8_6 t_7_6) 73) )) (or (>= (- t_7_6 t_9_6) 58) (>= (- t_9_6 t_7_6) 73) )) (or (>= (- t_8_6 t_9_6) 58) (>= (- t_9_6 t_8_6) 71) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_7 t_1_7) 94) (>= (- t_1_7 t_0_7) 99) )) (or (>= (- t_0_7 t_2_7) 78) (>= (- t_2_7 t_0_7) 99) )) (or (>= (- t_0_7 t_3_7) 94) (>= (- t_3_7 t_0_7) 99) )) (or (>= (- t_0_7 t_4_7) 67) (>= (- t_4_7 t_0_7) 99) )) (or (>= (- t_0_7 t_5_7) 69) (>= (- t_5_7 t_0_7) 99) )) (or (>= (- t_0_7 t_6_7) 50) (>= (- t_6_7 t_0_7) 99) )) (or (>= (- t_0_7 t_7_7) 85) (>= (- t_7_7 t_0_7) 99) )) (or (>= (- t_0_7 t_8_7) 85) (>= (- t_8_7 t_0_7) 99) )) (or (>= (- t_0_7 t_9_7) 56) (>= (- t_9_7 t_0_7) 99) )) (or (>= (- t_1_7 t_2_7) 78) (>= (- t_2_7 t_1_7) 94) )) (or (>= (- t_1_7 t_3_7) 94) (>= (- t_3_7 t_1_7) 94) )) (or (>= (- t_1_7 t_4_7) 67) (>= (- t_4_7 t_1_7) 94) )) (or (>= (- t_1_7 t_5_7) 69) (>= (- t_5_7 t_1_7) 94) )) (or (>= (- t_1_7 t_6_7) 50) (>= (- t_6_7 t_1_7) 94) )) (or (>= (- t_1_7 t_7_7) 85) (>= (- t_7_7 t_1_7) 94) )) (or (>= (- t_1_7 t_8_7) 85) (>= (- t_8_7 t_1_7) 94) )) (or (>= (- t_1_7 t_9_7) 56) (>= (- t_9_7 t_1_7) 94) )) (or (>= (- t_2_7 t_3_7) 94) (>= (- t_3_7 t_2_7) 78) )) (or (>= (- t_2_7 t_4_7) 67) (>= (- t_4_7 t_2_7) 78) )) (or (>= (- t_2_7 t_5_7) 69) (>= (- t_5_7 t_2_7) 78) )) (or (>= (- t_2_7 t_6_7) 50) (>= (- t_6_7 t_2_7) 78) )) (or (>= (- t_2_7 t_7_7) 85) (>= (- t_7_7 t_2_7) 78) )) (or (>= (- t_2_7 t_8_7) 85) (>= (- t_8_7 t_2_7) 78) )) (or (>= (- t_2_7 t_9_7) 56) (>= (- t_9_7 t_2_7) 78) )) (or (>= (- t_3_7 t_4_7) 67) (>= (- t_4_7 t_3_7) 94) )) (or (>= (- t_3_7 t_5_7) 69) (>= (- t_5_7 t_3_7) 94) )) (or (>= (- t_3_7 t_6_7) 50) (>= (- t_6_7 t_3_7) 94) )) (or (>= (- t_3_7 t_7_7) 85) (>= (- t_7_7 t_3_7) 94) )) (or (>= (- t_3_7 t_8_7) 85) (>= (- t_8_7 t_3_7) 94) )) (or (>= (- t_3_7 t_9_7) 56) (>= (- t_9_7 t_3_7) 94) )) (or (>= (- t_4_7 t_5_7) 69) (>= (- t_5_7 t_4_7) 67) )) (or (>= (- t_4_7 t_6_7) 50) (>= (- t_6_7 t_4_7) 67) )) (or (>= (- t_4_7 t_7_7) 85) (>= (- t_7_7 t_4_7) 67) )) (or (>= (- t_4_7 t_8_7) 85) (>= (- t_8_7 t_4_7) 67) )) (or (>= (- t_4_7 t_9_7) 56) (>= (- t_9_7 t_4_7) 67) )) (or (>= (- t_5_7 t_6_7) 50) (>= (- t_6_7 t_5_7) 69) )) (or (>= (- t_5_7 t_7_7) 85) (>= (- t_7_7 t_5_7) 69) )) (or (>= (- t_5_7 t_8_7) 85) (>= (- t_8_7 t_5_7) 69) )) (or (>= (- t_5_7 t_9_7) 56) (>= (- t_9_7 t_5_7) 69) )) (or (>= (- t_6_7 t_7_7) 85) (>= (- t_7_7 t_6_7) 50) )) (or (>= (- t_6_7 t_8_7) 85) (>= (- t_8_7 t_6_7) 50) )) (or (>= (- t_6_7 t_9_7) 56) (>= (- t_9_7 t_6_7) 50) )) (or (>= (- t_7_7 t_8_7) 85) (>= (- t_8_7 t_7_7) 85) )) (or (>= (- t_7_7 t_9_7) 56) (>= (- t_9_7 t_7_7) 85) )) (or (>= (- t_8_7 t_9_7) 56) (>= (- t_9_7 t_8_7) 85) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_8 t_1_8) 66) (>= (- t_1_8 t_0_8) 68) )) (or (>= (- t_0_8 t_2_8) 61) (>= (- t_2_8 t_0_8) 68) )) (or (>= (- t_0_8 t_3_8) 67) (>= (- t_3_8 t_0_8) 68) )) (or (>= (- t_0_8 t_4_8) 95) (>= (- t_4_8 t_0_8) 68) )) (or (>= (- t_0_8 t_5_8) 80) (>= (- t_5_8 t_0_8) 68) )) (or (>= (- t_0_8 t_6_8) 97) (>= (- t_6_8 t_0_8) 68) )) (or (>= (- t_0_8 t_7_8) 95) (>= (- t_7_8 t_0_8) 68) )) (or (>= (- t_0_8 t_8_8) 93) (>= (- t_8_8 t_0_8) 68) )) (or (>= (- t_0_8 t_9_8) 67) (>= (- t_9_8 t_0_8) 68) )) (or (>= (- t_1_8 t_2_8) 61) (>= (- t_2_8 t_1_8) 66) )) (or (>= (- t_1_8 t_3_8) 67) (>= (- t_3_8 t_1_8) 66) )) (or (>= (- t_1_8 t_4_8) 95) (>= (- t_4_8 t_1_8) 66) )) (or (>= (- t_1_8 t_5_8) 80) (>= (- t_5_8 t_1_8) 66) )) (or (>= (- t_1_8 t_6_8) 97) (>= (- t_6_8 t_1_8) 66) )) (or (>= (- t_1_8 t_7_8) 95) (>= (- t_7_8 t_1_8) 66) )) (or (>= (- t_1_8 t_8_8) 93) (>= (- t_8_8 t_1_8) 66) )) (or (>= (- t_1_8 t_9_8) 67) (>= (- t_9_8 t_1_8) 66) )) (or (>= (- t_2_8 t_3_8) 67) (>= (- t_3_8 t_2_8) 61) )) (or (>= (- t_2_8 t_4_8) 95) (>= (- t_4_8 t_2_8) 61) )) (or (>= (- t_2_8 t_5_8) 80) (>= (- t_5_8 t_2_8) 61) )) (or (>= (- t_2_8 t_6_8) 97) (>= (- t_6_8 t_2_8) 61) )) (or (>= (- t_2_8 t_7_8) 95) (>= (- t_7_8 t_2_8) 61) )) (or (>= (- t_2_8 t_8_8) 93) (>= (- t_8_8 t_2_8) 61) )) (or (>= (- t_2_8 t_9_8) 67) (>= (- t_9_8 t_2_8) 61) )) (or (>= (- t_3_8 t_4_8) 95) (>= (- t_4_8 t_3_8) 67) )) (or (>= (- t_3_8 t_5_8) 80) (>= (- t_5_8 t_3_8) 67) )) (or (>= (- t_3_8 t_6_8) 97) (>= (- t_6_8 t_3_8) 67) )) (or (>= (- t_3_8 t_7_8) 95) (>= (- t_7_8 t_3_8) 67) )) (or (>= (- t_3_8 t_8_8) 93) (>= (- t_8_8 t_3_8) 67) )) (or (>= (- t_3_8 t_9_8) 67) (>= (- t_9_8 t_3_8) 67) )) (or (>= (- t_4_8 t_5_8) 80) (>= (- t_5_8 t_4_8) 95) )) (or (>= (- t_4_8 t_6_8) 97) (>= (- t_6_8 t_4_8) 95) )) (or (>= (- t_4_8 t_7_8) 95) (>= (- t_7_8 t_4_8) 95) )) (or (>= (- t_4_8 t_8_8) 93) (>= (- t_8_8 t_4_8) 95) )) (or (>= (- t_4_8 t_9_8) 67) (>= (- t_9_8 t_4_8) 95) )) (or (>= (- t_5_8 t_6_8) 97) (>= (- t_6_8 t_5_8) 80) )) (or (>= (- t_5_8 t_7_8) 95) (>= (- t_7_8 t_5_8) 80) )) (or (>= (- t_5_8 t_8_8) 93) (>= (- t_8_8 t_5_8) 80) )) (or (>= (- t_5_8 t_9_8) 67) (>= (- t_9_8 t_5_8) 80) )) (or (>= (- t_6_8 t_7_8) 95) (>= (- t_7_8 t_6_8) 97) )) (or (>= (- t_6_8 t_8_8) 93) (>= (- t_8_8 t_6_8) 97) )) (or (>= (- t_6_8 t_9_8) 67) (>= (- t_9_8 t_6_8) 97) )) (or (>= (- t_7_8 t_8_8) 93) (>= (- t_8_8 t_7_8) 95) )) (or (>= (- t_7_8 t_9_8) 67) (>= (- t_9_8 t_7_8) 95) )) (or (>= (- t_8_8 t_9_8) 67) (>= (- t_9_8 t_8_8) 93) ))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and true (or (>= (- t_0_9 t_1_9) 63) (>= (- t_1_9 t_0_9) 77) )) (or (>= (- t_0_9 t_2_9) 83) (>= (- t_2_9 t_0_9) 77) )) (or (>= (- t_0_9 t_3_9) 63) (>= (- t_3_9 t_0_9) 77) )) (or (>= (- t_0_9 t_4_9) 82) (>= (- t_4_9 t_0_9) 77) )) (or (>= (- t_0_9 t_5_9) 62) (>= (- t_5_9 t_0_9) 77) )) (or (>= (- t_0_9 t_6_9) 71) (>= (- t_6_9 t_0_9) 77) )) (or (>= (- t_0_9 t_7_9) 79) (>= (- t_7_9 t_0_9) 77) )) (or (>= (- t_0_9 t_8_9) 97) (>= (- t_8_9 t_0_9) 77) )) (or (>= (- t_0_9 t_9_9) 96) (>= (- t_9_9 t_0_9) 77) )) (or (>= (- t_1_9 t_2_9) 83) (>= (- t_2_9 t_1_9) 63) )) (or (>= (- t_1_9 t_3_9) 63) (>= (- t_3_9 t_1_9) 63) )) (or (>= (- t_1_9 t_4_9) 82) (>= (- t_4_9 t_1_9) 63) )) (or (>= (- t_1_9 t_5_9) 62) (>= (- t_5_9 t_1_9) 63) )) (or (>= (- t_1_9 t_6_9) 71) (>= (- t_6_9 t_1_9) 63) )) (or (>= (- t_1_9 t_7_9) 79) (>= (- t_7_9 t_1_9) 63) )) (or (>= (- t_1_9 t_8_9) 97) (>= (- t_8_9 t_1_9) 63) )) (or (>= (- t_1_9 t_9_9) 96) (>= (- t_9_9 t_1_9) 63) )) (or (>= (- t_2_9 t_3_9) 63) (>= (- t_3_9 t_2_9) 83) )) (or (>= (- t_2_9 t_4_9) 82) (>= (- t_4_9 t_2_9) 83) )) (or (>= (- t_2_9 t_5_9) 62) (>= (- t_5_9 t_2_9) 83) )) (or (>= (- t_2_9 t_6_9) 71) (>= (- t_6_9 t_2_9) 83) )) (or (>= (- t_2_9 t_7_9) 79) (>= (- t_7_9 t_2_9) 83) )) (or (>= (- t_2_9 t_8_9) 97) (>= (- t_8_9 t_2_9) 83) )) (or (>= (- t_2_9 t_9_9) 96) (>= (- t_9_9 t_2_9) 83) )) (or (>= (- t_3_9 t_4_9) 82) (>= (- t_4_9 t_3_9) 63) )) (or (>= (- t_3_9 t_5_9) 62) (>= (- t_5_9 t_3_9) 63) )) (or (>= (- t_3_9 t_6_9) 71) (>= (- t_6_9 t_3_9) 63) )) (or (>= (- t_3_9 t_7_9) 79) (>= (- t_7_9 t_3_9) 63) )) (or (>= (- t_3_9 t_8_9) 97) (>= (- t_8_9 t_3_9) 63) )) (or (>= (- t_3_9 t_9_9) 96) (>= (- t_9_9 t_3_9) 63) )) (or (>= (- t_4_9 t_5_9) 62) (>= (- t_5_9 t_4_9) 82) )) (or (>= (- t_4_9 t_6_9) 71) (>= (- t_6_9 t_4_9) 82) )) (or (>= (- t_4_9 t_7_9) 79) (>= (- t_7_9 t_4_9) 82) )) (or (>= (- t_4_9 t_8_9) 97) (>= (- t_8_9 t_4_9) 82) )) (or (>= (- t_4_9 t_9_9) 96) (>= (- t_9_9 t_4_9) 82) )) (or (>= (- t_5_9 t_6_9) 71) (>= (- t_6_9 t_5_9) 62) )) (or (>= (- t_5_9 t_7_9) 79) (>= (- t_7_9 t_5_9) 62) )) (or (>= (- t_5_9 t_8_9) 97) (>= (- t_8_9 t_5_9) 62) )) (or (>= (- t_5_9 t_9_9) 96) (>= (- t_9_9 t_5_9) 62) )) (or (>= (- t_6_9 t_7_9) 79) (>= (- t_7_9 t_6_9) 71) )) (or (>= (- t_6_9 t_8_9) 97) (>= (- t_8_9 t_6_9) 71) )) (or (>= (- t_6_9 t_9_9) 96) (>= (- t_9_9 t_6_9) 71) )) (or (>= (- t_7_9 t_8_9) 97) (>= (- t_8_9 t_7_9) 79) )) (or (>= (- t_7_9 t_9_9) 96) (>= (- t_9_9 t_7_9) 79) )) (or (>= (- t_8_9 t_9_9) 96) (>= (- t_9_9 t_8_9) 97) ))) (<= (- Z cvclZero) 1400))
)
|
