(benchmark ckt_PROP8_tf_10.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 unknown
  :logic QF_IDL
  :extrafuns ((cvclZero Int))
  :extrapreds ((eoc_5))
  :extrapreds ((dsr_9))
  :extrapreds ((tre_9))
  :extrapreds ((eoc_8))
  :extrapreds ((bstate8_9))
  :extrapreds ((send_data_9))
  :extrafuns ((S1_9 Int))
  :extrapreds ((load_9))
  :extrapreds ((send_9))
  :extrafuns ((S2_9 Int))
  :extrapreds ((dsr_8))
  :extrapreds ((dsr_4))
  :extrapreds ((confirm_9))
  :extrapreds ((eoc_6))
  :extrafuns ((tx_conta_9 Int))
  :extrapreds ((dsr_5))
  :extrapreds ((tx_end_9))
  :extrapreds ((eoc_9))
  :extrapreds ((mpx_9))
  :extrapreds ((rdy_9))
  :extrapreds ((dsr_7))
  :extrafuns ((itfc_state_9 Int))
  :extrapreds ((send_en_9))
  :extrafuns ((next_bit_9 Int))
  :extrapreds ((shot_9))
  :extrapreds ((dsr_6))
  :extrapreds ((eoc_7))
  :formula
(flet ($cvcl_16 (if_then_else confirm_9 false true)) (flet ($cvcl_1 (if_then_else mpx_9 false true)) (flet ($cvcl_86 (if_then_else rdy_9 false true)) (flet ($cvcl_3 (and (if_then_else (and bstate8_9 (if_then_else (or confirm_9  $cvcl_1 ) false true)) false true) bstate8_9)) (flet ($cvcl_0 (and (= (- itfc_state_9 cvclZero) 3) tx_end_9)) (flet ($cvcl_124 (= (- itfc_state_9 cvclZero) 0)) (flet ($cvcl_8 (or $cvcl_0  (and (if_then_else (or $cvcl_124  $cvcl_0 ) false true) confirm_9) )) (flet ($cvcl_9 (= (- S2_9 cvclZero) 2)) (flet ($cvcl_2 (and $cvcl_9 confirm_9)) (flet ($cvcl_12 (or (and $cvcl_2 $cvcl_1)  (and (if_then_else $cvcl_2 false true) mpx_9) )) (flet ($cvcl_10 (if_then_else $cvcl_12 false true)) (flet ($cvcl_13 (and (if_then_else (and $cvcl_3 (if_then_else (or $cvcl_8  $cvcl_10 ) false true)) false true) $cvcl_3)) (flet ($cvcl_5 (= (- itfc_state_9 cvclZero) 1)) (flet ($cvcl_6 (= (- itfc_state_9 cvclZero) 2)) (flet ($cvcl_4 (= (- itfc_state_9 cvclZero) 0)) (flet ($cvcl_17 (if_then_else shot_9 false false)) (flet ($cvcl_21 (= (- next_bit_9 cvclZero) 1)) (flet ($cvcl_23 (> (- tx_conta_9 cvclZero) 104)) (flet ($cvcl_20 (if_then_else (and send_en_9 $cvcl_23) false true)) (flet ($cvcl_19 (and $cvcl_21 (if_then_else $cvcl_20 false true))) (flet ($cvcl_7 (and (if_then_else $cvcl_4 $cvcl_17 (if_then_else $cvcl_5 false (if_then_else $cvcl_6 true (if_then_else tx_end_9 false true)))) $cvcl_19)) (flet ($cvcl_14 (if_then_else $cvcl_4 (if_then_else shot_9 false true) (if_then_else $cvcl_5 false (if_then_else $cvcl_6 false (if_then_else tx_end_9 true false))))) (flet ($cvcl_89 (if_then_else (or $cvcl_14  $cvcl_7 ) false true)) (flet ($cvcl_28 (or $cvcl_7  (and $cvcl_89 $cvcl_8) )) (flet ($cvcl_15 (= (- S2_9 cvclZero) 1)) (flet ($cvcl_29 (= (- S2_9 cvclZero) 0)) (flet ($cvcl_30 (if_then_else $cvcl_1 false false)) (flet ($cvcl_32 (if_then_else $cvcl_29 (if_then_else send_data_9 false false) (if_then_else $cvcl_15 true (if_then_else $cvcl_9 (if_then_else $cvcl_16 true $cvcl_30) false)))) (flet ($cvcl_11 (and $cvcl_32 $cvcl_8)) (flet ($cvcl_35 (or (and $cvcl_11 $cvcl_10)  (and (if_then_else $cvcl_11 false true) $cvcl_12) )) (flet ($cvcl_33 (if_then_else $cvcl_35 false true)) (flet ($cvcl_36 (and (if_then_else (and $cvcl_13 (if_then_else (or $cvcl_28  $cvcl_33 ) false true)) false true) $cvcl_13)) (flet ($cvcl_24 (or $cvcl_15  (and (if_then_else (or $cvcl_15  (and $cvcl_9 $cvcl_16) ) false true) shot_9) )) (flet ($cvcl_18 (if_then_else $cvcl_6 false (if_then_else tx_end_9 false false))) (flet ($cvcl_25 (if_then_else $cvcl_4 (if_then_else shot_9 true false) (if_then_else $cvcl_5 false $cvcl_18))) (flet ($cvcl_26 (if_then_else $cvcl_4 $cvcl_17 (if_then_else $cvcl_5 true $cvcl_18))) (flet ($cvcl_40 (if_then_else $cvcl_24 false false)) (flet ($cvcl_45 (>= (- next_bit_9 cvclZero) 10)) (flet ($cvcl_44 (or $cvcl_20  $cvcl_45 )) (flet ($cvcl_47 (= (- next_bit_9 cvclZero) 2)) (flet ($cvcl_48 (= (- next_bit_9 cvclZero) 3)) (flet ($cvcl_49 (= (- next_bit_9 cvclZero) 4)) (flet ($cvcl_50 (= (- next_bit_9 cvclZero) 5)) (flet ($cvcl_51 (= (- next_bit_9 cvclZero) 6)) (flet ($cvcl_52 (= (- next_bit_9 cvclZero) 7)) (flet ($cvcl_53 (= (- next_bit_9 cvclZero) 8)) (flet ($cvcl_54 (= (- next_bit_9 cvclZero) 9)) (flet ($cvcl_46 (= (- next_bit_9 cvclZero) 0)) (flet ($cvcl_55 (if_then_else $cvcl_44 $cvcl_21 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 false (if_then_else $cvcl_51 false (if_then_else $cvcl_52 false (if_then_else $cvcl_53 false (if_then_else $cvcl_54 true false))))))))))) (flet ($cvcl_22 (and send_9 (and tre_9 dsr_9))) (flet ($cvcl_66 (or $cvcl_22  (and (if_then_else (or tx_end_9  $cvcl_22 ) false true) send_en_9) )) (flet ($cvcl_68 (if_then_else $cvcl_23 true false)) (flet ($cvcl_69 (> (- tx_conta_9 cvclZero) 103)) (flet ($cvcl_67 (if_then_else send_en_9 (if_then_else $cvcl_68 false $cvcl_69) $cvcl_23)) (flet ($cvcl_43 (if_then_else (and $cvcl_66 $cvcl_67) false true)) (flet ($cvcl_42 (and $cvcl_55 (if_then_else $cvcl_43 false true))) (flet ($cvcl_27 (and (if_then_else $cvcl_14 $cvcl_40 (if_then_else $cvcl_25 false (if_then_else $cvcl_26 true (if_then_else $cvcl_19 false true)))) $cvcl_42)) (flet ($cvcl_37 (if_then_else $cvcl_14 (if_then_else $cvcl_24 false true) (if_then_else $cvcl_25 false (if_then_else $cvcl_26 false (if_then_else $cvcl_19 true false))))) (flet ($cvcl_159 (if_then_else (or $cvcl_37  $cvcl_27 ) false true)) (flet ($cvcl_74 (or $cvcl_27  (and $cvcl_159 $cvcl_28) )) (flet ($cvcl_75 (if_then_else $cvcl_29 (if_then_else send_data_9 false true) (if_then_else $cvcl_15 false (if_then_else $cvcl_9 (if_then_else $cvcl_16 false $cvcl_30) true)))) (flet ($cvcl_31 (= (- S1_9 cvclZero) 7)) (flet ($cvcl_76 (or $cvcl_31  (and (if_then_else (or $cvcl_31  (and (= (- S1_9 cvclZero) 3) rdy_9) ) false true) send_data_9) )) (flet ($cvcl_38 (if_then_else $cvcl_29 (if_then_else send_data_9 true false) (if_then_else $cvcl_15 false (if_then_else $cvcl_9 (if_then_else $cvcl_16 false (if_then_else $cvcl_1 true false)) false)))) (flet ($cvcl_90 (or $cvcl_0  (and (if_then_else (or $cvcl_4  $cvcl_0 ) false true) confirm_9) )) (flet ($cvcl_39 (if_then_else $cvcl_90 false true)) (flet ($cvcl_77 (if_then_else $cvcl_10 false false)) (flet ($cvcl_88 (if_then_else $cvcl_75 (if_then_else $cvcl_76 false false) (if_then_else $cvcl_38 true (if_then_else $cvcl_32 (if_then_else $cvcl_39 true $cvcl_77) false)))) (flet ($cvcl_34 (and $cvcl_88 $cvcl_28)) (flet ($cvcl_94 (or (and $cvcl_34 $cvcl_33)  (and (if_then_else $cvcl_34 false true) $cvcl_35) )) (flet ($cvcl_92 (if_then_else $cvcl_94 false true)) (flet ($cvcl_95 (and (if_then_else (and $cvcl_36 (if_then_else (or $cvcl_74  $cvcl_92 ) false true)) false true) $cvcl_36)) (flet ($cvcl_358 (or $cvcl_38  (and (if_then_else (or $cvcl_38  (and $cvcl_32 (if_then_else $cvcl_8 false true)) ) false true) $cvcl_24) )) (flet ($cvcl_41 (if_then_else $cvcl_26 false (if_then_else $cvcl_19 false false))) (flet ($cvcl_71 (if_then_else $cvcl_14 (if_then_else $cvcl_24 true false) (if_then_else $cvcl_25 false $cvcl_41))) (flet ($cvcl_72 (if_then_else $cvcl_14 $cvcl_40 (if_then_else $cvcl_25 true $cvcl_41))) (flet ($cvcl_70 (or $cvcl_38  (and (if_then_else (or $cvcl_38  (and $cvcl_32 $cvcl_39) ) false true) $cvcl_24) )) (flet ($cvcl_99 (if_then_else $cvcl_70 false false)) (flet ($cvcl_63 (if_then_else $cvcl_54 false false)) (flet ($cvcl_62 (if_then_else $cvcl_53 false $cvcl_63)) (flet ($cvcl_61 (if_then_else $cvcl_52 false $cvcl_62)) (flet ($cvcl_60 (if_then_else $cvcl_51 false $cvcl_61)) (flet ($cvcl_59 (if_then_else $cvcl_50 false $cvcl_60)) (flet ($cvcl_58 (if_then_else $cvcl_49 false $cvcl_59)) (flet ($cvcl_57 (if_then_else $cvcl_48 false $cvcl_58)) (flet ($cvcl_56 (if_then_else $cvcl_47 false $cvcl_57)) (flet ($cvcl_104 (if_then_else $cvcl_44 $cvcl_45 (if_then_else $cvcl_46 false $cvcl_56))) (flet ($cvcl_103 (or $cvcl_43  $cvcl_104 )) (flet ($cvcl_106 (if_then_else $cvcl_44 $cvcl_47 (if_then_else $cvcl_46 true $cvcl_56))) (flet ($cvcl_107 (if_then_else $cvcl_44 $cvcl_48 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 true $cvcl_57)))) (flet ($cvcl_108 (if_then_else $cvcl_44 $cvcl_49 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 true $cvcl_58))))) (flet ($cvcl_109 (if_then_else $cvcl_44 $cvcl_50 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 true $cvcl_59)))))) (flet ($cvcl_110 (if_then_else $cvcl_44 $cvcl_51 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 true $cvcl_60))))))) (flet ($cvcl_111 (if_then_else $cvcl_44 $cvcl_52 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 false (if_then_else $cvcl_51 true $cvcl_61)))))))) (flet ($cvcl_112 (if_then_else $cvcl_44 $cvcl_53 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 false (if_then_else $cvcl_51 false (if_then_else $cvcl_52 true $cvcl_62))))))))) (flet ($cvcl_113 (if_then_else $cvcl_44 $cvcl_54 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 false (if_then_else $cvcl_51 false (if_then_else $cvcl_52 false (if_then_else $cvcl_53 true $cvcl_63)))))))))) (flet ($cvcl_105 (if_then_else $cvcl_44 $cvcl_46 (if_then_else $cvcl_46 false (if_then_else $cvcl_47 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false (if_then_else $cvcl_50 false (if_then_else $cvcl_51 false (if_then_else $cvcl_52 false (if_then_else $cvcl_53 false (if_then_else $cvcl_54 false true))))))))))) (flet ($cvcl_114 (if_then_else $cvcl_103 $cvcl_55 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false (if_then_else $cvcl_111 false (if_then_else $cvcl_112 false (if_then_else $cvcl_113 true false))))))))))) (flet ($cvcl_123 (or $cvcl_5  (and (if_then_else (or $cvcl_5  $cvcl_6 ) false true) send_9) )) (flet ($cvcl_64 (or tx_end_9  (and load_9 (if_then_else tre_9 false true)) )) (flet ($cvcl_126 (or $cvcl_64  (and (if_then_else $cvcl_64 false true) tre_9) )) (flet ($cvcl_65 (and $cvcl_123 (and $cvcl_126 dsr_8))) (flet ($cvcl_129 (or $cvcl_65  (and (if_then_else (or $cvcl_19  $cvcl_65 ) false true) $cvcl_66) )) (flet ($cvcl_131 (if_then_else $cvcl_67 true false)) (flet ($cvcl_132 (> (- tx_conta_9 cvclZero) 102)) (flet ($cvcl_133 (if_then_else send_en_9 (if_then_else $cvcl_68 false $cvcl_132) $cvcl_69)) (flet ($cvcl_130 (if_then_else $cvcl_66 (if_then_else $cvcl_131 false $cvcl_133) $cvcl_67)) (flet ($cvcl_102 (if_then_else (and $cvcl_129 $cvcl_130) false true)) (flet ($cvcl_101 (and $cvcl_114 (if_then_else $cvcl_102 false true))) (flet ($cvcl_73 (and (if_then_else $cvcl_37 $cvcl_99 (if_then_else $cvcl_71 false (if_then_else $cvcl_72 true (if_then_else $cvcl_42 false true)))) $cvcl_101)) (flet ($cvcl_96 (if_then_else $cvcl_37 (if_then_else $cvcl_70 false true) (if_then_else $cvcl_71 false (if_then_else $cvcl_72 false (if_then_else $cvcl_42 true false))))) (flet ($cvcl_236 (if_then_else (or $cvcl_96  $cvcl_73 ) false true)) (flet ($cvcl_138 (or $cvcl_73  (and $cvcl_236 $cvcl_74) )) (flet ($cvcl_139 (if_then_else $cvcl_75 (if_then_else $cvcl_76 false true) (if_then_else $cvcl_38 false (if_then_else $cvcl_32 (if_then_else $cvcl_39 false $cvcl_77) true)))) (flet ($cvcl_80 (= (- S1_9 cvclZero) 1)) (flet ($cvcl_81 (= (- S1_9 cvclZero) 2)) (flet ($cvcl_82 (= (- S1_9 cvclZero) 5)) (flet ($cvcl_84 (= (- S1_9 cvclZero) 6)) (flet ($cvcl_85 (= (- S1_9 cvclZero) 4)) (flet ($cvcl_79 (= (- S1_9 cvclZero) 0)) (flet ($cvcl_83 (if_then_else eoc_9 false false)) (flet ($cvcl_145 (if_then_else $cvcl_85 false (if_then_else $cvcl_86 false false))) (flet ($cvcl_142 (if_then_else $cvcl_31 false $cvcl_145)) (flet ($cvcl_78 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 false (if_then_else $cvcl_82 $cvcl_83 (if_then_else $cvcl_84 true $cvcl_142)))))) (flet ($cvcl_97 (if_then_else $cvcl_75 (if_then_else $cvcl_76 true false) (if_then_else $cvcl_38 false (if_then_else $cvcl_32 (if_then_else $cvcl_39 false (if_then_else $cvcl_10 true false)) false)))) (flet ($cvcl_87 (and $cvcl_29 send_data_9)) (flet ($cvcl_146 (or $cvcl_87  (and (if_then_else (or $cvcl_87  (and $cvcl_2 mpx_9) ) false true) rdy_9) )) (flet ($cvcl_140 (or $cvcl_78  (and (if_then_else (or $cvcl_78  (and (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 false (if_then_else $cvcl_82 $cvcl_83 (if_then_else $cvcl_84 false (if_then_else $cvcl_31 false (if_then_else $cvcl_85 true (if_then_else $cvcl_86 true false)))))))) $cvcl_146) ) false true) $cvcl_76) )) (flet ($cvcl_160 (or $cvcl_7  (and $cvcl_89 $cvcl_90) )) (flet ($cvcl_98 (if_then_else $cvcl_160 false true)) (flet ($cvcl_91 (and $cvcl_32 $cvcl_90)) (flet ($cvcl_162 (or (and $cvcl_91 $cvcl_10)  (and (if_then_else $cvcl_91 false true) $cvcl_12) )) (flet ($cvcl_157 (if_then_else $cvcl_162 false true)) (flet ($cvcl_141 (if_then_else $cvcl_157 false false)) (flet ($cvcl_158 (if_then_else $cvcl_139 (if_then_else $cvcl_140 false false) (if_then_else $cvcl_97 true (if_then_else $cvcl_88 (if_then_else $cvcl_98 true $cvcl_141) false)))) (flet ($cvcl_93 (and $cvcl_158 $cvcl_74)) (flet ($cvcl_165 (or (and $cvcl_93 $cvcl_92)  (and (if_then_else $cvcl_93 false true) $cvcl_94) )) (flet ($cvcl_163 (if_then_else $cvcl_165 false true)) (flet ($cvcl_166 (and (if_then_else (and $cvcl_95 (if_then_else (or $cvcl_138  $cvcl_163 ) false true)) false true) $cvcl_95)) (flet ($cvcl_100 (if_then_else $cvcl_72 false (if_then_else $cvcl_42 false false))) (flet ($cvcl_135 (if_then_else $cvcl_37 (if_then_else $cvcl_70 true false) (if_then_else $cvcl_71 false $cvcl_100))) (flet ($cvcl_136 (if_then_else $cvcl_37 $cvcl_99 (if_then_else $cvcl_71 true $cvcl_100))) (flet ($cvcl_134 (or $cvcl_97  (and (if_then_else (or $cvcl_97  (and $cvcl_88 $cvcl_98) ) false true) $cvcl_70) )) (flet ($cvcl_170 (if_then_else $cvcl_134 false false)) (flet ($cvcl_316 (if_then_else $cvcl_96 $cvcl_170 (if_then_else $cvcl_135 false (if_then_else $cvcl_136 true (if_then_else $cvcl_101 false true))))) (flet ($cvcl_122 (if_then_else $cvcl_113 false false)) (flet ($cvcl_121 (if_then_else $cvcl_112 false $cvcl_122)) (flet ($cvcl_120 (if_then_else $cvcl_111 false $cvcl_121)) (flet ($cvcl_119 (if_then_else $cvcl_110 false $cvcl_120)) (flet ($cvcl_118 (if_then_else $cvcl_109 false $cvcl_119)) (flet ($cvcl_117 (if_then_else $cvcl_108 false $cvcl_118)) (flet ($cvcl_116 (if_then_else $cvcl_107 false $cvcl_117)) (flet ($cvcl_115 (if_then_else $cvcl_106 false $cvcl_116)) (flet ($cvcl_181 (if_then_else $cvcl_103 $cvcl_104 (if_then_else $cvcl_105 false $cvcl_115))) (flet ($cvcl_180 (or $cvcl_102  $cvcl_181 )) (flet ($cvcl_183 (if_then_else $cvcl_103 $cvcl_106 (if_then_else $cvcl_105 true $cvcl_115))) (flet ($cvcl_184 (if_then_else $cvcl_103 $cvcl_107 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 true $cvcl_116)))) (flet ($cvcl_185 (if_then_else $cvcl_103 $cvcl_108 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 true $cvcl_117))))) (flet ($cvcl_186 (if_then_else $cvcl_103 $cvcl_109 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 true $cvcl_118)))))) (flet ($cvcl_187 (if_then_else $cvcl_103 $cvcl_110 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 true $cvcl_119))))))) (flet ($cvcl_188 (if_then_else $cvcl_103 $cvcl_111 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 true $cvcl_120)))))))) (flet ($cvcl_189 (if_then_else $cvcl_103 $cvcl_112 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false (if_then_else $cvcl_111 true $cvcl_121))))))))) (flet ($cvcl_190 (if_then_else $cvcl_103 $cvcl_113 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false (if_then_else $cvcl_111 false (if_then_else $cvcl_112 true $cvcl_122)))))))))) (flet ($cvcl_182 (if_then_else $cvcl_103 $cvcl_105 (if_then_else $cvcl_105 false (if_then_else $cvcl_106 false (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 false (if_then_else $cvcl_111 false (if_then_else $cvcl_112 false (if_then_else $cvcl_113 false true))))))))))) (flet ($cvcl_172 (if_then_else $cvcl_180 $cvcl_114 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 false (if_then_else $cvcl_187 false (if_then_else $cvcl_188 false (if_then_else $cvcl_189 false (if_then_else $cvcl_190 true false))))))))))) (flet ($cvcl_173 (or $cvcl_25  (and (if_then_else (or $cvcl_25  $cvcl_26 ) false true) $cvcl_123) )) (flet ($cvcl_125 (and $cvcl_124 shot_9)) (flet ($cvcl_200 (or $cvcl_125  (and (if_then_else (or $cvcl_125  $cvcl_5 ) false true) load_9) )) (flet ($cvcl_175 (if_then_else $cvcl_126 false true)) (flet ($cvcl_127 (or $cvcl_19  (and $cvcl_200 $cvcl_175) )) (flet ($cvcl_201 (or $cvcl_127  (and (if_then_else $cvcl_127 false true) $cvcl_126) )) (flet ($cvcl_128 (and $cvcl_173 (and $cvcl_201 dsr_7))) (flet ($cvcl_204 (or $cvcl_128  (and (if_then_else (or $cvcl_42  $cvcl_128 ) false true) $cvcl_129) )) (flet ($cvcl_206 (if_then_else $cvcl_130 true false)) (flet ($cvcl_207 (> (- tx_conta_9 cvclZero) 101)) (flet ($cvcl_208 (if_then_else send_en_9 (if_then_else $cvcl_68 false $cvcl_207) $cvcl_132)) (flet ($cvcl_209 (if_then_else $cvcl_66 (if_then_else $cvcl_131 false $cvcl_208) $cvcl_133)) (flet ($cvcl_178 (if_then_else $cvcl_129 (if_then_else $cvcl_206 false $cvcl_209) $cvcl_130)) (flet ($cvcl_281 (and $cvcl_172 (if_then_else (if_then_else (and $cvcl_204 $cvcl_178) false true) false true))) (flet ($cvcl_137 (and $cvcl_316 $cvcl_281)) (flet ($cvcl_167 (if_then_else $cvcl_96 (if_then_else $cvcl_134 false true) (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_101 true false))))) (flet ($cvcl_215 (or $cvcl_137  (and (if_then_else (or $cvcl_167  $cvcl_137 ) false true) $cvcl_138) )) (flet ($cvcl_216 (if_then_else $cvcl_139 (if_then_else $cvcl_140 false true) (if_then_else $cvcl_97 false (if_then_else $cvcl_88 (if_then_else $cvcl_98 false $cvcl_141) true)))) (flet ($cvcl_148 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 false (if_then_else $cvcl_82 $cvcl_83 (if_then_else $cvcl_84 false (if_then_else $cvcl_31 false (if_then_else $cvcl_85 false (if_then_else $cvcl_86 false true))))))))) (flet ($cvcl_144 (if_then_else $cvcl_84 false $cvcl_142)) (flet ($cvcl_143 (if_then_else $cvcl_81 false (if_then_else $cvcl_82 $cvcl_83 $cvcl_144))) (flet ($cvcl_149 (if_then_else $cvcl_79 true (if_then_else $cvcl_80 false $cvcl_143))) (flet ($cvcl_150 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 true $cvcl_143))) (flet ($cvcl_151 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 true (if_then_else $cvcl_82 (if_then_else eoc_9 true false) $cvcl_144))))) (flet ($cvcl_153 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 false (if_then_else $cvcl_82 (if_then_else eoc_9 false true) $cvcl_144))))) (flet ($cvcl_154 (if_then_else $cvcl_79 false (if_then_else $cvcl_80 false (if_then_else $cvcl_81 false (if_then_else $cvcl_82 $cvcl_83 (if_then_else $cvcl_84 false (if_then_else $cvcl_31 true $cvcl_145))))))) (flet ($cvcl_155 (if_then_else $cvcl_146 false true)) (flet ($cvcl_152 (if_then_else eoc_8 false false)) (flet ($cvcl_222 (if_then_else $cvcl_154 false (if_then_else $cvcl_155 false false))) (flet ($cvcl_219 (if_then_else $cvcl_78 false $cvcl_222)) (flet ($cvcl_147 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 false (if_then_else $cvcl_151 $cvcl_152 (if_then_else $cvcl_153 true $cvcl_219)))))) (flet ($cvcl_156 (and $cvcl_75 $cvcl_76)) (flet ($cvcl_168 (if_then_else $cvcl_139 (if_then_else $cvcl_140 true false) (if_then_else $cvcl_97 false (if_then_else $cvcl_88 (if_then_else $cvcl_98 false (if_then_else $cvcl_157 true false)) false)))) (flet ($cvcl_223 (or $cvcl_156  (and (if_then_else (or $cvcl_156  (and $cvcl_91 $cvcl_12) ) false true) $cvcl_146) )) (flet ($cvcl_217 (or $cvcl_147  (and (if_then_else (or $cvcl_147  (and (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 false (if_then_else $cvcl_151 $cvcl_152 (if_then_else $cvcl_153 false (if_then_else $cvcl_78 false (if_then_else $cvcl_154 true (if_then_else $cvcl_155 true false)))))))) $cvcl_223) ) false true) $cvcl_140) )) (flet ($cvcl_237 (or $cvcl_27  (and $cvcl_159 $cvcl_160) )) (flet ($cvcl_169 (if_then_else $cvcl_237 false true)) (flet ($cvcl_161 (and $cvcl_88 $cvcl_160)) (flet ($cvcl_239 (or (and $cvcl_161 $cvcl_157)  (and (if_then_else $cvcl_161 false true) $cvcl_162) )) (flet ($cvcl_234 (if_then_else $cvcl_239 false true)) (flet ($cvcl_218 (if_then_else $cvcl_234 false false)) (flet ($cvcl_235 (if_then_else $cvcl_216 (if_then_else $cvcl_217 false false) (if_then_else $cvcl_168 true (if_then_else $cvcl_158 (if_then_else $cvcl_169 true $cvcl_218) false)))) (flet ($cvcl_164 (and $cvcl_235 $cvcl_138)) (flet ($cvcl_242 (or (and $cvcl_164 $cvcl_163)  (and (if_then_else $cvcl_164 false true) $cvcl_165) )) (flet ($cvcl_240 (if_then_else $cvcl_242 false true)) (flet ($cvcl_243 (and (if_then_else (and $cvcl_166 (if_then_else (or $cvcl_215  $cvcl_240 ) false true)) false true) $cvcl_166)) (flet ($cvcl_171 (if_then_else $cvcl_136 false (if_then_else $cvcl_101 false false))) (flet ($cvcl_211 (if_then_else $cvcl_96 (if_then_else $cvcl_134 true false) (if_then_else $cvcl_135 false $cvcl_171))) (flet ($cvcl_212 (if_then_else $cvcl_96 $cvcl_170 (if_then_else $cvcl_135 true $cvcl_171))) (flet ($cvcl_210 (or $cvcl_168  (and (if_then_else (or $cvcl_168  (and $cvcl_158 $cvcl_169) ) false true) $cvcl_134) )) (flet ($cvcl_247 (if_then_else $cvcl_210 false false)) (flet ($cvcl_174 (and $cvcl_4 shot_9)) (flet ($cvcl_252 (or $cvcl_174  (and (if_then_else (or $cvcl_174  $cvcl_5 ) false true) load_9) )) (flet ($cvcl_176 (or $cvcl_19  (and $cvcl_252 $cvcl_175) )) (flet ($cvcl_253 (or $cvcl_176  (and (if_then_else $cvcl_176 false true) $cvcl_126) )) (flet ($cvcl_177 (and $cvcl_173 (and $cvcl_253 dsr_7))) (flet ($cvcl_205 (or $cvcl_177  (and (if_then_else (or $cvcl_42  $cvcl_177 ) false true) $cvcl_129) )) (flet ($cvcl_179 (if_then_else (and $cvcl_205 $cvcl_178) false true)) (flet ($cvcl_213 (and $cvcl_172 (if_then_else $cvcl_179 false true))) (flet ($cvcl_399 (if_then_else $cvcl_167 $cvcl_247 (if_then_else $cvcl_211 false (if_then_else $cvcl_212 true (if_then_else $cvcl_213 false true))))) (flet ($cvcl_198 (if_then_else $cvcl_190 false false)) (flet ($cvcl_197 (if_then_else $cvcl_189 false $cvcl_198)) (flet ($cvcl_196 (if_then_else $cvcl_188 false $cvcl_197)) (flet ($cvcl_195 (if_then_else $cvcl_187 false $cvcl_196)) (flet ($cvcl_194 (if_then_else $cvcl_186 false $cvcl_195)) (flet ($cvcl_193 (if_then_else $cvcl_185 false $cvcl_194)) (flet ($cvcl_192 (if_then_else $cvcl_184 false $cvcl_193)) (flet ($cvcl_191 (if_then_else $cvcl_183 false $cvcl_192)) (flet ($cvcl_259 (if_then_else $cvcl_180 $cvcl_181 (if_then_else $cvcl_182 false $cvcl_191))) (flet ($cvcl_261 (if_then_else $cvcl_180 $cvcl_183 (if_then_else $cvcl_182 true $cvcl_191))) (flet ($cvcl_262 (if_then_else $cvcl_180 $cvcl_184 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 true $cvcl_192)))) (flet ($cvcl_263 (if_then_else $cvcl_180 $cvcl_185 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 true $cvcl_193))))) (flet ($cvcl_264 (if_then_else $cvcl_180 $cvcl_186 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 true $cvcl_194)))))) (flet ($cvcl_265 (if_then_else $cvcl_180 $cvcl_187 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 true $cvcl_195))))))) (flet ($cvcl_266 (if_then_else $cvcl_180 $cvcl_188 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 false (if_then_else $cvcl_187 true $cvcl_196)))))))) (flet ($cvcl_267 (if_then_else $cvcl_180 $cvcl_189 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 false (if_then_else $cvcl_187 false (if_then_else $cvcl_188 true $cvcl_197))))))))) (flet ($cvcl_268 (if_then_else $cvcl_180 $cvcl_190 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 false (if_then_else $cvcl_187 false (if_then_else $cvcl_188 false (if_then_else $cvcl_189 true $cvcl_198)))))))))) (flet ($cvcl_258 (or $cvcl_179  $cvcl_259 )) (flet ($cvcl_260 (if_then_else $cvcl_180 $cvcl_182 (if_then_else $cvcl_182 false (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 false (if_then_else $cvcl_187 false (if_then_else $cvcl_188 false (if_then_else $cvcl_189 false (if_then_else $cvcl_190 false true))))))))))) (flet ($cvcl_249 (if_then_else $cvcl_258 $cvcl_172 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false (if_then_else $cvcl_265 false (if_then_else $cvcl_266 false (if_then_else $cvcl_267 false (if_then_else $cvcl_268 true false))))))))))) (flet ($cvcl_250 (or $cvcl_71  (and (if_then_else (or $cvcl_71  $cvcl_72 ) false true) $cvcl_173) )) (flet ($cvcl_199 (and $cvcl_14 $cvcl_24)) (flet ($cvcl_251 (if_then_else (or $cvcl_199  $cvcl_25 ) false true)) (flet ($cvcl_278 (or $cvcl_199  (and $cvcl_251 $cvcl_200) )) (flet ($cvcl_202 (or $cvcl_42  (and $cvcl_278 (if_then_else $cvcl_201 false true)) )) (flet ($cvcl_279 (or $cvcl_202  (and (if_then_else $cvcl_202 false true) $cvcl_201) )) (flet ($cvcl_203 (and $cvcl_250 (and $cvcl_279 dsr_6))) (flet ($cvcl_283 (or $cvcl_203  (and (if_then_else (or $cvcl_101  $cvcl_203 ) false true) $cvcl_204) )) (flet ($cvcl_285 (if_then_else $cvcl_178 true false)) (flet ($cvcl_286 (> (- tx_conta_9 cvclZero) 100)) (flet ($cvcl_287 (if_then_else send_en_9 (if_then_else $cvcl_68 false $cvcl_286) $cvcl_207)) (flet ($cvcl_288 (if_then_else $cvcl_66 (if_then_else $cvcl_131 false $cvcl_287) $cvcl_208)) (flet ($cvcl_289 (if_then_else $cvcl_129 (if_then_else $cvcl_206 false $cvcl_288) $cvcl_209)) (flet ($cvcl_256 (if_then_else $cvcl_205 (if_then_else $cvcl_285 false $cvcl_289) $cvcl_178)) (flet ($cvcl_363 (and $cvcl_249 (if_then_else (if_then_else (and $cvcl_283 $cvcl_256) false true) false true))) (flet ($cvcl_214 (and $cvcl_399 $cvcl_363)) (flet ($cvcl_244 (if_then_else $cvcl_167 (if_then_else $cvcl_210 false true) (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 true false))))) (flet ($cvcl_295 (or $cvcl_214  (and (if_then_else (or $cvcl_244  $cvcl_214 ) false true) $cvcl_215) )) (flet ($cvcl_296 (if_then_else $cvcl_216 (if_then_else $cvcl_217 false true) (if_then_else $cvcl_168 false (if_then_else $cvcl_158 (if_then_else $cvcl_169 false $cvcl_218) true)))) (flet ($cvcl_225 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 false (if_then_else $cvcl_151 $cvcl_152 (if_then_else $cvcl_153 false (if_then_else $cvcl_78 false (if_then_else $cvcl_154 false (if_then_else $cvcl_155 false true))))))))) (flet ($cvcl_221 (if_then_else $cvcl_153 false $cvcl_219)) (flet ($cvcl_220 (if_then_else $cvcl_150 false (if_then_else $cvcl_151 $cvcl_152 $cvcl_221))) (flet ($cvcl_226 (if_then_else $cvcl_148 true (if_then_else $cvcl_149 false $cvcl_220))) (flet ($cvcl_227 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 true $cvcl_220))) (flet ($cvcl_228 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 true (if_then_else $cvcl_151 (if_then_else eoc_8 true false) $cvcl_221))))) (flet ($cvcl_230 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 false (if_then_else $cvcl_151 (if_then_else eoc_8 false true) $cvcl_221))))) (flet ($cvcl_231 (if_then_else $cvcl_148 false (if_then_else $cvcl_149 false (if_then_else $cvcl_150 false (if_then_else $cvcl_151 $cvcl_152 (if_then_else $cvcl_153 false (if_then_else $cvcl_78 true $cvcl_222))))))) (flet ($cvcl_232 (if_then_else $cvcl_223 false true)) (flet ($cvcl_229 (if_then_else eoc_7 false false)) (flet ($cvcl_302 (if_then_else $cvcl_231 false (if_then_else $cvcl_232 false false))) (flet ($cvcl_299 (if_then_else $cvcl_147 false $cvcl_302)) (flet ($cvcl_224 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 false (if_then_else $cvcl_228 $cvcl_229 (if_then_else $cvcl_230 true $cvcl_299)))))) (flet ($cvcl_245 (if_then_else $cvcl_216 (if_then_else $cvcl_217 true false) (if_then_else $cvcl_168 false (if_then_else $cvcl_158 (if_then_else $cvcl_169 false (if_then_else $cvcl_234 true false)) false)))) (flet ($cvcl_233 (and $cvcl_139 $cvcl_140)) (flet ($cvcl_303 (or $cvcl_233  (and (if_then_else (or $cvcl_233  (and $cvcl_161 $cvcl_162) ) false true) $cvcl_223) )) (flet ($cvcl_297 (or $cvcl_224  (and (if_then_else (or $cvcl_224  (and (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 false (if_then_else $cvcl_228 $cvcl_229 (if_then_else $cvcl_230 false (if_then_else $cvcl_147 false (if_then_else $cvcl_231 true (if_then_else $cvcl_232 true false)))))))) $cvcl_303) ) false true) $cvcl_217) )) (flet ($cvcl_318 (or $cvcl_73  (and $cvcl_236 $cvcl_237) )) (flet ($cvcl_246 (if_then_else $cvcl_318 false true)) (flet ($cvcl_238 (and $cvcl_158 $cvcl_237)) (flet ($cvcl_320 (or (and $cvcl_238 $cvcl_234)  (and (if_then_else $cvcl_238 false true) $cvcl_239) )) (flet ($cvcl_314 (if_then_else $cvcl_320 false true)) (flet ($cvcl_298 (if_then_else $cvcl_314 false false)) (flet ($cvcl_315 (if_then_else $cvcl_296 (if_then_else $cvcl_297 false false) (if_then_else $cvcl_245 true (if_then_else $cvcl_235 (if_then_else $cvcl_246 true $cvcl_298) false)))) (flet ($cvcl_241 (and $cvcl_315 $cvcl_215)) (flet ($cvcl_323 (or (and $cvcl_241 $cvcl_240)  (and (if_then_else $cvcl_241 false true) $cvcl_242) )) (flet ($cvcl_321 (if_then_else $cvcl_323 false true)) (flet ($cvcl_324 (and (if_then_else (and $cvcl_243 (if_then_else (or $cvcl_295  $cvcl_321 ) false true)) false true) $cvcl_243)) (flet ($cvcl_248 (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false false))) (flet ($cvcl_291 (if_then_else $cvcl_167 (if_then_else $cvcl_210 true false) (if_then_else $cvcl_211 false $cvcl_248))) (flet ($cvcl_292 (if_then_else $cvcl_167 $cvcl_247 (if_then_else $cvcl_211 true $cvcl_248))) (flet ($cvcl_290 (or $cvcl_245  (and (if_then_else (or $cvcl_245  (and $cvcl_235 $cvcl_246) ) false true) $cvcl_210) )) (flet ($cvcl_328 (if_then_else $cvcl_290 false false)) (flet ($cvcl_333 (or $cvcl_199  (and $cvcl_251 $cvcl_252) )) (flet ($cvcl_254 (or $cvcl_42  (and $cvcl_333 (if_then_else $cvcl_253 false true)) )) (flet ($cvcl_334 (or $cvcl_254  (and (if_then_else $cvcl_254 false true) $cvcl_253) )) (flet ($cvcl_255 (and $cvcl_250 (and $cvcl_334 dsr_6))) (flet ($cvcl_284 (or $cvcl_255  (and (if_then_else (or $cvcl_101  $cvcl_255 ) false true) $cvcl_205) )) (flet ($cvcl_257 (if_then_else (and $cvcl_284 $cvcl_256) false true)) (flet ($cvcl_293 (and $cvcl_249 (if_then_else $cvcl_257 false true))) (flet ($cvcl_276 (if_then_else $cvcl_268 false false)) (flet ($cvcl_275 (if_then_else $cvcl_267 false $cvcl_276)) (flet ($cvcl_274 (if_then_else $cvcl_266 false $cvcl_275)) (flet ($cvcl_273 (if_then_else $cvcl_265 false $cvcl_274)) (flet ($cvcl_272 (if_then_else $cvcl_264 false $cvcl_273)) (flet ($cvcl_271 (if_then_else $cvcl_263 false $cvcl_272)) (flet ($cvcl_270 (if_then_else $cvcl_262 false $cvcl_271)) (flet ($cvcl_269 (if_then_else $cvcl_261 false $cvcl_270)) (flet ($cvcl_340 (if_then_else $cvcl_258 $cvcl_259 (if_then_else $cvcl_260 false $cvcl_269))) (flet ($cvcl_342 (if_then_else $cvcl_258 $cvcl_261 (if_then_else $cvcl_260 true $cvcl_269))) (flet ($cvcl_343 (if_then_else $cvcl_258 $cvcl_262 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 true $cvcl_270)))) (flet ($cvcl_344 (if_then_else $cvcl_258 $cvcl_263 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 true $cvcl_271))))) (flet ($cvcl_345 (if_then_else $cvcl_258 $cvcl_264 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 true $cvcl_272)))))) (flet ($cvcl_346 (if_then_else $cvcl_258 $cvcl_265 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 true $cvcl_273))))))) (flet ($cvcl_347 (if_then_else $cvcl_258 $cvcl_266 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false (if_then_else $cvcl_265 true $cvcl_274)))))))) (flet ($cvcl_348 (if_then_else $cvcl_258 $cvcl_267 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false (if_then_else $cvcl_265 false (if_then_else $cvcl_266 true $cvcl_275))))))))) (flet ($cvcl_349 (if_then_else $cvcl_258 $cvcl_268 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false (if_then_else $cvcl_265 false (if_then_else $cvcl_266 false (if_then_else $cvcl_267 true $cvcl_276)))))))))) (flet ($cvcl_339 (or $cvcl_257  $cvcl_340 )) (flet ($cvcl_341 (if_then_else $cvcl_258 $cvcl_260 (if_then_else $cvcl_260 false (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 false (if_then_else $cvcl_265 false (if_then_else $cvcl_266 false (if_then_else $cvcl_267 false (if_then_else $cvcl_268 false true))))))))))) (flet ($cvcl_330 (if_then_else $cvcl_339 $cvcl_249 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 false (if_then_else $cvcl_346 false (if_then_else $cvcl_347 false (if_then_else $cvcl_348 false (if_then_else $cvcl_349 true false))))))))))) (flet ($cvcl_331 (or $cvcl_135  (and (if_then_else (or $cvcl_135  $cvcl_136 ) false true) $cvcl_250) )) (flet ($cvcl_277 (and $cvcl_37 $cvcl_358)) (flet ($cvcl_360 (or $cvcl_277  (and (if_then_else (or $cvcl_277  $cvcl_71 ) false true) $cvcl_278) )) (flet ($cvcl_280 (or $cvcl_101  (and $cvcl_360 (if_then_else $cvcl_279 false true)) )) (flet ($cvcl_361 (or $cvcl_280  (and (if_then_else $cvcl_280 false true) $cvcl_279) )) (flet ($cvcl_282 (and $cvcl_331 (and $cvcl_361 dsr_5))) (flet ($cvcl_365 (or $cvcl_282  (and (if_then_else (or $cvcl_281  $cvcl_282 ) false true) $cvcl_283) )) (flet ($cvcl_367 (if_then_else $cvcl_256 true false)) (flet ($cvcl_368 (> (- tx_conta_9 cvclZero) 99)) (flet ($cvcl_369 (if_then_else send_en_9 (if_then_else $cvcl_68 false $cvcl_368) $cvcl_286)) (flet ($cvcl_370 (if_then_else $cvcl_66 (if_then_else $cvcl_131 false $cvcl_369) $cvcl_287)) (flet ($cvcl_371 (if_then_else $cvcl_129 (if_then_else $cvcl_206 false $cvcl_370) $cvcl_288)) (flet ($cvcl_372 (if_then_else $cvcl_205 (if_then_else $cvcl_285 false $cvcl_371) $cvcl_289)) (flet ($cvcl_337 (if_then_else $cvcl_284 (if_then_else $cvcl_367 false $cvcl_372) $cvcl_256)) (flet ($cvcl_294 (and (if_then_else $cvcl_244 $cvcl_328 (if_then_else $cvcl_291 false (if_then_else $cvcl_292 true (if_then_else $cvcl_293 false true)))) (and $cvcl_330 (if_then_else (if_then_else (and $cvcl_365 $cvcl_337) false true) false true)))) (flet ($cvcl_325 (if_then_else $cvcl_244 (if_then_else $cvcl_290 false true) (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 true false))))) (flet ($cvcl_378 (or $cvcl_294  (and (if_then_else (or $cvcl_325  $cvcl_294 ) false true) $cvcl_295) )) (flet ($cvcl_379 (if_then_else $cvcl_296 (if_then_else $cvcl_297 false true) (if_then_else $cvcl_245 false (if_then_else $cvcl_235 (if_then_else $cvcl_246 false $cvcl_298) true)))) (flet ($cvcl_305 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 false (if_then_else $cvcl_228 $cvcl_229 (if_then_else $cvcl_230 false (if_then_else $cvcl_147 false (if_then_else $cvcl_231 false (if_then_else $cvcl_232 false true))))))))) (flet ($cvcl_301 (if_then_else $cvcl_230 false $cvcl_299)) (flet ($cvcl_300 (if_then_else $cvcl_227 false (if_then_else $cvcl_228 $cvcl_229 $cvcl_301))) (flet ($cvcl_306 (if_then_else $cvcl_225 true (if_then_else $cvcl_226 false $cvcl_300))) (flet ($cvcl_307 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 true $cvcl_300))) (flet ($cvcl_308 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 true (if_then_else $cvcl_228 (if_then_else eoc_7 true false) $cvcl_301))))) (flet ($cvcl_310 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 false (if_then_else $cvcl_228 (if_then_else eoc_7 false true) $cvcl_301))))) (flet ($cvcl_311 (if_then_else $cvcl_225 false (if_then_else $cvcl_226 false (if_then_else $cvcl_227 false (if_then_else $cvcl_228 $cvcl_229 (if_then_else $cvcl_230 false (if_then_else $cvcl_147 true $cvcl_302))))))) (flet ($cvcl_312 (if_then_else $cvcl_303 false true)) (flet ($cvcl_309 (if_then_else eoc_6 false false)) (flet ($cvcl_385 (if_then_else $cvcl_311 false (if_then_else $cvcl_312 false false))) (flet ($cvcl_382 (if_then_else $cvcl_224 false $cvcl_385)) (flet ($cvcl_304 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 false (if_then_else $cvcl_308 $cvcl_309 (if_then_else $cvcl_310 true $cvcl_382)))))) (flet ($cvcl_326 (if_then_else $cvcl_296 (if_then_else $cvcl_297 true false) (if_then_else $cvcl_245 false (if_then_else $cvcl_235 (if_then_else $cvcl_246 false (if_then_else $cvcl_314 true false)) false)))) (flet ($cvcl_313 (and $cvcl_216 $cvcl_217)) (flet ($cvcl_386 (or $cvcl_313  (and (if_then_else (or $cvcl_313  (and $cvcl_238 $cvcl_239) ) false true) $cvcl_303) )) (flet ($cvcl_380 (or $cvcl_304  (and (if_then_else (or $cvcl_304  (and (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 false (if_then_else $cvcl_308 $cvcl_309 (if_then_else $cvcl_310 false (if_then_else $cvcl_224 false (if_then_else $cvcl_311 true (if_then_else $cvcl_312 true false)))))))) $cvcl_386) ) false true) $cvcl_297) )) (flet ($cvcl_317 (and $cvcl_316 $cvcl_213)) (flet ($cvcl_401 (or $cvcl_317  (and (if_then_else (or $cvcl_167  $cvcl_317 ) false true) $cvcl_318) )) (flet ($cvcl_327 (if_then_else $cvcl_401 false true)) (flet ($cvcl_319 (and $cvcl_235 $cvcl_318)) (flet ($cvcl_403 (or (and $cvcl_319 $cvcl_314)  (and (if_then_else $cvcl_319 false true) $cvcl_320) )) (flet ($cvcl_397 (if_then_else $cvcl_403 false true)) (flet ($cvcl_381 (if_then_else $cvcl_397 false false)) (flet ($cvcl_398 (if_then_else $cvcl_379 (if_then_else $cvcl_380 false false) (if_then_else $cvcl_326 true (if_then_else $cvcl_315 (if_then_else $cvcl_327 true $cvcl_381) false)))) (flet ($cvcl_322 (and $cvcl_398 $cvcl_295)) (flet ($cvcl_406 (or (and $cvcl_322 $cvcl_321)  (and (if_then_else $cvcl_322 false true) $cvcl_323) )) (flet ($cvcl_404 (if_then_else $cvcl_406 false true)) (flet ($cvcl_407 (and (if_then_else (and $cvcl_324 (if_then_else (or $cvcl_378  $cvcl_404 ) false true)) false true) $cvcl_324)) (flet ($cvcl_329 (if_then_else $cvcl_292 false (if_then_else $cvcl_293 false false))) (flet ($cvcl_374 (if_then_else $cvcl_244 (if_then_else $cvcl_290 true false) (if_then_else $cvcl_291 false $cvcl_329))) (flet ($cvcl_375 (if_then_else $cvcl_244 $cvcl_328 (if_then_else $cvcl_291 true $cvcl_329))) (flet ($cvcl_373 (or $cvcl_326  (and (if_then_else (or $cvcl_326  (and $cvcl_315 $cvcl_327) ) false true) $cvcl_290) )) (flet ($cvcl_332 (and $cvcl_37 $cvcl_70)) (flet ($cvcl_335 (or $cvcl_101  (and (or $cvcl_332  (and (if_then_else (or $cvcl_332  $cvcl_71 ) false true) $cvcl_333) ) (if_then_else $cvcl_334 false true)) )) (flet ($cvcl_336 (and $cvcl_331 (and (or $cvcl_335  (and (if_then_else $cvcl_335 false true) $cvcl_334) ) dsr_5))) (flet ($cvcl_366 (or $cvcl_336  (and (if_then_else (or $cvcl_213  $cvcl_336 ) false true) $cvcl_284) )) (flet ($cvcl_338 (if_then_else (and $cvcl_366 $cvcl_337) false true)) (flet ($cvcl_376 (and $cvcl_330 (if_then_else $cvcl_338 false true))) (flet ($cvcl_357 (if_then_else $cvcl_349 false false)) (flet ($cvcl_356 (if_then_else $cvcl_348 false $cvcl_357)) (flet ($cvcl_355 (if_then_else $cvcl_347 false $cvcl_356)) (flet ($cvcl_354 (if_then_else $cvcl_346 false $cvcl_355)) (flet ($cvcl_353 (if_then_else $cvcl_345 false $cvcl_354)) (flet ($cvcl_352 (if_then_else $cvcl_344 false $cvcl_353)) (flet ($cvcl_351 (if_then_else $cvcl_343 false $cvcl_352)) (flet ($cvcl_350 (if_then_else $cvcl_342 false $cvcl_351)) (flet ($cvcl_359 (and $cvcl_96 (or $cvcl_97  (and (if_then_else (or $cvcl_97  (and $cvcl_88 (if_then_else $cvcl_28 false true)) ) false true) $cvcl_358) ))) (flet ($cvcl_362 (or $cvcl_281  (and (or $cvcl_359  (and (if_then_else (or $cvcl_359  $cvcl_135 ) false true) $cvcl_360) ) (if_then_else $cvcl_361 false true)) )) (flet ($cvcl_364 (and (or $cvcl_211  (and (if_then_else (or $cvcl_211  $cvcl_212 ) false true) $cvcl_331) ) (and (or $cvcl_362  (and (if_then_else $cvcl_362 false true) $cvcl_361) ) dsr_4))) (flet ($cvcl_377 (and (if_then_else $cvcl_325 (if_then_else $cvcl_373 false false) (if_then_else $cvcl_374 false (if_then_else $cvcl_375 true (if_then_else $cvcl_376 false true)))) (and (if_then_else (or $cvcl_338  (if_then_else $cvcl_339 $cvcl_340 (if_then_else $cvcl_341 false $cvcl_350)) ) $cvcl_330 (if_then_else (if_then_else $cvcl_339 $cvcl_341 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 false (if_then_else $cvcl_346 false (if_then_else $cvcl_347 false (if_then_else $cvcl_348 false (if_then_else $cvcl_349 false true)))))))))) false (if_then_else (if_then_else $cvcl_339 $cvcl_342 (if_then_else $cvcl_341 true $cvcl_350)) false (if_then_else (if_then_else $cvcl_339 $cvcl_343 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 true $cvcl_351))) false (if_then_else (if_then_else $cvcl_339 $cvcl_344 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 true $cvcl_352)))) false (if_then_else (if_then_else $cvcl_339 $cvcl_345 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 true $cvcl_353))))) false (if_then_else (if_then_else $cvcl_339 $cvcl_346 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 true $cvcl_354)))))) false (if_then_else (if_then_else $cvcl_339 $cvcl_347 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 false (if_then_else $cvcl_346 true $cvcl_355))))))) false (if_then_else (if_then_else $cvcl_339 $cvcl_348 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 false (if_then_else $cvcl_346 false (if_then_else $cvcl_347 true $cvcl_356)))))))) false (if_then_else (if_then_else $cvcl_339 $cvcl_349 (if_then_else $cvcl_341 false (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 false (if_then_else $cvcl_346 false (if_then_else $cvcl_347 false (if_then_else $cvcl_348 true $cvcl_357))))))))) true false)))))))))) (if_then_else (if_then_else (and (or $cvcl_364  (and (if_then_else (or $cvcl_363  $cvcl_364 ) false true) $cvcl_365) ) (if_then_else $cvcl_366 (if_then_else (if_then_else $cvcl_337 true false) false (if_then_else $cvcl_284 (if_then_else $cvcl_367 false (if_then_else $cvcl_205 (if_then_else $cvcl_285 false (if_then_else $cvcl_129 (if_then_else $cvcl_206 false (if_then_else $cvcl_66 (if_then_else $cvcl_131 false (if_then_else send_en_9 (if_then_else $cvcl_68 false (> (- tx_conta_9 cvclZero) 98)) $cvcl_368)) $cvcl_369)) $cvcl_370)) $cvcl_371)) $cvcl_372)) $cvcl_337)) false true) false true)))) (flet ($cvcl_388 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 false (if_then_else $cvcl_308 $cvcl_309 (if_then_else $cvcl_310 false (if_then_else $cvcl_224 false (if_then_else $cvcl_311 false (if_then_else $cvcl_312 false true))))))))) (flet ($cvcl_384 (if_then_else $cvcl_310 false $cvcl_382)) (flet ($cvcl_383 (if_then_else $cvcl_307 false (if_then_else $cvcl_308 $cvcl_309 $cvcl_384))) (flet ($cvcl_389 (if_then_else $cvcl_305 true (if_then_else $cvcl_306 false $cvcl_383))) (flet ($cvcl_390 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 true $cvcl_383))) (flet ($cvcl_391 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 true (if_then_else $cvcl_308 (if_then_else eoc_6 true false) $cvcl_384))))) (flet ($cvcl_393 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 false (if_then_else $cvcl_308 (if_then_else eoc_6 false true) $cvcl_384))))) (flet ($cvcl_394 (if_then_else $cvcl_305 false (if_then_else $cvcl_306 false (if_then_else $cvcl_307 false (if_then_else $cvcl_308 $cvcl_309 (if_then_else $cvcl_310 false (if_then_else $cvcl_224 true $cvcl_385))))))) (flet ($cvcl_395 (if_then_else $cvcl_386 false true)) (flet ($cvcl_392 (if_then_else eoc_5 false false)) (flet ($cvcl_387 (if_then_else $cvcl_388 false (if_then_else $cvcl_389 false (if_then_else $cvcl_390 false (if_then_else $cvcl_391 $cvcl_392 (if_then_else $cvcl_393 true (if_then_else $cvcl_304 false (if_then_else $cvcl_394 false (if_then_else $cvcl_395 false false))))))))) (flet ($cvcl_396 (and $cvcl_296 $cvcl_297)) (flet ($cvcl_400 (and $cvcl_399 $cvcl_293)) (flet ($cvcl_402 (and $cvcl_315 $cvcl_401)) (flet ($cvcl_405 (and (if_then_else (if_then_else $cvcl_379 (if_then_else $cvcl_380 false true) (if_then_else $cvcl_326 false (if_then_else $cvcl_315 (if_then_else $cvcl_327 false $cvcl_381) true))) (if_then_else (or $cvcl_387  (and (if_then_else (or $cvcl_387  (and (if_then_else $cvcl_388 false (if_then_else $cvcl_389 false (if_then_else $cvcl_390 false (if_then_else $cvcl_391 $cvcl_392 (if_then_else $cvcl_393 false (if_then_else $cvcl_304 false (if_then_else $cvcl_394 true (if_then_else $cvcl_395 true false)))))))) (or $cvcl_396  (and (if_then_else (or $cvcl_396  (and $cvcl_319 $cvcl_320) ) false true) $cvcl_386) )) ) false true) $cvcl_380) ) false false) (if_then_else (if_then_else $cvcl_379 (if_then_else $cvcl_380 true false) (if_then_else $cvcl_326 false (if_then_else $cvcl_315 (if_then_else $cvcl_327 false (if_then_else $cvcl_397 true false)) false))) true (if_then_else $cvcl_398 (if_then_else (if_then_else (or $cvcl_400  (and (if_then_else (or $cvcl_244  $cvcl_400 ) false true) $cvcl_401) ) false true) true (if_then_else (if_then_else (or (and $cvcl_402 $cvcl_397)  (and (if_then_else $cvcl_402 false true) $cvcl_403) ) false true) false false)) false))) $cvcl_378)) (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_407 (if_then_else (or (or $cvcl_377  (and (if_then_else (or (if_then_else $cvcl_325 (if_then_else $cvcl_373 false true) (if_then_else $cvcl_374 false (if_then_else $cvcl_375 false (if_then_else $cvcl_376 true false))))  $cvcl_377 ) false true) $cvcl_378) )  (if_then_else (or (and $cvcl_405 $cvcl_404)  (and (if_then_else $cvcl_405 false true) $cvcl_406) ) false true) ) false true)) false true) $cvcl_407) false true) (iff send_data_9 false)) (iff rdy_9 false)) (iff shot_9 false)) (iff mpx_9 false)) (iff load_9 false)) (iff confirm_9 false)) (iff send_9 false)) (iff send_en_9 false)) (iff tre_9 false)) (iff tx_end_9 false)) (iff bstate8_9 true)) (= (- S1_9 cvclZero) 0)) (= (- S2_9 cvclZero) 0)) $cvcl_124) (= (- next_bit_9 cvclZero) 0)) (= (- tx_conta_9 cvclZero) 0)) false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)