source: vis_dev/cusp-1.1/examples/ckt_PROP14_tf_9/ckt_PROP14_tf_9.smt @ 12

(benchmark ckt_PROP14_tf_9.smt
  :source {
Mathsat benchmarks available from http://mathsat.itc.it

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))
  :extrapreds ((tx_end_8))
  :extrapreds ((rdy_8))
  :extrafuns ((S1_8 Int))
  :extrapreds ((dsr_8))
  :extrapreds ((tre_8))
  :extrapreds ((mpx_8))
  :extrapreds ((confirm_8))
  :extrafuns ((next_bit_8 Int))
  :extrapreds ((dsr_5))
  :extrapreds ((eoc_7))
  :extrapreds ((send_8))
  :extrapreds ((dsr_7))
  :extrafuns ((itfc_state_8 Int))
  :extrapreds ((bstate14_8))
  :extrafuns ((tx_conta_8 Int))
  :extrapreds ((send_data_8))
  :extrapreds ((eoc_5))
  :extrapreds ((dsr_6))
  :extrapreds ((eoc_4))
  :extrapreds ((send_en_8))
  :extrapreds ((eoc_8))
  :extrafuns ((S2_8 Int))
  :extrapreds ((load_8))
  :extrapreds ((eoc_6))
  :extrapreds ((shot_8))
  :formula
