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