(benchmark ckt_PROP40_tf_13.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_10))
  :extrapreds ((confirm_12))
  :extrapreds ((eoc_9))
  :extrafuns ((S1_12 Int))
  :extrapreds ((dsr_2))
  :extrapreds ((eoc_8))
  :extrapreds ((send_data_12))
  :extrafuns ((tx_conta_12 Int))
  :extrapreds ((eoc_7))
  :extrapreds ((dsr_12))
  :extrapreds ((send_en_12))
  :extrafuns ((S2_12 Int))
  :extrapreds ((dsr_3))
  :extrapreds ((dsr_11))
  :extrafuns ((itfc_state_12 Int))
  :extrapreds ((shot_12))
  :extrafuns ((next_bit_12 Int))
  :extrapreds ((send_12))
  :extrapreds ((tre_12))
  :extrapreds ((load_12))
  :extrapreds ((tx_end_12))
  :extrapreds ((dsr_10))
  :extrapreds ((error_12))
  :extrapreds ((dsr_9))
  :extrapreds ((bstate40_12))
  :extrapreds ((dsr_4))
  :extrapreds ((dsr_8))
  :extrapreds ((dsr_7))
  :extrapreds ((dsr_6))
  :extrapreds ((dsr_5))
  :extrapreds ((eoc_12))
  :extrapreds ((eoc_11))
  :extrapreds ((rdy_12))
  :extrapreds ((mpx_12))
  :formula