(flet ($cvcl_4 (if_then_else confirm_8 false true)) (flet ($cvcl_11 (if_then_else mpx_8 false true)) (flet ($cvcl_21 (if_then_else rdy_8 false true)) (flet ($cvcl_3 (and (if_then_else (and bstate14_8 (if_then_else (or $cvcl_21  shot_8 ) false true)) false true) bstate14_8)) (flet ($cvcl_317 (= (- S2_8 cvclZero) 0)) (flet ($cvcl_0 (and $cvcl_317 send_data_8)) (flet ($cvcl_2 (= (- S2_8 cvclZero) 2)) (flet ($cvcl_10 (and $cvcl_2 confirm_8)) (flet ($cvcl_48 (and $cvcl_10 mpx_8)) (flet ($cvcl_12 (or $cvcl_0  (and (if_then_else (or $cvcl_0  $cvcl_48 ) false true) rdy_8) )) (flet ($cvcl_1 (= (- S2_8 cvclZero) 1)) (flet ($cvcl_16 (or $cvcl_1  (and (if_then_else (or $cvcl_1  (and $cvcl_2 $cvcl_4) ) false true) shot_8) )) (flet ($cvcl_17 (and (if_then_else (and $cvcl_3 (if_then_else (or (if_then_else $cvcl_12 false true)  $cvcl_16 ) false true)) false true) $cvcl_3)) (flet ($cvcl_7 (= (- S2_8 cvclZero) 0)) (flet ($cvcl_8 (if_then_else $cvcl_11 false false)) (flet ($cvcl_18 (if_then_else $cvcl_7 (if_then_else send_data_8 false true) (if_then_else $cvcl_1 false (if_then_else $cvcl_2 (if_then_else $cvcl_4 false $cvcl_8) true)))) (flet ($cvcl_5 (= (- S1_8 cvclZero) 7)) (flet ($cvcl_19 (or $cvcl_5  (and (if_then_else (or $cvcl_5  (and (= (- S1_8 cvclZero) 3) rdy_8) ) false true) send_data_8) )) (flet ($cvcl_6 (and $cvcl_18 $cvcl_19)) (flet ($cvcl_14 (if_then_else $cvcl_7 (if_then_else send_data_8 false false) (if_then_else $cvcl_1 true (if_then_else $cvcl_2 (if_then_else $cvcl_4 true $cvcl_8) false)))) (flet ($cvcl_9 (and (= (- itfc_state_8 cvclZero) 3) tx_end_8)) (flet ($cvcl_212 (= (- itfc_state_8 cvclZero) 0)) (flet ($cvcl_15 (or $cvcl_9  (and (if_then_else (or $cvcl_212  $cvcl_9 ) false true) confirm_8) )) (flet ($cvcl_37 (and $cvcl_14 $cvcl_15)) (flet ($cvcl_20 (or (and $cvcl_10 $cvcl_11)  (and (if_then_else $cvcl_10 false true) mpx_8) )) (flet ($cvcl_39 (or $cvcl_6  (and (if_then_else (or $cvcl_6  (and $cvcl_37 $cvcl_20) ) false true) $cvcl_12) )) (flet ($cvcl_13 (if_then_else $cvcl_7 (if_then_else send_data_8 true false) (if_then_else $cvcl_1 false (if_then_else $cvcl_2 (if_then_else $cvcl_4 false (if_then_else $cvcl_11 true false)) false)))) (flet ($cvcl_43 (or $cvcl_13  (and (if_then_else (or $cvcl_13  (and $cvcl_14 (if_then_else $cvcl_15 false true)) ) false true) $cvcl_16) )) (flet ($cvcl_44 (and (if_then_else (and $cvcl_17 (if_then_else (or (if_then_else $cvcl_39 false true)  $cvcl_43 ) false true)) false true) $cvcl_17)) (flet ($cvcl_38 (if_then_else $cvcl_20 false true)) (flet ($cvcl_33 (= (- itfc_state_8 cvclZero) 0)) (flet ($cvcl_50 (or $cvcl_9  (and (if_then_else (or $cvcl_33  $cvcl_9 ) false true) confirm_8) )) (flet ($cvcl_31 (if_then_else $cvcl_50 false true)) (flet ($cvcl_32 (if_then_else $cvcl_38 false false)) (flet ($cvcl_45 (if_then_else $cvcl_18 (if_then_else $cvcl_19 false true) (if_then_else $cvcl_13 false (if_then_else $cvcl_14 (if_then_else $cvcl_31 false $cvcl_32) true)))) (flet ($cvcl_24 (= (- S1_8 cvclZero) 1)) (flet ($cvcl_25 (= (- S1_8 cvclZero) 2)) (flet ($cvcl_26 (= (- S1_8 cvclZero) 5)) (flet ($cvcl_28 (= (- S1_8 cvclZero) 6)) (flet ($cvcl_29 (= (- S1_8 cvclZero) 4)) (flet ($cvcl_23 (= (- S1_8 cvclZero) 0)) (flet ($cvcl_27 (if_then_else eoc_8 false false)) (flet ($cvcl_55 (if_then_else $cvcl_29 false (if_then_else $cvcl_21 false false))) (flet ($cvcl_52 (if_then_else $cvcl_5 false $cvcl_55)) (flet ($cvcl_22 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 false (if_then_else $cvcl_26 $cvcl_27 (if_then_else $cvcl_28 true $cvcl_52)))))) (flet ($cvcl_46 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 false (if_then_else $cvcl_26 $cvcl_27 (if_then_else $cvcl_28 false (if_then_else $cvcl_5 false (if_then_else $cvcl_29 true (if_then_else $cvcl_21 true false))))))))) (flet ($cvcl_66 (or $cvcl_22  (and (if_then_else (or $cvcl_22  (and $cvcl_46 $cvcl_12) ) false true) $cvcl_19) )) (flet ($cvcl_30 (and $cvcl_45 $cvcl_66)) (flet ($cvcl_41 (if_then_else $cvcl_18 (if_then_else $cvcl_19 false false) (if_then_else $cvcl_13 true (if_then_else $cvcl_14 (if_then_else $cvcl_31 true $cvcl_32) false)))) (flet ($cvcl_34 (= (- itfc_state_8 cvclZero) 1)) (flet ($cvcl_35 (= (- itfc_state_8 cvclZero) 2)) (flet ($cvcl_72 (if_then_else shot_8 false false)) (flet ($cvcl_76 (= (- next_bit_8 cvclZero) 1)) (flet ($cvcl_78 (> (- tx_conta_8 cvclZero) 104)) (flet ($cvcl_75 (if_then_else (and send_en_8 $cvcl_78) false true)) (flet ($cvcl_74 (and $cvcl_76 (if_then_else $cvcl_75 false true))) (flet ($cvcl_36 (and (if_then_else $cvcl_33 $cvcl_72 (if_then_else $cvcl_34 false (if_then_else $cvcl_35 true (if_then_else tx_end_8 false true)))) $cvcl_74)) (flet ($cvcl_71 (if_then_else $cvcl_33 (if_then_else shot_8 false true) (if_then_else $cvcl_34 false (if_then_else $cvcl_35 false (if_then_else tx_end_8 true false))))) (flet ($cvcl_49 (if_then_else (or $cvcl_71  $cvcl_36 ) false true)) (flet ($cvcl_42 (or $cvcl_36  (and $cvcl_49 $cvcl_15) )) (flet ($cvcl_82 (and $cvcl_41 $cvcl_42)) (flet ($cvcl_83 (or (and $cvcl_37 $cvcl_38)  (and (if_then_else $cvcl_37 false true) $cvcl_20) )) (flet ($cvcl_84 (or $cvcl_30  (and (if_then_else (or $cvcl_30  (and $cvcl_82 $cvcl_83) ) false true) $cvcl_39) )) (flet ($cvcl_40 (if_then_else $cvcl_18 (if_then_else $cvcl_19 true false) (if_then_else $cvcl_13 false (if_then_else $cvcl_14 (if_then_else $cvcl_31 false (if_then_else $cvcl_38 true false)) false)))) (flet ($cvcl_89 (or $cvcl_40  (and (if_then_else (or $cvcl_40  (and $cvcl_41 (if_then_else $cvcl_42 false true)) ) false true) $cvcl_43) )) (flet ($cvcl_90 (and (if_then_else (and $cvcl_44 (if_then_else (or (if_then_else $cvcl_84 false true)  $cvcl_89 ) false true)) false true) $cvcl_44)) (flet ($cvcl_47 (and $cvcl_7 send_data_8)) (flet ($cvcl_56 (or $cvcl_47  (and (if_then_else (or $cvcl_47  $cvcl_48 ) false true) rdy_8) )) (flet ($cvcl_68 (or $cvcl_22  (and (if_then_else (or $cvcl_22  (and $cvcl_46 $cvcl_56) ) false true) $cvcl_19) )) (flet ($cvcl_94 (or $cvcl_36  (and $cvcl_49 $cvcl_50) )) (flet ($cvcl_69 (if_then_else $cvcl_94 false true)) (flet ($cvcl_51 (and $cvcl_14 $cvcl_50)) (flet ($cvcl_96 (or (and $cvcl_51 $cvcl_38)  (and (if_then_else $cvcl_51 false true) $cvcl_20) )) (flet ($cvcl_85 (if_then_else $cvcl_96 false true)) (flet ($cvcl_70 (if_then_else $cvcl_85 false false)) (flet ($cvcl_91 (if_then_else $cvcl_45 (if_then_else $cvcl_68 false true) (if_then_else $cvcl_40 false (if_then_else $cvcl_41 (if_then_else $cvcl_69 false $cvcl_70) true)))) (flet ($cvcl_58 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 false (if_then_else $cvcl_26 $cvcl_27 (if_then_else $cvcl_28 false (if_then_else $cvcl_5 false (if_then_else $cvcl_29 false (if_then_else $cvcl_21 false true))))))))) (flet ($cvcl_54 (if_then_else $cvcl_28 false $cvcl_52)) (flet ($cvcl_53 (if_then_else $cvcl_25 false (if_then_else $cvcl_26 $cvcl_27 $cvcl_54))) (flet ($cvcl_59 (if_then_else $cvcl_23 true (if_then_else $cvcl_24 false $cvcl_53))) (flet ($cvcl_60 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 true $cvcl_53))) (flet ($cvcl_61 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 true (if_then_else $cvcl_26 (if_then_else eoc_8 true false) $cvcl_54))))) (flet ($cvcl_63 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 false (if_then_else $cvcl_26 (if_then_else eoc_8 false true) $cvcl_54))))) (flet ($cvcl_64 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false (if_then_else $cvcl_25 false (if_then_else $cvcl_26 $cvcl_27 (if_then_else $cvcl_28 false (if_then_else $cvcl_5 true $cvcl_55))))))) (flet ($cvcl_65 (if_then_else $cvcl_56 false true)) (flet ($cvcl_62 (if_then_else eoc_7 false false)) (flet ($cvcl_100 (if_then_else $cvcl_64 false (if_then_else $cvcl_65 false false))) (flet ($cvcl_97 (if_then_else $cvcl_22 false $cvcl_100)) (flet ($cvcl_57 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 false (if_then_else $cvcl_61 $cvcl_62 (if_then_else $cvcl_63 true $cvcl_97)))))) (flet ($cvcl_92 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 false (if_then_else $cvcl_61 $cvcl_62 (if_then_else $cvcl_63 false (if_then_else $cvcl_22 false (if_then_else $cvcl_64 true (if_then_else $cvcl_65 true false))))))))) (flet ($cvcl_111 (or $cvcl_57  (and (if_then_else (or $cvcl_57  (and $cvcl_92 $cvcl_39) ) false true) $cvcl_66) )) (flet ($cvcl_67 (and $cvcl_91 $cvcl_111)) (flet ($cvcl_87 (if_then_else $cvcl_45 (if_then_else $cvcl_68 false false) (if_then_else $cvcl_40 true (if_then_else $cvcl_41 (if_then_else $cvcl_69 true $cvcl_70) false)))) (flet ($cvcl_73 (if_then_else $cvcl_35 false (if_then_else tx_end_8 false false))) (flet ($cvcl_79 (if_then_else $cvcl_33 (if_then_else shot_8 true false) (if_then_else $cvcl_34 false $cvcl_73))) (flet ($cvcl_80 (if_then_else $cvcl_33 $cvcl_72 (if_then_else $cvcl_34 true $cvcl_73))) (flet ($cvcl_117 (if_then_else $cvcl_16 false false)) (flet ($cvcl_122 (>= (- next_bit_8 cvclZero) 10)) (flet ($cvcl_121 (or $cvcl_75  $cvcl_122 )) (flet ($cvcl_124 (= (- next_bit_8 cvclZero) 2)) (flet ($cvcl_125 (= (- next_bit_8 cvclZero) 3)) (flet ($cvcl_126 (= (- next_bit_8 cvclZero) 4)) (flet ($cvcl_127 (= (- next_bit_8 cvclZero) 5)) (flet ($cvcl_128 (= (- next_bit_8 cvclZero) 6)) (flet ($cvcl_129 (= (- next_bit_8 cvclZero) 7)) (flet ($cvcl_130 (= (- next_bit_8 cvclZero) 8)) (flet ($cvcl_131 (= (- next_bit_8 cvclZero) 9)) (flet ($cvcl_123 (= (- next_bit_8 cvclZero) 0)) (flet ($cvcl_132 (if_then_else $cvcl_121 $cvcl_76 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 false (if_then_else $cvcl_128 false (if_then_else $cvcl_129 false (if_then_else $cvcl_130 false (if_then_else $cvcl_131 true false))))))))))) (flet ($cvcl_77 (and send_8 (and tre_8 dsr_8))) (flet ($cvcl_143 (or $cvcl_77  (and (if_then_else (or tx_end_8  $cvcl_77 ) false true) send_en_8) )) (flet ($cvcl_145 (if_then_else $cvcl_78 true false)) (flet ($cvcl_146 (> (- tx_conta_8 cvclZero) 103)) (flet ($cvcl_144 (if_then_else send_en_8 (if_then_else $cvcl_145 false $cvcl_146) $cvcl_78)) (flet ($cvcl_120 (if_then_else (and $cvcl_143 $cvcl_144) false true)) (flet ($cvcl_119 (and $cvcl_132 (if_then_else $cvcl_120 false true))) (flet ($cvcl_81 (and (if_then_else $cvcl_71 $cvcl_117 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 true (if_then_else $cvcl_74 false true)))) $cvcl_119)) (flet ($cvcl_116 (if_then_else $cvcl_71 (if_then_else $cvcl_16 false true) (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_74 true false))))) (flet ($cvcl_93 (if_then_else (or $cvcl_116  $cvcl_81 ) false true)) (flet ($cvcl_88 (or $cvcl_81  (and $cvcl_93 $cvcl_42) )) (flet ($cvcl_151 (and $cvcl_87 $cvcl_88)) (flet ($cvcl_152 (or (and $cvcl_82 (if_then_else $cvcl_83 false true))  (and (if_then_else $cvcl_82 false true) $cvcl_83) )) (flet ($cvcl_153 (or $cvcl_67  (and (if_then_else (or $cvcl_67  (and $cvcl_151 $cvcl_152) ) false true) $cvcl_84) )) (flet ($cvcl_86 (if_then_else $cvcl_45 (if_then_else $cvcl_68 true false) (if_then_else $cvcl_40 false (if_then_else $cvcl_41 (if_then_else $cvcl_69 false (if_then_else $cvcl_85 true false)) false)))) (flet ($cvcl_158 (or $cvcl_86  (and (if_then_else (or $cvcl_86  (and $cvcl_87 (if_then_else $cvcl_88 false true)) ) false true) $cvcl_89) )) (flet ($cvcl_159 (and (if_then_else (and $cvcl_90 (if_then_else (or (if_then_else $cvcl_153 false true)  $cvcl_158 ) false true)) false true) $cvcl_90)) (flet ($cvcl_101 (or $cvcl_6  (and (if_then_else (or $cvcl_6  (and $cvcl_51 $cvcl_20) ) false true) $cvcl_56) )) (flet ($cvcl_113 (or $cvcl_57  (and (if_then_else (or $cvcl_57  (and $cvcl_92 $cvcl_101) ) false true) $cvcl_68) )) (flet ($cvcl_164 (or $cvcl_81  (and $cvcl_93 $cvcl_94) )) (flet ($cvcl_114 (if_then_else $cvcl_164 false true)) (flet ($cvcl_95 (and $cvcl_41 $cvcl_94)) (flet ($cvcl_166 (or (and $cvcl_95 $cvcl_85)  (and (if_then_else $cvcl_95 false true) $cvcl_96) )) (flet ($cvcl_154 (if_then_else $cvcl_166 false true)) (flet ($cvcl_115 (if_then_else $cvcl_154 false false)) (flet ($cvcl_160 (if_then_else $cvcl_91 (if_then_else $cvcl_113 false true) (if_then_else $cvcl_86 false (if_then_else $cvcl_87 (if_then_else $cvcl_114 false $cvcl_115) true)))) (flet ($cvcl_103 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 false (if_then_else $cvcl_61 $cvcl_62 (if_then_else $cvcl_63 false (if_then_else $cvcl_22 false (if_then_else $cvcl_64 false (if_then_else $cvcl_65 false true))))))))) (flet ($cvcl_99 (if_then_else $cvcl_63 false $cvcl_97)) (flet ($cvcl_98 (if_then_else $cvcl_60 false (if_then_else $cvcl_61 $cvcl_62 $cvcl_99))) (flet ($cvcl_104 (if_then_else $cvcl_58 true (if_then_else $cvcl_59 false $cvcl_98))) (flet ($cvcl_105 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 true $cvcl_98))) (flet ($cvcl_106 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 true (if_then_else $cvcl_61 (if_then_else eoc_7 true false) $cvcl_99))))) (flet ($cvcl_108 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 false (if_then_else $cvcl_61 (if_then_else eoc_7 false true) $cvcl_99))))) (flet ($cvcl_109 (if_then_else $cvcl_58 false (if_then_else $cvcl_59 false (if_then_else $cvcl_60 false (if_then_else $cvcl_61 $cvcl_62 (if_then_else $cvcl_63 false (if_then_else $cvcl_22 true $cvcl_100))))))) (flet ($cvcl_110 (if_then_else $cvcl_101 false true)) (flet ($cvcl_107 (if_then_else eoc_6 false false)) (flet ($cvcl_170 (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false false))) (flet ($cvcl_167 (if_then_else $cvcl_57 false $cvcl_170)) (flet ($cvcl_102 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 false (if_then_else $cvcl_106 $cvcl_107 (if_then_else $cvcl_108 true $cvcl_167)))))) (flet ($cvcl_161 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 false (if_then_else $cvcl_106 $cvcl_107 (if_then_else $cvcl_108 false (if_then_else $cvcl_57 false (if_then_else $cvcl_109 true (if_then_else $cvcl_110 true false))))))))) (flet ($cvcl_181 (or $cvcl_102  (and (if_then_else (or $cvcl_102  (and $cvcl_161 $cvcl_84) ) false true) $cvcl_111) )) (flet ($cvcl_112 (and $cvcl_160 $cvcl_181)) (flet ($cvcl_156 (if_then_else $cvcl_91 (if_then_else $cvcl_113 false false) (if_then_else $cvcl_86 true (if_then_else $cvcl_87 (if_then_else $cvcl_114 true $cvcl_115) false)))) (flet ($cvcl_118 (if_then_else $cvcl_80 false (if_then_else $cvcl_74 false false))) (flet ($cvcl_148 (if_then_else $cvcl_71 (if_then_else $cvcl_16 true false) (if_then_else $cvcl_79 false $cvcl_118))) (flet ($cvcl_149 (if_then_else $cvcl_71 $cvcl_117 (if_then_else $cvcl_79 true $cvcl_118))) (flet ($cvcl_147 (or $cvcl_13  (and (if_then_else (or $cvcl_13  (and $cvcl_14 $cvcl_31) ) false true) $cvcl_16) )) (flet ($cvcl_187 (if_then_else $cvcl_147 false false)) (flet ($cvcl_140 (if_then_else $cvcl_131 false false)) (flet ($cvcl_139 (if_then_else $cvcl_130 false $cvcl_140)) (flet ($cvcl_138 (if_then_else $cvcl_129 false $cvcl_139)) (flet ($cvcl_137 (if_then_else $cvcl_128 false $cvcl_138)) (flet ($cvcl_136 (if_then_else $cvcl_127 false $cvcl_137)) (flet ($cvcl_135 (if_then_else $cvcl_126 false $cvcl_136)) (flet ($cvcl_134 (if_then_else $cvcl_125 false $cvcl_135)) (flet ($cvcl_133 (if_then_else $cvcl_124 false $cvcl_134)) (flet ($cvcl_192 (if_then_else $cvcl_121 $cvcl_122 (if_then_else $cvcl_123 false $cvcl_133))) (flet ($cvcl_191 (or $cvcl_120  $cvcl_192 )) (flet ($cvcl_194 (if_then_else $cvcl_121 $cvcl_124 (if_then_else $cvcl_123 true $cvcl_133))) (flet ($cvcl_195 (if_then_else $cvcl_121 $cvcl_125 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 true $cvcl_134)))) (flet ($cvcl_196 (if_then_else $cvcl_121 $cvcl_126 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 true $cvcl_135))))) (flet ($cvcl_197 (if_then_else $cvcl_121 $cvcl_127 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 true $cvcl_136)))))) (flet ($cvcl_198 (if_then_else $cvcl_121 $cvcl_128 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 true $cvcl_137))))))) (flet ($cvcl_199 (if_then_else $cvcl_121 $cvcl_129 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 false (if_then_else $cvcl_128 true $cvcl_138)))))))) (flet ($cvcl_200 (if_then_else $cvcl_121 $cvcl_130 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 false (if_then_else $cvcl_128 false (if_then_else $cvcl_129 true $cvcl_139))))))))) (flet ($cvcl_201 (if_then_else $cvcl_121 $cvcl_131 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 false (if_then_else $cvcl_128 false (if_then_else $cvcl_129 false (if_then_else $cvcl_130 true $cvcl_140)))))))))) (flet ($cvcl_193 (if_then_else $cvcl_121 $cvcl_123 (if_then_else $cvcl_123 false (if_then_else $cvcl_124 false (if_then_else $cvcl_125 false (if_then_else $cvcl_126 false (if_then_else $cvcl_127 false (if_then_else $cvcl_128 false (if_then_else $cvcl_129 false (if_then_else $cvcl_130 false (if_then_else $cvcl_131 false true))))))))))) (flet ($cvcl_202 (if_then_else $cvcl_191 $cvcl_132 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 false (if_then_else $cvcl_198 false (if_then_else $cvcl_199 false (if_then_else $cvcl_200 false (if_then_else $cvcl_201 true false))))))))))) (flet ($cvcl_211 (or $cvcl_34  (and (if_then_else (or $cvcl_34  $cvcl_35 ) false true) send_8) )) (flet ($cvcl_141 (or tx_end_8  (and load_8 (if_then_else tre_8 false true)) )) (flet ($cvcl_214 (or $cvcl_141  (and (if_then_else $cvcl_141 false true) tre_8) )) (flet ($cvcl_142 (and $cvcl_211 (and $cvcl_214 dsr_7))) (flet ($cvcl_217 (or $cvcl_142  (and (if_then_else (or $cvcl_74  $cvcl_142 ) false true) $cvcl_143) )) (flet ($cvcl_219 (if_then_else $cvcl_144 true false)) (flet ($cvcl_220 (> (- tx_conta_8 cvclZero) 102)) (flet ($cvcl_221 (if_then_else send_en_8 (if_then_else $cvcl_145 false $cvcl_220) $cvcl_146)) (flet ($cvcl_218 (if_then_else $cvcl_143 (if_then_else $cvcl_219 false $cvcl_221) $cvcl_144)) (flet ($cvcl_190 (if_then_else (and $cvcl_217 $cvcl_218) false true)) (flet ($cvcl_189 (and $cvcl_202 (if_then_else $cvcl_190 false true))) (flet ($cvcl_150 (and (if_then_else $cvcl_116 $cvcl_187 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 true (if_then_else $cvcl_119 false true)))) $cvcl_189)) (flet ($cvcl_186 (if_then_else $cvcl_116 (if_then_else $cvcl_147 false true) (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_119 true false))))) (flet ($cvcl_163 (if_then_else (or $cvcl_186  $cvcl_150 ) false true)) (flet ($cvcl_157 (or $cvcl_150  (and $cvcl_163 $cvcl_88) )) (flet ($cvcl_226 (and $cvcl_156 $cvcl_157)) (flet ($cvcl_227 (or (and $cvcl_151 (if_then_else $cvcl_152 false true))  (and (if_then_else $cvcl_151 false true) $cvcl_152) )) (flet ($cvcl_228 (or $cvcl_112  (and (if_then_else (or $cvcl_112  (and $cvcl_226 $cvcl_227) ) false true) $cvcl_153) )) (flet ($cvcl_155 (if_then_else $cvcl_91 (if_then_else $cvcl_113 true false) (if_then_else $cvcl_86 false (if_then_else $cvcl_87 (if_then_else $cvcl_114 false (if_then_else $cvcl_154 true false)) false)))) (flet ($cvcl_233 (or $cvcl_155  (and (if_then_else (or $cvcl_155  (and $cvcl_156 (if_then_else $cvcl_157 false true)) ) false true) $cvcl_158) )) (flet ($cvcl_234 (and (if_then_else (and $cvcl_159 (if_then_else (or (if_then_else $cvcl_228 false true)  $cvcl_233 ) false true)) false true) $cvcl_159)) (flet ($cvcl_162 (and $cvcl_45 $cvcl_68)) (flet ($cvcl_171 (or $cvcl_162  (and (if_then_else (or $cvcl_162  (and $cvcl_95 $cvcl_96) ) false true) $cvcl_101) )) (flet ($cvcl_183 (or $cvcl_102  (and (if_then_else (or $cvcl_102  (and $cvcl_161 $cvcl_171) ) false true) $cvcl_113) )) (flet ($cvcl_248 (or $cvcl_150  (and $cvcl_163 $cvcl_164) )) (flet ($cvcl_184 (if_then_else $cvcl_248 false true)) (flet ($cvcl_165 (and $cvcl_87 $cvcl_164)) (flet ($cvcl_250 (or (and $cvcl_165 $cvcl_154)  (and (if_then_else $cvcl_165 false true) $cvcl_166) )) (flet ($cvcl_229 (if_then_else $cvcl_250 false true)) (flet ($cvcl_185 (if_then_else $cvcl_229 false false)) (flet ($cvcl_235 (if_then_else $cvcl_160 (if_then_else $cvcl_183 false true) (if_then_else $cvcl_155 false (if_then_else $cvcl_156 (if_then_else $cvcl_184 false $cvcl_185) true)))) (flet ($cvcl_173 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 false (if_then_else $cvcl_106 $cvcl_107 (if_then_else $cvcl_108 false (if_then_else $cvcl_57 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false true))))))))) (flet ($cvcl_169 (if_then_else $cvcl_108 false $cvcl_167)) (flet ($cvcl_168 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 $cvcl_107 $cvcl_169))) (flet ($cvcl_174 (if_then_else $cvcl_103 true (if_then_else $cvcl_104 false $cvcl_168))) (flet ($cvcl_175 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 true $cvcl_168))) (flet ($cvcl_176 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 true (if_then_else $cvcl_106 (if_then_else eoc_6 true false) $cvcl_169))))) (flet ($cvcl_178 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 false (if_then_else $cvcl_106 (if_then_else eoc_6 false true) $cvcl_169))))) (flet ($cvcl_179 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false (if_then_else $cvcl_105 false (if_then_else $cvcl_106 $cvcl_107 (if_then_else $cvcl_108 false (if_then_else $cvcl_57 true $cvcl_170))))))) (flet ($cvcl_180 (if_then_else $cvcl_171 false true)) (flet ($cvcl_177 (if_then_else eoc_5 false false)) (flet ($cvcl_254 (if_then_else $cvcl_179 false (if_then_else $cvcl_180 false false))) (flet ($cvcl_251 (if_then_else $cvcl_102 false $cvcl_254)) (flet ($cvcl_172 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 false (if_then_else $cvcl_176 $cvcl_177 (if_then_else $cvcl_178 true $cvcl_251)))))) (flet ($cvcl_236 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 false (if_then_else $cvcl_176 $cvcl_177 (if_then_else $cvcl_178 false (if_then_else $cvcl_102 false (if_then_else $cvcl_179 true (if_then_else $cvcl_180 true false))))))))) (flet ($cvcl_265 (or $cvcl_172  (and (if_then_else (or $cvcl_172  (and $cvcl_236 $cvcl_153) ) false true) $cvcl_181) )) (flet ($cvcl_182 (and $cvcl_235 $cvcl_265)) (flet ($cvcl_231 (if_then_else $cvcl_160 (if_then_else $cvcl_183 false false) (if_then_else $cvcl_155 true (if_then_else $cvcl_156 (if_then_else $cvcl_184 true $cvcl_185) false)))) (flet ($cvcl_188 (if_then_else $cvcl_149 false (if_then_else $cvcl_119 false false))) (flet ($cvcl_223 (if_then_else $cvcl_116 (if_then_else $cvcl_147 true false) (if_then_else $cvcl_148 false $cvcl_188))) (flet ($cvcl_224 (if_then_else $cvcl_116 $cvcl_187 (if_then_else $cvcl_148 true $cvcl_188))) (flet ($cvcl_222 (or $cvcl_40  (and (if_then_else (or $cvcl_40  (and $cvcl_41 $cvcl_69) ) false true) $cvcl_147) )) (flet ($cvcl_270 (if_then_else $cvcl_222 false false)) (flet ($cvcl_238 (if_then_else $cvcl_186 $cvcl_270 (if_then_else $cvcl_223 false (if_then_else $cvcl_224 true (if_then_else $cvcl_189 false true))))) (flet ($cvcl_210 (if_then_else $cvcl_201 false false)) (flet ($cvcl_209 (if_then_else $cvcl_200 false $cvcl_210)) (flet ($cvcl_208 (if_then_else $cvcl_199 false $cvcl_209)) (flet ($cvcl_207 (if_then_else $cvcl_198 false $cvcl_208)) (flet ($cvcl_206 (if_then_else $cvcl_197 false $cvcl_207)) (flet ($cvcl_205 (if_then_else $cvcl_196 false $cvcl_206)) (flet ($cvcl_204 (if_then_else $cvcl_195 false $cvcl_205)) (flet ($cvcl_203 (if_then_else $cvcl_194 false $cvcl_204)) (flet ($cvcl_275 (if_then_else $cvcl_191 $cvcl_192 (if_then_else $cvcl_193 false $cvcl_203))) (flet ($cvcl_274 (or $cvcl_190  $cvcl_275 )) (flet ($cvcl_277 (if_then_else $cvcl_191 $cvcl_194 (if_then_else $cvcl_193 true $cvcl_203))) (flet ($cvcl_278 (if_then_else $cvcl_191 $cvcl_195 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 true $cvcl_204)))) (flet ($cvcl_279 (if_then_else $cvcl_191 $cvcl_196 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 true $cvcl_205))))) (flet ($cvcl_280 (if_then_else $cvcl_191 $cvcl_197 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 true $cvcl_206)))))) (flet ($cvcl_281 (if_then_else $cvcl_191 $cvcl_198 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 true $cvcl_207))))))) (flet ($cvcl_282 (if_then_else $cvcl_191 $cvcl_199 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 false (if_then_else $cvcl_198 true $cvcl_208)))))))) (flet ($cvcl_283 (if_then_else $cvcl_191 $cvcl_200 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 false (if_then_else $cvcl_198 false (if_then_else $cvcl_199 true $cvcl_209))))))))) (flet ($cvcl_284 (if_then_else $cvcl_191 $cvcl_201 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 false (if_then_else $cvcl_198 false (if_then_else $cvcl_199 false (if_then_else $cvcl_200 true $cvcl_210)))))))))) (flet ($cvcl_276 (if_then_else $cvcl_191 $cvcl_193 (if_then_else $cvcl_193 false (if_then_else $cvcl_194 false (if_then_else $cvcl_195 false (if_then_else $cvcl_196 false (if_then_else $cvcl_197 false (if_then_else $cvcl_198 false (if_then_else $cvcl_199 false (if_then_else $cvcl_200 false (if_then_else $cvcl_201 false true))))))))))) (flet ($cvcl_239 (if_then_else $cvcl_274 $cvcl_202 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 false (if_then_else $cvcl_281 false (if_then_else $cvcl_282 false (if_then_else $cvcl_283 false (if_then_else $cvcl_284 true false))))))))))) (flet ($cvcl_240 (or $cvcl_79  (and (if_then_else (or $cvcl_79  $cvcl_80 ) false true) $cvcl_211) )) (flet ($cvcl_213 (and $cvcl_212 shot_8)) (flet ($cvcl_294 (or $cvcl_213  (and (if_then_else (or $cvcl_213  $cvcl_34 ) false true) load_8) )) (flet ($cvcl_242 (if_then_else $cvcl_214 false true)) (flet ($cvcl_215 (or $cvcl_74  (and $cvcl_294 $cvcl_242) )) (flet ($cvcl_295 (or $cvcl_215  (and (if_then_else $cvcl_215 false true) $cvcl_214) )) (flet ($cvcl_216 (and $cvcl_240 (and $cvcl_295 dsr_6))) (flet ($cvcl_298 (or $cvcl_216  (and (if_then_else (or $cvcl_119  $cvcl_216 ) false true) $cvcl_217) )) (flet ($cvcl_300 (if_then_else $cvcl_218 true false)) (flet ($cvcl_301 (> (- tx_conta_8 cvclZero) 101)) (flet ($cvcl_302 (if_then_else send_en_8 (if_then_else $cvcl_145 false $cvcl_301) $cvcl_220)) (flet ($cvcl_303 (if_then_else $cvcl_143 (if_then_else $cvcl_219 false $cvcl_302) $cvcl_221)) (flet ($cvcl_245 (if_then_else $cvcl_217 (if_then_else $cvcl_300 false $cvcl_303) $cvcl_218)) (flet ($cvcl_225 (and $cvcl_238 (and $cvcl_239 (if_then_else (if_then_else (and $cvcl_298 $cvcl_245) false true) false true)))) (flet ($cvcl_246 (if_then_else $cvcl_186 (if_then_else $cvcl_222 false true) (if_then_else $cvcl_223 false (if_then_else $cvcl_224 false (if_then_else $cvcl_189 true false))))) (flet ($cvcl_232 (or $cvcl_225  (and (if_then_else (or $cvcl_246  $cvcl_225 ) false true) $cvcl_157) )) (flet ($cvcl_308 (and $cvcl_231 $cvcl_232)) (flet ($cvcl_309 (or (and $cvcl_226 (if_then_else $cvcl_227 false true))  (and (if_then_else $cvcl_226 false true) $cvcl_227) )) (flet ($cvcl_310 (or $cvcl_182  (and (if_then_else (or $cvcl_182  (and $cvcl_308 $cvcl_309) ) false true) $cvcl_228) )) (flet ($cvcl_230 (if_then_else $cvcl_160 (if_then_else $cvcl_183 true false) (if_then_else $cvcl_155 false (if_then_else $cvcl_156 (if_then_else $cvcl_184 false (if_then_else $cvcl_229 true false)) false)))) (flet ($cvcl_315 (or $cvcl_230  (and (if_then_else (or $cvcl_230  (and $cvcl_231 (if_then_else $cvcl_232 false true)) ) false true) $cvcl_233) )) (flet ($cvcl_316 (and (if_then_else (and $cvcl_234 (if_then_else (or (if_then_else $cvcl_310 false true)  $cvcl_315 ) false true)) false true) $cvcl_234)) (flet ($cvcl_237 (and $cvcl_91 $cvcl_113)) (flet ($cvcl_255 (or $cvcl_237  (and (if_then_else (or $cvcl_237  (and $cvcl_165 $cvcl_166) ) false true) $cvcl_171) )) (flet ($cvcl_267 (or $cvcl_172  (and (if_then_else (or $cvcl_172  (and $cvcl_236 $cvcl_255) ) false true) $cvcl_183) )) (flet ($cvcl_241 (and $cvcl_33 shot_8)) (flet ($cvcl_243 (or $cvcl_74  (and (or $cvcl_241  (and (if_then_else (or $cvcl_241  $cvcl_34 ) false true) load_8) ) $cvcl_242) )) (flet ($cvcl_244 (and $cvcl_240 (and (or $cvcl_243  (and (if_then_else $cvcl_243 false true) $cvcl_214) ) dsr_6))) (flet ($cvcl_299 (or $cvcl_244  (and (if_then_else (or $cvcl_119  $cvcl_244 ) false true) $cvcl_217) )) (flet ($cvcl_273 (if_then_else (and $cvcl_299 $cvcl_245) false true)) (flet ($cvcl_272 (and $cvcl_239 (if_then_else $cvcl_273 false true))) (flet ($cvcl_247 (and $cvcl_238 $cvcl_272)) (flet ($cvcl_268 (if_then_else (or $cvcl_247  (and (if_then_else (or $cvcl_246  $cvcl_247 ) false true) $cvcl_248) ) false true)) (flet ($cvcl_249 (and $cvcl_156 $cvcl_248)) (flet ($cvcl_311 (if_then_else (or (and $cvcl_249 $cvcl_229)  (and (if_then_else $cvcl_249 false true) $cvcl_250) ) false true)) (flet ($cvcl_269 (if_then_else $cvcl_311 false false)) (flet ($cvcl_257 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 false (if_then_else $cvcl_176 $cvcl_177 (if_then_else $cvcl_178 false (if_then_else $cvcl_102 false (if_then_else $cvcl_179 false (if_then_else $cvcl_180 false true))))))))) (flet ($cvcl_253 (if_then_else $cvcl_178 false $cvcl_251)) (flet ($cvcl_252 (if_then_else $cvcl_175 false (if_then_else $cvcl_176 $cvcl_177 $cvcl_253))) (flet ($cvcl_258 (if_then_else $cvcl_173 true (if_then_else $cvcl_174 false $cvcl_252))) (flet ($cvcl_259 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 true $cvcl_252))) (flet ($cvcl_260 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 true (if_then_else $cvcl_176 (if_then_else eoc_5 true false) $cvcl_253))))) (flet ($cvcl_262 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 false (if_then_else $cvcl_176 (if_then_else eoc_5 false true) $cvcl_253))))) (flet ($cvcl_263 (if_then_else $cvcl_173 false (if_then_else $cvcl_174 false (if_then_else $cvcl_175 false (if_then_else $cvcl_176 $cvcl_177 (if_then_else $cvcl_178 false (if_then_else $cvcl_102 true $cvcl_254))))))) (flet ($cvcl_264 (if_then_else $cvcl_255 false true)) (flet ($cvcl_261 (if_then_else eoc_4 false false)) (flet ($cvcl_256 (if_then_else $cvcl_257 false (if_then_else $cvcl_258 false (if_then_else $cvcl_259 false (if_then_else $cvcl_260 $cvcl_261 (if_then_else $cvcl_262 true (if_then_else $cvcl_172 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false false))))))))) (flet ($cvcl_266 (and (if_then_else $cvcl_235 (if_then_else $cvcl_267 false true) (if_then_else $cvcl_230 false (if_then_else $cvcl_231 (if_then_else $cvcl_268 false $cvcl_269) true))) (or $cvcl_256  (and (if_then_else (or $cvcl_256  (and (if_then_else $cvcl_257 false (if_then_else $cvcl_258 false (if_then_else $cvcl_259 false (if_then_else $cvcl_260 $cvcl_261 (if_then_else $cvcl_262 false (if_then_else $cvcl_172 false (if_then_else $cvcl_263 true (if_then_else $cvcl_264 true false)))))))) $cvcl_228) ) false true) $cvcl_265) ))) (flet ($cvcl_313 (if_then_else $cvcl_235 (if_then_else $cvcl_267 false false) (if_then_else $cvcl_230 true (if_then_else $cvcl_231 (if_then_else $cvcl_268 true $cvcl_269) false)))) (flet ($cvcl_271 (if_then_else $cvcl_224 false (if_then_else $cvcl_189 false false))) (flet ($cvcl_305 (if_then_else $cvcl_186 (if_then_else $cvcl_222 true false) (if_then_else $cvcl_223 false $cvcl_271))) (flet ($cvcl_306 (if_then_else $cvcl_186 $cvcl_270 (if_then_else $cvcl_223 true $cvcl_271))) (flet ($cvcl_304 (or $cvcl_86  (and (if_then_else (or $cvcl_86  (and $cvcl_87 $cvcl_114) ) false true) $cvcl_222) )) (flet ($cvcl_292 (if_then_else $cvcl_284 false false)) (flet ($cvcl_291 (if_then_else $cvcl_283 false $cvcl_292)) (flet ($cvcl_290 (if_then_else $cvcl_282 false $cvcl_291)) (flet ($cvcl_289 (if_then_else $cvcl_281 false $cvcl_290)) (flet ($cvcl_288 (if_then_else $cvcl_280 false $cvcl_289)) (flet ($cvcl_287 (if_then_else $cvcl_279 false $cvcl_288)) (flet ($cvcl_286 (if_then_else $cvcl_278 false $cvcl_287)) (flet ($cvcl_285 (if_then_else $cvcl_277 false $cvcl_286)) (flet ($cvcl_293 (and $cvcl_71 $cvcl_16)) (flet ($cvcl_296 (or $cvcl_119  (and (or $cvcl_293  (and (if_then_else (or $cvcl_293  $cvcl_79 ) false true) $cvcl_294) ) (if_then_else $cvcl_295 false true)) )) (flet ($cvcl_297 (and (or $cvcl_148  (and (if_then_else (or $cvcl_148  $cvcl_149 ) false true) $cvcl_240) ) (and (or $cvcl_296  (and (if_then_else $cvcl_296 false true) $cvcl_295) ) dsr_5))) (flet ($cvcl_307 (and (if_then_else $cvcl_246 (if_then_else $cvcl_304 false false) (if_then_else $cvcl_305 false (if_then_else $cvcl_306 true (if_then_else $cvcl_272 false true)))) (and (if_then_else (or $cvcl_273  (if_then_else $cvcl_274 $cvcl_275 (if_then_else $cvcl_276 false $cvcl_285)) ) $cvcl_239 (if_then_else (if_then_else $cvcl_274 $cvcl_276 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 false (if_then_else $cvcl_281 false (if_then_else $cvcl_282 false (if_then_else $cvcl_283 false (if_then_else $cvcl_284 false true)))))))))) false (if_then_else (if_then_else $cvcl_274 $cvcl_277 (if_then_else $cvcl_276 true $cvcl_285)) false (if_then_else (if_then_else $cvcl_274 $cvcl_278 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 true $cvcl_286))) false (if_then_else (if_then_else $cvcl_274 $cvcl_279 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 true $cvcl_287)))) false (if_then_else (if_then_else $cvcl_274 $cvcl_280 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 true $cvcl_288))))) false (if_then_else (if_then_else $cvcl_274 $cvcl_281 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 true $cvcl_289)))))) false (if_then_else (if_then_else $cvcl_274 $cvcl_282 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 false (if_then_else $cvcl_281 true $cvcl_290))))))) false (if_then_else (if_then_else $cvcl_274 $cvcl_283 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 false (if_then_else $cvcl_281 false (if_then_else $cvcl_282 true $cvcl_291)))))))) false (if_then_else (if_then_else $cvcl_274 $cvcl_284 (if_then_else $cvcl_276 false (if_then_else $cvcl_277 false (if_then_else $cvcl_278 false (if_then_else $cvcl_279 false (if_then_else $cvcl_280 false (if_then_else $cvcl_281 false (if_then_else $cvcl_282 false (if_then_else $cvcl_283 true $cvcl_292))))))))) true false)))))))))) (if_then_else (if_then_else (and (or $cvcl_297  (and (if_then_else (or $cvcl_189  $cvcl_297 ) false true) $cvcl_298) ) (if_then_else $cvcl_299 (if_then_else (if_then_else $cvcl_245 true false) false (if_then_else $cvcl_217 (if_then_else $cvcl_300 false (if_then_else $cvcl_143 (if_then_else $cvcl_219 false (if_then_else send_en_8 (if_then_else $cvcl_145 false (> (- tx_conta_8 cvclZero) 100)) $cvcl_301)) $cvcl_302)) $cvcl_303)) $cvcl_245)) false true) false true)))) (flet ($cvcl_314 (or $cvcl_307  (and (if_then_else (or (if_then_else $cvcl_246 (if_then_else $cvcl_304 false true) (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_272 true false))))  $cvcl_307 ) false true) $cvcl_232) )) (flet ($cvcl_312 (if_then_else $cvcl_235 (if_then_else $cvcl_267 true false) (if_then_else $cvcl_230 false (if_then_else $cvcl_231 (if_then_else $cvcl_268 false (if_then_else $cvcl_311 true false)) false)))) (not (iff (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (if_then_else (and (if_then_else (and $cvcl_316 (if_then_else (or (if_then_else (or $cvcl_266  (and (if_then_else (or $cvcl_266  (and (and $cvcl_313 $cvcl_314) (or (and $cvcl_308 (if_then_else $cvcl_309 false true))  (and (if_then_else $cvcl_308 false true) $cvcl_309) )) ) false true) $cvcl_310) ) false true)  (or $cvcl_312  (and (if_then_else (or $cvcl_312  (and $cvcl_313 (if_then_else $cvcl_314 false true)) ) false true) $cvcl_315) ) ) false true)) false true) $cvcl_316) false true) (iff send_data_8 false)) (iff rdy_8 false)) (iff shot_8 false)) (iff mpx_8 false)) (iff load_8 false)) (iff confirm_8 false)) (iff send_8 false)) (iff send_en_8 false)) (iff tre_8 false)) (iff tx_end_8 false)) (iff bstate14_8 true)) (= (- S1_8 cvclZero) 0)) $cvcl_317) $cvcl_212) (= (- next_bit_8 cvclZero) 0)) (= (- tx_conta_8 cvclZero) 0)) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)