(set-option :incremental false)
(set-info :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")
(set-info :status sat)
(set-info :category "crafted")
(set-info :difficulty "0")
(set-logic QF_RDL)
(declare-fun cvclZero () Real)
(declare-fun Z () Real)
(declare-fun t_0_0 () Real)
(declare-fun t_0_1 () Real)
(declare-fun t_0_2 () Real)
(declare-fun t_0_3 () Real)
(declare-fun t_0_4 () Real)
(declare-fun t_0_5 () Real)
(declare-fun t_0_6 () Real)
(declare-fun t_0_7 () Real)
(declare-fun t_0_8 () Real)
(declare-fun t_0_9 () Real)
(declare-fun t_1_0 () Real)
(declare-fun t_1_1 () Real)
(declare-fun t_1_2 () Real)
(declare-fun t_1_3 () Real)
(declare-fun t_1_4 () Real)
(declare-fun t_1_5 () Real)
(declare-fun t_1_6 () Real)
(declare-fun t_1_7 () Real)
(declare-fun t_1_8 () Real)
(declare-fun t_1_9 () Real)
(declare-fun t_2_0 () Real)
(declare-fun t_2_1 () Real)
(declare-fun t_2_2 () Real)
(declare-fun t_2_3 () Real)
(declare-fun t_2_4 () Real)
(declare-fun t_2_5 () Real)
(declare-fun t_2_6 () Real)
(declare-fun t_2_7 () Real)
(declare-fun t_2_8 () Real)
(declare-fun t_2_9 () Real)
(declare-fun t_3_0 () Real)
(declare-fun t_3_1 () Real)
(declare-fun t_3_2 () Real)
(declare-fun t_3_3 () Real)
(declare-fun t_3_4 () Real)
(declare-fun t_3_5 () Real)
(declare-fun t_3_6 () Real)
(declare-fun t_3_7 () Real)
(declare-fun t_3_8 () Real)
(declare-fun t_3_9 () Real)
(declare-fun t_4_0 () Real)
(declare-fun t_4_1 () Real)
(declare-fun t_4_2 () Real)
(declare-fun t_4_3 () Real)
(declare-fun t_4_4 () Real)
(declare-fun t_4_5 () Real)
(declare-fun t_4_6 () Real)
(declare-fun t_4_7 () Real)
(declare-fun t_4_8 () Real)
(declare-fun t_4_9 () Real)
(declare-fun t_5_0 () Real)
(declare-fun t_5_1 () Real)
(declare-fun t_5_2 () Real)
(declare-fun t_5_3 () Real)
(declare-fun t_5_4 () Real)
(declare-fun t_5_5 () Real)
(declare-fun t_5_6 () Real)
(declare-fun t_5_7 () Real)
(declare-fun t_5_8 () Real)
(declare-fun t_5_9 () Real)
(declare-fun t_6_0 () Real)
(declare-fun t_6_1 () Real)
(declare-fun t_6_2 () Real)
(declare-fun t_6_3 () Real)
(declare-fun t_6_4 () Real)
(declare-fun t_6_5 () Real)
(declare-fun t_6_6 () Real)
(declare-fun t_6_7 () Real)
(declare-fun t_6_8 () Real)
(declare-fun t_6_9 () Real)
(declare-fun t_7_0 () Real)
(declare-fun t_7_1 () Real)
(declare-fun t_7_2 () Real)
(declare-fun t_7_3 () Real)
(declare-fun t_7_4 () Real)
(declare-fun t_7_5 () Real)
(declare-fun t_7_6 () Real)
(declare-fun t_7_7 () Real)
(declare-fun t_7_8 () Real)
(declare-fun t_7_9 () Real)
(declare-fun t_8_0 () Real)
(declare-fun t_8_1 () Real)
(declare-fun t_8_2 () Real)
(declare-fun t_8_3 () Real)
(declare-fun t_8_4 () Real)
(declare-fun t_8_5 () Real)
(declare-fun t_8_6 () Real)
(declare-fun t_8_7 () Real)
(declare-fun t_8_8 () Real)
(declare-fun t_8_9 () Real)
(declare-fun t_9_0 () Real)
(declare-fun t_9_1 () Real)
(declare-fun t_9_2 () Real)
(declare-fun t_9_3 () Real)
(declare-fun t_9_4 () Real)
(declare-fun t_9_5 () Real)
(declare-fun t_9_6 () Real)
(declare-fun t_9_7 () Real)
(declare-fun t_9_8 () Real)
(declare-fun t_9_9 () Real)
(check-sat-assuming ( (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.0) (>= (- t_0_8 t_0_4) 88.0)) (>= (- t_0_6 t_0_8) 68.0)) (>= (- t_0_5 t_0_6) 94.0)) (>= (- t_0_1 t_0_5) 99.0)) (>= (- t_0_2 t_0_1) 67.0)) (>= (- t_0_9 t_0_2) 89.0)) (>= (- t_0_7 t_0_9) 77.0)) (>= (- t_0_0 t_0_7) 99.0)) (>= (- t_0_3 t_0_0) 86.0)) (>= (- Z t_0_3) 92.0)) (and (and (and (and (and (and (and (and (and (and (>= (- t_1_5 cvclZero) 0.0) (>= (- t_1_3 t_1_5) 72.0)) (>= (- t_1_6 t_1_3) 50.0)) (>= (- t_1_4 t_1_6) 69.0)) (>= (- t_1_2 t_1_4) 75.0)) (>= (- t_1_8 t_1_2) 94.0)) (>= (- t_1_0 t_1_8) 66.0)) (>= (- t_1_1 t_1_0) 92.0)) (>= (- t_1_7 t_1_1) 82.0)) (>= (- t_1_9 t_1_7) 94.0)) (>= (- Z t_1_9) 63.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_2_9 cvclZero) 0.0) (>= (- t_2_8 t_2_9) 83.0)) (>= (- t_2_0 t_2_8) 61.0)) (>= (- t_2_1 t_2_0) 83.0)) (>= (- t_2_6 t_2_1) 65.0)) (>= (- t_2_5 t_2_6) 64.0)) (>= (- t_2_7 t_2_5) 85.0)) (>= (- t_2_4 t_2_7) 78.0)) (>= (- t_2_2 t_2_4) 85.0)) (>= (- t_2_3 t_2_2) 55.0)) (>= (- Z t_2_3) 77.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_3_7 cvclZero) 0.0) (>= (- t_3_2 t_3_7) 94.0)) (>= (- t_3_1 t_3_2) 68.0)) (>= (- t_3_4 t_3_1) 61.0)) (>= (- t_3_3 t_3_4) 99.0)) (>= (- t_3_6 t_3_3) 54.0)) (>= (- t_3_5 t_3_6) 75.0)) (>= (- t_3_0 t_3_5) 66.0)) (>= (- t_3_9 t_3_0) 76.0)) (>= (- t_3_8 t_3_9) 63.0)) (>= (- Z t_3_8) 67.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_4_3 cvclZero) 0.0) (>= (- t_4_4 t_4_3) 69.0)) (>= (- t_4_9 t_4_4) 88.0)) (>= (- t_4_8 t_4_9) 82.0)) (>= (- t_4_0 t_4_8) 95.0)) (>= (- t_4_2 t_4_0) 99.0)) (>= (- t_4_6 t_4_2) 67.0)) (>= (- t_4_5 t_4_6) 95.0)) (>= (- t_4_7 t_4_5) 68.0)) (>= (- t_4_1 t_4_7) 67.0)) (>= (- Z t_4_1) 86.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_5_1 cvclZero) 0.0) (>= (- t_5_4 t_5_1) 99.0)) (>= (- t_5_5 t_5_4) 81.0)) (>= (- t_5_6 t_5_5) 64.0)) (>= (- t_5_8 t_5_6) 66.0)) (>= (- t_5_2 t_5_8) 80.0)) (>= (- t_5_7 t_5_2) 80.0)) (>= (- t_5_9 t_5_7) 69.0)) (>= (- t_5_3 t_5_9) 62.0)) (>= (- t_5_0 t_5_3) 79.0)) (>= (- Z t_5_0) 88.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_6_7 cvclZero) 0.0) (>= (- t_6_1 t_6_7) 50.0)) (>= (- t_6_4 t_6_1) 86.0)) (>= (- t_6_3 t_6_4) 97.0)) (>= (- t_6_0 t_6_3) 96.0)) (>= (- t_6_8 t_6_0) 95.0)) (>= (- t_6_2 t_6_8) 97.0)) (>= (- t_6_5 t_6_2) 66.0)) (>= (- t_6_6 t_6_5) 99.0)) (>= (- t_6_9 t_6_6) 52.0)) (>= (- Z t_6_9) 71.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_7_4 cvclZero) 0.0) (>= (- t_7_6 t_7_4) 98.0)) (>= (- t_7_3 t_7_6) 73.0)) (>= (- t_7_2 t_7_3) 82.0)) (>= (- t_7_1 t_7_2) 51.0)) (>= (- t_7_5 t_7_1) 71.0)) (>= (- t_7_7 t_7_5) 94.0)) (>= (- t_7_0 t_7_7) 85.0)) (>= (- t_7_8 t_7_0) 62.0)) (>= (- t_7_9 t_7_8) 95.0)) (>= (- Z t_7_9) 79.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_8_0 cvclZero) 0.0) (>= (- t_8_6 t_8_0) 94.0)) (>= (- t_8_3 t_8_6) 71.0)) (>= (- t_8_7 t_8_3) 81.0)) (>= (- t_8_1 t_8_7) 85.0)) (>= (- t_8_2 t_8_1) 66.0)) (>= (- t_8_4 t_8_2) 90.0)) (>= (- t_8_5 t_8_4) 76.0)) (>= (- t_8_8 t_8_5) 58.0)) (>= (- t_8_9 t_8_8) 93.0)) (>= (- Z t_8_9) 97.0))) (and (and (and (and (and (and (and (and (and (and (>= (- t_9_3 cvclZero) 0.0) (>= (- t_9_0 t_9_3) 50.0)) (>= (- t_9_1 t_9_0) 59.0)) (>= (- t_9_8 t_9_1) 82.0)) (>= (- t_9_7 t_9_8) 67.0)) (>= (- t_9_9 t_9_7) 56.0)) (>= (- t_9_6 t_9_9) 96.0)) (>= (- t_9_4 t_9_6) 58.0)) (>= (- t_9_5 t_9_4) 81.0)) (>= (- t_9_2 t_9_5) 59.0)) (>= (- Z t_9_2) 96.0))) (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.0) (>= (- t_1_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_2_0) 83.0) (>= (- t_2_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_3_0) 76.0) (>= (- t_3_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_4_0) 99.0) (>= (- t_4_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_5_0) 88.0) (>= (- t_5_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_6_0) 95.0) (>= (- t_6_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_7_0) 62.0) (>= (- t_7_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_8_0) 94.0) (>= (- t_8_0 t_0_0) 86.0))) (or (>= (- t_0_0 t_9_0) 59.0) (>= (- t_9_0 t_0_0) 86.0))) (or (>= (- t_1_0 t_2_0) 83.0) (>= (- t_2_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_3_0) 76.0) (>= (- t_3_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_4_0) 99.0) (>= (- t_4_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_5_0) 88.0) (>= (- t_5_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_6_0) 95.0) (>= (- t_6_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_7_0) 62.0) (>= (- t_7_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_8_0) 94.0) (>= (- t_8_0 t_1_0) 92.0))) (or (>= (- t_1_0 t_9_0) 59.0) (>= (- t_9_0 t_1_0) 92.0))) (or (>= (- t_2_0 t_3_0) 76.0) (>= (- t_3_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_4_0) 99.0) (>= (- t_4_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_5_0) 88.0) (>= (- t_5_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_6_0) 95.0) (>= (- t_6_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_7_0) 62.0) (>= (- t_7_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_8_0) 94.0) (>= (- t_8_0 t_2_0) 83.0))) (or (>= (- t_2_0 t_9_0) 59.0) (>= (- t_9_0 t_2_0) 83.0))) (or (>= (- t_3_0 t_4_0) 99.0) (>= (- t_4_0 t_3_0) 76.0))) (or (>= (- t_3_0 t_5_0) 88.0) (>= (- t_5_0 t_3_0) 76.0))) (or (>= (- t_3_0 t_6_0) 95.0) (>= (- t_6_0 t_3_0) 76.0))) (or (>= (- t_3_0 t_7_0) 62.0) (>= (- t_7_0 t_3_0) 76.0))) (or (>= (- t_3_0 t_8_0) 94.0) (>= (- t_8_0 t_3_0) 76.0))) (or (>= (- t_3_0 t_9_0) 59.0) (>= (- t_9_0 t_3_0) 76.0))) (or (>= (- t_4_0 t_5_0) 88.0) (>= (- t_5_0 t_4_0) 99.0))) (or (>= (- t_4_0 t_6_0) 95.0) (>= (- t_6_0 t_4_0) 99.0))) (or (>= (- t_4_0 t_7_0) 62.0) (>= (- t_7_0 t_4_0) 99.0))) (or (>= (- t_4_0 t_8_0) 94.0) (>= (- t_8_0 t_4_0) 99.0))) (or (>= (- t_4_0 t_9_0) 59.0) (>= (- t_9_0 t_4_0) 99.0))) (or (>= (- t_5_0 t_6_0) 95.0) (>= (- t_6_0 t_5_0) 88.0))) (or (>= (- t_5_0 t_7_0) 62.0) (>= (- t_7_0 t_5_0) 88.0))) (or (>= (- t_5_0 t_8_0) 94.0) (>= (- t_8_0 t_5_0) 88.0))) (or (>= (- t_5_0 t_9_0) 59.0) (>= (- t_9_0 t_5_0) 88.0))) (or (>= (- t_6_0 t_7_0) 62.0) (>= (- t_7_0 t_6_0) 95.0))) (or (>= (- t_6_0 t_8_0) 94.0) (>= (- t_8_0 t_6_0) 95.0))) (or (>= (- t_6_0 t_9_0) 59.0) (>= (- t_9_0 t_6_0) 95.0))) (or (>= (- t_7_0 t_8_0) 94.0) (>= (- t_8_0 t_7_0) 62.0))) (or (>= (- t_7_0 t_9_0) 59.0) (>= (- t_9_0 t_7_0) 62.0))) (or (>= (- t_8_0 t_9_0) 59.0) (>= (- t_9_0 t_8_0) 94.0)))) (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.0) (>= (- t_1_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_2_1) 65.0) (>= (- t_2_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_3_1) 61.0) (>= (- t_3_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_4_1) 86.0) (>= (- t_4_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_5_1) 99.0) (>= (- t_5_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_6_1) 86.0) (>= (- t_6_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_7_1) 71.0) (>= (- t_7_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_8_1) 66.0) (>= (- t_8_1 t_0_1) 67.0))) (or (>= (- t_0_1 t_9_1) 82.0) (>= (- t_9_1 t_0_1) 67.0))) (or (>= (- t_1_1 t_2_1) 65.0) (>= (- t_2_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_3_1) 61.0) (>= (- t_3_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_4_1) 86.0) (>= (- t_4_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_5_1) 99.0) (>= (- t_5_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_6_1) 86.0) (>= (- t_6_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_7_1) 71.0) (>= (- t_7_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_8_1) 66.0) (>= (- t_8_1 t_1_1) 82.0))) (or (>= (- t_1_1 t_9_1) 82.0) (>= (- t_9_1 t_1_1) 82.0))) (or (>= (- t_2_1 t_3_1) 61.0) (>= (- t_3_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_4_1) 86.0) (>= (- t_4_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_5_1) 99.0) (>= (- t_5_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_6_1) 86.0) (>= (- t_6_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_7_1) 71.0) (>= (- t_7_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_8_1) 66.0) (>= (- t_8_1 t_2_1) 65.0))) (or (>= (- t_2_1 t_9_1) 82.0) (>= (- t_9_1 t_2_1) 65.0))) (or (>= (- t_3_1 t_4_1) 86.0) (>= (- t_4_1 t_3_1) 61.0))) (or (>= (- t_3_1 t_5_1) 99.0) (>= (- t_5_1 t_3_1) 61.0))) (or (>= (- t_3_1 t_6_1) 86.0) (>= (- t_6_1 t_3_1) 61.0))) (or (>= (- t_3_1 t_7_1) 71.0) (>= (- t_7_1 t_3_1) 61.0))) (or (>= (- t_3_1 t_8_1) 66.0) (>= (- t_8_1 t_3_1) 61.0))) (or (>= (- t_3_1 t_9_1) 82.0) (>= (- t_9_1 t_3_1) 61.0))) (or (>= (- t_4_1 t_5_1) 99.0) (>= (- t_5_1 t_4_1) 86.0))) (or (>= (- t_4_1 t_6_1) 86.0) (>= (- t_6_1 t_4_1) 86.0))) (or (>= (- t_4_1 t_7_1) 71.0) (>= (- t_7_1 t_4_1) 86.0))) (or (>= (- t_4_1 t_8_1) 66.0) (>= (- t_8_1 t_4_1) 86.0))) (or (>= (- t_4_1 t_9_1) 82.0) (>= (- t_9_1 t_4_1) 86.0))) (or (>= (- t_5_1 t_6_1) 86.0) (>= (- t_6_1 t_5_1) 99.0))) (or (>= (- t_5_1 t_7_1) 71.0) (>= (- t_7_1 t_5_1) 99.0))) (or (>= (- t_5_1 t_8_1) 66.0) (>= (- t_8_1 t_5_1) 99.0))) (or (>= (- t_5_1 t_9_1) 82.0) (>= (- t_9_1 t_5_1) 99.0))) (or (>= (- t_6_1 t_7_1) 71.0) (>= (- t_7_1 t_6_1) 86.0))) (or (>= (- t_6_1 t_8_1) 66.0) (>= (- t_8_1 t_6_1) 86.0))) (or (>= (- t_6_1 t_9_1) 82.0) (>= (- t_9_1 t_6_1) 86.0))) (or (>= (- t_7_1 t_8_1) 66.0) (>= (- t_8_1 t_7_1) 71.0))) (or (>= (- t_7_1 t_9_1) 82.0) (>= (- t_9_1 t_7_1) 71.0))) (or (>= (- t_8_1 t_9_1) 82.0) (>= (- t_9_1 t_8_1) 66.0)))) (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.0) (>= (- t_1_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_2_2) 55.0) (>= (- t_2_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_3_2) 68.0) (>= (- t_3_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_4_2) 67.0) (>= (- t_4_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_5_2) 80.0) (>= (- t_5_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_6_2) 66.0) (>= (- t_6_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_7_2) 51.0) (>= (- t_7_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_8_2) 90.0) (>= (- t_8_2 t_0_2) 89.0))) (or (>= (- t_0_2 t_9_2) 96.0) (>= (- t_9_2 t_0_2) 89.0))) (or (>= (- t_1_2 t_2_2) 55.0) (>= (- t_2_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_3_2) 68.0) (>= (- t_3_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_4_2) 67.0) (>= (- t_4_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_5_2) 80.0) (>= (- t_5_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_6_2) 66.0) (>= (- t_6_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_7_2) 51.0) (>= (- t_7_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_8_2) 90.0) (>= (- t_8_2 t_1_2) 94.0))) (or (>= (- t_1_2 t_9_2) 96.0) (>= (- t_9_2 t_1_2) 94.0))) (or (>= (- t_2_2 t_3_2) 68.0) (>= (- t_3_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_4_2) 67.0) (>= (- t_4_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_5_2) 80.0) (>= (- t_5_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_6_2) 66.0) (>= (- t_6_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_7_2) 51.0) (>= (- t_7_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_8_2) 90.0) (>= (- t_8_2 t_2_2) 55.0))) (or (>= (- t_2_2 t_9_2) 96.0) (>= (- t_9_2 t_2_2) 55.0))) (or (>= (- t_3_2 t_4_2) 67.0) (>= (- t_4_2 t_3_2) 68.0))) (or (>= (- t_3_2 t_5_2) 80.0) (>= (- t_5_2 t_3_2) 68.0))) (or (>= (- t_3_2 t_6_2) 66.0) (>= (- t_6_2 t_3_2) 68.0))) (or (>= (- t_3_2 t_7_2) 51.0) (>= (- t_7_2 t_3_2) 68.0))) (or (>= (- t_3_2 t_8_2) 90.0) (>= (- t_8_2 t_3_2) 68.0))) (or (>= (- t_3_2 t_9_2) 96.0) (>= (- t_9_2 t_3_2) 68.0))) (or (>= (- t_4_2 t_5_2) 80.0) (>= (- t_5_2 t_4_2) 67.0))) (or (>= (- t_4_2 t_6_2) 66.0) (>= (- t_6_2 t_4_2) 67.0))) (or (>= (- t_4_2 t_7_2) 51.0) (>= (- t_7_2 t_4_2) 67.0))) (or (>= (- t_4_2 t_8_2) 90.0) (>= (- t_8_2 t_4_2) 67.0))) (or (>= (- t_4_2 t_9_2) 96.0) (>= (- t_9_2 t_4_2) 67.0))) (or (>= (- t_5_2 t_6_2) 66.0) (>= (- t_6_2 t_5_2) 80.0))) (or (>= (- t_5_2 t_7_2) 51.0) (>= (- t_7_2 t_5_2) 80.0))) (or (>= (- t_5_2 t_8_2) 90.0) (>= (- t_8_2 t_5_2) 80.0))) (or (>= (- t_5_2 t_9_2) 96.0) (>= (- t_9_2 t_5_2) 80.0))) (or (>= (- t_6_2 t_7_2) 51.0) (>= (- t_7_2 t_6_2) 66.0))) (or (>= (- t_6_2 t_8_2) 90.0) (>= (- t_8_2 t_6_2) 66.0))) (or (>= (- t_6_2 t_9_2) 96.0) (>= (- t_9_2 t_6_2) 66.0))) (or (>= (- t_7_2 t_8_2) 90.0) (>= (- t_8_2 t_7_2) 51.0))) (or (>= (- t_7_2 t_9_2) 96.0) (>= (- t_9_2 t_7_2) 51.0))) (or (>= (- t_8_2 t_9_2) 96.0) (>= (- t_9_2 t_8_2) 90.0)))) (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.0) (>= (- t_1_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_2_3) 77.0) (>= (- t_2_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_3_3) 54.0) (>= (- t_3_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_4_3) 69.0) (>= (- t_4_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_5_3) 79.0) (>= (- t_5_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_6_3) 96.0) (>= (- t_6_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_7_3) 82.0) (>= (- t_7_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_8_3) 81.0) (>= (- t_8_3 t_0_3) 92.0))) (or (>= (- t_0_3 t_9_3) 50.0) (>= (- t_9_3 t_0_3) 92.0))) (or (>= (- t_1_3 t_2_3) 77.0) (>= (- t_2_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_3_3) 54.0) (>= (- t_3_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_4_3) 69.0) (>= (- t_4_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_5_3) 79.0) (>= (- t_5_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_6_3) 96.0) (>= (- t_6_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_7_3) 82.0) (>= (- t_7_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_8_3) 81.0) (>= (- t_8_3 t_1_3) 50.0))) (or (>= (- t_1_3 t_9_3) 50.0) (>= (- t_9_3 t_1_3) 50.0))) (or (>= (- t_2_3 t_3_3) 54.0) (>= (- t_3_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_4_3) 69.0) (>= (- t_4_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_5_3) 79.0) (>= (- t_5_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_6_3) 96.0) (>= (- t_6_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_7_3) 82.0) (>= (- t_7_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_8_3) 81.0) (>= (- t_8_3 t_2_3) 77.0))) (or (>= (- t_2_3 t_9_3) 50.0) (>= (- t_9_3 t_2_3) 77.0))) (or (>= (- t_3_3 t_4_3) 69.0) (>= (- t_4_3 t_3_3) 54.0))) (or (>= (- t_3_3 t_5_3) 79.0) (>= (- t_5_3 t_3_3) 54.0))) (or (>= (- t_3_3 t_6_3) 96.0) (>= (- t_6_3 t_3_3) 54.0))) (or (>= (- t_3_3 t_7_3) 82.0) (>= (- t_7_3 t_3_3) 54.0))) (or (>= (- t_3_3 t_8_3) 81.0) (>= (- t_8_3 t_3_3) 54.0))) (or (>= (- t_3_3 t_9_3) 50.0) (>= (- t_9_3 t_3_3) 54.0))) (or (>= (- t_4_3 t_5_3) 79.0) (>= (- t_5_3 t_4_3) 69.0))) (or (>= (- t_4_3 t_6_3) 96.0) (>= (- t_6_3 t_4_3) 69.0))) (or (>= (- t_4_3 t_7_3) 82.0) (>= (- t_7_3 t_4_3) 69.0))) (or (>= (- t_4_3 t_8_3) 81.0) (>= (- t_8_3 t_4_3) 69.0))) (or (>= (- t_4_3 t_9_3) 50.0) (>= (- t_9_3 t_4_3) 69.0))) (or (>= (- t_5_3 t_6_3) 96.0) (>= (- t_6_3 t_5_3) 79.0))) (or (>= (- t_5_3 t_7_3) 82.0) (>= (- t_7_3 t_5_3) 79.0))) (or (>= (- t_5_3 t_8_3) 81.0) (>= (- t_8_3 t_5_3) 79.0))) (or (>= (- t_5_3 t_9_3) 50.0) (>= (- t_9_3 t_5_3) 79.0))) (or (>= (- t_6_3 t_7_3) 82.0) (>= (- t_7_3 t_6_3) 96.0))) (or (>= (- t_6_3 t_8_3) 81.0) (>= (- t_8_3 t_6_3) 96.0))) (or (>= (- t_6_3 t_9_3) 50.0) (>= (- t_9_3 t_6_3) 96.0))) (or (>= (- t_7_3 t_8_3) 81.0) (>= (- t_8_3 t_7_3) 82.0))) (or (>= (- t_7_3 t_9_3) 50.0) (>= (- t_9_3 t_7_3) 82.0))) (or (>= (- t_8_3 t_9_3) 50.0) (>= (- t_9_3 t_8_3) 81.0)))) (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.0) (>= (- t_1_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_2_4) 85.0) (>= (- t_2_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_3_4) 99.0) (>= (- t_3_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_4_4) 88.0) (>= (- t_4_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_5_4) 81.0) (>= (- t_5_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_6_4) 97.0) (>= (- t_6_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_7_4) 98.0) (>= (- t_7_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_8_4) 76.0) (>= (- t_8_4 t_0_4) 88.0))) (or (>= (- t_0_4 t_9_4) 81.0) (>= (- t_9_4 t_0_4) 88.0))) (or (>= (- t_1_4 t_2_4) 85.0) (>= (- t_2_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_3_4) 99.0) (>= (- t_3_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_4_4) 88.0) (>= (- t_4_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_5_4) 81.0) (>= (- t_5_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_6_4) 97.0) (>= (- t_6_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_7_4) 98.0) (>= (- t_7_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_8_4) 76.0) (>= (- t_8_4 t_1_4) 75.0))) (or (>= (- t_1_4 t_9_4) 81.0) (>= (- t_9_4 t_1_4) 75.0))) (or (>= (- t_2_4 t_3_4) 99.0) (>= (- t_3_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_4_4) 88.0) (>= (- t_4_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_5_4) 81.0) (>= (- t_5_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_6_4) 97.0) (>= (- t_6_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_7_4) 98.0) (>= (- t_7_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_8_4) 76.0) (>= (- t_8_4 t_2_4) 85.0))) (or (>= (- t_2_4 t_9_4) 81.0) (>= (- t_9_4 t_2_4) 85.0))) (or (>= (- t_3_4 t_4_4) 88.0) (>= (- t_4_4 t_3_4) 99.0))) (or (>= (- t_3_4 t_5_4) 81.0) (>= (- t_5_4 t_3_4) 99.0))) (or (>= (- t_3_4 t_6_4) 97.0) (>= (- t_6_4 t_3_4) 99.0))) (or (>= (- t_3_4 t_7_4) 98.0) (>= (- t_7_4 t_3_4) 99.0))) (or (>= (- t_3_4 t_8_4) 76.0) (>= (- t_8_4 t_3_4) 99.0))) (or (>= (- t_3_4 t_9_4) 81.0) (>= (- t_9_4 t_3_4) 99.0))) (or (>= (- t_4_4 t_5_4) 81.0) (>= (- t_5_4 t_4_4) 88.0))) (or (>= (- t_4_4 t_6_4) 97.0) (>= (- t_6_4 t_4_4) 88.0))) (or (>= (- t_4_4 t_7_4) 98.0) (>= (- t_7_4 t_4_4) 88.0))) (or (>= (- t_4_4 t_8_4) 76.0) (>= (- t_8_4 t_4_4) 88.0))) (or (>= (- t_4_4 t_9_4) 81.0) (>= (- t_9_4 t_4_4) 88.0))) (or (>= (- t_5_4 t_6_4) 97.0) (>= (- t_6_4 t_5_4) 81.0))) (or (>= (- t_5_4 t_7_4) 98.0) (>= (- t_7_4 t_5_4) 81.0))) (or (>= (- t_5_4 t_8_4) 76.0) (>= (- t_8_4 t_5_4) 81.0))) (or (>= (- t_5_4 t_9_4) 81.0) (>= (- t_9_4 t_5_4) 81.0))) (or (>= (- t_6_4 t_7_4) 98.0) (>= (- t_7_4 t_6_4) 97.0))) (or (>= (- t_6_4 t_8_4) 76.0) (>= (- t_8_4 t_6_4) 97.0))) (or (>= (- t_6_4 t_9_4) 81.0) (>= (- t_9_4 t_6_4) 97.0))) (or (>= (- t_7_4 t_8_4) 76.0) (>= (- t_8_4 t_7_4) 98.0))) (or (>= (- t_7_4 t_9_4) 81.0) (>= (- t_9_4 t_7_4) 98.0))) (or (>= (- t_8_4 t_9_4) 81.0) (>= (- t_9_4 t_8_4) 76.0)))) (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.0) (>= (- t_1_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_2_5) 85.0) (>= (- t_2_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_3_5) 66.0) (>= (- t_3_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_4_5) 68.0) (>= (- t_4_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_5_5) 64.0) (>= (- t_5_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_6_5) 99.0) (>= (- t_6_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_7_5) 94.0) (>= (- t_7_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_8_5) 58.0) (>= (- t_8_5 t_0_5) 99.0))) (or (>= (- t_0_5 t_9_5) 59.0) (>= (- t_9_5 t_0_5) 99.0))) (or (>= (- t_1_5 t_2_5) 85.0) (>= (- t_2_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_3_5) 66.0) (>= (- t_3_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_4_5) 68.0) (>= (- t_4_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_5_5) 64.0) (>= (- t_5_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_6_5) 99.0) (>= (- t_6_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_7_5) 94.0) (>= (- t_7_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_8_5) 58.0) (>= (- t_8_5 t_1_5) 72.0))) (or (>= (- t_1_5 t_9_5) 59.0) (>= (- t_9_5 t_1_5) 72.0))) (or (>= (- t_2_5 t_3_5) 66.0) (>= (- t_3_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_4_5) 68.0) (>= (- t_4_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_5_5) 64.0) (>= (- t_5_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_6_5) 99.0) (>= (- t_6_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_7_5) 94.0) (>= (- t_7_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_8_5) 58.0) (>= (- t_8_5 t_2_5) 85.0))) (or (>= (- t_2_5 t_9_5) 59.0) (>= (- t_9_5 t_2_5) 85.0))) (or (>= (- t_3_5 t_4_5) 68.0) (>= (- t_4_5 t_3_5) 66.0))) (or (>= (- t_3_5 t_5_5) 64.0) (>= (- t_5_5 t_3_5) 66.0))) (or (>= (- t_3_5 t_6_5) 99.0) (>= (- t_6_5 t_3_5) 66.0))) (or (>= (- t_3_5 t_7_5) 94.0) (>= (- t_7_5 t_3_5) 66.0))) (or (>= (- t_3_5 t_8_5) 58.0) (>= (- t_8_5 t_3_5) 66.0))) (or (>= (- t_3_5 t_9_5) 59.0) (>= (- t_9_5 t_3_5) 66.0))) (or (>= (- t_4_5 t_5_5) 64.0) (>= (- t_5_5 t_4_5) 68.0))) (or (>= (- t_4_5 t_6_5) 99.0) (>= (- t_6_5 t_4_5) 68.0))) (or (>= (- t_4_5 t_7_5) 94.0) (>= (- t_7_5 t_4_5) 68.0))) (or (>= (- t_4_5 t_8_5) 58.0) (>= (- t_8_5 t_4_5) 68.0))) (or (>= (- t_4_5 t_9_5) 59.0) (>= (- t_9_5 t_4_5) 68.0))) (or (>= (- t_5_5 t_6_5) 99.0) (>= (- t_6_5 t_5_5) 64.0))) (or (>= (- t_5_5 t_7_5) 94.0) (>= (- t_7_5 t_5_5) 64.0))) (or (>= (- t_5_5 t_8_5) 58.0) (>= (- t_8_5 t_5_5) 64.0))) (or (>= (- t_5_5 t_9_5) 59.0) (>= (- t_9_5 t_5_5) 64.0))) (or (>= (- t_6_5 t_7_5) 94.0) (>= (- t_7_5 t_6_5) 99.0))) (or (>= (- t_6_5 t_8_5) 58.0) (>= (- t_8_5 t_6_5) 99.0))) (or (>= (- t_6_5 t_9_5) 59.0) (>= (- t_9_5 t_6_5) 99.0))) (or (>= (- t_7_5 t_8_5) 58.0) (>= (- t_8_5 t_7_5) 94.0))) (or (>= (- t_7_5 t_9_5) 59.0) (>= (- t_9_5 t_7_5) 94.0))) (or (>= (- t_8_5 t_9_5) 59.0) (>= (- t_9_5 t_8_5) 58.0)))) (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.0) (>= (- t_1_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_2_6) 64.0) (>= (- t_2_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_3_6) 75.0) (>= (- t_3_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_4_6) 95.0) (>= (- t_4_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_5_6) 66.0) (>= (- t_5_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_6_6) 52.0) (>= (- t_6_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_7_6) 73.0) (>= (- t_7_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_8_6) 71.0) (>= (- t_8_6 t_0_6) 94.0))) (or (>= (- t_0_6 t_9_6) 58.0) (>= (- t_9_6 t_0_6) 94.0))) (or (>= (- t_1_6 t_2_6) 64.0) (>= (- t_2_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_3_6) 75.0) (>= (- t_3_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_4_6) 95.0) (>= (- t_4_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_5_6) 66.0) (>= (- t_5_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_6_6) 52.0) (>= (- t_6_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_7_6) 73.0) (>= (- t_7_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_8_6) 71.0) (>= (- t_8_6 t_1_6) 69.0))) (or (>= (- t_1_6 t_9_6) 58.0) (>= (- t_9_6 t_1_6) 69.0))) (or (>= (- t_2_6 t_3_6) 75.0) (>= (- t_3_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_4_6) 95.0) (>= (- t_4_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_5_6) 66.0) (>= (- t_5_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_6_6) 52.0) (>= (- t_6_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_7_6) 73.0) (>= (- t_7_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_8_6) 71.0) (>= (- t_8_6 t_2_6) 64.0))) (or (>= (- t_2_6 t_9_6) 58.0) (>= (- t_9_6 t_2_6) 64.0))) (or (>= (- t_3_6 t_4_6) 95.0) (>= (- t_4_6 t_3_6) 75.0))) (or (>= (- t_3_6 t_5_6) 66.0) (>= (- t_5_6 t_3_6) 75.0))) (or (>= (- t_3_6 t_6_6) 52.0) (>= (- t_6_6 t_3_6) 75.0))) (or (>= (- t_3_6 t_7_6) 73.0) (>= (- t_7_6 t_3_6) 75.0))) (or (>= (- t_3_6 t_8_6) 71.0) (>= (- t_8_6 t_3_6) 75.0))) (or (>= (- t_3_6 t_9_6) 58.0) (>= (- t_9_6 t_3_6) 75.0))) (or (>= (- t_4_6 t_5_6) 66.0) (>= (- t_5_6 t_4_6) 95.0))) (or (>= (- t_4_6 t_6_6) 52.0) (>= (- t_6_6 t_4_6) 95.0))) (or (>= (- t_4_6 t_7_6) 73.0) (>= (- t_7_6 t_4_6) 95.0))) (or (>= (- t_4_6 t_8_6) 71.0) (>= (- t_8_6 t_4_6) 95.0))) (or (>= (- t_4_6 t_9_6) 58.0) (>= (- t_9_6 t_4_6) 95.0))) (or (>= (- t_5_6 t_6_6) 52.0) (>= (- t_6_6 t_5_6) 66.0))) (or (>= (- t_5_6 t_7_6) 73.0) (>= (- t_7_6 t_5_6) 66.0))) (or (>= (- t_5_6 t_8_6) 71.0) (>= (- t_8_6 t_5_6) 66.0))) (or (>= (- t_5_6 t_9_6) 58.0) (>= (- t_9_6 t_5_6) 66.0))) (or (>= (- t_6_6 t_7_6) 73.0) (>= (- t_7_6 t_6_6) 52.0))) (or (>= (- t_6_6 t_8_6) 71.0) (>= (- t_8_6 t_6_6) 52.0))) (or (>= (- t_6_6 t_9_6) 58.0) (>= (- t_9_6 t_6_6) 52.0))) (or (>= (- t_7_6 t_8_6) 71.0) (>= (- t_8_6 t_7_6) 73.0))) (or (>= (- t_7_6 t_9_6) 58.0) (>= (- t_9_6 t_7_6) 73.0))) (or (>= (- t_8_6 t_9_6) 58.0) (>= (- t_9_6 t_8_6) 71.0)))) (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.0) (>= (- t_1_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_2_7) 78.0) (>= (- t_2_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_3_7) 94.0) (>= (- t_3_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_4_7) 67.0) (>= (- t_4_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_5_7) 69.0) (>= (- t_5_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_6_7) 50.0) (>= (- t_6_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_7_7) 85.0) (>= (- t_7_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_8_7) 85.0) (>= (- t_8_7 t_0_7) 99.0))) (or (>= (- t_0_7 t_9_7) 56.0) (>= (- t_9_7 t_0_7) 99.0))) (or (>= (- t_1_7 t_2_7) 78.0) (>= (- t_2_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_3_7) 94.0) (>= (- t_3_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_4_7) 67.0) (>= (- t_4_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_5_7) 69.0) (>= (- t_5_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_6_7) 50.0) (>= (- t_6_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_7_7) 85.0) (>= (- t_7_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_8_7) 85.0) (>= (- t_8_7 t_1_7) 94.0))) (or (>= (- t_1_7 t_9_7) 56.0) (>= (- t_9_7 t_1_7) 94.0))) (or (>= (- t_2_7 t_3_7) 94.0) (>= (- t_3_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_4_7) 67.0) (>= (- t_4_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_5_7) 69.0) (>= (- t_5_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_6_7) 50.0) (>= (- t_6_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_7_7) 85.0) (>= (- t_7_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_8_7) 85.0) (>= (- t_8_7 t_2_7) 78.0))) (or (>= (- t_2_7 t_9_7) 56.0) (>= (- t_9_7 t_2_7) 78.0))) (or (>= (- t_3_7 t_4_7) 67.0) (>= (- t_4_7 t_3_7) 94.0))) (or (>= (- t_3_7 t_5_7) 69.0) (>= (- t_5_7 t_3_7) 94.0))) (or (>= (- t_3_7 t_6_7) 50.0) (>= (- t_6_7 t_3_7) 94.0))) (or (>= (- t_3_7 t_7_7) 85.0) (>= (- t_7_7 t_3_7) 94.0))) (or (>= (- t_3_7 t_8_7) 85.0) (>= (- t_8_7 t_3_7) 94.0))) (or (>= (- t_3_7 t_9_7) 56.0) (>= (- t_9_7 t_3_7) 94.0))) (or (>= (- t_4_7 t_5_7) 69.0) (>= (- t_5_7 t_4_7) 67.0))) (or (>= (- t_4_7 t_6_7) 50.0) (>= (- t_6_7 t_4_7) 67.0))) (or (>= (- t_4_7 t_7_7) 85.0) (>= (- t_7_7 t_4_7) 67.0))) (or (>= (- t_4_7 t_8_7) 85.0) (>= (- t_8_7 t_4_7) 67.0))) (or (>= (- t_4_7 t_9_7) 56.0) (>= (- t_9_7 t_4_7) 67.0))) (or (>= (- t_5_7 t_6_7) 50.0) (>= (- t_6_7 t_5_7) 69.0))) (or (>= (- t_5_7 t_7_7) 85.0) (>= (- t_7_7 t_5_7) 69.0))) (or (>= (- t_5_7 t_8_7) 85.0) (>= (- t_8_7 t_5_7) 69.0))) (or (>= (- t_5_7 t_9_7) 56.0) (>= (- t_9_7 t_5_7) 69.0))) (or (>= (- t_6_7 t_7_7) 85.0) (>= (- t_7_7 t_6_7) 50.0))) (or (>= (- t_6_7 t_8_7) 85.0) (>= (- t_8_7 t_6_7) 50.0))) (or (>= (- t_6_7 t_9_7) 56.0) (>= (- t_9_7 t_6_7) 50.0))) (or (>= (- t_7_7 t_8_7) 85.0) (>= (- t_8_7 t_7_7) 85.0))) (or (>= (- t_7_7 t_9_7) 56.0) (>= (- t_9_7 t_7_7) 85.0))) (or (>= (- t_8_7 t_9_7) 56.0) (>= (- t_9_7 t_8_7) 85.0)))) (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.0) (>= (- t_1_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_2_8) 61.0) (>= (- t_2_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_3_8) 67.0) (>= (- t_3_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_4_8) 95.0) (>= (- t_4_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_5_8) 80.0) (>= (- t_5_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_6_8) 97.0) (>= (- t_6_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_7_8) 95.0) (>= (- t_7_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_8_8) 93.0) (>= (- t_8_8 t_0_8) 68.0))) (or (>= (- t_0_8 t_9_8) 67.0) (>= (- t_9_8 t_0_8) 68.0))) (or (>= (- t_1_8 t_2_8) 61.0) (>= (- t_2_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_3_8) 67.0) (>= (- t_3_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_4_8) 95.0) (>= (- t_4_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_5_8) 80.0) (>= (- t_5_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_6_8) 97.0) (>= (- t_6_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_7_8) 95.0) (>= (- t_7_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_8_8) 93.0) (>= (- t_8_8 t_1_8) 66.0))) (or (>= (- t_1_8 t_9_8) 67.0) (>= (- t_9_8 t_1_8) 66.0))) (or (>= (- t_2_8 t_3_8) 67.0) (>= (- t_3_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_4_8) 95.0) (>= (- t_4_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_5_8) 80.0) (>= (- t_5_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_6_8) 97.0) (>= (- t_6_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_7_8) 95.0) (>= (- t_7_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_8_8) 93.0) (>= (- t_8_8 t_2_8) 61.0))) (or (>= (- t_2_8 t_9_8) 67.0) (>= (- t_9_8 t_2_8) 61.0))) (or (>= (- t_3_8 t_4_8) 95.0) (>= (- t_4_8 t_3_8) 67.0))) (or (>= (- t_3_8 t_5_8) 80.0) (>= (- t_5_8 t_3_8) 67.0))) (or (>= (- t_3_8 t_6_8) 97.0) (>= (- t_6_8 t_3_8) 67.0))) (or (>= (- t_3_8 t_7_8) 95.0) (>= (- t_7_8 t_3_8) 67.0))) (or (>= (- t_3_8 t_8_8) 93.0) (>= (- t_8_8 t_3_8) 67.0))) (or (>= (- t_3_8 t_9_8) 67.0) (>= (- t_9_8 t_3_8) 67.0))) (or (>= (- t_4_8 t_5_8) 80.0) (>= (- t_5_8 t_4_8) 95.0))) (or (>= (- t_4_8 t_6_8) 97.0) (>= (- t_6_8 t_4_8) 95.0))) (or (>= (- t_4_8 t_7_8) 95.0) (>= (- t_7_8 t_4_8) 95.0))) (or (>= (- t_4_8 t_8_8) 93.0) (>= (- t_8_8 t_4_8) 95.0))) (or (>= (- t_4_8 t_9_8) 67.0) (>= (- t_9_8 t_4_8) 95.0))) (or (>= (- t_5_8 t_6_8) 97.0) (>= (- t_6_8 t_5_8) 80.0))) (or (>= (- t_5_8 t_7_8) 95.0) (>= (- t_7_8 t_5_8) 80.0))) (or (>= (- t_5_8 t_8_8) 93.0) (>= (- t_8_8 t_5_8) 80.0))) (or (>= (- t_5_8 t_9_8) 67.0) (>= (- t_9_8 t_5_8) 80.0))) (or (>= (- t_6_8 t_7_8) 95.0) (>= (- t_7_8 t_6_8) 97.0))) (or (>= (- t_6_8 t_8_8) 93.0) (>= (- t_8_8 t_6_8) 97.0))) (or (>= (- t_6_8 t_9_8) 67.0) (>= (- t_9_8 t_6_8) 97.0))) (or (>= (- t_7_8 t_8_8) 93.0) (>= (- t_8_8 t_7_8) 95.0))) (or (>= (- t_7_8 t_9_8) 67.0) (>= (- t_9_8 t_7_8) 95.0))) (or (>= (- t_8_8 t_9_8) 67.0) (>= (- t_9_8 t_8_8) 93.0)))) (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.0) (>= (- t_1_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_2_9) 83.0) (>= (- t_2_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_3_9) 63.0) (>= (- t_3_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_4_9) 82.0) (>= (- t_4_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_5_9) 62.0) (>= (- t_5_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_6_9) 71.0) (>= (- t_6_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_7_9) 79.0) (>= (- t_7_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_8_9) 97.0) (>= (- t_8_9 t_0_9) 77.0))) (or (>= (- t_0_9 t_9_9) 96.0) (>= (- t_9_9 t_0_9) 77.0))) (or (>= (- t_1_9 t_2_9) 83.0) (>= (- t_2_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_3_9) 63.0) (>= (- t_3_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_4_9) 82.0) (>= (- t_4_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_5_9) 62.0) (>= (- t_5_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_6_9) 71.0) (>= (- t_6_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_7_9) 79.0) (>= (- t_7_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_8_9) 97.0) (>= (- t_8_9 t_1_9) 63.0))) (or (>= (- t_1_9 t_9_9) 96.0) (>= (- t_9_9 t_1_9) 63.0))) (or (>= (- t_2_9 t_3_9) 63.0) (>= (- t_3_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_4_9) 82.0) (>= (- t_4_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_5_9) 62.0) (>= (- t_5_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_6_9) 71.0) (>= (- t_6_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_7_9) 79.0) (>= (- t_7_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_8_9) 97.0) (>= (- t_8_9 t_2_9) 83.0))) (or (>= (- t_2_9 t_9_9) 96.0) (>= (- t_9_9 t_2_9) 83.0))) (or (>= (- t_3_9 t_4_9) 82.0) (>= (- t_4_9 t_3_9) 63.0))) (or (>= (- t_3_9 t_5_9) 62.0) (>= (- t_5_9 t_3_9) 63.0))) (or (>= (- t_3_9 t_6_9) 71.0) (>= (- t_6_9 t_3_9) 63.0))) (or (>= (- t_3_9 t_7_9) 79.0) (>= (- t_7_9 t_3_9) 63.0))) (or (>= (- t_3_9 t_8_9) 97.0) (>= (- t_8_9 t_3_9) 63.0))) (or (>= (- t_3_9 t_9_9) 96.0) (>= (- t_9_9 t_3_9) 63.0))) (or (>= (- t_4_9 t_5_9) 62.0) (>= (- t_5_9 t_4_9) 82.0))) (or (>= (- t_4_9 t_6_9) 71.0) (>= (- t_6_9 t_4_9) 82.0))) (or (>= (- t_4_9 t_7_9) 79.0) (>= (- t_7_9 t_4_9) 82.0))) (or (>= (- t_4_9 t_8_9) 97.0) (>= (- t_8_9 t_4_9) 82.0))) (or (>= (- t_4_9 t_9_9) 96.0) (>= (- t_9_9 t_4_9) 82.0))) (or (>= (- t_5_9 t_6_9) 71.0) (>= (- t_6_9 t_5_9) 62.0))) (or (>= (- t_5_9 t_7_9) 79.0) (>= (- t_7_9 t_5_9) 62.0))) (or (>= (- t_5_9 t_8_9) 97.0) (>= (- t_8_9 t_5_9) 62.0))) (or (>= (- t_5_9 t_9_9) 96.0) (>= (- t_9_9 t_5_9) 62.0))) (or (>= (- t_6_9 t_7_9) 79.0) (>= (- t_7_9 t_6_9) 71.0))) (or (>= (- t_6_9 t_8_9) 97.0) (>= (- t_8_9 t_6_9) 71.0))) (or (>= (- t_6_9 t_9_9) 96.0) (>= (- t_9_9 t_6_9) 71.0))) (or (>= (- t_7_9 t_8_9) 97.0) (>= (- t_8_9 t_7_9) 79.0))) (or (>= (- t_7_9 t_9_9) 96.0) (>= (- t_9_9 t_7_9) 79.0))) (or (>= (- t_8_9 t_9_9) 96.0) (>= (- t_9_9 t_8_9) 97.0)))) (<= (- Z cvclZero) 1400.0)) ))