(flet ($cvcl_35 (and tre_12 dsr_12)) (flet ($cvcl_114 (if_then_else rdy_12 false true)) (flet ($cvcl_29 (if_then_else mpx_12 false true)) (flet ($cvcl_26 (if_then_else confirm_12 false true)) (flet ($cvcl_0 (and (if_then_else (and bstate40_12 error_12) false true) bstate40_12)) (flet ($cvcl_7 (or (or (and load_12 tre_12)  (and send_12 (if_then_else $cvcl_35 false true)) )  (and (if_then_else (or load_12  send_12 ) false true) error_12) )) (flet ($cvcl_8 (and (if_then_else (and $cvcl_0 $cvcl_7) false true) $cvcl_0)) (flet ($cvcl_30 (= (- itfc_state_12 cvclZero) 0)) (flet ($cvcl_1 (and $cvcl_30 shot_12)) (flet ($cvcl_3 (= (- itfc_state_12 cvclZero) 1)) (flet ($cvcl_5 (or $cvcl_1  (and (if_then_else (or $cvcl_1  $cvcl_3 ) false true) load_12) )) (flet ($cvcl_2 (or tx_end_12  (and load_12 (if_then_else tre_12 false true)) )) (flet ($cvcl_4 (or $cvcl_2  (and (if_then_else $cvcl_2 false true) tre_12) )) (flet ($cvcl_9 (= (- itfc_state_12 cvclZero) 2)) (flet ($cvcl_6 (or $cvcl_3  (and (if_then_else (or $cvcl_3  $cvcl_9 ) false true) send_12) )) (flet ($cvcl_85 (and $cvcl_4 dsr_11)) (flet ($cvcl_19 (or (or (and $cvcl_5 $cvcl_4)  (and $cvcl_6 (if_then_else $cvcl_85 false true)) )  (and (if_then_else (or $cvcl_5  $cvcl_6 ) false true) $cvcl_7) )) (flet ($cvcl_20 (and (if_then_else (and $cvcl_8 $cvcl_19) false true) $cvcl_8)) (flet ($cvcl_12 (= (- itfc_state_12 cvclZero) 0)) (flet ($cvcl_21 (if_then_else $cvcl_12 (if_then_else shot_12 false true) (if_then_else $cvcl_3 false (if_then_else $cvcl_9 false (if_then_else tx_end_12 true false))))) (flet ($cvcl_10 (= (- S2_12 cvclZero) 1)) (flet ($cvcl_25 (= (- S2_12 cvclZero) 2)) (flet ($cvcl_22 (or $cvcl_10  (and (if_then_else (or $cvcl_10  (and $cvcl_25 $cvcl_26) ) false true) shot_12) )) (flet ($cvcl_11 (and $cvcl_21 $cvcl_22)) (flet ($cvcl_15 (if_then_else $cvcl_9 false (if_then_else tx_end_12 false false))) (flet ($cvcl_14 (if_then_else $cvcl_12 (if_then_else shot_12 true false) (if_then_else $cvcl_3 false $cvcl_15))) (flet ($cvcl_248 (if_then_else (or $cvcl_11  $cvcl_14 ) false true)) (flet ($cvcl_17 (or $cvcl_11  (and $cvcl_248 $cvcl_5) )) (flet ($cvcl_34 (= (- next_bit_12 cvclZero) 1)) (flet ($cvcl_37 (> (- tx_conta_12 cvclZero) 104)) (flet ($cvcl_33 (if_then_else (and send_en_12 $cvcl_37) false true)) (flet ($cvcl_24 (and $cvcl_34 (if_then_else $cvcl_33 false true))) (flet ($cvcl_172 (if_then_else $cvcl_4 false true)) (flet ($cvcl_13 (or $cvcl_24  (and $cvcl_5 $cvcl_172) )) (flet ($cvcl_16 (or $cvcl_13  (and (if_then_else $cvcl_13 false true) $cvcl_4) )) (flet ($cvcl_58 (if_then_else shot_12 false false)) (flet ($cvcl_23 (if_then_else $cvcl_12 $cvcl_58 (if_then_else $cvcl_3 true $cvcl_15))) (flet ($cvcl_18 (or $cvcl_14  (and (if_then_else (or $cvcl_14  $cvcl_23 ) false true) $cvcl_6) )) (flet ($cvcl_150 (and $cvcl_16 dsr_10)) (flet ($cvcl_44 (or (or (and $cvcl_17 $cvcl_16)  (and $cvcl_18 (if_then_else $cvcl_150 false true)) )  (and (if_then_else (or $cvcl_17  $cvcl_18 ) false true) $cvcl_19) )) (flet ($cvcl_45 (and (if_then_else (and $cvcl_20 $cvcl_44) false true) $cvcl_20)) (flet ($cvcl_46 (if_then_else $cvcl_21 (if_then_else $cvcl_22 false true) (if_then_else $cvcl_14 false (if_then_else $cvcl_23 false (if_then_else $cvcl_24 true false))))) (flet ($cvcl_28 (= (- S2_12 cvclZero) 0)) (flet ($cvcl_27 (if_then_else $cvcl_28 (if_then_else send_data_12 true false) (if_then_else $cvcl_10 false (if_then_else $cvcl_25 (if_then_else $cvcl_26 false (if_then_else $cvcl_29 true false)) false)))) (flet ($cvcl_50 (if_then_else $cvcl_29 false false)) (flet ($cvcl_47 (if_then_else $cvcl_28 (if_then_else send_data_12 false false) (if_then_else $cvcl_10 true (if_then_else $cvcl_25 (if_then_else $cvcl_26 true $cvcl_50) false)))) (flet ($cvcl_31 (and (= (- itfc_state_12 cvclZero) 3) tx_end_12)) (flet ($cvcl_60 (or $cvcl_31  (and (if_then_else (or $cvcl_30  $cvcl_31 ) false true) confirm_12) )) (flet ($cvcl_61 (or $cvcl_27  (and (if_then_else (or $cvcl_27  (and $cvcl_47 (if_then_else $cvcl_60 false true)) ) false true) $cvcl_22) )) (flet ($cvcl_32 (and $cvcl_46 $cvcl_61)) (flet ($cvcl_40 (if_then_else $cvcl_23 false (if_then_else $cvcl_24 false false))) (flet ($cvcl_39 (if_then_else $cvcl_21 (if_then_else $cvcl_22 true false) (if_then_else $cvcl_14 false $cvcl_40))) (flet ($cvcl_42 (or $cvcl_32  (and (if_then_else (or $cvcl_32  $cvcl_39 ) false true) $cvcl_17) )) (flet ($cvcl_66 (>= (- next_bit_12 cvclZero) 10)) (flet ($cvcl_65 (or $cvcl_33  $cvcl_66 )) (flet ($cvcl_68 (= (- next_bit_12 cvclZero) 2)) (flet ($cvcl_69 (= (- next_bit_12 cvclZero) 3)) (flet ($cvcl_70 (= (- next_bit_12 cvclZero) 4)) (flet ($cvcl_71 (= (- next_bit_12 cvclZero) 5)) (flet ($cvcl_72 (= (- next_bit_12 cvclZero) 6)) (flet ($cvcl_73 (= (- next_bit_12 cvclZero) 7)) (flet ($cvcl_74 (= (- next_bit_12 cvclZero) 8)) (flet ($cvcl_75 (= (- next_bit_12 cvclZero) 9)) (flet ($cvcl_67 (= (- next_bit_12 cvclZero) 0)) (flet ($cvcl_76 (if_then_else $cvcl_65 $cvcl_34 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 false (if_then_else $cvcl_72 false (if_then_else $cvcl_73 false (if_then_else $cvcl_74 false (if_then_else $cvcl_75 true false))))))))))) (flet ($cvcl_36 (and send_12 $cvcl_35)) (flet ($cvcl_87 (or $cvcl_36  (and (if_then_else (or tx_end_12  $cvcl_36 ) false true) send_en_12) )) (flet ($cvcl_89 (if_then_else $cvcl_37 true false)) (flet ($cvcl_90 (> (- tx_conta_12 cvclZero) 103)) (flet ($cvcl_88 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_90) $cvcl_37)) (flet ($cvcl_64 (if_then_else (and $cvcl_87 $cvcl_88) false true)) (flet ($cvcl_49 (and $cvcl_76 (if_then_else $cvcl_64 false true))) (flet ($cvcl_38 (or $cvcl_49  (and $cvcl_17 (if_then_else $cvcl_16 false true)) )) (flet ($cvcl_41 (or $cvcl_38  (and (if_then_else $cvcl_38 false true) $cvcl_16) )) (flet ($cvcl_123 (if_then_else $cvcl_22 false false)) (flet ($cvcl_48 (if_then_else $cvcl_21 $cvcl_123 (if_then_else $cvcl_14 true $cvcl_40))) (flet ($cvcl_43 (or $cvcl_39  (and (if_then_else (or $cvcl_39  $cvcl_48 ) false true) $cvcl_18) )) (flet ($cvcl_226 (and $cvcl_41 dsr_9)) (flet ($cvcl_97 (or (or (and $cvcl_42 $cvcl_41)  (and $cvcl_43 (if_then_else $cvcl_226 false true)) )  (and (if_then_else (or $cvcl_42  $cvcl_43 ) false true) $cvcl_44) )) (flet ($cvcl_98 (and (if_then_else (and $cvcl_45 $cvcl_97) false true) $cvcl_45)) (flet ($cvcl_102 (or $cvcl_31  (and (if_then_else (or $cvcl_12  $cvcl_31 ) false true) confirm_12) )) (flet ($cvcl_52 (if_then_else $cvcl_102 false true)) (flet ($cvcl_63 (or $cvcl_27  (and (if_then_else (or $cvcl_27  (and $cvcl_47 $cvcl_52) ) false true) $cvcl_22) )) (flet ($cvcl_99 (if_then_else $cvcl_46 (if_then_else $cvcl_63 false true) (if_then_else $cvcl_39 false (if_then_else $cvcl_48 false (if_then_else $cvcl_49 true false))))) (flet ($cvcl_55 (if_then_else $cvcl_28 (if_then_else send_data_12 false true) (if_then_else $cvcl_10 false (if_then_else $cvcl_25 (if_then_else $cvcl_26 false $cvcl_50) true)))) (flet ($cvcl_51 (= (- S1_12 cvclZero) 7)) (flet ($cvcl_56 (or $cvcl_51  (and (if_then_else (or $cvcl_51  (and (= (- S1_12 cvclZero) 3) rdy_12) ) false true) send_data_12) )) (flet ($cvcl_53 (and $cvcl_25 confirm_12)) (flet ($cvcl_118 (or (and $cvcl_53 $cvcl_29)  (and (if_then_else $cvcl_53 false true) mpx_12) )) (flet ($cvcl_57 (if_then_else $cvcl_118 false true)) (flet ($cvcl_54 (if_then_else $cvcl_55 (if_then_else $cvcl_56 true false) (if_then_else $cvcl_27 false (if_then_else $cvcl_47 (if_then_else $cvcl_52 false (if_then_else $cvcl_57 true false)) false)))) (flet ($cvcl_105 (if_then_else $cvcl_57 false false)) (flet ($cvcl_100 (if_then_else $cvcl_55 (if_then_else $cvcl_56 false false) (if_then_else $cvcl_27 true (if_then_else $cvcl_47 (if_then_else $cvcl_52 true $cvcl_105) false)))) (flet ($cvcl_59 (and (if_then_else $cvcl_12 $cvcl_58 (if_then_else $cvcl_3 false (if_then_else $cvcl_9 true (if_then_else tx_end_12 false true)))) $cvcl_24)) (flet ($cvcl_101 (if_then_else (or $cvcl_21  $cvcl_59 ) false true)) (flet ($cvcl_125 (or $cvcl_59  (and $cvcl_101 $cvcl_60) )) (flet ($cvcl_126 (or $cvcl_54  (and (if_then_else (or $cvcl_54  (and $cvcl_100 (if_then_else $cvcl_125 false true)) ) false true) $cvcl_61) )) (flet ($cvcl_62 (and $cvcl_99 $cvcl_126)) (flet ($cvcl_93 (if_then_else $cvcl_48 false (if_then_else $cvcl_49 false false))) (flet ($cvcl_92 (if_then_else $cvcl_46 (if_then_else $cvcl_63 true false) (if_then_else $cvcl_39 false $cvcl_93))) (flet ($cvcl_95 (or $cvcl_62  (and (if_then_else (or $cvcl_62  $cvcl_92 ) false true) $cvcl_42) )) (flet ($cvcl_84 (if_then_else $cvcl_75 false false)) (flet ($cvcl_83 (if_then_else $cvcl_74 false $cvcl_84)) (flet ($cvcl_82 (if_then_else $cvcl_73 false $cvcl_83)) (flet ($cvcl_81 (if_then_else $cvcl_72 false $cvcl_82)) (flet ($cvcl_80 (if_then_else $cvcl_71 false $cvcl_81)) (flet ($cvcl_79 (if_then_else $cvcl_70 false $cvcl_80)) (flet ($cvcl_78 (if_then_else $cvcl_69 false $cvcl_79)) (flet ($cvcl_77 (if_then_else $cvcl_68 false $cvcl_78)) (flet ($cvcl_131 (if_then_else $cvcl_65 $cvcl_66 (if_then_else $cvcl_67 false $cvcl_77))) (flet ($cvcl_130 (or $cvcl_64  $cvcl_131 )) (flet ($cvcl_133 (if_then_else $cvcl_65 $cvcl_68 (if_then_else $cvcl_67 true $cvcl_77))) (flet ($cvcl_134 (if_then_else $cvcl_65 $cvcl_69 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 true $cvcl_78)))) (flet ($cvcl_135 (if_then_else $cvcl_65 $cvcl_70 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 true $cvcl_79))))) (flet ($cvcl_136 (if_then_else $cvcl_65 $cvcl_71 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 true $cvcl_80)))))) (flet ($cvcl_137 (if_then_else $cvcl_65 $cvcl_72 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 true $cvcl_81))))))) (flet ($cvcl_138 (if_then_else $cvcl_65 $cvcl_73 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 false (if_then_else $cvcl_72 true $cvcl_82)))))))) (flet ($cvcl_139 (if_then_else $cvcl_65 $cvcl_74 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 false (if_then_else $cvcl_72 false (if_then_else $cvcl_73 true $cvcl_83))))))))) (flet ($cvcl_140 (if_then_else $cvcl_65 $cvcl_75 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 false (if_then_else $cvcl_72 false (if_then_else $cvcl_73 false (if_then_else $cvcl_74 true $cvcl_84)))))))))) (flet ($cvcl_132 (if_then_else $cvcl_65 $cvcl_67 (if_then_else $cvcl_67 false (if_then_else $cvcl_68 false (if_then_else $cvcl_69 false (if_then_else $cvcl_70 false (if_then_else $cvcl_71 false (if_then_else $cvcl_72 false (if_then_else $cvcl_73 false (if_then_else $cvcl_74 false (if_then_else $cvcl_75 false true))))))))))) (flet ($cvcl_141 (if_then_else $cvcl_130 $cvcl_76 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_137 false (if_then_else $cvcl_138 false (if_then_else $cvcl_139 false (if_then_else $cvcl_140 true false))))))))))) (flet ($cvcl_86 (and $cvcl_6 $cvcl_85)) (flet ($cvcl_152 (or $cvcl_86  (and (if_then_else (or $cvcl_24  $cvcl_86 ) false true) $cvcl_87) )) (flet ($cvcl_154 (if_then_else $cvcl_88 true false)) (flet ($cvcl_155 (> (- tx_conta_12 cvclZero) 102)) (flet ($cvcl_156 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_155) $cvcl_90)) (flet ($cvcl_153 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_156) $cvcl_88)) (flet ($cvcl_129 (if_then_else (and $cvcl_152 $cvcl_153) false true)) (flet ($cvcl_104 (and $cvcl_141 (if_then_else $cvcl_129 false true))) (flet ($cvcl_91 (or $cvcl_104  (and $cvcl_42 (if_then_else $cvcl_41 false true)) )) (flet ($cvcl_94 (or $cvcl_91  (and (if_then_else $cvcl_91 false true) $cvcl_41) )) (flet ($cvcl_199 (if_then_else $cvcl_63 false false)) (flet ($cvcl_103 (if_then_else $cvcl_46 $cvcl_199 (if_then_else $cvcl_39 true $cvcl_93))) (flet ($cvcl_96 (or $cvcl_92  (and (if_then_else (or $cvcl_92  $cvcl_103 ) false true) $cvcl_43) )) (flet ($cvcl_305 (and $cvcl_94 dsr_8)) (flet ($cvcl_163 (or (or (and $cvcl_95 $cvcl_94)  (and $cvcl_96 (if_then_else $cvcl_305 false true)) )  (and (if_then_else (or $cvcl_95  $cvcl_96 ) false true) $cvcl_97) )) (flet ($cvcl_164 (and (if_then_else (and $cvcl_98 $cvcl_163) false true) $cvcl_98)) (flet ($cvcl_168 (or $cvcl_59  (and $cvcl_101 $cvcl_102) )) (flet ($cvcl_116 (if_then_else $cvcl_168 false true)) (flet ($cvcl_128 (or $cvcl_54  (and (if_then_else (or $cvcl_54  (and $cvcl_100 $cvcl_116) ) false true) $cvcl_63) )) (flet ($cvcl_165 (if_then_else $cvcl_99 (if_then_else $cvcl_128 false true) (if_then_else $cvcl_92 false (if_then_else $cvcl_103 false (if_then_else $cvcl_104 true false))))) (flet ($cvcl_120 (if_then_else $cvcl_55 (if_then_else $cvcl_56 false true) (if_then_else $cvcl_27 false (if_then_else $cvcl_47 (if_then_else $cvcl_52 false $cvcl_105) true)))) (flet ($cvcl_108 (= (- S1_12 cvclZero) 1)) (flet ($cvcl_109 (= (- S1_12 cvclZero) 2)) (flet ($cvcl_110 (= (- S1_12 cvclZero) 5)) (flet ($cvcl_112 (= (- S1_12 cvclZero) 6)) (flet ($cvcl_113 (= (- S1_12 cvclZero) 4)) (flet ($cvcl_107 (= (- S1_12 cvclZero) 0)) (flet ($cvcl_111 (if_then_else eoc_12 false false)) (flet ($cvcl_180 (if_then_else $cvcl_113 false (if_then_else $cvcl_114 false false))) (flet ($cvcl_177 (if_then_else $cvcl_51 false $cvcl_180)) (flet ($cvcl_106 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 $cvcl_111 (if_then_else $cvcl_112 true $cvcl_177)))))) (flet ($cvcl_115 (and $cvcl_28 send_data_12)) (flet ($cvcl_181 (or $cvcl_115  (and (if_then_else (or $cvcl_115  (and $cvcl_53 mpx_12) ) false true) rdy_12) )) (flet ($cvcl_121 (or $cvcl_106  (and (if_then_else (or $cvcl_106  (and (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 $cvcl_111 (if_then_else $cvcl_112 false (if_then_else $cvcl_51 false (if_then_else $cvcl_113 true (if_then_else $cvcl_114 true false)))))))) $cvcl_181) ) false true) $cvcl_56) )) (flet ($cvcl_117 (and $cvcl_47 $cvcl_102)) (flet ($cvcl_194 (or (and $cvcl_117 $cvcl_57)  (and (if_then_else $cvcl_117 false true) $cvcl_118) )) (flet ($cvcl_122 (if_then_else $cvcl_194 false true)) (flet ($cvcl_119 (if_then_else $cvcl_120 (if_then_else $cvcl_121 true false) (if_then_else $cvcl_54 false (if_then_else $cvcl_100 (if_then_else $cvcl_116 false (if_then_else $cvcl_122 true false)) false)))) (flet ($cvcl_176 (if_then_else $cvcl_122 false false)) (flet ($cvcl_166 (if_then_else $cvcl_120 (if_then_else $cvcl_121 false false) (if_then_else $cvcl_54 true (if_then_else $cvcl_100 (if_then_else $cvcl_116 true $cvcl_176) false)))) (flet ($cvcl_124 (and (if_then_else $cvcl_21 $cvcl_123 (if_then_else $cvcl_14 false (if_then_else $cvcl_23 true (if_then_else $cvcl_24 false true)))) $cvcl_49)) (flet ($cvcl_167 (if_then_else (or $cvcl_46  $cvcl_124 ) false true)) (flet ($cvcl_201 (or $cvcl_124  (and $cvcl_167 $cvcl_125) )) (flet ($cvcl_202 (or $cvcl_119  (and (if_then_else (or $cvcl_119  (and $cvcl_166 (if_then_else $cvcl_201 false true)) ) false true) $cvcl_126) )) (flet ($cvcl_127 (and $cvcl_165 $cvcl_202)) (flet ($cvcl_159 (if_then_else $cvcl_103 false (if_then_else $cvcl_104 false false))) (flet ($cvcl_158 (if_then_else $cvcl_99 (if_then_else $cvcl_128 true false) (if_then_else $cvcl_92 false $cvcl_159))) (flet ($cvcl_161 (or $cvcl_127  (and (if_then_else (or $cvcl_127  $cvcl_158 ) false true) $cvcl_95) )) (flet ($cvcl_149 (if_then_else $cvcl_140 false false)) (flet ($cvcl_148 (if_then_else $cvcl_139 false $cvcl_149)) (flet ($cvcl_147 (if_then_else $cvcl_138 false $cvcl_148)) (flet ($cvcl_146 (if_then_else $cvcl_137 false $cvcl_147)) (flet ($cvcl_145 (if_then_else $cvcl_136 false $cvcl_146)) (flet ($cvcl_144 (if_then_else $cvcl_135 false $cvcl_145)) (flet ($cvcl_143 (if_then_else $cvcl_134 false $cvcl_144)) (flet ($cvcl_142 (if_then_else $cvcl_133 false $cvcl_143)) (flet ($cvcl_208 (if_then_else $cvcl_130 $cvcl_131 (if_then_else $cvcl_132 false $cvcl_142))) (flet ($cvcl_207 (or $cvcl_129  $cvcl_208 )) (flet ($cvcl_210 (if_then_else $cvcl_130 $cvcl_133 (if_then_else $cvcl_132 true $cvcl_142))) (flet ($cvcl_211 (if_then_else $cvcl_130 $cvcl_134 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 true $cvcl_143)))) (flet ($cvcl_212 (if_then_else $cvcl_130 $cvcl_135 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 true $cvcl_144))))) (flet ($cvcl_213 (if_then_else $cvcl_130 $cvcl_136 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 true $cvcl_145)))))) (flet ($cvcl_214 (if_then_else $cvcl_130 $cvcl_137 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 true $cvcl_146))))))) (flet ($cvcl_215 (if_then_else $cvcl_130 $cvcl_138 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_137 true $cvcl_147)))))))) (flet ($cvcl_216 (if_then_else $cvcl_130 $cvcl_139 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_137 false (if_then_else $cvcl_138 true $cvcl_148))))))))) (flet ($cvcl_217 (if_then_else $cvcl_130 $cvcl_140 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_137 false (if_then_else $cvcl_138 false (if_then_else $cvcl_139 true $cvcl_149)))))))))) (flet ($cvcl_209 (if_then_else $cvcl_130 $cvcl_132 (if_then_else $cvcl_132 false (if_then_else $cvcl_133 false (if_then_else $cvcl_134 false (if_then_else $cvcl_135 false (if_then_else $cvcl_136 false (if_then_else $cvcl_137 false (if_then_else $cvcl_138 false (if_then_else $cvcl_139 false (if_then_else $cvcl_140 false true))))))))))) (flet ($cvcl_170 (if_then_else $cvcl_207 $cvcl_141 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false (if_then_else $cvcl_214 false (if_then_else $cvcl_215 false (if_then_else $cvcl_216 false (if_then_else $cvcl_217 true false))))))))))) (flet ($cvcl_151 (and $cvcl_18 $cvcl_150)) (flet ($cvcl_228 (or $cvcl_151  (and (if_then_else (or $cvcl_49  $cvcl_151 ) false true) $cvcl_152) )) (flet ($cvcl_230 (if_then_else $cvcl_153 true false)) (flet ($cvcl_231 (> (- tx_conta_12 cvclZero) 101)) (flet ($cvcl_232 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_231) $cvcl_155)) (flet ($cvcl_233 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_232) $cvcl_156)) (flet ($cvcl_175 (if_then_else $cvcl_152 (if_then_else $cvcl_230 false $cvcl_233) $cvcl_153)) (flet ($cvcl_278 (and $cvcl_170 (if_then_else (if_then_else (and $cvcl_228 $cvcl_175) false true) false true))) (flet ($cvcl_157 (or $cvcl_278  (and $cvcl_95 (if_then_else $cvcl_94 false true)) )) (flet ($cvcl_160 (or $cvcl_157  (and (if_then_else $cvcl_157 false true) $cvcl_94) )) (flet ($cvcl_277 (if_then_else $cvcl_128 false false)) (flet ($cvcl_169 (if_then_else $cvcl_99 $cvcl_277 (if_then_else $cvcl_92 true $cvcl_159))) (flet ($cvcl_162 (or $cvcl_158  (and (if_then_else (or $cvcl_158  $cvcl_169 ) false true) $cvcl_96) )) (flet ($cvcl_386 (and $cvcl_160 dsr_7)) (flet ($cvcl_240 (or (or (and $cvcl_161 $cvcl_160)  (and $cvcl_162 (if_then_else $cvcl_386 false true)) )  (and (if_then_else (or $cvcl_161  $cvcl_162 ) false true) $cvcl_163) )) (flet ($cvcl_241 (and (if_then_else (and $cvcl_164 $cvcl_240) false true) $cvcl_164)) (flet ($cvcl_245 (or $cvcl_124  (and $cvcl_167 $cvcl_168) )) (flet ($cvcl_192 (if_then_else $cvcl_245 false true)) (flet ($cvcl_204 (or $cvcl_119  (and (if_then_else (or $cvcl_119  (and $cvcl_166 $cvcl_192) ) false true) $cvcl_128) )) (flet ($cvcl_171 (and $cvcl_12 shot_12)) (flet ($cvcl_249 (or $cvcl_171  (and (if_then_else (or $cvcl_171  $cvcl_3 ) false true) load_12) )) (flet ($cvcl_173 (or $cvcl_24  (and $cvcl_249 $cvcl_172) )) (flet ($cvcl_250 (or $cvcl_173  (and (if_then_else $cvcl_173 false true) $cvcl_4) )) (flet ($cvcl_174 (and $cvcl_18 (and $cvcl_250 dsr_10))) (flet ($cvcl_229 (or $cvcl_174  (and (if_then_else (or $cvcl_49  $cvcl_174 ) false true) $cvcl_152) )) (flet ($cvcl_206 (if_then_else (and $cvcl_229 $cvcl_175) false true)) (flet ($cvcl_205 (and $cvcl_170 (if_then_else $cvcl_206 false true))) (flet ($cvcl_242 (if_then_else $cvcl_165 (if_then_else $cvcl_204 false true) (if_then_else $cvcl_158 false (if_then_else $cvcl_169 false (if_then_else $cvcl_205 true false))))) (flet ($cvcl_196 (if_then_else $cvcl_120 (if_then_else $cvcl_121 false true) (if_then_else $cvcl_54 false (if_then_else $cvcl_100 (if_then_else $cvcl_116 false $cvcl_176) true)))) (flet ($cvcl_183 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 $cvcl_111 (if_then_else $cvcl_112 false (if_then_else $cvcl_51 false (if_then_else $cvcl_113 false (if_then_else $cvcl_114 false true))))))))) (flet ($cvcl_179 (if_then_else $cvcl_112 false $cvcl_177)) (flet ($cvcl_178 (if_then_else $cvcl_109 false (if_then_else $cvcl_110 $cvcl_111 $cvcl_179))) (flet ($cvcl_184 (if_then_else $cvcl_107 true (if_then_else $cvcl_108 false $cvcl_178))) (flet ($cvcl_185 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 true $cvcl_178))) (flet ($cvcl_186 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 true (if_then_else $cvcl_110 (if_then_else eoc_12 true false) $cvcl_179))))) (flet ($cvcl_188 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 (if_then_else eoc_12 false true) $cvcl_179))))) (flet ($cvcl_189 (if_then_else $cvcl_107 false (if_then_else $cvcl_108 false (if_then_else $cvcl_109 false (if_then_else $cvcl_110 $cvcl_111 (if_then_else $cvcl_112 false (if_then_else $cvcl_51 true $cvcl_180))))))) (flet ($cvcl_190 (if_then_else $cvcl_181 false true)) (flet ($cvcl_187 (if_then_else eoc_11 false false)) (flet ($cvcl_258 (if_then_else $cvcl_189 false (if_then_else $cvcl_190 false false))) (flet ($cvcl_255 (if_then_else $cvcl_106 false $cvcl_258)) (flet ($cvcl_182 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 $cvcl_187 (if_then_else $cvcl_188 true $cvcl_255)))))) (flet ($cvcl_191 (and $cvcl_55 $cvcl_56)) (flet ($cvcl_259 (or $cvcl_191  (and (if_then_else (or $cvcl_191  (and $cvcl_117 $cvcl_118) ) false true) $cvcl_181) )) (flet ($cvcl_197 (or $cvcl_182  (and (if_then_else (or $cvcl_182  (and (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 $cvcl_187 (if_then_else $cvcl_188 false (if_then_else $cvcl_106 false (if_then_else $cvcl_189 true (if_then_else $cvcl_190 true false)))))))) $cvcl_259) ) false true) $cvcl_121) )) (flet ($cvcl_193 (and $cvcl_100 $cvcl_168)) (flet ($cvcl_272 (or (and $cvcl_193 $cvcl_122)  (and (if_then_else $cvcl_193 false true) $cvcl_194) )) (flet ($cvcl_198 (if_then_else $cvcl_272 false true)) (flet ($cvcl_195 (if_then_else $cvcl_196 (if_then_else $cvcl_197 true false) (if_then_else $cvcl_119 false (if_then_else $cvcl_166 (if_then_else $cvcl_192 false (if_then_else $cvcl_198 true false)) false)))) (flet ($cvcl_254 (if_then_else $cvcl_198 false false)) (flet ($cvcl_243 (if_then_else $cvcl_196 (if_then_else $cvcl_197 false false) (if_then_else $cvcl_119 true (if_then_else $cvcl_166 (if_then_else $cvcl_192 true $cvcl_254) false)))) (flet ($cvcl_200 (and (if_then_else $cvcl_46 $cvcl_199 (if_then_else $cvcl_39 false (if_then_else $cvcl_48 true (if_then_else $cvcl_49 false true)))) $cvcl_104)) (flet ($cvcl_244 (if_then_else (or $cvcl_99  $cvcl_200 ) false true)) (flet ($cvcl_280 (or $cvcl_200  (and $cvcl_244 $cvcl_201) )) (flet ($cvcl_281 (or $cvcl_195  (and (if_then_else (or $cvcl_195  (and $cvcl_243 (if_then_else $cvcl_280 false true)) ) false true) $cvcl_202) )) (flet ($cvcl_203 (and $cvcl_242 $cvcl_281)) (flet ($cvcl_236 (if_then_else $cvcl_169 false (if_then_else $cvcl_205 false false))) (flet ($cvcl_235 (if_then_else $cvcl_165 (if_then_else $cvcl_204 true false) (if_then_else $cvcl_158 false $cvcl_236))) (flet ($cvcl_238 (or $cvcl_203  (and (if_then_else (or $cvcl_203  $cvcl_235 ) false true) $cvcl_161) )) (flet ($cvcl_225 (if_then_else $cvcl_217 false false)) (flet ($cvcl_224 (if_then_else $cvcl_216 false $cvcl_225)) (flet ($cvcl_223 (if_then_else $cvcl_215 false $cvcl_224)) (flet ($cvcl_222 (if_then_else $cvcl_214 false $cvcl_223)) (flet ($cvcl_221 (if_then_else $cvcl_213 false $cvcl_222)) (flet ($cvcl_220 (if_then_else $cvcl_212 false $cvcl_221)) (flet ($cvcl_219 (if_then_else $cvcl_211 false $cvcl_220)) (flet ($cvcl_218 (if_then_else $cvcl_210 false $cvcl_219)) (flet ($cvcl_287 (if_then_else $cvcl_207 $cvcl_208 (if_then_else $cvcl_209 false $cvcl_218))) (flet ($cvcl_289 (if_then_else $cvcl_207 $cvcl_210 (if_then_else $cvcl_209 true $cvcl_218))) (flet ($cvcl_290 (if_then_else $cvcl_207 $cvcl_211 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 true $cvcl_219)))) (flet ($cvcl_291 (if_then_else $cvcl_207 $cvcl_212 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 true $cvcl_220))))) (flet ($cvcl_292 (if_then_else $cvcl_207 $cvcl_213 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 true $cvcl_221)))))) (flet ($cvcl_293 (if_then_else $cvcl_207 $cvcl_214 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 true $cvcl_222))))))) (flet ($cvcl_294 (if_then_else $cvcl_207 $cvcl_215 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false (if_then_else $cvcl_214 true $cvcl_223)))))))) (flet ($cvcl_295 (if_then_else $cvcl_207 $cvcl_216 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false (if_then_else $cvcl_214 false (if_then_else $cvcl_215 true $cvcl_224))))))))) (flet ($cvcl_296 (if_then_else $cvcl_207 $cvcl_217 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false (if_then_else $cvcl_214 false (if_then_else $cvcl_215 false (if_then_else $cvcl_216 true $cvcl_225)))))))))) (flet ($cvcl_286 (or $cvcl_206  $cvcl_287 )) (flet ($cvcl_288 (if_then_else $cvcl_207 $cvcl_209 (if_then_else $cvcl_209 false (if_then_else $cvcl_210 false (if_then_else $cvcl_211 false (if_then_else $cvcl_212 false (if_then_else $cvcl_213 false (if_then_else $cvcl_214 false (if_then_else $cvcl_215 false (if_then_else $cvcl_216 false (if_then_else $cvcl_217 false true))))))))))) (flet ($cvcl_247 (if_then_else $cvcl_286 $cvcl_170 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 false (if_then_else $cvcl_294 false (if_then_else $cvcl_295 false (if_then_else $cvcl_296 true false))))))))))) (flet ($cvcl_227 (and $cvcl_43 $cvcl_226)) (flet ($cvcl_307 (or $cvcl_227  (and (if_then_else (or $cvcl_104  $cvcl_227 ) false true) $cvcl_228) )) (flet ($cvcl_309 (if_then_else $cvcl_175 true false)) (flet ($cvcl_310 (> (- tx_conta_12 cvclZero) 100)) (flet ($cvcl_311 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_310) $cvcl_231)) (flet ($cvcl_312 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_311) $cvcl_232)) (flet ($cvcl_313 (if_then_else $cvcl_152 (if_then_else $cvcl_230 false $cvcl_312) $cvcl_233)) (flet ($cvcl_253 (if_then_else $cvcl_229 (if_then_else $cvcl_309 false $cvcl_313) $cvcl_175)) (flet ($cvcl_359 (and $cvcl_247 (if_then_else (if_then_else (and $cvcl_307 $cvcl_253) false true) false true))) (flet ($cvcl_234 (or $cvcl_359  (and $cvcl_161 (if_then_else $cvcl_160 false true)) )) (flet ($cvcl_237 (or $cvcl_234  (and (if_then_else $cvcl_234 false true) $cvcl_160) )) (flet ($cvcl_358 (if_then_else $cvcl_204 false false)) (flet ($cvcl_246 (if_then_else $cvcl_165 $cvcl_358 (if_then_else $cvcl_158 true $cvcl_236))) (flet ($cvcl_239 (or $cvcl_235  (and (if_then_else (or $cvcl_235  $cvcl_246 ) false true) $cvcl_162) )) (flet ($cvcl_468 (and $cvcl_237 dsr_6)) (flet ($cvcl_320 (or (or (and $cvcl_238 $cvcl_237)  (and $cvcl_239 (if_then_else $cvcl_468 false true)) )  (and (if_then_else (or $cvcl_238  $cvcl_239 ) false true) $cvcl_240) )) (flet ($cvcl_321 (and (if_then_else (and $cvcl_241 $cvcl_320) false true) $cvcl_241)) (flet ($cvcl_326 (or $cvcl_200  (and $cvcl_244 $cvcl_245) )) (flet ($cvcl_270 (if_then_else $cvcl_326 false true)) (flet ($cvcl_283 (or $cvcl_195  (and (if_then_else (or $cvcl_195  (and $cvcl_243 $cvcl_270) ) false true) $cvcl_204) )) (flet ($cvcl_330 (or $cvcl_11  (and $cvcl_248 $cvcl_249) )) (flet ($cvcl_251 (or $cvcl_49  (and $cvcl_330 (if_then_else $cvcl_250 false true)) )) (flet ($cvcl_331 (or $cvcl_251  (and (if_then_else $cvcl_251 false true) $cvcl_250) )) (flet ($cvcl_252 (and $cvcl_43 (and $cvcl_331 dsr_9))) (flet ($cvcl_308 (or $cvcl_252  (and (if_then_else (or $cvcl_104  $cvcl_252 ) false true) $cvcl_229) )) (flet ($cvcl_285 (if_then_else (and $cvcl_308 $cvcl_253) false true)) (flet ($cvcl_284 (and $cvcl_247 (if_then_else $cvcl_285 false true))) (flet ($cvcl_322 (if_then_else $cvcl_242 (if_then_else $cvcl_283 false true) (if_then_else $cvcl_235 false (if_then_else $cvcl_246 false (if_then_else $cvcl_284 true false))))) (flet ($cvcl_274 (if_then_else $cvcl_196 (if_then_else $cvcl_197 false true) (if_then_else $cvcl_119 false (if_then_else $cvcl_166 (if_then_else $cvcl_192 false $cvcl_254) true)))) (flet ($cvcl_261 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 $cvcl_187 (if_then_else $cvcl_188 false (if_then_else $cvcl_106 false (if_then_else $cvcl_189 false (if_then_else $cvcl_190 false true))))))))) (flet ($cvcl_257 (if_then_else $cvcl_188 false $cvcl_255)) (flet ($cvcl_256 (if_then_else $cvcl_185 false (if_then_else $cvcl_186 $cvcl_187 $cvcl_257))) (flet ($cvcl_262 (if_then_else $cvcl_183 true (if_then_else $cvcl_184 false $cvcl_256))) (flet ($cvcl_263 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 true $cvcl_256))) (flet ($cvcl_264 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 true (if_then_else $cvcl_186 (if_then_else eoc_11 true false) $cvcl_257))))) (flet ($cvcl_266 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 (if_then_else eoc_11 false true) $cvcl_257))))) (flet ($cvcl_267 (if_then_else $cvcl_183 false (if_then_else $cvcl_184 false (if_then_else $cvcl_185 false (if_then_else $cvcl_186 $cvcl_187 (if_then_else $cvcl_188 false (if_then_else $cvcl_106 true $cvcl_258))))))) (flet ($cvcl_268 (if_then_else $cvcl_259 false true)) (flet ($cvcl_265 (if_then_else eoc_10 false false)) (flet ($cvcl_339 (if_then_else $cvcl_267 false (if_then_else $cvcl_268 false false))) (flet ($cvcl_336 (if_then_else $cvcl_182 false $cvcl_339)) (flet ($cvcl_260 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 $cvcl_265 (if_then_else $cvcl_266 true $cvcl_336)))))) (flet ($cvcl_269 (and $cvcl_120 $cvcl_121)) (flet ($cvcl_340 (or $cvcl_269  (and (if_then_else (or $cvcl_269  (and $cvcl_193 $cvcl_194) ) false true) $cvcl_259) )) (flet ($cvcl_275 (or $cvcl_260  (and (if_then_else (or $cvcl_260  (and (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 $cvcl_265 (if_then_else $cvcl_266 false (if_then_else $cvcl_182 false (if_then_else $cvcl_267 true (if_then_else $cvcl_268 true false)))))))) $cvcl_340) ) false true) $cvcl_197) )) (flet ($cvcl_271 (and $cvcl_166 $cvcl_245)) (flet ($cvcl_353 (or (and $cvcl_271 $cvcl_198)  (and (if_then_else $cvcl_271 false true) $cvcl_272) )) (flet ($cvcl_276 (if_then_else $cvcl_353 false true)) (flet ($cvcl_273 (if_then_else $cvcl_274 (if_then_else $cvcl_275 true false) (if_then_else $cvcl_195 false (if_then_else $cvcl_243 (if_then_else $cvcl_270 false (if_then_else $cvcl_276 true false)) false)))) (flet ($cvcl_335 (if_then_else $cvcl_276 false false)) (flet ($cvcl_323 (if_then_else $cvcl_274 (if_then_else $cvcl_275 false false) (if_then_else $cvcl_195 true (if_then_else $cvcl_243 (if_then_else $cvcl_270 true $cvcl_335) false)))) (flet ($cvcl_324 (if_then_else $cvcl_99 $cvcl_277 (if_then_else $cvcl_92 false (if_then_else $cvcl_103 true (if_then_else $cvcl_104 false true))))) (flet ($cvcl_279 (and $cvcl_324 $cvcl_278)) (flet ($cvcl_361 (or $cvcl_279  (and (if_then_else (or $cvcl_165  $cvcl_279 ) false true) $cvcl_280) )) (flet ($cvcl_362 (or $cvcl_273  (and (if_then_else (or $cvcl_273  (and $cvcl_323 (if_then_else $cvcl_361 false true)) ) false true) $cvcl_281) )) (flet ($cvcl_282 (and $cvcl_322 $cvcl_362)) (flet ($cvcl_316 (if_then_else $cvcl_246 false (if_then_else $cvcl_284 false false))) (flet ($cvcl_315 (if_then_else $cvcl_242 (if_then_else $cvcl_283 true false) (if_then_else $cvcl_235 false $cvcl_316))) (flet ($cvcl_318 (or $cvcl_282  (and (if_then_else (or $cvcl_282  $cvcl_315 ) false true) $cvcl_238) )) (flet ($cvcl_304 (if_then_else $cvcl_296 false false)) (flet ($cvcl_303 (if_then_else $cvcl_295 false $cvcl_304)) (flet ($cvcl_302 (if_then_else $cvcl_294 false $cvcl_303)) (flet ($cvcl_301 (if_then_else $cvcl_293 false $cvcl_302)) (flet ($cvcl_300 (if_then_else $cvcl_292 false $cvcl_301)) (flet ($cvcl_299 (if_then_else $cvcl_291 false $cvcl_300)) (flet ($cvcl_298 (if_then_else $cvcl_290 false $cvcl_299)) (flet ($cvcl_297 (if_then_else $cvcl_289 false $cvcl_298)) (flet ($cvcl_368 (if_then_else $cvcl_286 $cvcl_287 (if_then_else $cvcl_288 false $cvcl_297))) (flet ($cvcl_370 (if_then_else $cvcl_286 $cvcl_289 (if_then_else $cvcl_288 true $cvcl_297))) (flet ($cvcl_371 (if_then_else $cvcl_286 $cvcl_290 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 true $cvcl_298)))) (flet ($cvcl_372 (if_then_else $cvcl_286 $cvcl_291 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 true $cvcl_299))))) (flet ($cvcl_373 (if_then_else $cvcl_286 $cvcl_292 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 true $cvcl_300)))))) (flet ($cvcl_374 (if_then_else $cvcl_286 $cvcl_293 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 true $cvcl_301))))))) (flet ($cvcl_375 (if_then_else $cvcl_286 $cvcl_294 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 true $cvcl_302)))))))) (flet ($cvcl_376 (if_then_else $cvcl_286 $cvcl_295 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 false (if_then_else $cvcl_294 true $cvcl_303))))))))) (flet ($cvcl_377 (if_then_else $cvcl_286 $cvcl_296 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 false (if_then_else $cvcl_294 false (if_then_else $cvcl_295 true $cvcl_304)))))))))) (flet ($cvcl_367 (or $cvcl_285  $cvcl_368 )) (flet ($cvcl_369 (if_then_else $cvcl_286 $cvcl_288 (if_then_else $cvcl_288 false (if_then_else $cvcl_289 false (if_then_else $cvcl_290 false (if_then_else $cvcl_291 false (if_then_else $cvcl_292 false (if_then_else $cvcl_293 false (if_then_else $cvcl_294 false (if_then_else $cvcl_295 false (if_then_else $cvcl_296 false true))))))))))) (flet ($cvcl_328 (if_then_else $cvcl_367 $cvcl_247 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 false (if_then_else $cvcl_374 false (if_then_else $cvcl_375 false (if_then_else $cvcl_376 false (if_then_else $cvcl_377 true false))))))))))) (flet ($cvcl_306 (and $cvcl_96 $cvcl_305)) (flet ($cvcl_388 (or $cvcl_306  (and (if_then_else (or $cvcl_278  $cvcl_306 ) false true) $cvcl_307) )) (flet ($cvcl_390 (if_then_else $cvcl_253 true false)) (flet ($cvcl_391 (> (- tx_conta_12 cvclZero) 99)) (flet ($cvcl_392 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_391) $cvcl_310)) (flet ($cvcl_393 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_392) $cvcl_311)) (flet ($cvcl_394 (if_then_else $cvcl_152 (if_then_else $cvcl_230 false $cvcl_393) $cvcl_312)) (flet ($cvcl_395 (if_then_else $cvcl_229 (if_then_else $cvcl_309 false $cvcl_394) $cvcl_313)) (flet ($cvcl_334 (if_then_else $cvcl_308 (if_then_else $cvcl_390 false $cvcl_395) $cvcl_253)) (flet ($cvcl_441 (and $cvcl_328 (if_then_else (if_then_else (and $cvcl_388 $cvcl_334) false true) false true))) (flet ($cvcl_314 (or $cvcl_441  (and $cvcl_238 (if_then_else $cvcl_237 false true)) )) (flet ($cvcl_317 (or $cvcl_314  (and (if_then_else $cvcl_314 false true) $cvcl_237) )) (flet ($cvcl_440 (if_then_else $cvcl_283 false false)) (flet ($cvcl_327 (if_then_else $cvcl_242 $cvcl_440 (if_then_else $cvcl_235 true $cvcl_316))) (flet ($cvcl_319 (or $cvcl_315  (and (if_then_else (or $cvcl_315  $cvcl_327 ) false true) $cvcl_239) )) (flet ($cvcl_551 (and $cvcl_317 dsr_5)) (flet ($cvcl_402 (or (or (and $cvcl_318 $cvcl_317)  (and $cvcl_319 (if_then_else $cvcl_551 false true)) )  (and (if_then_else (or $cvcl_318  $cvcl_319 ) false true) $cvcl_320) )) (flet ($cvcl_403 (and (if_then_else (and $cvcl_321 $cvcl_402) false true) $cvcl_321)) (flet ($cvcl_325 (and $cvcl_324 $cvcl_205)) (flet ($cvcl_408 (or $cvcl_325  (and (if_then_else (or $cvcl_165  $cvcl_325 ) false true) $cvcl_326) )) (flet ($cvcl_351 (if_then_else $cvcl_408 false true)) (flet ($cvcl_364 (or $cvcl_273  (and (if_then_else (or $cvcl_273  (and $cvcl_323 $cvcl_351) ) false true) $cvcl_283) )) (flet ($cvcl_329 (and $cvcl_46 $cvcl_63)) (flet ($cvcl_412 (or $cvcl_329  (and (if_then_else (or $cvcl_329  $cvcl_39 ) false true) $cvcl_330) )) (flet ($cvcl_332 (or $cvcl_104  (and $cvcl_412 (if_then_else $cvcl_331 false true)) )) (flet ($cvcl_413 (or $cvcl_332  (and (if_then_else $cvcl_332 false true) $cvcl_331) )) (flet ($cvcl_333 (and $cvcl_96 (and $cvcl_413 dsr_8))) (flet ($cvcl_389 (or $cvcl_333  (and (if_then_else (or $cvcl_205  $cvcl_333 ) false true) $cvcl_308) )) (flet ($cvcl_366 (if_then_else (and $cvcl_389 $cvcl_334) false true)) (flet ($cvcl_365 (and $cvcl_328 (if_then_else $cvcl_366 false true))) (flet ($cvcl_404 (if_then_else $cvcl_322 (if_then_else $cvcl_364 false true) (if_then_else $cvcl_315 false (if_then_else $cvcl_327 false (if_then_else $cvcl_365 true false))))) (flet ($cvcl_355 (if_then_else $cvcl_274 (if_then_else $cvcl_275 false true) (if_then_else $cvcl_195 false (if_then_else $cvcl_243 (if_then_else $cvcl_270 false $cvcl_335) true)))) (flet ($cvcl_342 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 $cvcl_265 (if_then_else $cvcl_266 false (if_then_else $cvcl_182 false (if_then_else $cvcl_267 false (if_then_else $cvcl_268 false true))))))))) (flet ($cvcl_338 (if_then_else $cvcl_266 false $cvcl_336)) (flet ($cvcl_337 (if_then_else $cvcl_263 false (if_then_else $cvcl_264 $cvcl_265 $cvcl_338))) (flet ($cvcl_343 (if_then_else $cvcl_261 true (if_then_else $cvcl_262 false $cvcl_337))) (flet ($cvcl_344 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 true $cvcl_337))) (flet ($cvcl_345 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 true (if_then_else $cvcl_264 (if_then_else eoc_10 true false) $cvcl_338))))) (flet ($cvcl_347 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 (if_then_else eoc_10 false true) $cvcl_338))))) (flet ($cvcl_348 (if_then_else $cvcl_261 false (if_then_else $cvcl_262 false (if_then_else $cvcl_263 false (if_then_else $cvcl_264 $cvcl_265 (if_then_else $cvcl_266 false (if_then_else $cvcl_182 true $cvcl_339))))))) (flet ($cvcl_349 (if_then_else $cvcl_340 false true)) (flet ($cvcl_346 (if_then_else eoc_9 false false)) (flet ($cvcl_421 (if_then_else $cvcl_348 false (if_then_else $cvcl_349 false false))) (flet ($cvcl_418 (if_then_else $cvcl_260 false $cvcl_421)) (flet ($cvcl_341 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 $cvcl_346 (if_then_else $cvcl_347 true $cvcl_418)))))) (flet ($cvcl_350 (and $cvcl_196 $cvcl_197)) (flet ($cvcl_422 (or $cvcl_350  (and (if_then_else (or $cvcl_350  (and $cvcl_271 $cvcl_272) ) false true) $cvcl_340) )) (flet ($cvcl_356 (or $cvcl_341  (and (if_then_else (or $cvcl_341  (and (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 $cvcl_346 (if_then_else $cvcl_347 false (if_then_else $cvcl_260 false (if_then_else $cvcl_348 true (if_then_else $cvcl_349 true false)))))))) $cvcl_422) ) false true) $cvcl_275) )) (flet ($cvcl_352 (and $cvcl_243 $cvcl_326)) (flet ($cvcl_435 (or (and $cvcl_352 $cvcl_276)  (and (if_then_else $cvcl_352 false true) $cvcl_353) )) (flet ($cvcl_357 (if_then_else $cvcl_435 false true)) (flet ($cvcl_354 (if_then_else $cvcl_355 (if_then_else $cvcl_356 true false) (if_then_else $cvcl_273 false (if_then_else $cvcl_323 (if_then_else $cvcl_351 false (if_then_else $cvcl_357 true false)) false)))) (flet ($cvcl_417 (if_then_else $cvcl_357 false false)) (flet ($cvcl_405 (if_then_else $cvcl_355 (if_then_else $cvcl_356 false false) (if_then_else $cvcl_273 true (if_then_else $cvcl_323 (if_then_else $cvcl_351 true $cvcl_417) false)))) (flet ($cvcl_406 (if_then_else $cvcl_165 $cvcl_358 (if_then_else $cvcl_158 false (if_then_else $cvcl_169 true (if_then_else $cvcl_205 false true))))) (flet ($cvcl_360 (and $cvcl_406 $cvcl_359)) (flet ($cvcl_443 (or $cvcl_360  (and (if_then_else (or $cvcl_242  $cvcl_360 ) false true) $cvcl_361) )) (flet ($cvcl_444 (or $cvcl_354  (and (if_then_else (or $cvcl_354  (and $cvcl_405 (if_then_else $cvcl_443 false true)) ) false true) $cvcl_362) )) (flet ($cvcl_363 (and $cvcl_404 $cvcl_444)) (flet ($cvcl_398 (if_then_else $cvcl_327 false (if_then_else $cvcl_365 false false))) (flet ($cvcl_397 (if_then_else $cvcl_322 (if_then_else $cvcl_364 true false) (if_then_else $cvcl_315 false $cvcl_398))) (flet ($cvcl_400 (or $cvcl_363  (and (if_then_else (or $cvcl_363  $cvcl_397 ) false true) $cvcl_318) )) (flet ($cvcl_385 (if_then_else $cvcl_377 false false)) (flet ($cvcl_384 (if_then_else $cvcl_376 false $cvcl_385)) (flet ($cvcl_383 (if_then_else $cvcl_375 false $cvcl_384)) (flet ($cvcl_382 (if_then_else $cvcl_374 false $cvcl_383)) (flet ($cvcl_381 (if_then_else $cvcl_373 false $cvcl_382)) (flet ($cvcl_380 (if_then_else $cvcl_372 false $cvcl_381)) (flet ($cvcl_379 (if_then_else $cvcl_371 false $cvcl_380)) (flet ($cvcl_378 (if_then_else $cvcl_370 false $cvcl_379)) (flet ($cvcl_450 (if_then_else $cvcl_367 $cvcl_368 (if_then_else $cvcl_369 false $cvcl_378))) (flet ($cvcl_452 (if_then_else $cvcl_367 $cvcl_370 (if_then_else $cvcl_369 true $cvcl_378))) (flet ($cvcl_453 (if_then_else $cvcl_367 $cvcl_371 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 true $cvcl_379)))) (flet ($cvcl_454 (if_then_else $cvcl_367 $cvcl_372 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 true $cvcl_380))))) (flet ($cvcl_455 (if_then_else $cvcl_367 $cvcl_373 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 true $cvcl_381)))))) (flet ($cvcl_456 (if_then_else $cvcl_367 $cvcl_374 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 true $cvcl_382))))))) (flet ($cvcl_457 (if_then_else $cvcl_367 $cvcl_375 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 false (if_then_else $cvcl_374 true $cvcl_383)))))))) (flet ($cvcl_458 (if_then_else $cvcl_367 $cvcl_376 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 false (if_then_else $cvcl_374 false (if_then_else $cvcl_375 true $cvcl_384))))))))) (flet ($cvcl_459 (if_then_else $cvcl_367 $cvcl_377 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 false (if_then_else $cvcl_374 false (if_then_else $cvcl_375 false (if_then_else $cvcl_376 true $cvcl_385)))))))))) (flet ($cvcl_449 (or $cvcl_366  $cvcl_450 )) (flet ($cvcl_451 (if_then_else $cvcl_367 $cvcl_369 (if_then_else $cvcl_369 false (if_then_else $cvcl_370 false (if_then_else $cvcl_371 false (if_then_else $cvcl_372 false (if_then_else $cvcl_373 false (if_then_else $cvcl_374 false (if_then_else $cvcl_375 false (if_then_else $cvcl_376 false (if_then_else $cvcl_377 false true))))))))))) (flet ($cvcl_410 (if_then_else $cvcl_449 $cvcl_328 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 false (if_then_else $cvcl_456 false (if_then_else $cvcl_457 false (if_then_else $cvcl_458 false (if_then_else $cvcl_459 true false))))))))))) (flet ($cvcl_387 (and $cvcl_162 $cvcl_386)) (flet ($cvcl_470 (or $cvcl_387  (and (if_then_else (or $cvcl_359  $cvcl_387 ) false true) $cvcl_388) )) (flet ($cvcl_472 (if_then_else $cvcl_334 true false)) (flet ($cvcl_473 (> (- tx_conta_12 cvclZero) 98)) (flet ($cvcl_474 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_473) $cvcl_391)) (flet ($cvcl_475 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_474) $cvcl_392)) (flet ($cvcl_476 (if_then_else $cvcl_152 (if_then_else $cvcl_230 false $cvcl_475) $cvcl_393)) (flet ($cvcl_477 (if_then_else $cvcl_229 (if_then_else $cvcl_309 false $cvcl_476) $cvcl_394)) (flet ($cvcl_478 (if_then_else $cvcl_308 (if_then_else $cvcl_390 false $cvcl_477) $cvcl_395)) (flet ($cvcl_416 (if_then_else $cvcl_389 (if_then_else $cvcl_472 false $cvcl_478) $cvcl_334)) (flet ($cvcl_524 (and $cvcl_410 (if_then_else (if_then_else (and $cvcl_470 $cvcl_416) false true) false true))) (flet ($cvcl_396 (or $cvcl_524  (and $cvcl_318 (if_then_else $cvcl_317 false true)) )) (flet ($cvcl_399 (or $cvcl_396  (and (if_then_else $cvcl_396 false true) $cvcl_317) )) (flet ($cvcl_523 (if_then_else $cvcl_364 false false)) (flet ($cvcl_409 (if_then_else $cvcl_322 $cvcl_523 (if_then_else $cvcl_315 true $cvcl_398))) (flet ($cvcl_401 (or $cvcl_397  (and (if_then_else (or $cvcl_397  $cvcl_409 ) false true) $cvcl_319) )) (flet ($cvcl_485 (or (or (and $cvcl_400 $cvcl_399)  (and $cvcl_401 (if_then_else (and $cvcl_399 dsr_4) false true)) )  (and (if_then_else (or $cvcl_400  $cvcl_401 ) false true) $cvcl_402) )) (flet ($cvcl_486 (and (if_then_else (and $cvcl_403 $cvcl_485) false true) $cvcl_403)) (flet ($cvcl_407 (and $cvcl_406 $cvcl_284)) (flet ($cvcl_491 (or $cvcl_407  (and (if_then_else (or $cvcl_242  $cvcl_407 ) false true) $cvcl_408) )) (flet ($cvcl_433 (if_then_else $cvcl_491 false true)) (flet ($cvcl_446 (or $cvcl_354  (and (if_then_else (or $cvcl_354  (and $cvcl_405 $cvcl_433) ) false true) $cvcl_364) )) (flet ($cvcl_411 (and $cvcl_99 $cvcl_128)) (flet ($cvcl_495 (or $cvcl_411  (and (if_then_else (or $cvcl_411  $cvcl_92 ) false true) $cvcl_412) )) (flet ($cvcl_414 (or $cvcl_205  (and $cvcl_495 (if_then_else $cvcl_413 false true)) )) (flet ($cvcl_496 (or $cvcl_414  (and (if_then_else $cvcl_414 false true) $cvcl_413) )) (flet ($cvcl_415 (and $cvcl_162 (and $cvcl_496 dsr_7))) (flet ($cvcl_471 (or $cvcl_415  (and (if_then_else (or $cvcl_284  $cvcl_415 ) false true) $cvcl_389) )) (flet ($cvcl_448 (if_then_else (and $cvcl_471 $cvcl_416) false true)) (flet ($cvcl_447 (and $cvcl_410 (if_then_else $cvcl_448 false true))) (flet ($cvcl_487 (if_then_else $cvcl_404 (if_then_else $cvcl_446 false true) (if_then_else $cvcl_397 false (if_then_else $cvcl_409 false (if_then_else $cvcl_447 true false))))) (flet ($cvcl_437 (if_then_else $cvcl_355 (if_then_else $cvcl_356 false true) (if_then_else $cvcl_273 false (if_then_else $cvcl_323 (if_then_else $cvcl_351 false $cvcl_417) true)))) (flet ($cvcl_424 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 $cvcl_346 (if_then_else $cvcl_347 false (if_then_else $cvcl_260 false (if_then_else $cvcl_348 false (if_then_else $cvcl_349 false true))))))))) (flet ($cvcl_420 (if_then_else $cvcl_347 false $cvcl_418)) (flet ($cvcl_419 (if_then_else $cvcl_344 false (if_then_else $cvcl_345 $cvcl_346 $cvcl_420))) (flet ($cvcl_425 (if_then_else $cvcl_342 true (if_then_else $cvcl_343 false $cvcl_419))) (flet ($cvcl_426 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 true $cvcl_419))) (flet ($cvcl_427 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 true (if_then_else $cvcl_345 (if_then_else eoc_9 true false) $cvcl_420))))) (flet ($cvcl_429 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 (if_then_else eoc_9 false true) $cvcl_420))))) (flet ($cvcl_430 (if_then_else $cvcl_342 false (if_then_else $cvcl_343 false (if_then_else $cvcl_344 false (if_then_else $cvcl_345 $cvcl_346 (if_then_else $cvcl_347 false (if_then_else $cvcl_260 true $cvcl_421))))))) (flet ($cvcl_431 (if_then_else $cvcl_422 false true)) (flet ($cvcl_428 (if_then_else eoc_8 false false)) (flet ($cvcl_504 (if_then_else $cvcl_430 false (if_then_else $cvcl_431 false false))) (flet ($cvcl_501 (if_then_else $cvcl_341 false $cvcl_504)) (flet ($cvcl_423 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 false (if_then_else $cvcl_427 $cvcl_428 (if_then_else $cvcl_429 true $cvcl_501)))))) (flet ($cvcl_432 (and $cvcl_274 $cvcl_275)) (flet ($cvcl_505 (or $cvcl_432  (and (if_then_else (or $cvcl_432  (and $cvcl_352 $cvcl_353) ) false true) $cvcl_422) )) (flet ($cvcl_438 (or $cvcl_423  (and (if_then_else (or $cvcl_423  (and (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 false (if_then_else $cvcl_427 $cvcl_428 (if_then_else $cvcl_429 false (if_then_else $cvcl_341 false (if_then_else $cvcl_430 true (if_then_else $cvcl_431 true false)))))))) $cvcl_505) ) false true) $cvcl_356) )) (flet ($cvcl_434 (and $cvcl_323 $cvcl_408)) (flet ($cvcl_518 (or (and $cvcl_434 $cvcl_357)  (and (if_then_else $cvcl_434 false true) $cvcl_435) )) (flet ($cvcl_439 (if_then_else $cvcl_518 false true)) (flet ($cvcl_436 (if_then_else $cvcl_437 (if_then_else $cvcl_438 true false) (if_then_else $cvcl_354 false (if_then_else $cvcl_405 (if_then_else $cvcl_433 false (if_then_else $cvcl_439 true false)) false)))) (flet ($cvcl_500 (if_then_else $cvcl_439 false false)) (flet ($cvcl_488 (if_then_else $cvcl_437 (if_then_else $cvcl_438 false false) (if_then_else $cvcl_354 true (if_then_else $cvcl_405 (if_then_else $cvcl_433 true $cvcl_500) false)))) (flet ($cvcl_489 (if_then_else $cvcl_242 $cvcl_440 (if_then_else $cvcl_235 false (if_then_else $cvcl_246 true (if_then_else $cvcl_284 false true))))) (flet ($cvcl_442 (and $cvcl_489 $cvcl_441)) (flet ($cvcl_526 (or $cvcl_442  (and (if_then_else (or $cvcl_322  $cvcl_442 ) false true) $cvcl_443) )) (flet ($cvcl_527 (or $cvcl_436  (and (if_then_else (or $cvcl_436  (and $cvcl_488 (if_then_else $cvcl_526 false true)) ) false true) $cvcl_444) )) (flet ($cvcl_445 (and $cvcl_487 $cvcl_527)) (flet ($cvcl_481 (if_then_else $cvcl_409 false (if_then_else $cvcl_447 false false))) (flet ($cvcl_480 (if_then_else $cvcl_404 (if_then_else $cvcl_446 true false) (if_then_else $cvcl_397 false $cvcl_481))) (flet ($cvcl_483 (or $cvcl_445  (and (if_then_else (or $cvcl_445  $cvcl_480 ) false true) $cvcl_400) )) (flet ($cvcl_467 (if_then_else $cvcl_459 false false)) (flet ($cvcl_466 (if_then_else $cvcl_458 false $cvcl_467)) (flet ($cvcl_465 (if_then_else $cvcl_457 false $cvcl_466)) (flet ($cvcl_464 (if_then_else $cvcl_456 false $cvcl_465)) (flet ($cvcl_463 (if_then_else $cvcl_455 false $cvcl_464)) (flet ($cvcl_462 (if_then_else $cvcl_454 false $cvcl_463)) (flet ($cvcl_461 (if_then_else $cvcl_453 false $cvcl_462)) (flet ($cvcl_460 (if_then_else $cvcl_452 false $cvcl_461)) (flet ($cvcl_533 (if_then_else $cvcl_449 $cvcl_450 (if_then_else $cvcl_451 false $cvcl_460))) (flet ($cvcl_535 (if_then_else $cvcl_449 $cvcl_452 (if_then_else $cvcl_451 true $cvcl_460))) (flet ($cvcl_536 (if_then_else $cvcl_449 $cvcl_453 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 true $cvcl_461)))) (flet ($cvcl_537 (if_then_else $cvcl_449 $cvcl_454 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 true $cvcl_462))))) (flet ($cvcl_538 (if_then_else $cvcl_449 $cvcl_455 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 true $cvcl_463)))))) (flet ($cvcl_539 (if_then_else $cvcl_449 $cvcl_456 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 true $cvcl_464))))))) (flet ($cvcl_540 (if_then_else $cvcl_449 $cvcl_457 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 false (if_then_else $cvcl_456 true $cvcl_465)))))))) (flet ($cvcl_541 (if_then_else $cvcl_449 $cvcl_458 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 false (if_then_else $cvcl_456 false (if_then_else $cvcl_457 true $cvcl_466))))))))) (flet ($cvcl_542 (if_then_else $cvcl_449 $cvcl_459 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 false (if_then_else $cvcl_456 false (if_then_else $cvcl_457 false (if_then_else $cvcl_458 true $cvcl_467)))))))))) (flet ($cvcl_532 (or $cvcl_448  $cvcl_533 )) (flet ($cvcl_534 (if_then_else $cvcl_449 $cvcl_451 (if_then_else $cvcl_451 false (if_then_else $cvcl_452 false (if_then_else $cvcl_453 false (if_then_else $cvcl_454 false (if_then_else $cvcl_455 false (if_then_else $cvcl_456 false (if_then_else $cvcl_457 false (if_then_else $cvcl_458 false (if_then_else $cvcl_459 false true))))))))))) (flet ($cvcl_493 (if_then_else $cvcl_532 $cvcl_410 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 false (if_then_else $cvcl_539 false (if_then_else $cvcl_540 false (if_then_else $cvcl_541 false (if_then_else $cvcl_542 true false))))))))))) (flet ($cvcl_469 (and $cvcl_239 $cvcl_468)) (flet ($cvcl_553 (or $cvcl_469  (and (if_then_else (or $cvcl_441  $cvcl_469 ) false true) $cvcl_470) )) (flet ($cvcl_555 (if_then_else $cvcl_416 true false)) (flet ($cvcl_556 (> (- tx_conta_12 cvclZero) 97)) (flet ($cvcl_557 (if_then_else send_en_12 (if_then_else $cvcl_89 false $cvcl_556) $cvcl_473)) (flet ($cvcl_558 (if_then_else $cvcl_87 (if_then_else $cvcl_154 false $cvcl_557) $cvcl_474)) (flet ($cvcl_559 (if_then_else $cvcl_152 (if_then_else $cvcl_230 false $cvcl_558) $cvcl_475)) (flet ($cvcl_560 (if_then_else $cvcl_229 (if_then_else $cvcl_309 false $cvcl_559) $cvcl_476)) (flet ($cvcl_561 (if_then_else $cvcl_308 (if_then_else $cvcl_390 false $cvcl_560) $cvcl_477)) (flet ($cvcl_562 (if_then_else $cvcl_389 (if_then_else $cvcl_472 false $cvcl_561) $cvcl_478)) (flet ($cvcl_499 (if_then_else $cvcl_471 (if_then_else $cvcl_555 false $cvcl_562) $cvcl_416)) (flet ($cvcl_479 (or (and $cvcl_493 (if_then_else (if_then_else (and $cvcl_553 $cvcl_499) false true) false true))  (and $cvcl_400 (if_then_else $cvcl_399 false true)) )) (flet ($cvcl_482 (or $cvcl_479  (and (if_then_else $cvcl_479 false true) $cvcl_399) )) (flet ($cvcl_492 (if_then_else $cvcl_404 (if_then_else $cvcl_446 false false) (if_then_else $cvcl_397 true $cvcl_481))) (flet ($cvcl_484 (or $cvcl_480  (and (if_then_else (or $cvcl_480  $cvcl_492 ) false true) $cvcl_401) )) (flet ($cvcl_569 (or (or (and $cvcl_483 $cvcl_482)  (and $cvcl_484 (if_then_else (and $cvcl_482 dsr_3) false true)) )  (and (if_then_else (or $cvcl_483  $cvcl_484 ) false true) $cvcl_485) )) (flet ($cvcl_570 (and (if_then_else (and $cvcl_486 $cvcl_569) false true) $cvcl_486)) (flet ($cvcl_490 (and $cvcl_489 $cvcl_365)) (flet ($cvcl_516 (if_then_else (or $cvcl_490  (and (if_then_else (or $cvcl_322  $cvcl_490 ) false true) $cvcl_491) ) false true)) (flet ($cvcl_529 (or $cvcl_436  (and (if_then_else (or $cvcl_436  (and $cvcl_488 $cvcl_516) ) false true) $cvcl_446) )) (flet ($cvcl_494 (and $cvcl_165 $cvcl_204)) (flet ($cvcl_497 (or $cvcl_284  (and (or $cvcl_494  (and (if_then_else (or $cvcl_494  $cvcl_158 ) false true) $cvcl_495) ) (if_then_else $cvcl_496 false true)) )) (flet ($cvcl_498 (and $cvcl_239 (and (or $cvcl_497  (and (if_then_else $cvcl_497 false true) $cvcl_496) ) dsr_6))) (flet ($cvcl_554 (or $cvcl_498  (and (if_then_else (or $cvcl_365  $cvcl_498 ) false true) $cvcl_471) )) (flet ($cvcl_531 (if_then_else (and $cvcl_554 $cvcl_499) false true)) (flet ($cvcl_530 (and $cvcl_493 (if_then_else $cvcl_531 false true))) (flet ($cvcl_520 (if_then_else $cvcl_437 (if_then_else $cvcl_438 false true) (if_then_else $cvcl_354 false (if_then_else $cvcl_405 (if_then_else $cvcl_433 false $cvcl_500) true)))) (flet ($cvcl_507 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 false (if_then_else $cvcl_427 $cvcl_428 (if_then_else $cvcl_429 false (if_then_else $cvcl_341 false (if_then_else $cvcl_430 false (if_then_else $cvcl_431 false true))))))))) (flet ($cvcl_503 (if_then_else $cvcl_429 false $cvcl_501)) (flet ($cvcl_502 (if_then_else $cvcl_426 false (if_then_else $cvcl_427 $cvcl_428 $cvcl_503))) (flet ($cvcl_508 (if_then_else $cvcl_424 true (if_then_else $cvcl_425 false $cvcl_502))) (flet ($cvcl_509 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 true $cvcl_502))) (flet ($cvcl_510 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 true (if_then_else $cvcl_427 (if_then_else eoc_8 true false) $cvcl_503))))) (flet ($cvcl_512 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 false (if_then_else $cvcl_427 (if_then_else eoc_8 false true) $cvcl_503))))) (flet ($cvcl_513 (if_then_else $cvcl_424 false (if_then_else $cvcl_425 false (if_then_else $cvcl_426 false (if_then_else $cvcl_427 $cvcl_428 (if_then_else $cvcl_429 false (if_then_else $cvcl_341 true $cvcl_504))))))) (flet ($cvcl_514 (if_then_else $cvcl_505 false true)) (flet ($cvcl_511 (if_then_else eoc_7 false false)) (flet ($cvcl_506 (if_then_else $cvcl_507 false (if_then_else $cvcl_508 false (if_then_else $cvcl_509 false (if_then_else $cvcl_510 $cvcl_511 (if_then_else $cvcl_512 true (if_then_else $cvcl_423 false (if_then_else $cvcl_513 false (if_then_else $cvcl_514 false false))))))))) (flet ($cvcl_515 (and $cvcl_355 $cvcl_356)) (flet ($cvcl_521 (or $cvcl_506  (and (if_then_else (or $cvcl_506  (and (if_then_else $cvcl_507 false (if_then_else $cvcl_508 false (if_then_else $cvcl_509 false (if_then_else $cvcl_510 $cvcl_511 (if_then_else $cvcl_512 false (if_then_else $cvcl_423 false (if_then_else $cvcl_513 true (if_then_else $cvcl_514 true false)))))))) (or $cvcl_515  (and (if_then_else (or $cvcl_515  (and $cvcl_434 $cvcl_435) ) false true) $cvcl_505) )) ) false true) $cvcl_438) )) (flet ($cvcl_517 (and $cvcl_405 $cvcl_491)) (flet ($cvcl_522 (if_then_else (or (and $cvcl_517 $cvcl_439)  (and (if_then_else $cvcl_517 false true) $cvcl_518) ) false true)) (flet ($cvcl_519 (if_then_else $cvcl_520 (if_then_else $cvcl_521 true false) (if_then_else $cvcl_436 false (if_then_else $cvcl_488 (if_then_else $cvcl_516 false (if_then_else $cvcl_522 true false)) false)))) (flet ($cvcl_525 (and (if_then_else $cvcl_322 $cvcl_523 (if_then_else $cvcl_315 false (if_then_else $cvcl_327 true (if_then_else $cvcl_365 false true)))) $cvcl_524)) (flet ($cvcl_528 (and (if_then_else $cvcl_487 (if_then_else $cvcl_529 false true) (if_then_else $cvcl_480 false (if_then_else $cvcl_492 false (if_then_else $cvcl_530 true false)))) (or $cvcl_519  (and (if_then_else (or $cvcl_519  (and (if_then_else $cvcl_520 (if_then_else $cvcl_521 false false) (if_then_else $cvcl_436 true (if_then_else $cvcl_488 (if_then_else $cvcl_516 true (if_then_else $cvcl_522 false false)) false))) (if_then_else (or $cvcl_525  (and (if_then_else (or $cvcl_404  $cvcl_525 ) false true) $cvcl_526) ) false true)) ) false true) $cvcl_527) ))) (flet ($cvcl_565 (if_then_else $cvcl_492 false (if_then_else $cvcl_530 false false))) (flet ($cvcl_564 (if_then_else $cvcl_487 (if_then_else $cvcl_529 true false) (if_then_else $cvcl_480 false $cvcl_565))) (flet ($cvcl_567 (or $cvcl_528  (and (if_then_else (or $cvcl_528  $cvcl_564 ) false true) $cvcl_483) )) (flet ($cvcl_550 (if_then_else $cvcl_542 false false)) (flet ($cvcl_549 (if_then_else $cvcl_541 false $cvcl_550)) (flet ($cvcl_548 (if_then_else $cvcl_540 false $cvcl_549)) (flet ($cvcl_547 (if_then_else $cvcl_539 false $cvcl_548)) (flet ($cvcl_546 (if_then_else $cvcl_538 false $cvcl_547)) (flet ($cvcl_545 (if_then_else $cvcl_537 false $cvcl_546)) (flet ($cvcl_544 (if_then_else $cvcl_536 false $cvcl_545)) (flet ($cvcl_543 (if_then_else $cvcl_535 false $cvcl_544)) (flet ($cvcl_552 (and $cvcl_319 $cvcl_551)) (flet ($cvcl_563 (or (and (if_then_else (or $cvcl_531  (if_then_else $cvcl_532 $cvcl_533 (if_then_else $cvcl_534 false $cvcl_543)) ) $cvcl_493 (if_then_else (if_then_else $cvcl_532 $cvcl_534 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 false (if_then_else $cvcl_539 false (if_then_else $cvcl_540 false (if_then_else $cvcl_541 false (if_then_else $cvcl_542 false true)))))))))) false (if_then_else (if_then_else $cvcl_532 $cvcl_535 (if_then_else $cvcl_534 true $cvcl_543)) false (if_then_else (if_then_else $cvcl_532 $cvcl_536 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 true $cvcl_544))) false (if_then_else (if_then_else $cvcl_532 $cvcl_537 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 true $cvcl_545)))) false (if_then_else (if_then_else $cvcl_532 $cvcl_538 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 true $cvcl_546))))) false (if_then_else (if_then_else $cvcl_532 $cvcl_539 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 true $cvcl_547)))))) false (if_then_else (if_then_else $cvcl_532 $cvcl_540 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 false (if_then_else $cvcl_539 true $cvcl_548))))))) false (if_then_else (if_then_else $cvcl_532 $cvcl_541 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 false (if_then_else $cvcl_539 false (if_then_else $cvcl_540 true $cvcl_549)))))))) false (if_then_else (if_then_else $cvcl_532 $cvcl_542 (if_then_else $cvcl_534 false (if_then_else $cvcl_535 false (if_then_else $cvcl_536 false (if_then_else $cvcl_537 false (if_then_else $cvcl_538 false (if_then_else $cvcl_539 false (if_then_else $cvcl_540 false (if_then_else $cvcl_541 true $cvcl_550))))))))) true false)))))))))) (if_then_else (if_then_else (and (or $cvcl_552  (and (if_then_else (or $cvcl_524  $cvcl_552 ) false true) $cvcl_553) ) (if_then_else $cvcl_554 (if_then_else (if_then_else $cvcl_499 true false) false (if_then_else $cvcl_471 (if_then_else $cvcl_555 false (if_then_else $cvcl_389 (if_then_else $cvcl_472 false (if_then_else $cvcl_308 (if_then_else $cvcl_390 false (if_then_else $cvcl_229 (if_then_else $cvcl_309 false (if_then_else $cvcl_152 (if_then_else $cvcl_230 false (if_then_else $cvcl_87 (if_then_else $cvcl_154 false (if_then_else send_en_12 (if_then_else $cvcl_89 false (> (- tx_conta_12 cvclZero) 96)) $cvcl_556)) $cvcl_557)) $cvcl_558)) $cvcl_559)) $cvcl_560)) $cvcl_561)) $cvcl_562)) $cvcl_499)) false true) false true))  (and $cvcl_483 (if_then_else $cvcl_482 false true)) )) (flet ($cvcl_566 (or $cvcl_563  (and (if_then_else $cvcl_563 false true) $cvcl_482) )) (flet ($cvcl_568 (or $cvcl_564  (and (if_then_else (or $cvcl_564  (if_then_else $cvcl_487 (if_then_else $cvcl_529 false false) (if_then_else $cvcl_480 true $cvcl_565)) ) false true) $cvcl_484) )) (not (iff (and (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_570 (or (or (and $cvcl_567 $cvcl_566)  (and $cvcl_568 (if_then_else (and $cvcl_566 dsr_2) false true)) )  (and (if_then_else (or $cvcl_567  $cvcl_568 ) false true) $cvcl_569) )) false true) $cvcl_570) false true) (iff send_data_12 false)) (iff rdy_12 false)) (iff shot_12 false)) (iff mpx_12 false)) (iff load_12 false)) (iff confirm_12 false)) (iff send_12 false)) (iff send_en_12 false)) (iff error_12 false)) (iff tre_12 false)) (iff tx_end_12 false)) (iff bstate40_12 true)) (= (- S1_12 cvclZero) 0)) (= (- S2_12 cvclZero) 0)) $cvcl_30) (= (- next_bit_12 cvclZero) 0)) (= (- tx_conta_12 cvclZero) 0)) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)