source: vis_dev/cusp-1.1/examples/2ba/2ba.smt @ 82

(benchmark B_2ba
  :source {
Source unknown
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status sat
:category { industrial }
:difficulty { 0 }
  :logic QF_IDL
  :extrafuns ((cvclZero Int))
  :extrafuns ((CVC_C_s1_2 Int))
  :extrapreds ((CVC__x1_0))
  :extrafuns ((CVC_C_s1_3 Int))
  :extrapreds ((CVC__x1_1))
  :extrapreds ((CVC__x1_2))
  :extrapreds ((CVC__x1_3))
  :extrapreds ((CVC_s1_0))
  :extrapreds ((CVC_s1_1))
  :extrapreds ((CVC_s1_2))
  :extrapreds ((CVC_s1_3))
  :extrafuns ((CVC_C_x2_0 Int))
  :extrafuns ((CVC_C_x2_1 Int))
  :extrafuns ((CVC_C_x2_2 Int))
  :extrafuns ((CVC_C_x2_3 Int))
  :extrapreds ((CVC_x2_0))
  :extrapreds ((CVC_x2_1))
  :extrapreds ((CVC_x2_2))
  :extrafuns ((CVC_C_y1_0 Int))
  :extrapreds ((CVC__s2_0))
  :extrapreds ((CVC_x2_3))
  :extrapreds ((CVC__s2_1))
  :extrafuns ((CVC_C_y1_1 Int))
  :extrapreds ((CVC__s2_2))
  :extrafuns ((CVC_C_y1_2 Int))
  :extrafuns ((CVC_C_y1_3 Int))
  :extrapreds ((CVC__s2_3))
  :extrapreds ((CVC_y1_0))
  :extrapreds ((CVC_y1_1))
  :extrapreds ((CVC_y1_2))
  :extrafuns ((CVC_T_0 Int))
  :extrapreds ((CVC_y1_3))
  :extrafuns ((CVC_T_1 Int))
  :extrafuns ((CVC_T_2 Int))
  :extrafuns ((CVC_T_3 Int))
  :extrapreds ((CVC__y2_0))
  :extrapreds ((CVC__y2_1))
  :extrapreds ((CVC__y2_2))
  :extrapreds ((CVC__y2_3))
  :extrafuns ((CVC_C_x1_0 Int))
  :extrafuns ((CVC_C_x1_1 Int))
  :extrafuns ((CVC_C_x1_2 Int))
  :extrafuns ((CVC_C_x1_3 Int))
  :extrapreds ((CVC_x1_0))
  :extrapreds ((CVC_x1_1))
  :extrapreds ((CVC_x1_2))
  :extrapreds ((CVC__s1_0))
  :extrapreds ((CVC_x1_3))
  :extrapreds ((CVC__s1_1))
  :extrapreds ((CVC__s1_2))
  :extrapreds ((CVC__s1_3))
  :extrafuns ((CVC_C_s2_0 Int))
  :extrafuns ((CVC_C_s2_1 Int))
  :extrafuns ((CVC_C_s2_2 Int))
  :extrapreds ((CVC__x2_0))
  :extrafuns ((CVC_C_s2_3 Int))
  :extrapreds ((CVC__x2_1))
  :extrapreds ((CVC__x2_2))
  :extrapreds ((CVC__x2_3))
  :extrapreds ((CVC_s2_0))
  :extrapreds ((CVC_s2_1))
  :extrapreds ((CVC_s2_2))
  :extrapreds ((CVC_s2_3))
  :extrapreds ((CVC__y1_0))
  :extrapreds ((CVC__y1_1))
  :extrapreds ((CVC__y1_2))
  :extrapreds ((CVC__y1_3))
  :extrafuns ((CVC_C_y2_0 Int))
  :extrafuns ((CVC_C_y2_1 Int))
  :extrafuns ((CVC_C_y2_2 Int))
  :extrafuns ((CVC_C_y2_3 Int))
  :extrapreds ((CVC_y2_0))
  :extrapreds ((CVC_y2_1))
  :extrapreds ((CVC_y2_2))
  :extrapreds ((CVC_y2_3))
  :extrafuns ((CVC_C_s1_0 Int))
  :extrafuns ((CVC_C_s1_1 Int))
  :formula
(flet ($cvcl_5 (not CVC_x1_0)) (flet ($cvcl_0 (not CVC__x1_0)) (flet ($cvcl_14 (not CVC_x2_0)) (flet ($cvcl_9 (not CVC__x2_0)) (flet ($cvcl_23 (not CVC_y1_0)) (flet ($cvcl_18 (not CVC__y1_0)) (flet ($cvcl_31 (not CVC_y2_0)) (flet ($cvcl_26 (not CVC__y2_0)) (flet ($cvcl_40 (not CVC_s1_0)) (flet ($cvcl_34 (not CVC__s1_0)) (flet ($cvcl_49 (not CVC_s2_0)) (flet ($cvcl_43 (not CVC__s2_0)) (flet ($cvcl_8 (not true)) (flet ($cvcl_4 (iff CVC_x1_0 $cvcl_8)) (flet ($cvcl_1 (iff CVC_x1_1 CVC_x1_0)) (flet ($cvcl_2 (iff CVC__x1_1 $cvcl_0)) (flet ($cvcl_3 (iff CVC_x1_0 $cvcl_0)) (flet ($cvcl_7 (iff CVC__x1_1 CVC__x1_0)) (flet ($cvcl_52 (iff CVC_x1_1 CVC__x1_1)) (flet ($cvcl_55 (iff CVC_x1_1 true)) (flet ($cvcl_53 (not CVC__x1_1)) (flet ($cvcl_54 (iff CVC_x1_1 $cvcl_53)) (flet ($cvcl_13 (iff CVC_x2_0 $cvcl_8)) (flet ($cvcl_10 (iff CVC_x2_1 CVC_x2_0)) (flet ($cvcl_11 (iff CVC__x2_1 $cvcl_9)) (flet ($cvcl_12 (iff CVC_x2_0 $cvcl_9)) (flet ($cvcl_16 (iff CVC__x2_1 CVC__x2_0)) (flet ($cvcl_62 (iff CVC_x2_1 CVC__x2_1)) (flet ($cvcl_65 (iff CVC_x2_1 true)) (flet ($cvcl_63 (not CVC__x2_1)) (flet ($cvcl_64 (iff CVC_x2_1 $cvcl_63)) (flet ($cvcl_22 (iff CVC_y1_0 $cvcl_8)) (flet ($cvcl_19 (iff CVC_y1_1 CVC_y1_0)) (flet ($cvcl_20 (iff CVC__y1_1 $cvcl_18)) (flet ($cvcl_21 (iff CVC_y1_0 $cvcl_18)) (flet ($cvcl_25 (iff CVC__y1_1 CVC__y1_0)) (flet ($cvcl_73 (iff CVC_y1_1 CVC__y1_1)) (flet ($cvcl_76 (iff CVC_y1_1 true)) (flet ($cvcl_74 (not CVC__y1_1)) (flet ($cvcl_75 (iff CVC_y1_1 $cvcl_74)) (flet ($cvcl_30 (iff CVC_y2_0 $cvcl_8)) (flet ($cvcl_27 (iff CVC_y2_1 CVC_y2_0)) (flet ($cvcl_28 (iff CVC__y2_1 $cvcl_26)) (flet ($cvcl_29 (iff CVC_y2_0 $cvcl_26)) (flet ($cvcl_33 (iff CVC__y2_1 CVC__y2_0)) (flet ($cvcl_82 (iff CVC_y2_1 CVC__y2_1)) (flet ($cvcl_85 (iff CVC_y2_1 true)) (flet ($cvcl_83 (not CVC__y2_1)) (flet ($cvcl_84 (iff CVC_y2_1 $cvcl_83)) (flet ($cvcl_59 (not CVC_x1_1)) (flet ($cvcl_35 (iff $cvcl_59 CVC_y1_1)) (flet ($cvcl_39 (iff CVC_s1_0 (not $cvcl_35))) (flet ($cvcl_36 (iff CVC_s1_1 CVC_s1_0)) (flet ($cvcl_37 (iff CVC__s1_1 $cvcl_34)) (flet ($cvcl_38 (iff CVC_s1_0 $cvcl_34)) (flet ($cvcl_42 (iff CVC__s1_1 CVC__s1_0)) (flet ($cvcl_91 (iff CVC_s1_1 CVC__s1_1)) (flet ($cvcl_92 (not CVC__s1_1)) (flet ($cvcl_93 (iff CVC_s1_1 $cvcl_92)) (flet ($cvcl_69 (not CVC_x2_1)) (flet ($cvcl_44 (iff (not (and CVC_x1_1 CVC_y1_1)) (iff $cvcl_69 CVC_y2_1))) (flet ($cvcl_48 (iff CVC_s2_0 (not $cvcl_44))) (flet ($cvcl_45 (iff CVC_s2_1 CVC_s2_0)) (flet ($cvcl_46 (iff CVC__s2_1 $cvcl_43)) (flet ($cvcl_47 (iff CVC_s2_0 $cvcl_43)) (flet ($cvcl_51 (iff CVC__s2_1 CVC__s2_0)) (flet ($cvcl_100 (iff CVC_s2_1 CVC__s2_1)) (flet ($cvcl_101 (not CVC__s2_1)) (flet ($cvcl_102 (iff CVC_s2_1 $cvcl_101)) (flet ($cvcl_58 (iff CVC_x1_1 $cvcl_8)) (flet ($cvcl_56 (iff CVC_x1_2 CVC_x1_1)) (flet ($cvcl_57 (iff CVC__x1_2 $cvcl_53)) (flet ($cvcl_61 (iff CVC__x1_2 CVC__x1_1)) (flet ($cvcl_109 (iff CVC_x1_2 CVC__x1_2)) (flet ($cvcl_112 (iff CVC_x1_2 true)) (flet ($cvcl_110 (not CVC__x1_2)) (flet ($cvcl_111 (iff CVC_x1_2 $cvcl_110)) (flet ($cvcl_68 (iff CVC_x2_1 $cvcl_8)) (flet ($cvcl_66 (iff CVC_x2_2 CVC_x2_1)) (flet ($cvcl_67 (iff CVC__x2_2 $cvcl_63)) (flet ($cvcl_71 (iff CVC__x2_2 CVC__x2_1)) (flet ($cvcl_119 (iff CVC_x2_2 CVC__x2_2)) (flet ($cvcl_122 (iff CVC_x2_2 true)) (flet ($cvcl_120 (not CVC__x2_2)) (flet ($cvcl_121 (iff CVC_x2_2 $cvcl_120)) (flet ($cvcl_79 (iff CVC_y1_1 $cvcl_8)) (flet ($cvcl_77 (iff CVC_y1_2 CVC_y1_1)) (flet ($cvcl_78 (iff CVC__y1_2 $cvcl_74)) (flet ($cvcl_81 (iff CVC__y1_2 CVC__y1_1)) (flet ($cvcl_130 (iff CVC_y1_2 CVC__y1_2)) (flet ($cvcl_133 (iff CVC_y1_2 true)) (flet ($cvcl_131 (not CVC__y1_2)) (flet ($cvcl_132 (iff CVC_y1_2 $cvcl_131)) (flet ($cvcl_88 (iff CVC_y2_1 $cvcl_8)) (flet ($cvcl_86 (iff CVC_y2_2 CVC_y2_1)) (flet ($cvcl_87 (iff CVC__y2_2 $cvcl_83)) (flet ($cvcl_90 (iff CVC__y2_2 CVC__y2_1)) (flet ($cvcl_139 (iff CVC_y2_2 CVC__y2_2)) (flet ($cvcl_142 (iff CVC_y2_2 true)) (flet ($cvcl_140 (not CVC__y2_2)) (flet ($cvcl_141 (iff CVC_y2_2 $cvcl_140)) (flet ($cvcl_116 (not CVC_x1_2)) (flet ($cvcl_94 (iff $cvcl_116 CVC_y1_2)) (flet ($cvcl_97 (iff CVC_s1_1 (not $cvcl_94))) (flet ($cvcl_95 (iff CVC_s1_2 CVC_s1_1)) (flet ($cvcl_96 (iff CVC__s1_2 $cvcl_92)) (flet ($cvcl_99 (iff CVC__s1_2 CVC__s1_1)) (flet ($cvcl_148 (iff CVC_s1_2 CVC__s1_2)) (flet ($cvcl_149 (not CVC__s1_2)) (flet ($cvcl_150 (iff CVC_s1_2 $cvcl_149)) (flet ($cvcl_126 (not CVC_x2_2)) (flet ($cvcl_103 (iff (not (and CVC_x1_2 CVC_y1_2)) (iff $cvcl_126 CVC_y2_2))) (flet ($cvcl_106 (iff CVC_s2_1 (not $cvcl_103))) (flet ($cvcl_104 (iff CVC_s2_2 CVC_s2_1)) (flet ($cvcl_105 (iff CVC__s2_2 $cvcl_101)) (flet ($cvcl_108 (iff CVC__s2_2 CVC__s2_1)) (flet ($cvcl_157 (iff CVC_s2_2 CVC__s2_2)) (flet ($cvcl_158 (not CVC__s2_2)) (flet ($cvcl_159 (iff CVC_s2_2 $cvcl_158)) (flet ($cvcl_115 (iff CVC_x1_2 $cvcl_8)) (flet ($cvcl_113 (iff CVC_x1_3 CVC_x1_2)) (flet ($cvcl_114 (iff CVC__x1_3 $cvcl_110)) (flet ($cvcl_118 (iff CVC__x1_3 CVC__x1_2)) (flet ($cvcl_125 (iff CVC_x2_2 $cvcl_8)) (flet ($cvcl_123 (iff CVC_x2_3 CVC_x2_2)) (flet ($cvcl_124 (iff CVC__x2_3 $cvcl_120)) (flet ($cvcl_128 (iff CVC__x2_3 CVC__x2_2)) (flet ($cvcl_136 (iff CVC_y1_2 $cvcl_8)) (flet ($cvcl_134 (iff CVC_y1_3 CVC_y1_2)) (flet ($cvcl_135 (iff CVC__y1_3 $cvcl_131)) (flet ($cvcl_138 (iff CVC__y1_3 CVC__y1_2)) (flet ($cvcl_145 (iff CVC_y2_2 $cvcl_8)) (flet ($cvcl_143 (iff CVC_y2_3 CVC_y2_2)) (flet ($cvcl_144 (iff CVC__y2_3 $cvcl_140)) (flet ($cvcl_147 (iff CVC__y2_3 CVC__y2_2)) (flet ($cvcl_151 (iff (not CVC_x1_3) CVC_y1_3)) (flet ($cvcl_154 (iff CVC_s1_2 (not $cvcl_151))) (flet ($cvcl_152 (iff CVC_s1_3 CVC_s1_2)) (flet ($cvcl_153 (iff CVC__s1_3 $cvcl_149)) (flet ($cvcl_156 (iff CVC__s1_3 CVC__s1_2)) (flet ($cvcl_160 (iff (not (and CVC_x1_3 CVC_y1_3)) (iff (not CVC_x2_3) CVC_y2_3))) (flet ($cvcl_163 (iff CVC_s2_2 (not $cvcl_160))) (flet ($cvcl_161 (iff CVC_s2_3 CVC_s2_2)) (flet ($cvcl_162 (iff CVC__s2_3 $cvcl_158)) (flet ($cvcl_165 (iff CVC__s2_3 CVC__s2_2)) (flet ($cvcl_6 (= (- CVC_C_x1_1 CVC_C_x1_0) 0)) (flet ($cvcl_17 (>= (- CVC_T_1 CVC_T_0) 0)) (flet ($cvcl_15 (= (- CVC_C_x2_1 CVC_C_x2_0) 0)) (flet ($cvcl_24 (= (- CVC_C_y1_1 CVC_C_y1_0) 0)) (flet ($cvcl_32 (= (- CVC_C_y2_1 CVC_C_y2_0) 0)) (flet ($cvcl_41 (= (- CVC_C_s1_1 CVC_C_s1_0) 0)) (flet ($cvcl_50 (= (- CVC_C_s2_1 CVC_C_s2_0) 0)) (flet ($cvcl_60 (= (- CVC_C_x1_2 CVC_C_x1_1) 0)) (flet ($cvcl_72 (>= (- CVC_T_2 CVC_T_1) 0)) (flet ($cvcl_70 (= (- CVC_C_x2_2 CVC_C_x2_1) 0)) (flet ($cvcl_80 (= (- CVC_C_y1_2 CVC_C_y1_1) 0)) (flet ($cvcl_89 (= (- CVC_C_y2_2 CVC_C_y2_1) 0)) (flet ($cvcl_98 (= (- CVC_C_s1_2 CVC_C_s1_1) 0)) (flet ($cvcl_107 (= (- CVC_C_s2_2 CVC_C_s2_1) 0)) (flet ($cvcl_117 (= (- CVC_C_x1_3 CVC_C_x1_2) 0)) (flet ($cvcl_129 (>= (- CVC_T_3 CVC_T_2) 0)) (flet ($cvcl_127 (= (- CVC_C_x2_3 CVC_C_x2_2) 0)) (flet ($cvcl_137 (= (- CVC_C_y1_3 CVC_C_y1_2) 0)) (flet ($cvcl_146 (= (- CVC_C_y2_3 CVC_C_y2_2) 0)) (flet ($cvcl_155 (= (- CVC_C_s1_3 CVC_C_s1_2) 0)) (flet ($cvcl_164 (= (- CVC_C_s2_3 CVC_C_s2_2) 0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and $cvcl_5 $cvcl_0) $cvcl_14) $cvcl_9) $cvcl_23) $cvcl_18) $cvcl_31) $cvcl_26) $cvcl_40) $cvcl_34) $cvcl_49) $cvcl_43) CVC_s2_3) CVC__s2_3) (and (and (and (and (and (and (and (and (or (or (or (and (and (and (and (iff CVC_x1_0 CVC__x1_0) $cvcl_4) $cvcl_1) $cvcl_2) (= (- CVC_C_x1_1 CVC_T_0) 0))  (and (and (and (and $cvcl_3 (iff CVC_x1_0 true)) $cvcl_1) $cvcl_2) $cvcl_6) )  (and (and (and (and (and $cvcl_3 $cvcl_4) (>= (- CVC_T_0 CVC_C_x1_0) 1)) (iff CVC_x1_1 $cvcl_5)) $cvcl_7) $cvcl_6) )  (and (and (and true $cvcl_1) $cvcl_7) $cvcl_6) ) (or (and $cvcl_52 $cvcl_55)  (and $cvcl_54 (<= (- CVC_T_1 CVC_C_x1_1) 1)) )) $cvcl_17) (and (and (or (or (or (and (and (and (and (iff CVC_x2_0 CVC__x2_0) $cvcl_13) $cvcl_10) $cvcl_11) (= (- CVC_C_x2_1 CVC_T_0) 0))  (and (and (and (and $cvcl_12 (iff CVC_x2_0 true)) $cvcl_10) $cvcl_11) $cvcl_15) )  (and (and (and (and (and $cvcl_12 $cvcl_13) (>= (- CVC_T_0 CVC_C_x2_0) 1)) (iff CVC_x2_1 $cvcl_14)) $cvcl_16) $cvcl_15) )  (and (and (and true $cvcl_10) $cvcl_16) $cvcl_15) ) (or (and $cvcl_62 $cvcl_65)  (and $cvcl_64 (<= (- CVC_T_1 CVC_C_x2_1) 1)) )) $cvcl_17)) (and (and (or (or (or (and (and (and (and (iff CVC_y1_0 CVC__y1_0) $cvcl_22) $cvcl_19) $cvcl_20) (= (- CVC_C_y1_1 CVC_T_0) 0))  (and (and (and (and $cvcl_21 (iff CVC_y1_0 true)) $cvcl_19) $cvcl_20) $cvcl_24) )  (and (and (and (and (and $cvcl_21 $cvcl_22) (>= (- CVC_T_0 CVC_C_y1_0) 1)) (iff CVC_y1_1 $cvcl_23)) $cvcl_25) $cvcl_24) )  (and (and (and true $cvcl_19) $cvcl_25) $cvcl_24) ) (or (and $cvcl_73 $cvcl_76)  (and $cvcl_75 (<= (- CVC_T_1 CVC_C_y1_1) 1)) )) $cvcl_17)) (and (and (or (or (or (and (and (and (and (iff CVC_y2_0 CVC__y2_0) $cvcl_30) $cvcl_27) $cvcl_28) (= (- CVC_C_y2_1 CVC_T_0) 0))  (and (and (and (and $cvcl_29 (iff CVC_y2_0 true)) $cvcl_27) $cvcl_28) $cvcl_32) )  (and (and (and (and (and $cvcl_29 $cvcl_30) (>= (- CVC_T_0 CVC_C_y2_0) 1)) (iff CVC_y2_1 $cvcl_31)) $cvcl_33) $cvcl_32) )  (and (and (and true $cvcl_27) $cvcl_33) $cvcl_32) ) (or (and $cvcl_82 $cvcl_85)  (and $cvcl_84 (<= (- CVC_T_1 CVC_C_y2_1) 1)) )) $cvcl_17)) (and (and (or (or (or (and (and (and (and (iff CVC_s1_0 CVC__s1_0) $cvcl_39) $cvcl_36) $cvcl_37) (= (- CVC_C_s1_1 CVC_T_0) 0))  (and (and (and (and $cvcl_38 (iff CVC_s1_0 $cvcl_35)) $cvcl_36) $cvcl_37) $cvcl_41) )  (and (and (and (and (and $cvcl_38 $cvcl_39) (>= (- CVC_T_0 CVC_C_s1_0) 2)) (iff CVC_s1_1 $cvcl_40)) $cvcl_42) $cvcl_41) )  (and (and (and true $cvcl_36) $cvcl_42) $cvcl_41) ) (or (and $cvcl_91 (iff CVC_s1_1 $cvcl_35))  (and $cvcl_93 (<= (- CVC_T_1 CVC_C_s1_1) 3)) )) $cvcl_17)) (and (and (or (or (or (and (and (and (and (iff CVC_s2_0 CVC__s2_0) $cvcl_48) $cvcl_45) $cvcl_46) (= (- CVC_C_s2_1 CVC_T_0) 0))  (and (and (and (and $cvcl_47 (iff CVC_s2_0 $cvcl_44)) $cvcl_45) $cvcl_46) $cvcl_50) )  (and (and (and (and (and $cvcl_47 $cvcl_48) (>= (- CVC_T_0 CVC_C_s2_0) 2)) (iff CVC_s2_1 $cvcl_49)) $cvcl_51) $cvcl_50) )  (and (and (and true $cvcl_45) $cvcl_51) $cvcl_50) ) (or (and $cvcl_100 (iff CVC_s2_1 $cvcl_44))  (and $cvcl_102 (<= (- CVC_T_1 CVC_C_s2_1) 3)) )) $cvcl_17)) true)) (and (and (and (and (and (and (and (and (or (or (or (and (and (and (and $cvcl_52 $cvcl_58) $cvcl_56) $cvcl_57) (= (- CVC_C_x1_2 CVC_T_1) 0))  (and (and (and (and $cvcl_54 $cvcl_55) $cvcl_56) $cvcl_57) $cvcl_60) )  (and (and (and (and (and $cvcl_54 $cvcl_58) (>= (- CVC_T_1 CVC_C_x1_1) 1)) (iff CVC_x1_2 $cvcl_59)) $cvcl_61) $cvcl_60) )  (and (and (and true $cvcl_56) $cvcl_61) $cvcl_60) ) (or (and $cvcl_109 $cvcl_112)  (and $cvcl_111 (<= (- CVC_T_2 CVC_C_x1_2) 1)) )) $cvcl_72) (and (and (or (or (or (and (and (and (and $cvcl_62 $cvcl_68) $cvcl_66) $cvcl_67) (= (- CVC_C_x2_2 CVC_T_1) 0))  (and (and (and (and $cvcl_64 $cvcl_65) $cvcl_66) $cvcl_67) $cvcl_70) )  (and (and (and (and (and $cvcl_64 $cvcl_68) (>= (- CVC_T_1 CVC_C_x2_1) 1)) (iff CVC_x2_2 $cvcl_69)) $cvcl_71) $cvcl_70) )  (and (and (and true $cvcl_66) $cvcl_71) $cvcl_70) ) (or (and $cvcl_119 $cvcl_122)  (and $cvcl_121 (<= (- CVC_T_2 CVC_C_x2_2) 1)) )) $cvcl_72)) (and (and (or (or (or (and (and (and (and $cvcl_73 $cvcl_79) $cvcl_77) $cvcl_78) (= (- CVC_C_y1_2 CVC_T_1) 0))  (and (and (and (and $cvcl_75 $cvcl_76) $cvcl_77) $cvcl_78) $cvcl_80) )  (and (and (and (and (and $cvcl_75 $cvcl_79) (>= (- CVC_T_1 CVC_C_y1_1) 1)) (iff CVC_y1_2 (not CVC_y1_1))) $cvcl_81) $cvcl_80) )  (and (and (and true $cvcl_77) $cvcl_81) $cvcl_80) ) (or (and $cvcl_130 $cvcl_133)  (and $cvcl_132 (<= (- CVC_T_2 CVC_C_y1_2) 1)) )) $cvcl_72)) (and (and (or (or (or (and (and (and (and $cvcl_82 $cvcl_88) $cvcl_86) $cvcl_87) (= (- CVC_C_y2_2 CVC_T_1) 0))  (and (and (and (and $cvcl_84 $cvcl_85) $cvcl_86) $cvcl_87) $cvcl_89) )  (and (and (and (and (and $cvcl_84 $cvcl_88) (>= (- CVC_T_1 CVC_C_y2_1) 1)) (iff CVC_y2_2 (not CVC_y2_1))) $cvcl_90) $cvcl_89) )  (and (and (and true $cvcl_86) $cvcl_90) $cvcl_89) ) (or (and $cvcl_139 $cvcl_142)  (and $cvcl_141 (<= (- CVC_T_2 CVC_C_y2_2) 1)) )) $cvcl_72)) (and (and (or (or (or (and (and (and (and $cvcl_91 $cvcl_97) $cvcl_95) $cvcl_96) (= (- CVC_C_s1_2 CVC_T_1) 0))  (and (and (and (and $cvcl_93 (iff CVC_s1_1 $cvcl_94)) $cvcl_95) $cvcl_96) $cvcl_98) )  (and (and (and (and (and $cvcl_93 $cvcl_97) (>= (- CVC_T_1 CVC_C_s1_1) 2)) (iff CVC_s1_2 (not CVC_s1_1))) $cvcl_99) $cvcl_98) )  (and (and (and true $cvcl_95) $cvcl_99) $cvcl_98) ) (or (and $cvcl_148 (iff CVC_s1_2 $cvcl_94))  (and $cvcl_150 (<= (- CVC_T_2 CVC_C_s1_2) 3)) )) $cvcl_72)) (and (and (or (or (or (and (and (and (and $cvcl_100 $cvcl_106) $cvcl_104) $cvcl_105) (= (- CVC_C_s2_2 CVC_T_1) 0))  (and (and (and (and $cvcl_102 (iff CVC_s2_1 $cvcl_103)) $cvcl_104) $cvcl_105) $cvcl_107) )  (and (and (and (and (and $cvcl_102 $cvcl_106) (>= (- CVC_T_1 CVC_C_s2_1) 2)) (iff CVC_s2_2 (not CVC_s2_1))) $cvcl_108) $cvcl_107) )  (and (and (and true $cvcl_104) $cvcl_108) $cvcl_107) ) (or (and $cvcl_157 (iff CVC_s2_2 $cvcl_103))  (and $cvcl_159 (<= (- CVC_T_2 CVC_C_s2_2) 3)) )) $cvcl_72)) true)) (and (and (and (and (and (and (and (and (or (or (or (and (and (and (and $cvcl_109 $cvcl_115) $cvcl_113) $cvcl_114) (= (- CVC_C_x1_3 CVC_T_2) 0))  (and (and (and (and $cvcl_111 $cvcl_112) $cvcl_113) $cvcl_114) $cvcl_117) )  (and (and (and (and (and $cvcl_111 $cvcl_115) (>= (- CVC_T_2 CVC_C_x1_2) 1)) (iff CVC_x1_3 $cvcl_116)) $cvcl_118) $cvcl_117) )  (and (and (and true $cvcl_113) $cvcl_118) $cvcl_117) ) (or (and (iff CVC_x1_3 CVC__x1_3) (iff CVC_x1_3 true))  (and (iff CVC_x1_3 (not CVC__x1_3)) (<= (- CVC_T_3 CVC_C_x1_3) 1)) )) $cvcl_129) (and (and (or (or (or (and (and (and (and $cvcl_119 $cvcl_125) $cvcl_123) $cvcl_124) (= (- CVC_C_x2_3 CVC_T_2) 0))  (and (and (and (and $cvcl_121 $cvcl_122) $cvcl_123) $cvcl_124) $cvcl_127) )  (and (and (and (and (and $cvcl_121 $cvcl_125) (>= (- CVC_T_2 CVC_C_x2_2) 1)) (iff CVC_x2_3 $cvcl_126)) $cvcl_128) $cvcl_127) )  (and (and (and true $cvcl_123) $cvcl_128) $cvcl_127) ) (or (and (iff CVC_x2_3 CVC__x2_3) (iff CVC_x2_3 true))  (and (iff CVC_x2_3 (not CVC__x2_3)) (<= (- CVC_T_3 CVC_C_x2_3) 1)) )) $cvcl_129)) (and (and (or (or (or (and (and (and (and $cvcl_130 $cvcl_136) $cvcl_134) $cvcl_135) (= (- CVC_C_y1_3 CVC_T_2) 0))  (and (and (and (and $cvcl_132 $cvcl_133) $cvcl_134) $cvcl_135) $cvcl_137) )  (and (and (and (and (and $cvcl_132 $cvcl_136) (>= (- CVC_T_2 CVC_C_y1_2) 1)) (iff CVC_y1_3 (not CVC_y1_2))) $cvcl_138) $cvcl_137) )  (and (and (and true $cvcl_134) $cvcl_138) $cvcl_137) ) (or (and (iff CVC_y1_3 CVC__y1_3) (iff CVC_y1_3 true))  (and (iff CVC_y1_3 (not CVC__y1_3)) (<= (- CVC_T_3 CVC_C_y1_3) 1)) )) $cvcl_129)) (and (and (or (or (or (and (and (and (and $cvcl_139 $cvcl_145) $cvcl_143) $cvcl_144) (= (- CVC_C_y2_3 CVC_T_2) 0))  (and (and (and (and $cvcl_141 $cvcl_142) $cvcl_143) $cvcl_144) $cvcl_146) )  (and (and (and (and (and $cvcl_141 $cvcl_145) (>= (- CVC_T_2 CVC_C_y2_2) 1)) (iff CVC_y2_3 (not CVC_y2_2))) $cvcl_147) $cvcl_146) )  (and (and (and true $cvcl_143) $cvcl_147) $cvcl_146) ) (or (and (iff CVC_y2_3 CVC__y2_3) (iff CVC_y2_3 true))  (and (iff CVC_y2_3 (not CVC__y2_3)) (<= (- CVC_T_3 CVC_C_y2_3) 1)) )) $cvcl_129)) (and (and (or (or (or (and (and (and (and $cvcl_148 $cvcl_154) $cvcl_152) $cvcl_153) (= (- CVC_C_s1_3 CVC_T_2) 0))  (and (and (and (and $cvcl_150 (iff CVC_s1_2 $cvcl_151)) $cvcl_152) $cvcl_153) $cvcl_155) )  (and (and (and (and (and $cvcl_150 $cvcl_154) (>= (- CVC_T_2 CVC_C_s1_2) 2)) (iff CVC_s1_3 (not CVC_s1_2))) $cvcl_156) $cvcl_155) )  (and (and (and true $cvcl_152) $cvcl_156) $cvcl_155) ) (or (and (iff CVC_s1_3 CVC__s1_3) (iff CVC_s1_3 $cvcl_151))  (and (iff CVC_s1_3 (not CVC__s1_3)) (<= (- CVC_T_3 CVC_C_s1_3) 3)) )) $cvcl_129)) (and (and (or (or (or (and (and (and (and $cvcl_157 $cvcl_163) $cvcl_161) $cvcl_162) (= (- CVC_C_s2_3 CVC_T_2) 0))  (and (and (and (and $cvcl_159 (iff CVC_s2_2 $cvcl_160)) $cvcl_161) $cvcl_162) $cvcl_164) )  (and (and (and (and (and $cvcl_159 $cvcl_163) (>= (- CVC_T_2 CVC_C_s2_2) 2)) (iff CVC_s2_3 (not CVC_s2_2))) $cvcl_165) $cvcl_164) )  (and (and (and true $cvcl_161) $cvcl_165) $cvcl_164) ) (or (and (iff CVC_s2_3 CVC__s2_3) (iff CVC_s2_3 $cvcl_160))  (and (iff CVC_s2_3 (not CVC__s2_3)) (<= (- CVC_T_3 CVC_C_s2_3) 3)) )) $cvcl_129)) true)) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)