diff options
Diffstat (limited to 'test/regress/regress1/nl')
48 files changed, 2135 insertions, 24 deletions
diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am index a7e4c1411..bafaf665a 100644 --- a/test/regress/regress1/nl/Makefile.am +++ b/test/regress/regress1/nl/Makefile.am @@ -17,8 +17,53 @@ endif # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - siegel-nl-bases.smt2 \ - mirko-050417.smt2 + mirko-050417.smt2 \ + arrowsmith-050317.smt2 \ + bug698.smt2 \ + dist-big.smt2 \ + dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \ + exp-4.5-lt.smt2 \ + metitarski_3_4_2e.smt2 \ + metitarski-3-4.smt2 \ + nl-help-unsat-quant.smt2 \ + poly-1025.smt2 \ + quant-nl.smt2 \ + red-exp.smt2 \ + rewriting-sums.smt2 \ + simple-mono.smt2 \ + sin1-sat.smt2 \ + sin-compare.smt2 \ + sin-compare-across-phase.smt2 \ + sqrt-problem-1.smt2 \ + sugar-ident-2.smt2 \ + sugar-ident-3.smt2 \ + tan-rewrite2.smt2 \ + bad-050217.smt2 \ + coeff-unsat-base.smt2 \ + coeff-unsat.smt2 \ + combine.smt2 \ + cos-bound.smt2 \ + cos1-tc.smt2 \ + disj-eval.smt2 \ + div-mod-partial.smt2 \ + exp_monotone.smt2 \ + exp1-lb.smt2 \ + metitarski-1025.smt2 \ + NAVIGATION2.smt2 \ + nl-unk-quant.smt2 \ + ones.smt2 \ + shifting.smt2 \ + shifting2.smt2 \ + simple-mono-unsat.smt2 \ + sin-init-tangents.smt2 \ + sin-sign.smt2 \ + sin-sym2.smt2 \ + sin1-lb.smt2 \ + sin1-ub.smt2 \ + sin2-lb.smt2 \ + sin2-ub.smt2 \ + sugar-ident.smt2 \ + zero-subset.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/nl/NAVIGATION2.smt2 b/test/regress/regress1/nl/NAVIGATION2.smt2 new file mode 100644 index 000000000..445b8a21e --- /dev/null +++ b/test/regress/regress1/nl/NAVIGATION2.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :source |printed by MathSAT|) +(declare-fun X () Real) + +(assert (let ((.def_44 (* (- (/ 11 10)) X))) +(let ((.def_45 (exp .def_44))) +(let ((.def_50 (* 250 .def_45))) +(let ((.def_40 (* (- (/ 13 10)) X))) +(let ((.def_41 (exp .def_40))) +(let ((.def_52 (* 173 .def_41))) +(let ((.def_53 (+ .def_52 .def_50))) +(let ((.def_54 (* 250 X))) +(let ((.def_55 (+ .def_54 .def_53))) +(let ((.def_56 (<= .def_55 (/ 595 2)))) +(let ((.def_57 (not .def_56))) +(let ((.def_31 (<= 0 X))) +(let ((.def_32 (not .def_31))) +(let ((.def_58 (or .def_32 .def_57))) +(let ((.def_59 (not .def_58))) +.def_59)))))))))))))))) +(check-sat) diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2 new file mode 100644 index 000000000..04b06e1f5 --- /dev/null +++ b/test/regress/regress1/nl/arrowsmith-050317.smt2 @@ -0,0 +1,95 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.location.0__AT0@0 () Bool) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.location.0__AT0@4 () Bool) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.location.0__AT0@1 () Bool) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun time__AT0@1 () Real) +(declare-fun event_is_timed__AT0@3 () Bool) +(declare-fun instance.location.0__AT0@3 () Bool) +(declare-fun instance.x__AT0@3 () Real) +(declare-fun instance.y__AT0@3 () Real) +(declare-fun instance.EVENT.0__AT0@2 () Bool) +(declare-fun instance.EVENT.1__AT0@2 () Bool) +(declare-fun time__AT0@3 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.location.0__AT0@2 () Bool) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun time__AT0@2 () Real) +(declare-fun event_is_timed__AT0@4 () Bool) +(declare-fun instance.x__AT0@4 () Real) +(declare-fun instance.y__AT0@4 () Real) +(declare-fun instance.EVENT.0__AT0@3 () Bool) +(declare-fun instance.EVENT.1__AT0@3 () Bool) +(declare-fun time__AT0@4 () Real) +(assert (let ((.def_0 (not instance.EVENT.1__AT0@3))) (let ((.def_1 (not instance.EVENT.0__AT0@3))) (let ((.def_2 (or .def_1 .def_0))) (let ((.def_3 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_4 (<= time__AT0@3 +time__AT0@4))) (let ((.def_5 (or .def_0 .def_4))) (let ((.def_6 (and .def_5 .def_3))) (let ((.def_7 (= time__AT0@3 time__AT0@4))) (let ((.def_8 (or instance.EVENT.1__AT0@3 .def_7))) (let ((.def_9 (and .def_8 .def_6))) (let +((.def_10 (<= instance.x__AT0@3 0.0))) (let ((.def_11 (not .def_10))) (let ((.def_12 (not instance.location.0__AT0@3))) (let ((.def_13 (and .def_12 .def_11))) (let ((.def_14 (and instance.location.0__AT0@4 .def_13))) (let ((.def_15 +(= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_16 (and .def_15 .def_14))) (let ((.def_17 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_18 (and .def_17 .def_16))) (let ((.def_19 (<= instance.y__AT0@3 0.0))) (let +((.def_20 (and .def_12 .def_19))) (let ((.def_21 (and instance.location.0__AT0@4 .def_20))) (let ((.def_22 (and .def_15 .def_21))) (let ((.def_23 (and .def_17 .def_22))) (let ((.def_24 (or .def_23 .def_18))) (let ((.def_25 (and +.def_7 .def_24))) (let ((.def_26 (or instance.EVENT.1__AT0@3 .def_25))) (let ((.def_27 (not .def_7))) (let ((.def_28 (and .def_15 .def_17))) (let ((.def_29 (or .def_28 .def_27))) (let ((.def_30 (and .def_28 .def_29))) (let +((.def_31 (or .def_30 .def_12))) (let ((.def_32 (* (- 1.0) time__AT0@3))) (let ((.def_33 (+ .def_32 time__AT0@4))) (let ((.def_34 (exp .def_33))) (let ((.def_35 (* instance.x__AT0@3 .def_34))) (let ((.def_36 (= instance.x__AT0@4 +.def_35))) (let ((.def_37 (* 2.0 instance.x__AT0@4))) (let ((.def_38 (* instance.y__AT0@4 .def_37))) (let ((.def_39 (* (- 1.0) .def_38))) (let ((.def_40 (* 2.0 instance.x__AT0@3))) (let ((.def_41 (* instance.y__AT0@3 .def_40))) +(let ((.def_42 (* (- 1.0) .def_41))) (let ((.def_43 (+ instance.y__AT0@3 .def_42))) (let ((.def_44 (* .def_43 .def_34))) (let ((.def_45 (* (- 1.0) .def_44))) (let ((.def_46 (+ .def_45 .def_39))) (let ((.def_47 (+ instance.y__AT0@4 +.def_46))) (let ((.def_48 (= .def_47 0.0))) (let ((.def_49 (and .def_48 .def_36))) (let ((.def_50 (and .def_49 .def_29))) (let ((.def_51 (or instance.location.0__AT0@3 .def_50))) (let ((.def_52 (and .def_51 .def_31))) (let +((.def_53 (and .def_52 .def_4))) (let ((.def_54 (= instance.location.0__AT0@4 instance.location.0__AT0@3))) (let ((.def_55 (and .def_54 .def_53))) (let ((.def_56 (or .def_0 .def_55))) (let ((.def_57 (and .def_56 .def_26))) (let +((.def_58 (and .def_1 .def_0))) (let ((.def_59 (or .def_58 .def_57))) (let ((.def_60 (and .def_59 .def_9))) (let ((.def_61 (not .def_58))) (let ((.def_62 (and .def_54 .def_15))) (let ((.def_63 (and .def_62 .def_17))) (let ((.def_64 +(or .def_63 .def_61))) (let ((.def_65 (and .def_64 .def_60))) (let ((.def_66 (not event_is_timed__AT0@3))) (let ((.def_67 (= event_is_timed__AT0@4 .def_66))) (let ((.def_68 (and .def_67 .def_65))) (let ((.def_69 (and .def_68 +.def_2))) (let ((.def_70 (not instance.EVENT.1__AT0@2))) (let ((.def_71 (not instance.EVENT.0__AT0@2))) (let ((.def_72 (or .def_71 .def_70))) (let ((.def_73 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_74 (<= +time__AT0@2 time__AT0@3))) (let ((.def_75 (or .def_70 .def_74))) (let ((.def_76 (and .def_75 .def_73))) (let ((.def_77 (= time__AT0@2 time__AT0@3))) (let ((.def_78 (or instance.EVENT.1__AT0@2 .def_77))) (let ((.def_79 (and .def_78 +.def_76))) (let ((.def_80 (<= instance.x__AT0@2 0.0))) (let ((.def_81 (not .def_80))) (let ((.def_82 (not instance.location.0__AT0@2))) (let ((.def_83 (and .def_82 .def_81))) (let ((.def_84 (and instance.location.0__AT0@3 +.def_83))) (let ((.def_85 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_86 (and .def_85 .def_84))) (let ((.def_87 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_88 (and .def_87 .def_86))) (let ((.def_89 (<= +instance.y__AT0@2 0.0))) (let ((.def_90 (and .def_82 .def_89))) (let ((.def_91 (and instance.location.0__AT0@3 .def_90))) (let ((.def_92 (and .def_85 .def_91))) (let ((.def_93 (and .def_87 .def_92))) (let ((.def_94 (or .def_93 +.def_88))) (let ((.def_95 (and .def_77 .def_94))) (let ((.def_96 (or instance.EVENT.1__AT0@2 .def_95))) (let ((.def_97 (not .def_77))) (let ((.def_98 (and .def_85 .def_87))) (let ((.def_99 (or .def_98 .def_97))) (let ((.def_100 +(and .def_98 .def_99))) (let ((.def_101 (or .def_100 .def_82))) (let ((.def_102 (* (- 1.0) time__AT0@2))) (let ((.def_103 (+ .def_102 time__AT0@3))) (let ((.def_104 (exp .def_103))) (let ((.def_105 (* instance.x__AT0@2 .def_104))) +(let ((.def_106 (= instance.x__AT0@3 .def_105))) (let ((.def_107 (* 2.0 instance.x__AT0@2))) (let ((.def_108 (* instance.y__AT0@2 .def_107))) (let ((.def_109 (* (- 1.0) .def_108))) (let ((.def_110 (+ instance.y__AT0@2 .def_109))) +(let ((.def_111 (* .def_110 .def_104))) (let ((.def_112 (* (- 1.0) .def_111))) (let ((.def_113 (+ .def_112 .def_42))) (let ((.def_114 (+ instance.y__AT0@3 .def_113))) (let ((.def_115 (= .def_114 0.0))) (let ((.def_116 (and .def_115 +.def_106))) (let ((.def_117 (and .def_116 .def_99))) (let ((.def_118 (or instance.location.0__AT0@2 .def_117))) (let ((.def_119 (and .def_118 .def_101))) (let ((.def_120 (and .def_119 .def_74))) (let ((.def_121 (= +instance.location.0__AT0@2 instance.location.0__AT0@3))) (let ((.def_122 (and .def_121 .def_120))) (let ((.def_123 (or .def_70 .def_122))) (let ((.def_124 (and .def_123 .def_96))) (let ((.def_125 (and .def_71 .def_70))) (let +((.def_126 (or .def_125 .def_124))) (let ((.def_127 (and .def_126 .def_79))) (let ((.def_128 (not .def_125))) (let ((.def_129 (and .def_121 .def_85))) (let ((.def_130 (and .def_129 .def_87))) (let ((.def_131 (or .def_130 +.def_128))) (let ((.def_132 (and .def_131 .def_127))) (let ((.def_133 (not event_is_timed__AT0@2))) (let ((.def_134 (= event_is_timed__AT0@3 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (and .def_135 +.def_72))) (let ((.def_137 (not instance.EVENT.1__AT0@1))) (let ((.def_138 (not instance.EVENT.0__AT0@1))) (let ((.def_139 (or .def_138 .def_137))) (let ((.def_140 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_141 +(<= time__AT0@1 time__AT0@2))) (let ((.def_142 (or .def_137 .def_141))) (let ((.def_143 (and .def_142 .def_140))) (let ((.def_144 (= time__AT0@1 time__AT0@2))) (let ((.def_145 (or instance.EVENT.1__AT0@1 .def_144))) (let ((.def_146 +(and .def_145 .def_143))) (let ((.def_147 (<= instance.x__AT0@1 0.0))) (let ((.def_148 (not .def_147))) (let ((.def_149 (not instance.location.0__AT0@1))) (let ((.def_150 (and .def_149 .def_148))) (let ((.def_151 (and +instance.location.0__AT0@2 .def_150))) (let ((.def_152 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_153 (and .def_152 .def_151))) (let ((.def_154 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_155 (and .def_154 +.def_153))) (let ((.def_156 (<= instance.y__AT0@1 0.0))) (let ((.def_157 (and .def_149 .def_156))) (let ((.def_158 (and instance.location.0__AT0@2 .def_157))) (let ((.def_159 (and .def_152 .def_158))) (let ((.def_160 (and .def_154 +.def_159))) (let ((.def_161 (or .def_160 .def_155))) (let ((.def_162 (and .def_144 .def_161))) (let ((.def_163 (or instance.EVENT.1__AT0@1 .def_162))) (let ((.def_164 (not .def_144))) (let ((.def_165 (and .def_152 .def_154))) (let +((.def_166 (or .def_165 .def_164))) (let ((.def_167 (and .def_165 .def_166))) (let ((.def_168 (or .def_167 .def_149))) (let ((.def_169 (* (- 1.0) time__AT0@1))) (let ((.def_170 (+ .def_169 time__AT0@2))) (let ((.def_171 (exp +.def_170))) (let ((.def_172 (* instance.x__AT0@1 .def_171))) (let ((.def_173 (= instance.x__AT0@2 .def_172))) (let ((.def_174 (* 2.0 instance.x__AT0@1))) (let ((.def_175 (* instance.y__AT0@1 .def_174))) (let ((.def_176 (* (- 1.0) +.def_175))) (let ((.def_177 (+ instance.y__AT0@1 .def_176))) (let ((.def_178 (* .def_177 .def_171))) (let ((.def_179 (* (- 1.0) .def_178))) (let ((.def_180 (+ .def_179 .def_109))) (let ((.def_181 (+ instance.y__AT0@2 .def_180))) +(let ((.def_182 (= .def_181 0.0))) (let ((.def_183 (and .def_182 .def_173))) (let ((.def_184 (and .def_183 .def_166))) (let ((.def_185 (or instance.location.0__AT0@1 .def_184))) (let ((.def_186 (and .def_185 .def_168))) (let +((.def_187 (and .def_186 .def_141))) (let ((.def_188 (= instance.location.0__AT0@1 instance.location.0__AT0@2))) (let ((.def_189 (and .def_188 .def_187))) (let ((.def_190 (or .def_137 .def_189))) (let ((.def_191 (and .def_190 +.def_163))) (let ((.def_192 (and .def_138 .def_137))) (let ((.def_193 (or .def_192 .def_191))) (let ((.def_194 (and .def_193 .def_146))) (let ((.def_195 (not .def_192))) (let ((.def_196 (and .def_188 .def_152))) (let ((.def_197 +(and .def_196 .def_154))) (let ((.def_198 (or .def_197 .def_195))) (let ((.def_199 (and .def_198 .def_194))) (let ((.def_200 (not event_is_timed__AT0@1))) (let ((.def_201 (= event_is_timed__AT0@2 .def_200))) (let ((.def_202 (and +.def_201 .def_199))) (let ((.def_203 (and .def_202 .def_139))) (let ((.def_204 (not instance.EVENT.1__AT0@0))) (let ((.def_205 (not instance.EVENT.0__AT0@0))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (= +event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_208 (<= time__AT0@0 time__AT0@1))) (let ((.def_209 (or .def_204 .def_208))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (= time__AT0@0 time__AT0@1))) (let +((.def_212 (or instance.EVENT.1__AT0@0 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (<= instance.x__AT0@0 0.0))) (let ((.def_215 (not .def_214))) (let ((.def_216 (not instance.location.0__AT0@0))) (let +((.def_217 (and .def_216 .def_215))) (let ((.def_218 (and instance.location.0__AT0@1 .def_217))) (let ((.def_219 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_220 (and .def_219 .def_218))) (let ((.def_221 (= +instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_222 (and .def_221 .def_220))) (let ((.def_223 (<= instance.y__AT0@0 0.0))) (let ((.def_224 (and .def_216 .def_223))) (let ((.def_225 (and instance.location.0__AT0@1 .def_224))) +(let ((.def_226 (and .def_219 .def_225))) (let ((.def_227 (and .def_221 .def_226))) (let ((.def_228 (or .def_227 .def_222))) (let ((.def_229 (and .def_211 .def_228))) (let ((.def_230 (or instance.EVENT.1__AT0@0 .def_229))) (let +((.def_231 (not .def_211))) (let ((.def_232 (and .def_219 .def_221))) (let ((.def_233 (or .def_232 .def_231))) (let ((.def_234 (and .def_232 .def_233))) (let ((.def_235 (or .def_216 .def_234))) (let ((.def_236 (* (- 1.0) +time__AT0@0))) (let ((.def_237 (+ .def_236 time__AT0@1))) (let ((.def_238 (exp .def_237))) (let ((.def_239 (* instance.x__AT0@0 .def_238))) (let ((.def_240 (= instance.x__AT0@1 .def_239))) (let ((.def_241 (* 2.0 +instance.x__AT0@0))) (let ((.def_242 (* instance.y__AT0@0 .def_241))) (let ((.def_243 (* (- 1.0) .def_242))) (let ((.def_244 (+ instance.y__AT0@0 .def_243))) (let ((.def_245 (* .def_244 .def_238))) (let ((.def_246 (* (- 1.0) +.def_245))) (let ((.def_247 (+ .def_246 .def_176))) (let ((.def_248 (+ instance.y__AT0@1 .def_247))) (let ((.def_249 (= .def_248 0.0))) (let ((.def_250 (and .def_249 .def_240))) (let ((.def_251 (and .def_250 .def_233))) (let +((.def_252 (or instance.location.0__AT0@0 .def_251))) (let ((.def_253 (and .def_252 .def_235))) (let ((.def_254 (and .def_253 .def_208))) (let ((.def_255 (= instance.location.0__AT0@0 instance.location.0__AT0@1))) (let ((.def_256 +(and .def_255 .def_254))) (let ((.def_257 (or .def_204 .def_256))) (let ((.def_258 (and .def_257 .def_230))) (let ((.def_259 (and .def_205 .def_204))) (let ((.def_260 (or .def_259 .def_258))) (let ((.def_261 (and .def_260 +.def_213))) (let ((.def_262 (not .def_259))) (let ((.def_263 (and .def_255 .def_219))) (let ((.def_264 (and .def_263 .def_221))) (let ((.def_265 (or .def_264 .def_262))) (let ((.def_266 (and .def_265 .def_261))) (let ((.def_267 +(not event_is_timed__AT0@0))) (let ((.def_268 (= event_is_timed__AT0@1 .def_267))) (let ((.def_269 (and .def_268 .def_266))) (let ((.def_270 (and .def_269 .def_206))) (let ((.def_271 (= instance.x__AT0@0 (- 1.0)))) (let ((.def_272 +(= instance.y__AT0@0 1.0))) (let ((.def_273 (and .def_272 .def_271))) (let ((.def_274 (and .def_216 .def_273))) (let ((.def_275 (= time__AT0@0 0.0))) (let ((.def_276 (and .def_275 .def_274))) (let ((.def_277 (and .def_276 .def_270 +.def_203 .def_136 .def_69 instance.location.0__AT0@4))) +.def_277))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/bad-050217.smt2 b/test/regress/regress1/nl/bad-050217.smt2 new file mode 100644 index 000000000..3b9310748 --- /dev/null +++ b/test/regress/regress1/nl/bad-050217.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(assert (let ((.def_0 (<= 0.0 instance.x__AT0@1))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@0))) (let ((.def_3 (not instance.EVENT.0__AT0@0))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_6 (<= time__AT0@0 time__AT0@1))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@0 time__AT0@1))) (let ((.def_10 (or instance.EVENT.1__AT0@0 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) instance.y__AT0@0))) (let ((.def_13 (+ instance.x__AT0@0 .def_12))) (let ((.def_14 (* (- 1.0) time__AT0@0))) (let ((.def_15 (+ .def_14 time__AT0@1))) (let ((.def_16 (exp .def_15))) (let ((.def_17 (* .def_16 .def_13))) (let ((.def_18 (* (- 1.0) .def_17))) (let ((.def_19 (* (- 1.0) instance.y__AT0@1))) (let ((.def_20 (+ .def_19 .def_18))) (let ((.def_21 (+ instance.x__AT0@1 .def_20))) (let ((.def_22 (= .def_21 0.0))) (let ((.def_23 (+ instance.y__AT0@0 instance.x__AT0@0))) (let ((.def_24 (* .def_23 .def_16))) (let ((.def_25 (* (- 1.0) .def_24))) (let ((.def_26 (+ instance.y__AT0@1 .def_25))) (let ((.def_27 (+ instance.x__AT0@1 .def_26))) (let ((.def_28 (= .def_27 0.0))) (let ((.def_29 (and .def_28 .def_22))) (let ((.def_30 (not .def_9))) (let ((.def_31 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_32 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_33 (and .def_32 .def_31))) (let ((.def_34 (or .def_33 .def_30))) (let ((.def_35 (and .def_34 .def_29))) (let ((.def_36 (and .def_35 .def_6))) (let ((.def_37 (or .def_2 .def_36))) (let ((.def_38 (and .def_37 .def_10))) (let ((.def_39 (and .def_3 .def_2))) (let ((.def_40 (or .def_39 .def_38))) (let ((.def_41 (and .def_40 .def_11))) (let ((.def_42 (not .def_39))) (let ((.def_43 (or .def_42 .def_33))) (let ((.def_44 (and .def_43 .def_41))) (let ((.def_45 (not event_is_timed__AT0@0))) (let ((.def_46 (= event_is_timed__AT0@1 .def_45))) (let ((.def_47 (and .def_46 .def_44))) (let ((.def_48 (and .def_47 .def_4))) (let ((.def_49 (= instance.x__AT0@0 1.0))) (let ((.def_50 (= instance.y__AT0@0 0.0))) (let ((.def_51 (and .def_50 .def_49))) (let ((.def_52 (= time__AT0@0 0.0))) (let ((.def_53 (and .def_52 .def_51))) (let ((.def_54 (and .def_53 .def_48 .def_1))) .def_54)))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/bug698.smt2 b/test/regress/regress1/nl/bug698.smt2 new file mode 100644 index 000000000..ffb1eead2 --- /dev/null +++ b/test/regress/regress1/nl/bug698.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --incremental --nl-ext --fmf-fun-rlv --no-check-models +(set-logic UFNIA) +(set-info :smt-lib-version 2.5) + +; EXPECT: sat +(declare-fun fixedAdd() Int) +(assert (= fixedAdd (+ 2 (+ 2 (+ 2 0))))) +(check-sat) + +(define-fun-rec $$add$$ ((a Int)(b Int)) Int + (ite (= b 0) + 0 + (+ a ($$add$$ a (- b 1))))) + +; EXPECT: sat +(declare-fun variableAdd() Int) +(assert (= variableAdd ($$add$$ 2 3))) +(check-sat) + +; EXPECT: sat +(declare-fun fixedTimes() Int) +(assert (= fixedTimes (* 2 (* 2 (* 2 1))))) +(check-sat) + +; EXPECT: sat +(define-fun-rec $$pow$$ ((a Int)(b Int)) Int + (ite (= b 0) + 1 + (* a ($$pow$$ a (- b 1))))) + +(declare-fun variableTimes() Int) +(assert (= variableTimes ($$pow$$ 2 3))) +(check-sat) diff --git a/test/regress/regress1/nl/coeff-unsat-base.smt2 b/test/regress/regress1/nl/coeff-unsat-base.smt2 new file mode 100644 index 000000000..d56421bf9 --- /dev/null +++ b/test/regress/regress1/nl/coeff-unsat-base.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) + +(declare-fun a () Real) +(declare-fun b () Real) + +(assert (> a 0)) +(assert (> b 0)) + +(assert (>= a (* 3 b))) + +(assert (< (* a a) (* 3 a b))) + +(check-sat) diff --git a/test/regress/regress1/nl/coeff-unsat.smt2 b/test/regress/regress1/nl/coeff-unsat.smt2 new file mode 100644 index 000000000..f86d08fe7 --- /dev/null +++ b/test/regress/regress1/nl/coeff-unsat.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) + +(declare-fun a () Real) +(declare-fun b () Real) + +(assert (> a 0)) +(assert (> b 0)) + +(assert (>= a (* 3 b))) + +(assert (< (* a a) (* 8 b b))) + +(check-sat) diff --git a/test/regress/regress1/nl/combine.smt2 b/test/regress/regress1/nl/combine.smt2 new file mode 100644 index 000000000..9f7e7a548 --- /dev/null +++ b/test/regress/regress1/nl/combine.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(assert (> c 1)) +(assert (> (* a b) 1)) + +(assert (< (* a b c) 1)) + +(check-sat) diff --git a/test/regress/regress1/nl/cos-bound.smt2 b/test/regress/regress1/nl/cos-bound.smt2 new file mode 100644 index 000000000..e19260d63 --- /dev/null +++ b/test/regress/regress1/nl/cos-bound.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(declare-fun x () Real) +(assert (> (cos x) 1.0)) +(check-sat) diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2 new file mode 100644 index 000000000..7ddae1453 --- /dev/null +++ b/test/regress/regress1/nl/cos1-tc.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --nl-ext --no-nl-ext-tf-inc-prec +; EXPECT: unknown +(set-logic UFNRA) +(declare-fun f (Real) Real) + +(assert (= (f 0.0) (cos 1))) + +(check-sat) diff --git a/test/regress/regress1/nl/disj-eval.smt2 b/test/regress/regress1/nl/disj-eval.smt2 new file mode 100644 index 000000000..ac8cfc937 --- /dev/null +++ b/test/regress/regress1/nl/disj-eval.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NIA) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (or (= x 5) (= x 7) (= x 9) (= x 27) (= x 10))) +(assert (or (= y 0) (= y 1) (= y 9) (= y 8))) + + +(assert (= (* x x) (* y y y))) + +(check-sat) diff --git a/test/regress/regress1/nl/dist-big.smt2 b/test/regress/regress1/nl/dist-big.smt2 new file mode 100644 index 000000000..53c9c3f1d --- /dev/null +++ b/test/regress/regress1/nl/dist-big.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun v1 () Real) +(declare-fun v2 () Real) +(declare-fun v3 () Real) +(declare-fun v4 () Real) +(declare-fun v5 () Real) +(declare-fun v6 () Real) +(declare-fun v7 () Real) +(declare-fun v8 () Real) + +(assert (= (* (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8) (+ v1 v2 v3 v4 v5 v6 v7 v8)) 0)) + +(check-sat) diff --git a/test/regress/regress1/nl/div-mod-partial.smt2 b/test/regress/regress1/nl/div-mod-partial.smt2 new file mode 100644 index 000000000..fa75ee594 --- /dev/null +++ b/test/regress/regress1/nl/div-mod-partial.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: sat +(set-logic QF_UFNIA) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (not (= y 0))) +; should be SAT if the partial functions for div and mod are different +(assert (not (= (- y (* (div y x) x)) (mod y x)))) +(check-sat) diff --git a/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 new file mode 100644 index 000000000..5dce6ddca --- /dev/null +++ b/test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: sat +(set-logic QF_NRA) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun time__AT0@2 () Real) +(assert (let ((.def_0 (<= instance.y__AT0@2 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@1))) (let ((.def_3 (not instance.EVENT.0__AT0@1))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_6 (<= time__AT0@1 time__AT0@2))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@1 time__AT0@2))) (let ((.def_10 (or instance.EVENT.1__AT0@1 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@1))) (let ((.def_13 (+ .def_12 time__AT0@2))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@1 .def_14))) (let ((.def_16 (= instance.y__AT0@2 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@2))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@2))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_28 (= instance.y__AT0@2 instance.y__AT0@1))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@1))) (let ((.def_42 (= event_is_timed__AT0@2 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@0))) (let ((.def_46 (not instance.EVENT.0__AT0@0))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_49 (<= time__AT0@0 time__AT0@1))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@0 time__AT0@1))) (let ((.def_53 (or instance.EVENT.1__AT0@0 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@0))) (let ((.def_56 (+ .def_55 time__AT0@1))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@0 .def_57))) (let ((.def_59 (= instance.y__AT0@1 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@0))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@0))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_69 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@0))) (let ((.def_83 (= event_is_timed__AT0@1 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_87 (not .def_86))) (let ((.def_88 (<= 0.0 instance.x__AT0@0))) (let ((.def_89 (not .def_88))) (let ((.def_90 (and .def_89 .def_87))) (let ((.def_91 (<= 0.0 instance.y__AT0@0))) (let ((.def_92 (not .def_91))) (let ((.def_93 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_94 (and .def_93 .def_92))) (let ((.def_95 (and .def_94 .def_90))) (let ((.def_96 (= time__AT0@0 0.0))) (let ((.def_97 (and .def_96 .def_95))) (let ((.def_98 (and .def_97 .def_85 .def_44 .def_1))) .def_98)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/exp-4.5-lt.smt2 b/test/regress/regress1/nl/exp-4.5-lt.smt2 new file mode 100644 index 000000000..b0d39ff44 --- /dev/null +++ b/test/regress/regress1/nl/exp-4.5-lt.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (> (exp x) 2000.0)) +(assert (< x 4.5)) + +(check-sat) diff --git a/test/regress/regress1/nl/exp1-lb.smt2 b/test/regress/regress1/nl/exp1-lb.smt2 new file mode 100644 index 000000000..b0bc3079c --- /dev/null +++ b/test/regress/regress1/nl/exp1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (exp 1) 2.719)) +(assert (= x (exp 1))) + +(check-sat) diff --git a/test/regress/regress1/nl/exp_monotone.smt2 b/test/regress/regress1/nl/exp_monotone.smt2 new file mode 100644 index 000000000..a1360dc22 --- /dev/null +++ b/test/regress/regress1/nl/exp_monotone.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) +(declare-fun w () Real) + +(assert (< x w)) + +(assert (> (exp x) (exp y))) +(assert (> (exp y) (exp z))) +(assert (> (exp z) (exp w))) + + +(check-sat) diff --git a/test/regress/regress1/nl/metitarski-1025.smt2 b/test/regress/regress1/nl/metitarski-1025.smt2 new file mode 100644 index 000000000..5a95364f3 --- /dev/null +++ b/test/regress/regress1/nl/metitarski-1025.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoCOSS () Real) +(declare-fun skoSINS () Real) +(declare-fun skoS () Real) +(declare-fun pi () Real) +(assert (and (= (* skoSINS skoSINS) (+ 1 (* skoCOSS (* skoCOSS (- 1))))) (and (not (<= (* pi (/ 1 2)) skoS)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (<= 0 skoS) (and (<= 0 skoCOSS) (<= skoSINS skoS)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/metitarski-3-4.smt2 b/test/regress/regress1/nl/metitarski-3-4.smt2 new file mode 100644 index 000000000..835d60732 --- /dev/null +++ b/test/regress/regress1/nl/metitarski-3-4.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(declare-fun skoZ () Real) +(assert (let ((?v_0 (<= 0 skoY)) (?v_2 (<= (* skoZ (+ (- 1) (* skoY skoX))) (+ skoX skoY))) (?v_1 (* skoX (- 1)))) (let ((?v_3 (* skoX ?v_1))) (let ((?v_4 (* skoY (* skoX (+ (- 3) ?v_3))))) (and (<= (- 1) skoY) (and (not (= skoY 0)) (and (or (not ?v_2) ?v_0) (and (or ?v_0 (<= (* skoZ (+ 1 (* skoY ?v_1))) (+ (+ 1 ?v_1) (* skoY (+ (- 1) ?v_1))))) (and (or (not ?v_0) (or ?v_2 (<= (* skoZ (+ (+ 3 (* skoX skoX)) ?v_4)) (+ (* skoX ?v_3) (* skoY (+ (* skoX (* skoX (- 3))) ?v_4)))))) (and (not (<= skoZ 0)) (and (not (<= skoX (- 1))) (and (not (<= 1 skoY)) (not (<= skoY skoX)))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/metitarski_3_4_2e.smt2 b/test/regress/regress1/nl/metitarski_3_4_2e.smt2 new file mode 100644 index 000000000..3f12ec34b --- /dev/null +++ b/test/regress/regress1/nl/metitarski_3_4_2e.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoS () Real) +(declare-fun skoC () Real) +(assert (let ((?v_0 (<= skoX 0)) (?v_2 (* skoC (/ 86400000 2025130727)))) (let ((?v_1 (<= ?v_2 skoS))) (and (<= (* skoX (+ (/ (- 69) 2000) (* skoX (/ (- 529) 16000000)))) 12) (and (not ?v_0) (and (or (not (<= (* skoX (+ (+ (+ (/ (- 23) 13) (* skoC (/ 621 8125))) (* skoS (/ (- 46578006721) 26000000000))) (* skoX (+ (+ (/ (- 529) 312000) (* skoC (/ (- 4761) 65000000))) (* skoS (/ 1071294154583 624000000000000)))))) (+ (+ (/ 8000 13) (* skoC (/ 1728 65))) (* skoS (/ (- 2025130727) 3250000))))) ?v_0) (and ?v_1 (and (or (not ?v_1) (not (<= skoS ?v_2))) (and (= (* skoS skoS) (+ 1 (* skoC (* skoC (- 1))))) (and (<= skoX 75) (<= 0 skoX))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/nl-help-unsat-quant.smt2 b/test/regress/regress1/nl/nl-help-unsat-quant.smt2 new file mode 100644 index 000000000..f2f7667c8 --- /dev/null +++ b/test/regress/regress1/nl/nl-help-unsat-quant.smt2 @@ -0,0 +1,419 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic UFNIA) +(set-info :status unsat) +(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-sort S14 0) +(declare-sort S15 0) +(declare-sort S16 0) +(declare-sort S17 0) +(declare-sort S18 0) +(declare-sort S19 0) +(declare-sort S20 0) +(declare-sort S21 0) +(declare-sort S22 0) +(declare-sort S23 0) +(declare-sort S24 0) +(declare-sort S25 0) +(declare-sort S26 0) +(declare-sort S27 0) +(declare-sort S28 0) +(declare-sort S29 0) +(declare-sort S30 0) +(declare-sort S31 0) +(declare-sort S32 0) +(declare-sort S33 0) +(declare-sort S34 0) +(declare-sort S35 0) +(declare-sort S36 0) +(declare-sort S37 0) +(declare-sort S38 0) +(declare-sort S39 0) +(declare-sort S40 0) +(declare-sort S41 0) +(declare-sort S42 0) +(declare-sort S43 0) +(declare-sort S44 0) +(declare-sort S45 0) +(declare-sort S46 0) +(declare-sort S47 0) +(declare-sort S48 0) +(declare-sort S49 0) +(declare-sort S50 0) +(declare-sort S51 0) +(declare-sort S52 0) +(declare-sort S53 0) +(declare-sort S54 0) +(declare-sort S55 0) +(declare-sort S56 0) +(declare-sort S57 0) +(declare-sort S58 0) +(declare-sort S59 0) +(declare-sort S60 0) +(declare-sort S61 0) +(declare-sort S62 0) +(declare-sort S63 0) +(declare-sort S64 0) +(declare-sort S65 0) +(declare-sort S66 0) +(declare-sort S67 0) +(declare-sort S68 0) +(declare-sort S69 0) +(declare-sort S70 0) +(declare-sort S71 0) +(declare-sort S72 0) +(declare-sort S73 0) +(declare-sort S74 0) +(declare-sort S75 0) +(declare-sort S76 0) +(declare-sort S77 0) +(declare-sort S78 0) +(declare-sort S79 0) +(declare-sort S80 0) +(declare-sort S81 0) +(declare-sort S82 0) +(declare-sort S83 0) +(declare-sort S84 0) +(declare-sort S85 0) +(declare-sort S86 0) +(declare-sort S87 0) +(declare-sort S88 0) +(declare-sort S89 0) +(declare-sort S90 0) +(declare-sort S91 0) +(declare-sort S92 0) +(declare-sort S93 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (Int) S1) +(declare-fun f4 () Int) +(declare-fun f5 () Int) +(declare-fun f6 (S2 S3) Int) +(declare-fun f7 () S2) +(declare-fun f8 (S4 Int) S3) +(declare-fun f9 (S5 Int) S4) +(declare-fun f10 () S5) +(declare-fun f11 (S6 S3) S1) +(declare-fun f12 (S7 S8) S1) +(declare-fun f13 (S10 S9) S8) +(declare-fun f14 (S11 S9) S10) +(declare-fun f15 () S11) +(declare-fun f16 (S12 S13) S1) +(declare-fun f17 (S15 S14) S13) +(declare-fun f18 (S16 S14) S15) +(declare-fun f19 () S16) +(declare-fun f20 (S17 S14) S1) +(declare-fun f21 (S18 S3) S14) +(declare-fun f22 (S19 Int) S18) +(declare-fun f23 () S19) +(declare-fun f24 (S20 S21) S1) +(declare-fun f25 (S23 S22) S21) +(declare-fun f26 (S24 S22) S23) +(declare-fun f27 () S24) +(declare-fun f28 (S25 S22) S1) +(declare-fun f29 (S26 Int) S22) +(declare-fun f30 (S27 S3) S26) +(declare-fun f31 () S27) +(declare-fun f32 (S28 S9) S1) +(declare-fun f33 (S29 S3) S9) +(declare-fun f34 (S30 S3) S29) +(declare-fun f35 () S30) +(declare-fun f36 (S31 Int) S1) +(declare-fun f37 (S32 Int) S31) +(declare-fun f38 (S6) S32) +(declare-fun f39 (S3 S6) S1) +(declare-fun f40 (S33 S9) S28) +(declare-fun f41 (S7) S33) +(declare-fun f42 (S8 S7) S1) +(declare-fun f43 (S34 S14) S17) +(declare-fun f44 (S12) S34) +(declare-fun f45 (S13 S12) S1) +(declare-fun f46 (S35 S22) S25) +(declare-fun f47 (S20) S35) +(declare-fun f48 (S21 S20) S1) +(declare-fun f49 (S36 Int) S6) +(declare-fun f50 (S17) S36) +(declare-fun f51 (S14 S17) S1) +(declare-fun f52 (S37 S3) S31) +(declare-fun f53 (S25) S37) +(declare-fun f54 (S22 S25) S1) +(declare-fun f55 (S38 S3) S6) +(declare-fun f56 (S28) S38) +(declare-fun f57 (S9 S28) S1) +(declare-fun f58 (S39 S36) S28) +(declare-fun f59 (S31) S39) +(declare-fun f60 (S40 S38) S20) +(declare-fun f61 (S6) S40) +(declare-fun f62 (S41 S9) S7) +(declare-fun f63 (S42 S43) S1) +(declare-fun f64 (S8 S8) S42) +(declare-fun f65 (S44 S41) S43) +(declare-fun f66 (S28) S44) +(declare-fun f67 (S45 S14) S12) +(declare-fun f68 (S46 S47) S1) +(declare-fun f69 (S13 S13) S46) +(declare-fun f70 (S48 S45) S47) +(declare-fun f71 (S17) S48) +(declare-fun f72 (S49 S22) S20) +(declare-fun f73 (S50 S51) S1) +(declare-fun f74 (S21 S21) S50) +(declare-fun f75 (S52 S49) S51) +(declare-fun f76 (S25) S52) +(declare-fun f77 (S53 S3) S28) +(declare-fun f78 (S54 S53) S7) +(declare-fun f79 (S6) S54) +(declare-fun f80 (S55 Int) S28) +(declare-fun f81 (S56 S55) S12) +(declare-fun f82 (S31) S56) +(declare-fun f83 (S6) S1) +(declare-fun f84 (S7) S1) +(declare-fun f85 (S12) S1) +(declare-fun f86 (S20) S1) +(declare-fun f87 (S28) S1) +(declare-fun f88 (S6) S1) +(declare-fun f89 (S7) S1) +(declare-fun f90 (S12) S1) +(declare-fun f91 (S20) S1) +(declare-fun f92 (S28) S1) +(declare-fun f93 (S6) S32) +(declare-fun f94 (S7) S33) +(declare-fun f95 (S12) S34) +(declare-fun f96 (S17) S36) +(declare-fun f97 (S20) S35) +(declare-fun f98 (S25) S37) +(declare-fun f99 (S28) S38) +(declare-fun f100 (S57 S58) S1) +(declare-fun f101 (S59 S59) S57) +(declare-fun f102 (S9 Int) S59) +(declare-fun f103 (S7 S6) S58) +(declare-fun f104 (S60 S61) S1) +(declare-fun f105 (S62 S62) S60) +(declare-fun f106 (S14 Int) S62) +(declare-fun f107 (S12 S6) S61) +(declare-fun f108 (S63 S64) S1) +(declare-fun f109 (S65 S65) S63) +(declare-fun f110 (S22 Int) S65) +(declare-fun f111 (S20 S6) S64) +(declare-fun f112 (S66 S6) S20) +(declare-fun f113 (S28) S66) +(declare-fun f114 (S67 S68) S1) +(declare-fun f115 (S69 S69) S67) +(declare-fun f116 (Int S9) S69) +(declare-fun f117 (S6 S7) S68) +(declare-fun f118 (S70 S71) S1) +(declare-fun f119 (S72 S72) S70) +(declare-fun f120 (Int S14) S72) +(declare-fun f121 (S6 S12) S71) +(declare-fun f122 (S73 S74) S1) +(declare-fun f123 (S75 S75) S73) +(declare-fun f124 (Int S22) S75) +(declare-fun f125 (S6 S20) S74) +(declare-fun f126 (S76 S28) S12) +(declare-fun f127 (S6) S76) +(declare-fun f128 (S77 S6) S28) +(declare-fun f129 (S6) S77) +(declare-fun f130 (S78 S7) S43) +(declare-fun f131 (S7) S78) +(declare-fun f132 (S79 S12) S47) +(declare-fun f133 (S12) S79) +(declare-fun f134 (S80 S20) S51) +(declare-fun f135 (S20) S80) +(declare-fun f136 (S81 S28) S7) +(declare-fun f137 (S28) S81) +(declare-fun f138 (S82) S6) +(declare-fun f139 (S83 S84) Int) +(declare-fun f140 () S83) +(declare-fun f141 (S82 Int) S84) +(declare-fun f142 (S85) S7) +(declare-fun f143 (S85 S9) S84) +(declare-fun f144 (S86) S12) +(declare-fun f145 (S86 S14) S84) +(declare-fun f146 (S87) S20) +(declare-fun f147 (S87 S22) S84) +(declare-fun f148 (S88) S28) +(declare-fun f149 (S88 S3) S84) +(declare-fun f150 (S89 S6) S6) +(declare-fun f151 (S82) S89) +(declare-fun f152 (S90 S7) S7) +(declare-fun f153 (S85) S90) +(declare-fun f154 (S91 S12) S12) +(declare-fun f155 (S86) S91) +(declare-fun f156 (S92 S20) S20) +(declare-fun f157 (S87) S92) +(declare-fun f158 (S93 S28) S28) +(declare-fun f159 (S88) S93) +(declare-fun f160 (S31 S6) S1) +(declare-fun f161 (Int S31) S1) +(declare-fun f162 (S17 S12) S1) +(declare-fun f163 (S25 S20) S1) +(declare-fun f164 (S7 S43) S1) +(declare-fun f165 (S12 S47) S1) +(declare-fun f166 (S20 S51) S1) +(declare-fun f167 (S28 S7) S1) +(declare-fun f168 (S6 S28) S1) +(declare-fun f169 () S82) +(assert (not (= f1 f2))) +(assert (not (= (f3 (* f4 f5)) f1))) +(assert (= (f3 f4) f1)) +(assert (= (f3 f5) f1)) +(assert (forall ((?v0 Int)) (= (= (f3 ?v0) f1) (exists ((?v1 Int) (?v2 Int)) (= (f6 f7 (f8 (f9 f10 ?v1) ?v2)) ?v0))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (* (f6 f7 (f8 (f9 f10 ?v0) ?v1)) (f6 f7 (f8 (f9 f10 ?v2) ?v3))) (f6 f7 (f8 (f9 f10 (+ (* ?v0 ?v2) (* ?v1 ?v3))) (- (* ?v0 ?v3) (* ?v1 ?v2))))))) +(assert (forall ((?v0 S6)) (= (forall ((?v1 S3)) (= (f11 ?v0 ?v1) f1)) (forall ((?v1 Int) (?v2 Int)) (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S7)) (= (forall ((?v1 S8)) (= (f12 ?v0 ?v1) f1)) (forall ((?v1 S9) (?v2 S9)) (= (f12 ?v0 (f13 (f14 f15 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S12)) (= (forall ((?v1 S13)) (= (f16 ?v0 ?v1) f1)) (forall ((?v1 S14) (?v2 S14)) (= (f16 ?v0 (f17 (f18 f19 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S17)) (= (forall ((?v1 S14)) (= (f20 ?v0 ?v1) f1)) (forall ((?v1 Int) (?v2 S3)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S20)) (= (forall ((?v1 S21)) (= (f24 ?v0 ?v1) f1)) (forall ((?v1 S22) (?v2 S22)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S25)) (= (forall ((?v1 S22)) (= (f28 ?v0 ?v1) f1)) (forall ((?v1 S3) (?v2 Int)) (= (f28 ?v0 (f29 (f30 f31 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S28)) (= (forall ((?v1 S9)) (= (f32 ?v0 ?v1) f1)) (forall ((?v1 S3) (?v2 S3)) (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S9) (?v1 S9) (?v2 S9) (?v3 S9)) (= (= (f13 (f14 f15 ?v0) ?v1) (f13 (f14 f15 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S14) (?v1 S14) (?v2 S14) (?v3 S14)) (= (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 Int) (?v3 S3)) (= (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S22) (?v3 S22)) (= (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S3) (?v1 Int) (?v2 S3) (?v3 Int)) (= (= (f29 (f30 f31 ?v0) ?v1) (f29 (f30 f31 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (= (= (f33 (f34 f35 ?v0) ?v1) (f33 (f34 f35 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (=> (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S9) (?v1 S9) (?v2 S9) (?v3 S9)) (=> (= (f13 (f14 f15 ?v0) ?v1) (f13 (f14 f15 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S14) (?v1 S14) (?v2 S14) (?v3 S14)) (=> (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 Int) (?v3 S3)) (=> (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S22) (?v3 S22)) (=> (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S3) (?v1 Int) (?v2 S3) (?v3 Int)) (=> (= (f29 (f30 f31 ?v0) ?v1) (f29 (f30 f31 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (=> (= (f33 (f34 f35 ?v0) ?v1) (f33 (f34 f35 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S6) (?v1 Int) (?v2 Int)) (= (= (f36 (f37 (f38 ?v0) ?v1) ?v2) f1) (= (f39 (f8 (f9 f10 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S7) (?v1 S9) (?v2 S9)) (= (= (f32 (f40 (f41 ?v0) ?v1) ?v2) f1) (= (f42 (f13 (f14 f15 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S12) (?v1 S14) (?v2 S14)) (= (= (f20 (f43 (f44 ?v0) ?v1) ?v2) f1) (= (f45 (f17 (f18 f19 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S20) (?v1 S22) (?v2 S22)) (= (= (f28 (f46 (f47 ?v0) ?v1) ?v2) f1) (= (f48 (f25 (f26 f27 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S17) (?v1 Int) (?v2 S3)) (= (= (f11 (f49 (f50 ?v0) ?v1) ?v2) f1) (= (f51 (f21 (f22 f23 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 Int)) (= (= (f36 (f52 (f53 ?v0) ?v1) ?v2) f1) (= (f54 (f29 (f30 f31 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S28) (?v1 S3) (?v2 S3)) (= (= (f11 (f55 (f56 ?v0) ?v1) ?v2) f1) (= (f57 (f33 (f34 f35 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S31) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S36)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f36 ?v0 ?v1) f1) (=> (= (f39 (f8 (f9 f10 ?v2) ?v3) (f49 ?v4 ?v1)) f1) (= (f57 (f33 (f34 f35 (f8 ?v_0 ?v2)) (f8 ?v_0 ?v3)) (f58 (f59 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S6) (?v1 S3) (?v2 Int) (?v3 Int) (?v4 S38)) (let ((?v_0 (f30 f31 ?v1))) (=> (= (f11 ?v0 ?v1) f1) (=> (= (f39 (f8 (f9 f10 ?v2) ?v3) (f55 ?v4 ?v1)) f1) (= (f48 (f25 (f26 f27 (f29 ?v_0 ?v2)) (f29 ?v_0 ?v3)) (f60 (f61 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S28) (?v1 S9) (?v2 S9) (?v3 S9) (?v4 S41)) (let ((?v_0 (f14 f15 ?v1))) (=> (= (f32 ?v0 ?v1) f1) (=> (= (f42 (f13 (f14 f15 ?v2) ?v3) (f62 ?v4 ?v1)) f1) (= (f63 (f64 (f13 ?v_0 ?v2) (f13 ?v_0 ?v3)) (f65 (f66 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S17) (?v1 S14) (?v2 S14) (?v3 S14) (?v4 S45)) (let ((?v_0 (f18 f19 ?v1))) (=> (= (f20 ?v0 ?v1) f1) (=> (= (f45 (f17 (f18 f19 ?v2) ?v3) (f67 ?v4 ?v1)) f1) (= (f68 (f69 (f17 ?v_0 ?v2) (f17 ?v_0 ?v3)) (f70 (f71 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S25) (?v1 S22) (?v2 S22) (?v3 S22) (?v4 S49)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f28 ?v0 ?v1) f1) (=> (= (f48 (f25 (f26 f27 ?v2) ?v3) (f72 ?v4 ?v1)) f1) (= (f73 (f74 (f25 ?v_0 ?v2) (f25 ?v_0 ?v3)) (f75 (f76 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S6) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S53)) (let ((?v_0 (f34 f35 ?v1))) (=> (= (f11 ?v0 ?v1) f1) (=> (= (f57 (f33 (f34 f35 ?v2) ?v3) (f77 ?v4 ?v1)) f1) (= (f42 (f13 (f14 f15 (f33 ?v_0 ?v2)) (f33 ?v_0 ?v3)) (f78 (f79 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S31) (?v1 Int) (?v2 S3) (?v3 S3) (?v4 S55)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f36 ?v0 ?v1) f1) (=> (= (f57 (f33 (f34 f35 ?v2) ?v3) (f80 ?v4 ?v1)) f1) (= (f45 (f17 (f18 f19 (f21 ?v_0 ?v2)) (f21 ?v_0 ?v3)) (f81 (f82 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S6)) (= (= (f83 ?v0) f1) (forall ((?v1 Int)) (= (f39 (f8 (f9 f10 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S7)) (= (= (f84 ?v0) f1) (forall ((?v1 S9)) (= (f42 (f13 (f14 f15 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S12)) (= (= (f85 ?v0) f1) (forall ((?v1 S14)) (= (f45 (f17 (f18 f19 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S20)) (= (= (f86 ?v0) f1) (forall ((?v1 S22)) (= (f48 (f25 (f26 f27 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S28)) (= (= (f87 ?v0) f1) (forall ((?v1 S3)) (= (f57 (f33 (f34 f35 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S6)) (= (= (f88 ?v0) f1) (forall ((?v1 Int)) (not (= (f39 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S7)) (= (= (f89 ?v0) f1) (forall ((?v1 S9)) (not (= (f42 (f13 (f14 f15 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S12)) (= (= (f90 ?v0) f1) (forall ((?v1 S14)) (not (= (f45 (f17 (f18 f19 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S20)) (= (= (f91 ?v0) f1) (forall ((?v1 S22)) (not (= (f48 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S28)) (= (= (f92 ?v0) f1) (forall ((?v1 S3)) (not (= (f57 (f33 (f34 f35 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S6)) (= (exists ((?v1 S3)) (= (f11 ?v0 ?v1) f1)) (exists ((?v1 Int) (?v2 Int)) (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S7)) (= (exists ((?v1 S8)) (= (f12 ?v0 ?v1) f1)) (exists ((?v1 S9) (?v2 S9)) (= (f12 ?v0 (f13 (f14 f15 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S12)) (= (exists ((?v1 S13)) (= (f16 ?v0 ?v1) f1)) (exists ((?v1 S14) (?v2 S14)) (= (f16 ?v0 (f17 (f18 f19 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S17)) (= (exists ((?v1 S14)) (= (f20 ?v0 ?v1) f1)) (exists ((?v1 Int) (?v2 S3)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S20)) (= (exists ((?v1 S21)) (= (f24 ?v0 ?v1) f1)) (exists ((?v1 S22) (?v2 S22)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S25)) (= (exists ((?v1 S22)) (= (f28 ?v0 ?v1) f1)) (exists ((?v1 S3) (?v2 Int)) (= (f28 ?v0 (f29 (f30 f31 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S28)) (= (exists ((?v1 S9)) (= (f32 ?v0 ?v1) f1)) (exists ((?v1 S3) (?v2 S3)) (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S9) (?v2 S3) (?v3 Int) (?v4 Int)) (=> (= ?v0 (f13 (f14 f15 ?v1) (f33 (f34 f35 ?v2) (f8 (f9 f10 ?v3) ?v4)))) false)) false))) +(assert (forall ((?v0 S13)) (=> (forall ((?v1 S14) (?v2 Int) (?v3 Int) (?v4 Int)) (=> (= ?v0 (f17 (f18 f19 ?v1) (f21 (f22 f23 ?v2) (f8 (f9 f10 ?v3) ?v4)))) false)) false))) +(assert (forall ((?v0 S7) (?v1 S8)) (=> (forall ((?v2 S9) (?v3 S3) (?v4 Int) (?v5 Int)) (= (f12 ?v0 (f13 (f14 f15 ?v2) (f33 (f34 f35 ?v3) (f8 (f9 f10 ?v4) ?v5)))) f1)) (= (f12 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S12) (?v1 S13)) (=> (forall ((?v2 S14) (?v3 Int) (?v4 Int) (?v5 Int)) (= (f16 ?v0 (f17 (f18 f19 ?v2) (f21 (f22 f23 ?v3) (f8 (f9 f10 ?v4) ?v5)))) f1)) (= (f16 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S9)) (=> (forall ((?v1 S3) (?v2 Int) (?v3 Int)) (=> (= ?v0 (f33 (f34 f35 ?v1) (f8 (f9 f10 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S13)) (=> (forall ((?v1 S14) (?v2 Int) (?v3 S3)) (=> (= ?v0 (f17 (f18 f19 ?v1) (f21 (f22 f23 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S14)) (=> (forall ((?v1 Int) (?v2 Int) (?v3 Int)) (=> (= ?v0 (f21 (f22 f23 ?v1) (f8 (f9 f10 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S22) (?v2 S3) (?v3 Int)) (=> (= ?v0 (f25 (f26 f27 ?v1) (f29 (f30 f31 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S9) (?v2 S3) (?v3 S3)) (=> (= ?v0 (f13 (f14 f15 ?v1) (f33 (f34 f35 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S28) (?v1 S9)) (=> (forall ((?v2 S3) (?v3 Int) (?v4 Int)) (= (f32 ?v0 (f33 (f34 f35 ?v2) (f8 (f9 f10 ?v3) ?v4))) f1)) (= (f32 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S12) (?v1 S13)) (=> (forall ((?v2 S14) (?v3 Int) (?v4 S3)) (= (f16 ?v0 (f17 (f18 f19 ?v2) (f21 (f22 f23 ?v3) ?v4))) f1)) (= (f16 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S17) (?v1 S14)) (=> (forall ((?v2 Int) (?v3 Int) (?v4 Int)) (= (f20 ?v0 (f21 (f22 f23 ?v2) (f8 (f9 f10 ?v3) ?v4))) f1)) (= (f20 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S20) (?v1 S21)) (=> (forall ((?v2 S22) (?v3 S3) (?v4 Int)) (= (f24 ?v0 (f25 (f26 f27 ?v2) (f29 (f30 f31 ?v3) ?v4))) f1)) (= (f24 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S7) (?v1 S8)) (=> (forall ((?v2 S9) (?v3 S3) (?v4 S3)) (= (f12 ?v0 (f13 (f14 f15 ?v2) (f33 (f34 f35 ?v3) ?v4))) f1)) (= (f12 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S9) (?v2 S9)) (=> (= ?v0 (f13 (f14 f15 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S13)) (=> (forall ((?v1 S14) (?v2 S14)) (=> (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S14)) (=> (forall ((?v1 Int) (?v2 S3)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S22) (?v2 S22)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S22)) (=> (forall ((?v1 S3) (?v2 Int)) (=> (= ?v0 (f29 (f30 f31 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S9)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f33 (f34 f35 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S9) (?v2 S9)) (=> (= ?v0 (f13 (f14 f15 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S13)) (=> (forall ((?v1 S14) (?v2 S14)) (=> (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S14)) (=> (forall ((?v1 Int) (?v2 S3)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S22) (?v2 S22)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S22)) (=> (forall ((?v1 S3) (?v2 Int)) (=> (= ?v0 (f29 (f30 f31 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S9)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f33 (f34 f35 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S6) (?v1 Int) (?v2 Int)) (=> (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) (= (f36 (f37 (f93 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S7) (?v1 S9) (?v2 S9)) (=> (= (f12 ?v0 (f13 (f14 f15 ?v1) ?v2)) f1) (= (f32 (f40 (f94 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S12) (?v1 S14) (?v2 S14)) (=> (= (f16 ?v0 (f17 (f18 f19 ?v1) ?v2)) f1) (= (f20 (f43 (f95 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S17) (?v1 Int) (?v2 S3)) (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) (= (f11 (f49 (f96 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S20) (?v1 S22) (?v2 S22)) (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) (= (f28 (f46 (f97 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 Int)) (=> (= (f28 ?v0 (f29 (f30 f31 ?v1) ?v2)) f1) (= (f36 (f52 (f98 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S28) (?v1 S3) (?v2 S3)) (=> (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1) (= (f11 (f55 (f99 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S9) (?v1 Int) (?v2 S9) (?v3 Int) (?v4 S7) (?v5 S6)) (= (= (f100 (f101 (f102 ?v0 ?v1) (f102 ?v2 ?v3)) (f103 ?v4 ?v5)) f1) (or (= (f42 (f13 (f14 f15 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f39 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S14) (?v1 Int) (?v2 S14) (?v3 Int) (?v4 S12) (?v5 S6)) (= (= (f104 (f105 (f106 ?v0 ?v1) (f106 ?v2 ?v3)) (f107 ?v4 ?v5)) f1) (or (= (f45 (f17 (f18 f19 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f39 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S22) (?v1 Int) (?v2 S22) (?v3 Int) (?v4 S20) (?v5 S6)) (= (= (f108 (f109 (f110 ?v0 ?v1) (f110 ?v2 ?v3)) (f111 ?v4 ?v5)) f1) (or (= (f48 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f39 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S3) (?v1 Int) (?v2 S3) (?v3 Int) (?v4 S28) (?v5 S6)) (= (= (f48 (f25 (f26 f27 (f29 (f30 f31 ?v0) ?v1)) (f29 (f30 f31 ?v2) ?v3)) (f112 (f113 ?v4) ?v5)) f1) (or (= (f57 (f33 (f34 f35 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f39 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S9) (?v2 Int) (?v3 S9) (?v4 S6) (?v5 S7)) (= (= (f114 (f115 (f116 ?v0 ?v1) (f116 ?v2 ?v3)) (f117 ?v4 ?v5)) f1) (or (= (f39 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f42 (f13 (f14 f15 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S14) (?v2 Int) (?v3 S14) (?v4 S6) (?v5 S12)) (= (= (f118 (f119 (f120 ?v0 ?v1) (f120 ?v2 ?v3)) (f121 ?v4 ?v5)) f1) (or (= (f39 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f45 (f17 (f18 f19 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S22) (?v2 Int) (?v3 S22) (?v4 S6) (?v5 S20)) (= (= (f122 (f123 (f124 ?v0 ?v1) (f124 ?v2 ?v3)) (f125 ?v4 ?v5)) f1) (or (= (f39 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f48 (f25 (f26 f27 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 Int) (?v3 S3) (?v4 S6) (?v5 S28)) (= (= (f45 (f17 (f18 f19 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f126 (f127 ?v4) ?v5)) f1) (or (= (f39 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f57 (f33 (f34 f35 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S6) (?v5 S6)) (let ((?v_0 (f9 f10 ?v0))) (= (= (f57 (f33 (f34 f35 (f8 ?v_0 ?v1)) (f8 (f9 f10 ?v2) ?v3)) (f128 (f129 ?v4) ?v5)) f1) (or (= (f39 (f8 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f39 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S9) (?v1 S9) (?v2 S9) (?v3 S9) (?v4 S7) (?v5 S7)) (let ((?v_0 (f14 f15 ?v0))) (= (= (f63 (f64 (f13 ?v_0 ?v1) (f13 (f14 f15 ?v2) ?v3)) (f130 (f131 ?v4) ?v5)) f1) (or (= (f42 (f13 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f42 (f13 (f14 f15 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S14) (?v1 S14) (?v2 S14) (?v3 S14) (?v4 S12) (?v5 S12)) (let ((?v_0 (f18 f19 ?v0))) (= (= (f68 (f69 (f17 ?v_0 ?v1) (f17 (f18 f19 ?v2) ?v3)) (f132 (f133 ?v4) ?v5)) f1) (or (= (f45 (f17 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f45 (f17 (f18 f19 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S22) (?v3 S22) (?v4 S20) (?v5 S20)) (let ((?v_0 (f26 f27 ?v0))) (= (= (f73 (f74 (f25 ?v_0 ?v1) (f25 (f26 f27 ?v2) ?v3)) (f134 (f135 ?v4) ?v5)) f1) (or (= (f48 (f25 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f48 (f25 (f26 f27 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S28) (?v5 S28)) (let ((?v_0 (f34 f35 ?v0))) (= (= (f42 (f13 (f14 f15 (f33 ?v_0 ?v1)) (f33 (f34 f35 ?v2) ?v3)) (f136 (f137 ?v4) ?v5)) f1) (or (= (f57 (f33 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f57 (f33 (f34 f35 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S6) (?v1 Int) (?v2 Int)) (= (= (f36 (f37 (f93 ?v0) ?v1) ?v2) f1) (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S28) (?v1 S3) (?v2 S3)) (= (= (f11 (f55 (f99 ?v0) ?v1) ?v2) f1) (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S6) (?v1 Int) (?v2 Int)) (=> (= (f36 (f37 (f93 ?v0) ?v1) ?v2) f1) (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S7) (?v1 S9) (?v2 S9)) (=> (= (f32 (f40 (f94 ?v0) ?v1) ?v2) f1) (= (f12 ?v0 (f13 (f14 f15 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S12) (?v1 S14) (?v2 S14)) (=> (= (f20 (f43 (f95 ?v0) ?v1) ?v2) f1) (= (f16 ?v0 (f17 (f18 f19 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S17) (?v1 Int) (?v2 S3)) (=> (= (f11 (f49 (f96 ?v0) ?v1) ?v2) f1) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S20) (?v1 S22) (?v2 S22)) (=> (= (f28 (f46 (f97 ?v0) ?v1) ?v2) f1) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 Int)) (=> (= (f36 (f52 (f98 ?v0) ?v1) ?v2) f1) (= (f28 ?v0 (f29 (f30 f31 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S28) (?v1 S3) (?v2 S3)) (=> (= (f11 (f55 (f99 ?v0) ?v1) ?v2) f1) (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S6) (?v1 Int) (?v2 Int)) (=> (= (f36 (f37 (f93 ?v0) ?v1) ?v2) f1) (=> (=> (= (f11 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S7) (?v1 S9) (?v2 S9)) (=> (= (f32 (f40 (f94 ?v0) ?v1) ?v2) f1) (=> (=> (= (f12 ?v0 (f13 (f14 f15 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S12) (?v1 S14) (?v2 S14)) (=> (= (f20 (f43 (f95 ?v0) ?v1) ?v2) f1) (=> (=> (= (f16 ?v0 (f17 (f18 f19 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S17) (?v1 Int) (?v2 S3)) (=> (= (f11 (f49 (f96 ?v0) ?v1) ?v2) f1) (=> (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S20) (?v1 S22) (?v2 S22)) (=> (= (f28 (f46 (f97 ?v0) ?v1) ?v2) f1) (=> (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 Int)) (=> (= (f36 (f52 (f98 ?v0) ?v1) ?v2) f1) (=> (=> (= (f28 ?v0 (f29 (f30 f31 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S28) (?v1 S3) (?v2 S3)) (=> (= (f11 (f55 (f99 ?v0) ?v1) ?v2) f1) (=> (=> (= (f32 ?v0 (f33 (f34 f35 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S82)) (= (= (f39 (f8 (f9 f10 ?v0) ?v1) (f138 ?v2)) f1) (< (f139 f140 (f141 ?v2 ?v0)) (f139 f140 (f141 ?v2 ?v1)))))) +(assert (forall ((?v0 S9) (?v1 S9) (?v2 S85)) (= (= (f42 (f13 (f14 f15 ?v0) ?v1) (f142 ?v2)) f1) (< (f139 f140 (f143 ?v2 ?v0)) (f139 f140 (f143 ?v2 ?v1)))))) +(assert (forall ((?v0 S14) (?v1 S14) (?v2 S86)) (= (= (f45 (f17 (f18 f19 ?v0) ?v1) (f144 ?v2)) f1) (< (f139 f140 (f145 ?v2 ?v0)) (f139 f140 (f145 ?v2 ?v1)))))) +(assert (forall ((?v0 S22) (?v1 S22) (?v2 S87)) (= (= (f48 (f25 (f26 f27 ?v0) ?v1) (f146 ?v2)) f1) (< (f139 f140 (f147 ?v2 ?v0)) (f139 f140 (f147 ?v2 ?v1)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S88)) (= (= (f57 (f33 (f34 f35 ?v0) ?v1) (f148 ?v2)) f1) (< (f139 f140 (f149 ?v2 ?v0)) (f139 f140 (f149 ?v2 ?v1)))))) +(assert (forall ((?v0 S82) (?v1 Int) (?v2 Int) (?v3 S6)) (=> (< (f139 f140 (f141 ?v0 ?v1)) (f139 f140 (f141 ?v0 ?v2))) (= (f39 (f8 (f9 f10 ?v1) ?v2) (f150 (f151 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S85) (?v1 S9) (?v2 S9) (?v3 S7)) (=> (< (f139 f140 (f143 ?v0 ?v1)) (f139 f140 (f143 ?v0 ?v2))) (= (f42 (f13 (f14 f15 ?v1) ?v2) (f152 (f153 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S86) (?v1 S14) (?v2 S14) (?v3 S12)) (=> (< (f139 f140 (f145 ?v0 ?v1)) (f139 f140 (f145 ?v0 ?v2))) (= (f45 (f17 (f18 f19 ?v1) ?v2) (f154 (f155 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S87) (?v1 S22) (?v2 S22) (?v3 S20)) (=> (< (f139 f140 (f147 ?v0 ?v1)) (f139 f140 (f147 ?v0 ?v2))) (= (f48 (f25 (f26 f27 ?v1) ?v2) (f156 (f157 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S88) (?v1 S3) (?v2 S3) (?v3 S28)) (=> (< (f139 f140 (f149 ?v0 ?v1)) (f139 f140 (f149 ?v0 ?v2))) (= (f57 (f33 (f34 f35 ?v1) ?v2) (f158 (f159 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S82) (?v1 Int) (?v2 Int) (?v3 S6)) (let ((?v_0 (f8 (f9 f10 ?v1) ?v2))) (=> (<= (f139 f140 (f141 ?v0 ?v1)) (f139 f140 (f141 ?v0 ?v2))) (=> (= (f39 ?v_0 ?v3) f1) (= (f39 ?v_0 (f150 (f151 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S85) (?v1 S9) (?v2 S9) (?v3 S7)) (let ((?v_0 (f13 (f14 f15 ?v1) ?v2))) (=> (<= (f139 f140 (f143 ?v0 ?v1)) (f139 f140 (f143 ?v0 ?v2))) (=> (= (f42 ?v_0 ?v3) f1) (= (f42 ?v_0 (f152 (f153 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S86) (?v1 S14) (?v2 S14) (?v3 S12)) (let ((?v_0 (f17 (f18 f19 ?v1) ?v2))) (=> (<= (f139 f140 (f145 ?v0 ?v1)) (f139 f140 (f145 ?v0 ?v2))) (=> (= (f45 ?v_0 ?v3) f1) (= (f45 ?v_0 (f154 (f155 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S87) (?v1 S22) (?v2 S22) (?v3 S20)) (let ((?v_0 (f25 (f26 f27 ?v1) ?v2))) (=> (<= (f139 f140 (f147 ?v0 ?v1)) (f139 f140 (f147 ?v0 ?v2))) (=> (= (f48 ?v_0 ?v3) f1) (= (f48 ?v_0 (f156 (f157 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S88) (?v1 S3) (?v2 S3) (?v3 S28)) (let ((?v_0 (f33 (f34 f35 ?v1) ?v2))) (=> (<= (f139 f140 (f149 ?v0 ?v1)) (f139 f140 (f149 ?v0 ?v2))) (=> (= (f57 ?v_0 ?v3) f1) (= (f57 ?v_0 (f158 (f159 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S31) (?v1 S6)) (= (= (f160 ?v0 ?v1) f1) (forall ((?v2 Int)) (=> (= (f161 ?v2 ?v0) f1) (forall ((?v3 Int)) (=> (= (f161 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f39 (f8 (f9 f10 ?v2) ?v3) ?v1) f1) (= (f39 (f8 (f9 f10 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S17) (?v1 S12)) (= (= (f162 ?v0 ?v1) f1) (forall ((?v2 S14)) (=> (= (f51 ?v2 ?v0) f1) (forall ((?v3 S14)) (=> (= (f51 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f45 (f17 (f18 f19 ?v2) ?v3) ?v1) f1) (= (f45 (f17 (f18 f19 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S25) (?v1 S20)) (= (= (f163 ?v0 ?v1) f1) (forall ((?v2 S22)) (=> (= (f54 ?v2 ?v0) f1) (forall ((?v3 S22)) (=> (= (f54 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f48 (f25 (f26 f27 ?v2) ?v3) ?v1) f1) (= (f48 (f25 (f26 f27 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S7) (?v1 S43)) (= (= (f164 ?v0 ?v1) f1) (forall ((?v2 S8)) (=> (= (f42 ?v2 ?v0) f1) (forall ((?v3 S8)) (=> (= (f42 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f63 (f64 ?v2 ?v3) ?v1) f1) (= (f63 (f64 ?v3 ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S12) (?v1 S47)) (= (= (f165 ?v0 ?v1) f1) (forall ((?v2 S13)) (=> (= (f45 ?v2 ?v0) f1) (forall ((?v3 S13)) (=> (= (f45 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f68 (f69 ?v2 ?v3) ?v1) f1) (= (f68 (f69 ?v3 ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S20) (?v1 S51)) (= (= (f166 ?v0 ?v1) f1) (forall ((?v2 S21)) (=> (= (f48 ?v2 ?v0) f1) (forall ((?v3 S21)) (=> (= (f48 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f73 (f74 ?v2 ?v3) ?v1) f1) (= (f73 (f74 ?v3 ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S28) (?v1 S7)) (= (= (f167 ?v0 ?v1) f1) (forall ((?v2 S9)) (=> (= (f57 ?v2 ?v0) f1) (forall ((?v3 S9)) (=> (= (f57 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f42 (f13 (f14 f15 ?v2) ?v3) ?v1) f1) (= (f42 (f13 (f14 f15 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S6) (?v1 S28)) (= (= (f168 ?v0 ?v1) f1) (forall ((?v2 S3)) (=> (= (f39 ?v2 ?v0) f1) (forall ((?v3 S3)) (=> (= (f39 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f57 (f33 (f34 f35 ?v2) ?v3) ?v1) f1) (= (f57 (f33 (f34 f35 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S84)) (= (f141 f169 (f139 f140 ?v0)) ?v0))) +(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f139 f140 (f141 f169 ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f139 f140 (f141 f169 ?v0)) 0)))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/nl-unk-quant.smt2 b/test/regress/regress1/nl/nl-unk-quant.smt2 new file mode 100644 index 000000000..bb5cd43df --- /dev/null +++ b/test/regress/regress1/nl/nl-unk-quant.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic UFNIA) +(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 () S2) +(declare-fun f4 (S3 Int) S2) +(declare-fun f5 () S3) +(declare-fun f6 (S4 S2) Int) +(declare-fun f7 () S4) +(declare-fun f8 () Int) +(declare-fun f9 (Int) S1) +(declare-fun f10 () Int) +(declare-fun f11 () S2) +(assert (not (= f1 f2))) +(assert (let ((?v_0 (f6 f7 f3)) (?v_1 (f6 f7 f11))) (not (=> (and (= f3 (f4 f5 (- (f6 f7 (f4 f5 f8)) 1))) (= (f9 (* (+ (* 4 f10) 1) (+ 1 ?v_0))) f1)) (=> (< f8 (+ 1 ?v_1)) (=> (< 0 f8) (< ?v_0 ?v_1))))))) +(assert (forall ((?v0 S2)) (= (f4 f5 (f6 f7 ?v0)) ?v0))) +(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f6 f7 (f4 f5 ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f6 f7 (f4 f5 ?v0)) 0)))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/ones.smt2 b/test/regress/regress1/nl/ones.smt2 new file mode 100644 index 000000000..be06912d0 --- /dev/null +++ b/test/regress/regress1/nl/ones.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) + +(assert (>= a 1)) +(assert (>= b 1)) +(assert (>= c 1)) +(assert (>= d 1)) +(assert (or (= a 1) (= b 1) (= c 1) (= d 1))) + +(assert (< (* a b c d) 1)) + +(check-sat) diff --git a/test/regress/regress1/nl/poly-1025.smt2 b/test/regress/regress1/nl/poly-1025.smt2 new file mode 100644 index 000000000..482696532 --- /dev/null +++ b/test/regress/regress1/nl/poly-1025.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :source | +These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The meti-tarski benchmarks are proof obligations extracted from the +Meti-Tarski project, see: + + B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover + for real-valued special functions. Journal of Automated Reasoning, + 44(3):175-205, 2010. + +Submitted by Dejan Jovanovic for SMT-LIB. + + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(declare-fun skoZ () Real) +(assert (let ((?v_2 (not (<= skoZ 1)))) (let ((?v_3 (or (not (<= skoY 1)) ?v_2)) (?v_4 (not (<= skoX 1))) (?v_0 (* skoX (/ 1 4))) (?v_1 (* skoX (/ (- 5) 4))) (?v_5 (* skoX (/ 1 2))) (?v_6 (+ (/ (- 1) 4) (* skoX (/ (- 1) 4))))) (and (not (<= skoX 0)) (and (or (not (<= (* skoZ (* skoY (* skoY (+ (* skoX (* skoX (+ (/ (- 15) 4) ?v_0))) (* skoY (* skoX (* skoX (+ (/ 1 4) ?v_0)))))))) (* skoY (+ (* skoX (+ (/ 11 4) ?v_1)) (* skoY (* skoX (+ (/ (- 5) 4) ?v_1))))))) ?v_2) (and ?v_3 (and (or ?v_4 ?v_3) (and (<= skoZ 2) (and (<= skoY 2) (and (<= skoX 2) (and (<= 1 skoZ) (and (<= 1 skoY) (and (<= 1 skoX) (and (or ?v_4 ?v_2) (or (not (<= (* skoZ (* skoY (+ (* skoX (+ (/ (- 7) 2) ?v_5)) (* skoY (* skoX (+ (/ 1 2) ?v_5)))))) (+ ?v_6 (* skoY ?v_6)))) ?v_2))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/quant-nl.smt2 b/test/regress/regress1/nl/quant-nl.smt2 new file mode 100644 index 000000000..7d251ab7d --- /dev/null +++ b/test/regress/regress1/nl/quant-nl.smt2 @@ -0,0 +1,857 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic UFNIA) +(set-info :status unsat) +(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-sort S14 0) +(declare-sort S15 0) +(declare-sort S16 0) +(declare-sort S17 0) +(declare-sort S18 0) +(declare-sort S19 0) +(declare-sort S20 0) +(declare-sort S21 0) +(declare-sort S22 0) +(declare-sort S23 0) +(declare-sort S24 0) +(declare-sort S25 0) +(declare-sort S26 0) +(declare-sort S27 0) +(declare-sort S28 0) +(declare-sort S29 0) +(declare-sort S30 0) +(declare-sort S31 0) +(declare-sort S32 0) +(declare-sort S33 0) +(declare-sort S34 0) +(declare-sort S35 0) +(declare-sort S36 0) +(declare-sort S37 0) +(declare-sort S38 0) +(declare-sort S39 0) +(declare-sort S40 0) +(declare-sort S41 0) +(declare-sort S42 0) +(declare-sort S43 0) +(declare-sort S44 0) +(declare-sort S45 0) +(declare-sort S46 0) +(declare-sort S47 0) +(declare-sort S48 0) +(declare-sort S49 0) +(declare-sort S50 0) +(declare-sort S51 0) +(declare-sort S52 0) +(declare-sort S53 0) +(declare-sort S54 0) +(declare-sort S55 0) +(declare-sort S56 0) +(declare-sort S57 0) +(declare-sort S58 0) +(declare-sort S59 0) +(declare-sort S60 0) +(declare-sort S61 0) +(declare-sort S62 0) +(declare-sort S63 0) +(declare-sort S64 0) +(declare-sort S65 0) +(declare-sort S66 0) +(declare-sort S67 0) +(declare-sort S68 0) +(declare-sort S69 0) +(declare-sort S70 0) +(declare-sort S71 0) +(declare-sort S72 0) +(declare-sort S73 0) +(declare-sort S74 0) +(declare-sort S75 0) +(declare-sort S76 0) +(declare-sort S77 0) +(declare-sort S78 0) +(declare-sort S79 0) +(declare-sort S80 0) +(declare-sort S81 0) +(declare-sort S82 0) +(declare-sort S83 0) +(declare-sort S84 0) +(declare-sort S85 0) +(declare-sort S86 0) +(declare-sort S87 0) +(declare-sort S88 0) +(declare-sort S89 0) +(declare-sort S90 0) +(declare-sort S91 0) +(declare-sort S92 0) +(declare-sort S93 0) +(declare-sort S94 0) +(declare-sort S95 0) +(declare-sort S96 0) +(declare-sort S97 0) +(declare-sort S98 0) +(declare-sort S99 0) +(declare-sort S100 0) +(declare-sort S101 0) +(declare-sort S102 0) +(declare-sort S103 0) +(declare-sort S104 0) +(declare-sort S105 0) +(declare-sort S106 0) +(declare-sort S107 0) +(declare-sort S108 0) +(declare-sort S109 0) +(declare-sort S110 0) +(declare-sort S111 0) +(declare-sort S112 0) +(declare-sort S113 0) +(declare-sort S114 0) +(declare-sort S115 0) +(declare-sort S116 0) +(declare-sort S117 0) +(declare-sort S118 0) +(declare-sort S119 0) +(declare-sort S120 0) +(declare-sort S121 0) +(declare-sort S122 0) +(declare-sort S123 0) +(declare-sort S124 0) +(declare-sort S125 0) +(declare-sort S126 0) +(declare-sort S127 0) +(declare-sort S128 0) +(declare-sort S129 0) +(declare-sort S130 0) +(declare-sort S131 0) +(declare-sort S132 0) +(declare-sort S133 0) +(declare-sort S134 0) +(declare-sort S135 0) +(declare-sort S136 0) +(declare-sort S137 0) +(declare-sort S138 0) +(declare-sort S139 0) +(declare-sort S140 0) +(declare-sort S141 0) +(declare-sort S142 0) +(declare-sort S143 0) +(declare-sort S144 0) +(declare-sort S145 0) +(declare-sort S146 0) +(declare-sort S147 0) +(declare-sort S148 0) +(declare-sort S149 0) +(declare-sort S150 0) +(declare-sort S151 0) +(declare-sort S152 0) +(declare-sort S153 0) +(declare-sort S154 0) +(declare-sort S155 0) +(declare-sort S156 0) +(declare-sort S157 0) +(declare-sort S158 0) +(declare-sort S159 0) +(declare-sort S160 0) +(declare-sort S161 0) +(declare-sort S162 0) +(declare-sort S163 0) +(declare-sort S164 0) +(declare-sort S165 0) +(declare-sort S166 0) +(declare-sort S167 0) +(declare-sort S168 0) +(declare-sort S169 0) +(declare-sort S170 0) +(declare-sort S171 0) +(declare-sort S172 0) +(declare-sort S173 0) +(declare-sort S174 0) +(declare-sort S175 0) +(declare-sort S176 0) +(declare-sort S177 0) +(declare-sort S178 0) +(declare-sort S179 0) +(declare-sort S180 0) +(declare-sort S181 0) +(declare-sort S182 0) +(declare-sort S183 0) +(declare-sort S184 0) +(declare-sort S185 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (Int) S1) +(declare-fun f4 () Int) +(declare-fun f5 () Int) +(declare-fun f6 (S2 S3) Int) +(declare-fun f7 () S2) +(declare-fun f8 (S4 Int) S3) +(declare-fun f9 (S5 Int) S4) +(declare-fun f10 () S5) +(declare-fun f11 (S6 S7) S1) +(declare-fun f12 (S9 S8) S7) +(declare-fun f13 (S10 S8) S9) +(declare-fun f14 () S10) +(declare-fun f15 (S11 S12) S1) +(declare-fun f16 (S13 S3) S12) +(declare-fun f17 (S14 S3) S13) +(declare-fun f18 () S14) +(declare-fun f19 (S15 S3) S1) +(declare-fun f20 (S16 S17) S1) +(declare-fun f21 (S19 S18) S17) +(declare-fun f22 (S20 S18) S19) +(declare-fun f23 () S20) +(declare-fun f24 (S21 S8) S1) +(declare-fun f25 (S22 S17) S8) +(declare-fun f26 (S23 S17) S22) +(declare-fun f27 () S23) +(declare-fun f28 (S24 S8) S21) +(declare-fun f29 (S6) S24) +(declare-fun f30 (S7 S6) S1) +(declare-fun f31 (S25 S3) S15) +(declare-fun f32 (S11) S25) +(declare-fun f33 (S12 S11) S1) +(declare-fun f34 (S26 Int) S1) +(declare-fun f35 (S27 Int) S26) +(declare-fun f36 (S15) S27) +(declare-fun f37 (S3 S15) S1) +(declare-fun f38 (S28 S18) S1) +(declare-fun f39 (S29 S18) S28) +(declare-fun f40 (S16) S29) +(declare-fun f41 (S17 S16) S1) +(declare-fun f42 (S30 S17) S16) +(declare-fun f43 (S21) S30) +(declare-fun f44 (S8 S21) S1) +(declare-fun f45 (S31 S8) S6) +(declare-fun f46 (S32 S33) S1) +(declare-fun f47 (S7 S7) S32) +(declare-fun f48 (S34 S31) S33) +(declare-fun f49 (S21) S34) +(declare-fun f50 (S35 S3) S11) +(declare-fun f51 (S36 S37) S1) +(declare-fun f52 (S12 S12) S36) +(declare-fun f53 (S38 S35) S37) +(declare-fun f54 (S15) S38) +(declare-fun f55 (S39 Int) S15) +(declare-fun f56 (S40 S39) S11) +(declare-fun f57 (S26) S40) +(declare-fun f58 (S41 S17) S21) +(declare-fun f59 (S42 S41) S6) +(declare-fun f60 (S16) S42) +(declare-fun f61 (S43 S18) S16) +(declare-fun f62 (S44 S43) S21) +(declare-fun f63 (S28) S44) +(declare-fun f64 (S6) S1) +(declare-fun f65 (S11) S1) +(declare-fun f66 (S15) S1) +(declare-fun f67 (S16) S1) +(declare-fun f68 (S21) S1) +(declare-fun f69 (S6) S1) +(declare-fun f70 (S11) S1) +(declare-fun f71 (S15) S1) +(declare-fun f72 (S16) S1) +(declare-fun f73 (S21) S1) +(declare-fun f74 (S6) S24) +(declare-fun f75 (S11) S25) +(declare-fun f76 (S15) S27) +(declare-fun f77 (S16) S29) +(declare-fun f78 (S21) S30) +(declare-fun f79 (S45 S6) S33) +(declare-fun f80 (S6) S45) +(declare-fun f81 (S46 S11) S37) +(declare-fun f82 (S11) S46) +(declare-fun f83 (S47 S15) S11) +(declare-fun f84 (S15) S47) +(declare-fun f85 (S48 S21) S6) +(declare-fun f86 (S21) S48) +(declare-fun f87 (S49 S50) S1) +(declare-fun f88 (S51 S51) S49) +(declare-fun f89 (Int S8) S51) +(declare-fun f90 (S15 S6) S50) +(declare-fun f91 (S52 S53) S1) +(declare-fun f92 (S54 S54) S52) +(declare-fun f93 (Int S3) S54) +(declare-fun f94 (S15 S11) S53) +(declare-fun f95 (S55 S56) S1) +(declare-fun f96 (S57 S57) S55) +(declare-fun f97 (S8 Int) S57) +(declare-fun f98 (S6 S15) S56) +(declare-fun f99 (S58 S59) S1) +(declare-fun f100 (S60 S60) S58) +(declare-fun f101 (S3 Int) S60) +(declare-fun f102 (S11 S15) S59) +(declare-fun f103 (S61 S16) S21) +(declare-fun f104 (S16) S61) +(declare-fun f105 (S62 S63) S1) +(declare-fun f106 (S64 S64) S62) +(declare-fun f107 (S18 Int) S64) +(declare-fun f108 (S16 S15) S63) +(declare-fun f109 (S65 S66) S1) +(declare-fun f110 (S67 S67) S65) +(declare-fun f111 (S18 S8) S67) +(declare-fun f112 (S16 S6) S66) +(declare-fun f113 (S68 S69) S1) +(declare-fun f114 (S70 S70) S68) +(declare-fun f115 (S18 S3) S70) +(declare-fun f116 (S16 S11) S69) +(declare-fun f117 (S71 S72) S1) +(declare-fun f118 (S73 S73) S71) +(declare-fun f119 (S17 Int) S73) +(declare-fun f120 (S21 S15) S72) +(declare-fun f121 (S74 S75) S1) +(declare-fun f122 (S76 S76) S74) +(declare-fun f123 (S17 S8) S76) +(declare-fun f124 (S21 S6) S75) +(declare-fun f125 (S77 S78) S1) +(declare-fun f126 (S79 S79) S77) +(declare-fun f127 (S17 S3) S79) +(declare-fun f128 (S21 S11) S78) +(declare-fun f129 (S80 S81) S1) +(declare-fun f130 (S82 S82) S80) +(declare-fun f131 (Int S18) S82) +(declare-fun f132 (S15 S16) S81) +(declare-fun f133 (S83 S84) S1) +(declare-fun f134 (S85 S85) S83) +(declare-fun f135 (S8 S18) S85) +(declare-fun f136 (S6 S16) S84) +(declare-fun f137 (S86 S87) S1) +(declare-fun f138 (S88 S88) S86) +(declare-fun f139 (S3 S18) S88) +(declare-fun f140 (S11 S16) S87) +(declare-fun f141 (S89 S90) S1) +(declare-fun f142 (S91 S91) S89) +(declare-fun f143 (Int S17) S91) +(declare-fun f144 (S15 S21) S90) +(declare-fun f145 (S92 S93) S1) +(declare-fun f146 (S94 S94) S92) +(declare-fun f147 (S8 S17) S94) +(declare-fun f148 (S6 S21) S93) +(declare-fun f149 (S95 S96) S1) +(declare-fun f150 (S97 S97) S95) +(declare-fun f151 (S3 S17) S97) +(declare-fun f152 (S11 S21) S96) +(declare-fun f153 (S98) S6) +(declare-fun f154 (S99 S18) Int) +(declare-fun f155 () S99) +(declare-fun f156 (S98 S8) S18) +(declare-fun f157 (S100) S11) +(declare-fun f158 (S100 S3) S18) +(declare-fun f159 (S101) S15) +(declare-fun f160 (S101 Int) S18) +(declare-fun f161 (S102) S16) +(declare-fun f162 (S102 S18) S18) +(declare-fun f163 (S103) S21) +(declare-fun f164 (S103 S17) S18) +(declare-fun f165 (S104 S6) S6) +(declare-fun f166 (S98) S104) +(declare-fun f167 (S105 S11) S11) +(declare-fun f168 (S100) S105) +(declare-fun f169 (S106 S15) S15) +(declare-fun f170 (S101) S106) +(declare-fun f171 (S107 S16) S16) +(declare-fun f172 (S102) S107) +(declare-fun f173 (S108 S21) S21) +(declare-fun f174 (S103) S108) +(declare-fun f175 (S15 S11) S1) +(declare-fun f176 (S6 S33) S1) +(declare-fun f177 (S11 S37) S1) +(declare-fun f178 (S26 S15) S1) +(declare-fun f179 (Int S26) S1) +(declare-fun f180 (S21 S6) S1) +(declare-fun f181 (S28 S16) S1) +(declare-fun f182 (S18 S28) S1) +(declare-fun f183 (S16 S21) S1) +(declare-fun f184 () S109) +(declare-fun f185 () S109) +(declare-fun f186 () S110) +(declare-fun f187 () S110) +(declare-fun f188 () S111) +(declare-fun f189 () S111) +(declare-fun f190 (S113 S112) S15) +(declare-fun f191 (S6) S113) +(declare-fun f192 (S112 Int) S8) +(declare-fun f193 (S114 S4) S15) +(declare-fun f194 (S11) S114) +(declare-fun f195 (S116 S115) S15) +(declare-fun f196 (S15) S116) +(declare-fun f197 (S115 Int) Int) +(declare-fun f198 (S118 S117) S6) +(declare-fun f199 (S15) S118) +(declare-fun f200 (S117 S8) Int) +(declare-fun f201 (S119 S2) S11) +(declare-fun f202 (S15) S119) +(declare-fun f203 (S120 S99) S16) +(declare-fun f204 (S15) S120) +(declare-fun f205 (S122 S121) S16) +(declare-fun f206 (S6) S122) +(declare-fun f207 (S121 S18) S8) +(declare-fun f208 (S124 S123) S16) +(declare-fun f209 (S11) S124) +(declare-fun f210 (S123 S18) S3) +(declare-fun f211 (S126 S125) S21) +(declare-fun f212 (S15) S126) +(declare-fun f213 (S125 S17) Int) +(declare-fun f214 (S127 S22) S21) +(declare-fun f215 (S6) S127) +(declare-fun f216 (S129 S128) S21) +(declare-fun f217 (S11) S129) +(declare-fun f218 (S128 S17) S3) +(declare-fun f219 (S130 S101) S15) +(declare-fun f220 (S16) S130) +(declare-fun f221 (S131 S98) S6) +(declare-fun f222 (S16) S131) +(declare-fun f223 (S132 S100) S11) +(declare-fun f224 (S16) S132) +(declare-fun f225 (S134 S133) S15) +(declare-fun f226 (S21) S134) +(declare-fun f227 (S133 Int) S17) +(declare-fun f228 (S136 S135) S6) +(declare-fun f229 (S21) S136) +(declare-fun f230 (S135 S8) S17) +(declare-fun f231 (S138 S137) S11) +(declare-fun f232 (S21) S138) +(declare-fun f233 (S137 S3) S17) +(declare-fun f234 (S24) S6) +(declare-fun f235 (S25) S11) +(declare-fun f236 (S111 S27) S15) +(declare-fun f237 (S110 S29) S16) +(declare-fun f238 (S109 S30) S21) +(declare-fun f239 (S139 Int) S39) +(declare-fun f240 (S139) S25) +(declare-fun f241 (S141 Int) S6) +(declare-fun f242 (S140 Int) S141) +(declare-fun f243 (S142 S3) S6) +(declare-fun f244 (S140) S142) +(declare-fun f245 (S144 Int) S11) +(declare-fun f246 (S143 Int) S144) +(declare-fun f247 (S143) S35) +(declare-fun f248 (S146 Int) S28) +(declare-fun f249 (S145 Int) S146) +(declare-fun f250 (S147 S3) S28) +(declare-fun f251 (S145) S147) +(declare-fun f252 (S148 Int) S27) +(declare-fun f253 (S149 S3) S26) +(declare-fun f254 (S148) S149) +(declare-fun f255 (S151 S18) S15) +(declare-fun f256 (S150 S18) S151) +(declare-fun f257 (S152 S17) S15) +(declare-fun f258 (S150) S152) +(declare-fun f259 (S154 S18) S6) +(declare-fun f260 (S153 S18) S154) +(declare-fun f261 (S155 S17) S6) +(declare-fun f262 (S153) S155) +(declare-fun f263 (S157 S18) S11) +(declare-fun f264 (S156 S18) S157) +(declare-fun f265 (S158 S17) S11) +(declare-fun f266 (S156) S158) +(declare-fun f267 (S159 S18) S29) +(declare-fun f268 (S160 S17) S28) +(declare-fun f269 (S159) S160) +(declare-fun f270 (S162 S18) S26) +(declare-fun f271 (S161 S18) S162) +(declare-fun f272 (S163 S17) S26) +(declare-fun f273 (S161) S163) +(declare-fun f274 (S164 S17) S152) +(declare-fun f275 (S165 S8) S15) +(declare-fun f276 (S164) S165) +(declare-fun f277 (S166 S17) S155) +(declare-fun f278 (S166) S31) +(declare-fun f279 (S167 S17) S158) +(declare-fun f280 (S168 S8) S11) +(declare-fun f281 (S167) S168) +(declare-fun f282 (S169 S17) S160) +(declare-fun f283 (S170 S8) S28) +(declare-fun f284 (S169) S170) +(declare-fun f285 (S171 S17) S163) +(declare-fun f286 (S172 S8) S26) +(declare-fun f287 (S171) S172) +(declare-fun f288 (S174 S8) S16) +(declare-fun f289 (S173 S8) S174) +(declare-fun f290 (S175 S7) S16) +(declare-fun f291 (S173) S175) +(declare-fun f292 (S177 S3) S16) +(declare-fun f293 (S176 S3) S177) +(declare-fun f294 (S178 S12) S16) +(declare-fun f295 (S176) S178) +(declare-fun f296 (S179 S8) S24) +(declare-fun f297 (S180 S7) S21) +(declare-fun f298 (S179) S180) +(declare-fun f299 (S182 S3) S21) +(declare-fun f300 (S181 S3) S182) +(declare-fun f301 (S183 S12) S21) +(declare-fun f302 (S181) S183) +(declare-fun f303 () S16) +(declare-fun f304 () S21) +(declare-fun f305 (S16) S1) +(declare-fun f306 (S21) S1) +(declare-fun f307 (S16) S1) +(declare-fun f308 (S21) S1) +(declare-fun f309 (S16) S1) +(declare-fun f310 (S15) S1) +(declare-fun f311 (S21) S1) +(declare-fun f312 (S15) S1) +(declare-fun f313 (S15) S1) +(declare-fun f314 (S6) S1) +(declare-fun f315 () S101) +(declare-fun f316 (S30) S1) +(declare-fun f317 (S29) S1) +(declare-fun f318 (S24) S1) +(declare-fun f319 () S16) +(declare-fun f320 () S21) +(declare-fun f321 (S184) S1) +(declare-fun f322 (S21) S184) +(declare-fun f323 (S185) S1) +(declare-fun f324 (S16) S185) +(declare-fun f325 (S16) S16) +(declare-fun f326 (S21) S21) +(declare-fun f327 (S15) S15) +(declare-fun f328 (S21) S184) +(declare-fun f329 (S16) S185) +(declare-fun f330 (S6) S6) +(declare-fun f331 (S11) S11) +(assert (not (= f1 f2))) +(assert (not (= (f3 (* f4 f5)) f1))) +(assert (= (f3 f4) f1)) +(assert (= (f3 f5) f1)) +(assert (forall ((?v0 Int)) (= (= (f3 ?v0) f1) (exists ((?v1 Int) (?v2 Int)) (= (f6 f7 (f8 (f9 f10 ?v1) ?v2)) ?v0))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (* (f6 f7 (f8 (f9 f10 ?v0) ?v1)) (f6 f7 (f8 (f9 f10 ?v2) ?v3))) (f6 f7 (f8 (f9 f10 (+ (* ?v0 ?v2) (* ?v1 ?v3))) (- (* ?v0 ?v3) (* ?v1 ?v2))))))) +(assert (forall ((?v0 S6)) (= (forall ((?v1 S7)) (= (f11 ?v0 ?v1) f1)) (forall ((?v1 S8) (?v2 S8)) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S11)) (= (forall ((?v1 S12)) (= (f15 ?v0 ?v1) f1)) (forall ((?v1 S3) (?v2 S3)) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S15)) (= (forall ((?v1 S3)) (= (f19 ?v0 ?v1) f1)) (forall ((?v1 Int) (?v2 Int)) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S16)) (= (forall ((?v1 S17)) (= (f20 ?v0 ?v1) f1)) (forall ((?v1 S18) (?v2 S18)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S21)) (= (forall ((?v1 S8)) (= (f24 ?v0 ?v1) f1)) (forall ((?v1 S17) (?v2 S17)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (= (= (f12 (f13 f14 ?v0) ?v1) (f12 (f13 f14 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (= (= (f16 (f17 f18 ?v0) ?v1) (f16 (f17 f18 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (= (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17)) (= (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (=> (= (f12 (f13 f14 ?v0) ?v1) (f12 (f13 f14 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (=> (= (f16 (f17 f18 ?v0) ?v1) (f16 (f17 f18 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (=> (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17)) (=> (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false)))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (= (= (f24 (f28 (f29 ?v0) ?v1) ?v2) f1) (= (f30 (f12 (f13 f14 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (= (= (f19 (f31 (f32 ?v0) ?v1) ?v2) f1) (= (f33 (f16 (f17 f18 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (= (= (f34 (f35 (f36 ?v0) ?v1) ?v2) f1) (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (= (= (f38 (f39 (f40 ?v0) ?v1) ?v2) f1) (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (= (= (f20 (f42 (f43 ?v0) ?v1) ?v2) f1) (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1)))) +(assert (forall ((?v0 S21) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S31)) (let ((?v_0 (f13 f14 ?v1))) (=> (= (f24 ?v0 ?v1) f1) (=> (= (f30 (f12 (f13 f14 ?v2) ?v3) (f45 ?v4 ?v1)) f1) (= (f46 (f47 (f12 ?v_0 ?v2) (f12 ?v_0 ?v3)) (f48 (f49 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S15) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S35)) (let ((?v_0 (f17 f18 ?v1))) (=> (= (f19 ?v0 ?v1) f1) (=> (= (f33 (f16 (f17 f18 ?v2) ?v3) (f50 ?v4 ?v1)) f1) (= (f51 (f52 (f16 ?v_0 ?v2) (f16 ?v_0 ?v3)) (f53 (f54 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S26) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S39)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) (f55 ?v4 ?v1)) f1) (= (f33 (f16 (f17 f18 (f8 ?v_0 ?v2)) (f8 ?v_0 ?v3)) (f56 (f57 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S16) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S41)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f20 ?v0 ?v1) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) (f58 ?v4 ?v1)) f1) (= (f30 (f12 (f13 f14 (f25 ?v_0 ?v2)) (f25 ?v_0 ?v3)) (f59 (f60 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S28) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S43)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f38 ?v0 ?v1) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) (f61 ?v4 ?v1)) f1) (= (f44 (f25 (f26 f27 (f21 ?v_0 ?v2)) (f21 ?v_0 ?v3)) (f62 (f63 ?v0) ?v4)) f1)))))) +(assert (forall ((?v0 S6)) (= (= (f64 ?v0) f1) (forall ((?v1 S8)) (= (f30 (f12 (f13 f14 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S11)) (= (= (f65 ?v0) f1) (forall ((?v1 S3)) (= (f33 (f16 (f17 f18 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S15)) (= (= (f66 ?v0) f1) (forall ((?v1 Int)) (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S16)) (= (= (f67 ?v0) f1) (forall ((?v1 S18)) (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S21)) (= (= (f68 ?v0) f1) (forall ((?v1 S17)) (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S6)) (= (= (f69 ?v0) f1) (forall ((?v1 S8)) (not (= (f30 (f12 (f13 f14 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S11)) (= (= (f70 ?v0) f1) (forall ((?v1 S3)) (not (= (f33 (f16 (f17 f18 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S15)) (= (= (f71 ?v0) f1) (forall ((?v1 Int)) (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S16)) (= (= (f72 ?v0) f1) (forall ((?v1 S18)) (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S21)) (= (= (f73 ?v0) f1) (forall ((?v1 S17)) (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S6)) (= (exists ((?v1 S7)) (= (f11 ?v0 ?v1) f1)) (exists ((?v1 S8) (?v2 S8)) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S11)) (= (exists ((?v1 S12)) (= (f15 ?v0 ?v1) f1)) (exists ((?v1 S3) (?v2 S3)) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S15)) (= (exists ((?v1 S3)) (= (f19 ?v0 ?v1) f1)) (exists ((?v1 Int) (?v2 Int)) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S16)) (= (exists ((?v1 S17)) (= (f20 ?v0 ?v1) f1)) (exists ((?v1 S18) (?v2 S18)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S21)) (= (exists ((?v1 S8)) (= (f24 ?v0 ?v1) f1)) (exists ((?v1 S17) (?v2 S17)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))) +(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S17) (?v3 S18) (?v4 S18)) (=> (= ?v0 (f12 (f13 f14 ?v1) (f25 (f26 f27 ?v2) (f21 (f22 f23 ?v3) ?v4)))) false)) false))) +(assert (forall ((?v0 S6) (?v1 S7)) (=> (forall ((?v2 S8) (?v3 S17) (?v4 S18) (?v5 S18)) (= (f11 ?v0 (f12 (f13 f14 ?v2) (f25 (f26 f27 ?v3) (f21 (f22 f23 ?v4) ?v5)))) f1)) (= (f11 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S18) (?v3 S18)) (=> (= ?v0 (f25 (f26 f27 ?v1) (f21 (f22 f23 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 Int) (?v3 Int)) (=> (= ?v0 (f16 (f17 f18 ?v1) (f8 (f9 f10 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S17) (?v3 S17)) (=> (= ?v0 (f12 (f13 f14 ?v1) (f25 (f26 f27 ?v2) ?v3))) false)) false))) +(assert (forall ((?v0 S21) (?v1 S8)) (=> (forall ((?v2 S17) (?v3 S18) (?v4 S18)) (= (f24 ?v0 (f25 (f26 f27 ?v2) (f21 (f22 f23 ?v3) ?v4))) f1)) (= (f24 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S11) (?v1 S12)) (=> (forall ((?v2 S3) (?v3 Int) (?v4 Int)) (= (f15 ?v0 (f16 (f17 f18 ?v2) (f8 (f9 f10 ?v3) ?v4))) f1)) (= (f15 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S6) (?v1 S7)) (=> (forall ((?v2 S8) (?v3 S17) (?v4 S17)) (= (f11 ?v0 (f12 (f13 f14 ?v2) (f25 (f26 f27 ?v3) ?v4))) f1)) (= (f11 ?v0 ?v1) f1)))) +(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S8)) (=> (= ?v0 (f12 (f13 f14 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f16 (f17 f18 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S17)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S8)) (=> (= ?v0 (f12 (f13 f14 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f16 (f17 f18 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S17)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1) (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1) (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S6) (?v5 S6)) (let ((?v_0 (f13 f14 ?v0))) (= (= (f46 (f47 (f12 ?v_0 ?v1) (f12 (f13 f14 ?v2) ?v3)) (f79 (f80 ?v4) ?v5)) f1) (or (= (f30 (f12 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S11) (?v5 S11)) (let ((?v_0 (f17 f18 ?v0))) (= (= (f51 (f52 (f16 ?v_0 ?v1) (f16 (f17 f18 ?v2) ?v3)) (f81 (f82 ?v4) ?v5)) f1) (or (= (f33 (f16 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S15) (?v5 S15)) (let ((?v_0 (f9 f10 ?v0))) (= (= (f33 (f16 (f17 f18 (f8 ?v_0 ?v1)) (f8 (f9 f10 ?v2) ?v3)) (f83 (f84 ?v4) ?v5)) f1) (or (= (f37 (f8 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S21) (?v5 S21)) (let ((?v_0 (f26 f27 ?v0))) (= (= (f30 (f12 (f13 f14 (f25 ?v_0 ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f85 (f86 ?v4) ?v5)) f1) (or (= (f44 (f25 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 Int) (?v1 S8) (?v2 Int) (?v3 S8) (?v4 S15) (?v5 S6)) (= (= (f87 (f88 (f89 ?v0 ?v1) (f89 ?v2 ?v3)) (f90 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S3) (?v2 Int) (?v3 S3) (?v4 S15) (?v5 S11)) (= (= (f91 (f92 (f93 ?v0 ?v1) (f93 ?v2 ?v3)) (f94 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S8) (?v1 Int) (?v2 S8) (?v3 Int) (?v4 S6) (?v5 S15)) (= (= (f95 (f96 (f97 ?v0 ?v1) (f97 ?v2 ?v3)) (f98 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S3) (?v1 Int) (?v2 S3) (?v3 Int) (?v4 S11) (?v5 S15)) (= (= (f99 (f100 (f101 ?v0 ?v1) (f101 ?v2 ?v3)) (f102 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S16) (?v5 S16)) (let ((?v_0 (f22 f23 ?v0))) (= (= (f44 (f25 (f26 f27 (f21 ?v_0 ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f103 (f104 ?v4) ?v5)) f1) (or (= (f41 (f21 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1))))))) +(assert (forall ((?v0 S18) (?v1 Int) (?v2 S18) (?v3 Int) (?v4 S16) (?v5 S15)) (= (= (f105 (f106 (f107 ?v0 ?v1) (f107 ?v2 ?v3)) (f108 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S18) (?v1 S8) (?v2 S18) (?v3 S8) (?v4 S16) (?v5 S6)) (= (= (f109 (f110 (f111 ?v0 ?v1) (f111 ?v2 ?v3)) (f112 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18) (?v3 S3) (?v4 S16) (?v5 S11)) (= (= (f113 (f114 (f115 ?v0 ?v1) (f115 ?v2 ?v3)) (f116 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S17) (?v1 Int) (?v2 S17) (?v3 Int) (?v4 S21) (?v5 S15)) (= (= (f117 (f118 (f119 ?v0 ?v1) (f119 ?v2 ?v3)) (f120 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S17) (?v1 S8) (?v2 S17) (?v3 S8) (?v4 S21) (?v5 S6)) (= (= (f121 (f122 (f123 ?v0 ?v1) (f123 ?v2 ?v3)) (f124 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S17) (?v1 S3) (?v2 S17) (?v3 S3) (?v4 S21) (?v5 S11)) (= (= (f125 (f126 (f127 ?v0 ?v1) (f127 ?v2 ?v3)) (f128 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18) (?v4 S15) (?v5 S16)) (= (= (f129 (f130 (f131 ?v0 ?v1) (f131 ?v2 ?v3)) (f132 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S8) (?v1 S18) (?v2 S8) (?v3 S18) (?v4 S6) (?v5 S16)) (= (= (f133 (f134 (f135 ?v0 ?v1) (f135 ?v2 ?v3)) (f136 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S3) (?v1 S18) (?v2 S3) (?v3 S18) (?v4 S11) (?v5 S16)) (= (= (f137 (f138 (f139 ?v0 ?v1) (f139 ?v2 ?v3)) (f140 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 Int) (?v1 S17) (?v2 Int) (?v3 S17) (?v4 S15) (?v5 S21)) (= (= (f141 (f142 (f143 ?v0 ?v1) (f143 ?v2 ?v3)) (f144 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S8) (?v1 S17) (?v2 S8) (?v3 S17) (?v4 S6) (?v5 S21)) (= (= (f145 (f146 (f147 ?v0 ?v1) (f147 ?v2 ?v3)) (f148 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S3) (?v1 S17) (?v2 S3) (?v3 S17) (?v4 S11) (?v5 S21)) (= (= (f149 (f150 (f151 ?v0 ?v1) (f151 ?v2 ?v3)) (f152 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1)))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (= (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (= (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (= (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1) (=> (=> (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1) (=> (=> (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (=> (=> (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (=> (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (=> (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) false) false)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S98)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f153 ?v2)) f1) (< (f154 f155 (f156 ?v2 ?v0)) (f154 f155 (f156 ?v2 ?v1)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S100)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f157 ?v2)) f1) (< (f154 f155 (f158 ?v2 ?v0)) (f154 f155 (f158 ?v2 ?v1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S101)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f159 ?v2)) f1) (< (f154 f155 (f160 ?v2 ?v0)) (f154 f155 (f160 ?v2 ?v1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S102)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f161 ?v2)) f1) (< (f154 f155 (f162 ?v2 ?v0)) (f154 f155 (f162 ?v2 ?v1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S103)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f163 ?v2)) f1) (< (f154 f155 (f164 ?v2 ?v0)) (f154 f155 (f164 ?v2 ?v1)))))) +(assert (forall ((?v0 S98) (?v1 S8) (?v2 S8) (?v3 S6)) (=> (< (f154 f155 (f156 ?v0 ?v1)) (f154 f155 (f156 ?v0 ?v2))) (= (f30 (f12 (f13 f14 ?v1) ?v2) (f165 (f166 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S100) (?v1 S3) (?v2 S3) (?v3 S11)) (=> (< (f154 f155 (f158 ?v0 ?v1)) (f154 f155 (f158 ?v0 ?v2))) (= (f33 (f16 (f17 f18 ?v1) ?v2) (f167 (f168 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S101) (?v1 Int) (?v2 Int) (?v3 S15)) (=> (< (f154 f155 (f160 ?v0 ?v1)) (f154 f155 (f160 ?v0 ?v2))) (= (f37 (f8 (f9 f10 ?v1) ?v2) (f169 (f170 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S102) (?v1 S18) (?v2 S18) (?v3 S16)) (=> (< (f154 f155 (f162 ?v0 ?v1)) (f154 f155 (f162 ?v0 ?v2))) (= (f41 (f21 (f22 f23 ?v1) ?v2) (f171 (f172 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S103) (?v1 S17) (?v2 S17) (?v3 S21)) (=> (< (f154 f155 (f164 ?v0 ?v1)) (f154 f155 (f164 ?v0 ?v2))) (= (f44 (f25 (f26 f27 ?v1) ?v2) (f173 (f174 ?v0) ?v3)) f1)))) +(assert (forall ((?v0 S98) (?v1 S8) (?v2 S8) (?v3 S6)) (let ((?v_0 (f12 (f13 f14 ?v1) ?v2))) (=> (<= (f154 f155 (f156 ?v0 ?v1)) (f154 f155 (f156 ?v0 ?v2))) (=> (= (f30 ?v_0 ?v3) f1) (= (f30 ?v_0 (f165 (f166 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S100) (?v1 S3) (?v2 S3) (?v3 S11)) (let ((?v_0 (f16 (f17 f18 ?v1) ?v2))) (=> (<= (f154 f155 (f158 ?v0 ?v1)) (f154 f155 (f158 ?v0 ?v2))) (=> (= (f33 ?v_0 ?v3) f1) (= (f33 ?v_0 (f167 (f168 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S101) (?v1 Int) (?v2 Int) (?v3 S15)) (let ((?v_0 (f8 (f9 f10 ?v1) ?v2))) (=> (<= (f154 f155 (f160 ?v0 ?v1)) (f154 f155 (f160 ?v0 ?v2))) (=> (= (f37 ?v_0 ?v3) f1) (= (f37 ?v_0 (f169 (f170 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S102) (?v1 S18) (?v2 S18) (?v3 S16)) (let ((?v_0 (f21 (f22 f23 ?v1) ?v2))) (=> (<= (f154 f155 (f162 ?v0 ?v1)) (f154 f155 (f162 ?v0 ?v2))) (=> (= (f41 ?v_0 ?v3) f1) (= (f41 ?v_0 (f171 (f172 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S103) (?v1 S17) (?v2 S17) (?v3 S21)) (let ((?v_0 (f25 (f26 f27 ?v1) ?v2))) (=> (<= (f154 f155 (f164 ?v0 ?v1)) (f154 f155 (f164 ?v0 ?v2))) (=> (= (f44 ?v_0 ?v3) f1) (= (f44 ?v_0 (f173 (f174 ?v0) ?v3)) f1)))))) +(assert (forall ((?v0 S15) (?v1 S11)) (= (= (f175 ?v0 ?v1) f1) (forall ((?v2 S3)) (=> (= (f37 ?v2 ?v0) f1) (forall ((?v3 S3)) (=> (= (f37 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f33 (f16 (f17 f18 ?v2) ?v3) ?v1) f1) (= (f33 (f16 (f17 f18 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S6) (?v1 S33)) (= (= (f176 ?v0 ?v1) f1) (forall ((?v2 S7)) (=> (= (f30 ?v2 ?v0) f1) (forall ((?v3 S7)) (=> (= (f30 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f46 (f47 ?v2 ?v3) ?v1) f1) (= (f46 (f47 ?v3 ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S11) (?v1 S37)) (= (= (f177 ?v0 ?v1) f1) (forall ((?v2 S12)) (=> (= (f33 ?v2 ?v0) f1) (forall ((?v3 S12)) (=> (= (f33 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f51 (f52 ?v2 ?v3) ?v1) f1) (= (f51 (f52 ?v3 ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S26) (?v1 S15)) (= (= (f178 ?v0 ?v1) f1) (forall ((?v2 Int)) (=> (= (f179 ?v2 ?v0) f1) (forall ((?v3 Int)) (=> (= (f179 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v1) f1) (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S21) (?v1 S6)) (= (= (f180 ?v0 ?v1) f1) (forall ((?v2 S8)) (=> (= (f44 ?v2 ?v0) f1) (forall ((?v3 S8)) (=> (= (f44 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f30 (f12 (f13 f14 ?v2) ?v3) ?v1) f1) (= (f30 (f12 (f13 f14 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S28) (?v1 S16)) (= (= (f181 ?v0 ?v1) f1) (forall ((?v2 S18)) (=> (= (f182 ?v2 ?v0) f1) (forall ((?v3 S18)) (=> (= (f182 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v1) f1) (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v1) f1)))))))))) +(assert (forall ((?v0 S16) (?v1 S21)) (= (= (f183 ?v0 ?v1) f1) (forall ((?v2 S17)) (=> (= (f41 ?v2 ?v0) f1) (forall ((?v3 S17)) (=> (= (f41 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v1) f1) (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v1) f1)))))))))) +(assert (= f184 f185)) +(assert (= f186 f187)) +(assert (= f188 f189)) +(assert (forall ((?v0 S7)) (exists ((?v1 S8) (?v2 S8)) (= ?v0 (f12 (f13 f14 ?v1) ?v2))))) +(assert (forall ((?v0 S12)) (exists ((?v1 S3) (?v2 S3)) (= ?v0 (f16 (f17 f18 ?v1) ?v2))))) +(assert (forall ((?v0 S3)) (exists ((?v1 Int) (?v2 Int)) (= ?v0 (f8 (f9 f10 ?v1) ?v2))))) +(assert (forall ((?v0 S17)) (exists ((?v1 S18) (?v2 S18)) (= ?v0 (f21 (f22 f23 ?v1) ?v2))))) +(assert (forall ((?v0 S8)) (exists ((?v1 S17) (?v2 S17)) (= ?v0 (f25 (f26 f27 ?v1) ?v2))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S6) (?v3 S112)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f190 (f191 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f192 ?v3 ?v0)) (f192 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S11) (?v3 S4)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f193 (f194 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f8 ?v3 ?v0)) (f8 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S115)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f195 (f196 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f197 ?v3 ?v0)) (f197 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S15) (?v3 S117)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f198 (f199 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f200 ?v3 ?v0)) (f200 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S15) (?v3 S2)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f201 (f202 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f6 ?v3 ?v0)) (f6 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S15) (?v3 S99)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f203 (f204 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f154 ?v3 ?v0)) (f154 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S6) (?v3 S121)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f205 (f206 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f207 ?v3 ?v0)) (f207 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S11) (?v3 S123)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f208 (f209 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f210 ?v3 ?v0)) (f210 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S15) (?v3 S125)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f211 (f212 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f213 ?v3 ?v0)) (f213 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S6) (?v3 S22)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f214 (f215 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f25 ?v3 ?v0)) (f25 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S11) (?v3 S128)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f216 (f217 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f218 ?v3 ?v0)) (f218 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S16) (?v3 S101)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f219 (f220 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f160 ?v3 ?v0)) (f160 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S16) (?v3 S98)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f221 (f222 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f156 ?v3 ?v0)) (f156 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S16) (?v3 S100)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f223 (f224 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f158 ?v3 ?v0)) (f158 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S21) (?v3 S133)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f225 (f226 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f227 ?v3 ?v0)) (f227 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S21) (?v3 S135)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f228 (f229 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f230 ?v3 ?v0)) (f230 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S21) (?v3 S137)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f231 (f232 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f233 ?v3 ?v0)) (f233 ?v3 ?v1)) ?v2) f1)))) +(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 ?v0 ?v1) ?v2) f1) (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 ?v0 ?v1) ?v2) f1) (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 ?v0 ?v1) ?v2) f1) (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 ?v0 ?v1) ?v2) f1) (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 ?v0 ?v1) ?v2) f1) (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 ?v0 ?v1) ?v2) f1) (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 ?v0 ?v1) ?v2) f1) (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 ?v0 ?v1) ?v2) f1) (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 ?v0 ?v1) ?v2) f1) (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 ?v0 ?v1) ?v2) f1) (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1)))) +(assert (forall ((?v0 S3) (?v1 S139) (?v2 Int) (?v3 Int)) (=> (= (f37 ?v0 (f55 (f239 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f31 (f240 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S7) (?v1 S140) (?v2 Int) (?v3 Int)) (=> (= (f30 ?v0 (f241 (f242 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f243 (f244 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S12) (?v1 S143) (?v2 Int) (?v3 Int)) (=> (= (f33 ?v0 (f245 (f246 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f50 (f247 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S18) (?v1 S145) (?v2 Int) (?v3 Int)) (=> (= (f182 ?v0 (f248 (f249 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f250 (f251 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 Int) (?v1 S148) (?v2 Int) (?v3 Int)) (=> (= (f179 ?v0 (f35 (f252 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f253 (f254 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S3) (?v1 S150) (?v2 S18) (?v3 S18)) (=> (= (f37 ?v0 (f255 (f256 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f257 (f258 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S7) (?v1 S153) (?v2 S18) (?v3 S18)) (=> (= (f30 ?v0 (f259 (f260 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f261 (f262 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S12) (?v1 S156) (?v2 S18) (?v3 S18)) (=> (= (f33 ?v0 (f263 (f264 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f265 (f266 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S18) (?v1 S159) (?v2 S18) (?v3 S18)) (=> (= (f182 ?v0 (f39 (f267 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f268 (f269 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 Int) (?v1 S161) (?v2 S18) (?v3 S18)) (=> (= (f179 ?v0 (f270 (f271 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f272 (f273 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S3) (?v1 S164) (?v2 S17) (?v3 S17)) (=> (= (f37 ?v0 (f257 (f274 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f275 (f276 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S7) (?v1 S166) (?v2 S17) (?v3 S17)) (=> (= (f30 ?v0 (f261 (f277 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f45 (f278 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S12) (?v1 S167) (?v2 S17) (?v3 S17)) (=> (= (f33 ?v0 (f265 (f279 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f280 (f281 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S18) (?v1 S169) (?v2 S17) (?v3 S17)) (=> (= (f182 ?v0 (f268 (f282 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f283 (f284 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 Int) (?v1 S171) (?v2 S17) (?v3 S17)) (=> (= (f179 ?v0 (f272 (f285 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f286 (f287 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S17) (?v1 S173) (?v2 S8) (?v3 S8)) (=> (= (f41 ?v0 (f288 (f289 ?v1 ?v2) ?v3)) f1) (= (f41 ?v0 (f290 (f291 ?v1) (f12 (f13 f14 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S17) (?v1 S176) (?v2 S3) (?v3 S3)) (=> (= (f41 ?v0 (f292 (f293 ?v1 ?v2) ?v3)) f1) (= (f41 ?v0 (f294 (f295 ?v1) (f16 (f17 f18 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S8) (?v1 S179) (?v2 S8) (?v3 S8)) (=> (= (f44 ?v0 (f28 (f296 ?v1 ?v2) ?v3)) f1) (= (f44 ?v0 (f297 (f298 ?v1) (f12 (f13 f14 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S8) (?v1 S181) (?v2 S3) (?v3 S3)) (=> (= (f44 ?v0 (f299 (f300 ?v1 ?v2) ?v3)) f1) (= (f44 ?v0 (f301 (f302 ?v1) (f16 (f17 f18 ?v2) ?v3))) f1)))) +(assert (forall ((?v0 S8) (?v1 S8) (?v2 S30)) (let ((?v_0 (f238 f185 ?v2))) (=> (= ?v0 ?v1) (= (= (f24 ?v_0 ?v0) f1) (= (f24 ?v_0 ?v1) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S29)) (let ((?v_0 (f237 f187 ?v2))) (=> (= ?v0 ?v1) (= (= (f20 ?v_0 ?v0) f1) (= (f20 ?v_0 ?v1) f1)))))) +(assert (forall ((?v0 S3) (?v1 S3) (?v2 S27)) (let ((?v_0 (f236 f189 ?v2))) (=> (= ?v0 ?v1) (= (= (f19 ?v_0 ?v0) f1) (= (f19 ?v_0 ?v1) f1)))))) +(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1) (= (f24 (f28 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1) (= (f19 (f31 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (= (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (= (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (= (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (= (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (= (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1)))) +(assert (forall ((?v0 S30) (?v1 S8)) (=> (= (f24 (f238 f185 ?v0) ?v1) f1) (=> (forall ((?v2 S17) (?v3 S17)) (=> (= ?v1 (f25 (f26 f27 ?v2) ?v3)) (=> (= (f20 (f42 ?v0 ?v2) ?v3) f1) false))) false)))) +(assert (forall ((?v0 S29) (?v1 S17)) (=> (= (f20 (f237 f187 ?v0) ?v1) f1) (=> (forall ((?v2 S18) (?v3 S18)) (=> (= ?v1 (f21 (f22 f23 ?v2) ?v3)) (=> (= (f38 (f39 ?v0 ?v2) ?v3) f1) false))) false)))) +(assert (forall ((?v0 S27) (?v1 S3)) (=> (= (f19 (f236 f189 ?v0) ?v1) f1) (=> (forall ((?v2 Int) (?v3 Int)) (=> (= ?v1 (f8 (f9 f10 ?v2) ?v3)) (=> (= (f34 (f35 ?v0 ?v2) ?v3) f1) false))) false)))) +(assert (forall ((?v0 S8) (?v1 S30)) (=> (forall ((?v2 S17) (?v3 S17)) (=> (= ?v0 (f25 (f26 f27 ?v2) ?v3)) (= (f20 (f42 ?v1 ?v2) ?v3) f1))) (= (f24 (f238 f185 ?v1) ?v0) f1)))) +(assert (forall ((?v0 S17) (?v1 S29)) (=> (forall ((?v2 S18) (?v3 S18)) (=> (= ?v0 (f21 (f22 f23 ?v2) ?v3)) (= (f38 (f39 ?v1 ?v2) ?v3) f1))) (= (f20 (f237 f187 ?v1) ?v0) f1)))) +(assert (forall ((?v0 S3) (?v1 S27)) (=> (forall ((?v2 Int) (?v3 Int)) (=> (= ?v0 (f8 (f9 f10 ?v2) ?v3)) (= (f34 (f35 ?v1 ?v2) ?v3) f1))) (= (f19 (f236 f189 ?v1) ?v0) f1)))) +(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) f303) f1) (< (f154 f155 ?v0) (f154 f155 ?v1))))) +(assert (= f304 (f103 (f104 f303) f303))) +(assert (= (f305 f303) f1)) +(assert (forall ((?v0 S103)) (= (f306 (f163 ?v0)) f1))) +(assert (forall ((?v0 S102)) (= (f307 (f161 ?v0)) f1))) +(assert (forall ((?v0 S21)) (= (= (f308 ?v0) f1) (forall ((?v1 S17) (?v2 S17)) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))) +(assert (forall ((?v0 S16)) (= (= (f309 ?v0) f1) (forall ((?v1 S18) (?v2 S18)) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))) +(assert (forall ((?v0 S15)) (= (= (f310 ?v0) f1) (forall ((?v1 Int) (?v2 Int)) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))) +(assert (= (f307 f303) f1)) +(assert (forall ((?v0 S16) (?v1 S16)) (=> (= (f307 ?v0) f1) (=> (= (f307 ?v1) f1) (= (f306 (f103 (f104 ?v0) ?v1)) f1))))) +(assert (forall ((?v0 S16) (?v1 S16)) (=> (= (f305 ?v0) f1) (=> (= (f305 ?v1) f1) (= (f311 (f103 (f104 ?v0) ?v1)) f1))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (<= (f154 f155 ?v0) (f154 f155 ?v1)) (=> (< (f154 f155 ?v2) (f154 f155 ?v3)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f304) f1))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (< (f154 f155 ?v0) (f154 f155 ?v1)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f304) f1)))) +(assert (= (f306 f304) f1)) +(assert (forall ((?v0 S21) (?v1 S17)) (=> (= (f306 ?v0) f1) (=> (=> (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)) false) false)))) +(assert (forall ((?v0 S16) (?v1 S18)) (=> (= (f307 ?v0) f1) (=> (=> (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1)) false) false)))) +(assert (forall ((?v0 S15) (?v1 Int)) (=> (= (f312 ?v0) f1) (=> (=> (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)) false) false)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1)) false) false))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1)) false) false))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1)) false) false))))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (not (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (not (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (not (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1)))))) +(assert (forall ((?v0 S21) (?v1 S17)) (=> (= (f306 ?v0) f1) (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S16) (?v1 S18)) (=> (= (f307 ?v0) f1) (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S15) (?v1 Int)) (=> (= (f312 ?v0) f1) (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1))))) +(assert (forall ((?v0 S8) (?v1 S21)) (= (= (f44 ?v0 ?v1) f1) (= (f24 ?v1 ?v0) f1)))) +(assert (forall ((?v0 S17) (?v1 S16)) (= (= (f41 ?v0 ?v1) f1) (= (f20 ?v1 ?v0) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f311 ?v0) f1) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1))))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f305 ?v0) f1) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1))))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f313 ?v0) f1) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1))))))) +(assert (forall ((?v0 S21)) (= (= (f311 ?v0) f1) (forall ((?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1)))))))) +(assert (forall ((?v0 S16)) (= (= (f305 ?v0) f1) (forall ((?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1)))))))) +(assert (forall ((?v0 S15)) (= (= (f313 ?v0) f1) (forall ((?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1)))))))) +(assert (forall ((?v0 S21) (?v1 S103)) (=> (= (f306 ?v0) f1) (= (f306 (f173 (f174 ?v1) ?v0)) f1)))) +(assert (forall ((?v0 S16) (?v1 S102)) (=> (= (f307 ?v0) f1) (= (f307 (f171 (f172 ?v1) ?v0)) f1)))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f308 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f309 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f310 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))) +(assert (forall ((?v0 S28) (?v1 S43)) (=> (forall ((?v2 S18)) (=> (= (f38 ?v0 ?v2) f1) (= (f307 (f61 ?v1 ?v2)) f1))) (= (f306 (f62 (f63 ?v0) ?v1)) f1)))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f308 ?v0) f1)))) +(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f309 ?v0) f1)))) +(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f310 ?v0) f1)))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1))))) (= (f311 ?v0) f1)))) +(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1))))) (= (f305 ?v0) f1)))) +(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1))))) (= (f313 ?v0) f1)))) +(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (forall ((?v1 S16) (?v2 S17)) (=> (= (f41 ?v2 ?v1) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v1) f1) (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v1) f1))))))))))) +(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (forall ((?v1 S28) (?v2 S18)) (=> (= (f182 ?v2 ?v1) f1) (exists ((?v3 S18)) (and (= (f182 ?v3 ?v1) f1) (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v1) f1))))))))))) +(assert (forall ((?v0 S6)) (= (= (f314 ?v0) f1) (forall ((?v1 S21) (?v2 S8)) (=> (= (f44 ?v2 ?v1) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v1) f1) (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v1) f1))))))))))) +(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (forall ((?v1 S26) (?v2 Int)) (=> (= (f179 ?v2 ?v1) f1) (exists ((?v3 Int)) (and (= (f179 ?v3 ?v1) f1) (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v1) f1))))))))))) +(assert (forall ((?v0 S21) (?v1 S103) (?v2 S103)) (=> (forall ((?v3 S17) (?v4 S17)) (let ((?v_0 (f154 f155 (f164 ?v1 ?v3))) (?v_1 (f154 f155 (f164 ?v2 ?v4)))) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f164 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f164 ?v2 ?v3)) ?v_1)))))) (= (f306 ?v0) f1)))) +(assert (forall ((?v0 S16) (?v1 S102) (?v2 S102)) (=> (forall ((?v3 S18) (?v4 S18)) (let ((?v_0 (f154 f155 (f162 ?v1 ?v3))) (?v_1 (f154 f155 (f162 ?v2 ?v4)))) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f162 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f162 ?v2 ?v3)) ?v_1)))))) (= (f307 ?v0) f1)))) +(assert (forall ((?v0 S15) (?v1 S101) (?v2 S101)) (=> (forall ((?v3 Int) (?v4 Int)) (let ((?v_0 (f154 f155 (f160 ?v1 ?v3))) (?v_1 (f154 f155 (f160 ?v2 ?v4)))) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f160 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f160 ?v2 ?v3)) ?v_1)))))) (= (f312 ?v0) f1)))) +(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (not (exists ((?v1 S19)) (forall ((?v2 S18)) (= (f44 (f25 (f26 f27 (f21 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f21 ?v1 ?v2)) ?v0) f1))))))) +(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (not (exists ((?v1 S102)) (forall ((?v2 S18)) (= (f41 (f21 (f22 f23 (f162 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f162 ?v1 ?v2)) ?v0) f1))))))) +(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (not (exists ((?v1 S99)) (forall ((?v2 S18)) (= (f37 (f8 (f9 f10 (f154 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f154 ?v1 ?v2)) ?v0) f1))))))) +(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f316 (f43 ?v0)) f1)))) +(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f317 (f40 ?v0)) f1)))) +(assert (forall ((?v0 S21) (?v1 S19)) (=> (= (f306 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f44 (f25 (f26 f27 (f21 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f21 ?v1 ?v2)) ?v0) f1)) false)) false)))) +(assert (forall ((?v0 S16) (?v1 S102)) (=> (= (f307 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f41 (f21 (f22 f23 (f162 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f162 ?v1 ?v2)) ?v0) f1)) false)) false)))) +(assert (forall ((?v0 S15) (?v1 S99)) (=> (= (f312 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f37 (f8 (f9 f10 (f154 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f154 ?v1 ?v2)) ?v0) f1)) false)) false)))) +(assert (forall ((?v0 S24)) (= (= (f318 ?v0) f1) (forall ((?v1 S21) (?v2 S8)) (=> (= (f44 ?v2 ?v1) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v1) f1) (forall ((?v4 S8)) (=> (= (f24 (f28 ?v0 ?v4) ?v3) f1) (not (= (f44 ?v4 ?v1) f1))))))))))) +(assert (forall ((?v0 S30)) (= (= (f316 ?v0) f1) (forall ((?v1 S16) (?v2 S17)) (=> (= (f41 ?v2 ?v1) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v1) f1) (forall ((?v4 S17)) (=> (= (f20 (f42 ?v0 ?v4) ?v3) f1) (not (= (f41 ?v4 ?v1) f1))))))))))) +(assert (= (f307 f319) f1)) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (< (f154 f155 ?v0) (f154 f155 ?v1)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f320) f1)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (<= (f154 f155 ?v0) (f154 f155 ?v1)) (=> (<= (f154 f155 ?v2) (f154 f155 ?v3)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f320) f1))))) +(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (forall ((?v1 S16)) (=> (forall ((?v2 S17)) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v0) f1) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))) (forall ((?v2 S17)) (= (f20 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (forall ((?v1 S28)) (=> (forall ((?v2 S18)) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v0) f1) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))) (forall ((?v2 S18)) (= (f38 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (forall ((?v1 S26)) (=> (forall ((?v2 Int)) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v0) f1) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))) (forall ((?v2 Int)) (= (f34 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S16)) (=> (= (f41 ?v1 ?v2) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v2) f1) (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v2) f1)))))))) (= (f306 ?v0) f1)))) +(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S28)) (=> (= (f182 ?v1 ?v2) f1) (exists ((?v3 S18)) (and (= (f182 ?v3 ?v2) f1) (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v2) f1)))))))) (= (f307 ?v0) f1)))) +(assert (forall ((?v0 S6)) (=> (forall ((?v1 S8) (?v2 S21)) (=> (= (f44 ?v1 ?v2) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v2) f1) (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v2) f1)))))))) (= (f314 ?v0) f1)))) +(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 S26)) (=> (= (f179 ?v1 ?v2) f1) (exists ((?v3 Int)) (and (= (f179 ?v3 ?v2) f1) (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v2) f1)))))))) (= (f312 ?v0) f1)))) +(assert (forall ((?v0 S21) (?v1 S16) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (forall ((?v3 S17)) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (= (f20 ?v1 ?v4) f1))) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S16) (?v1 S28) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (forall ((?v3 S18)) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (= (f38 ?v1 ?v4) f1))) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S15) (?v1 S26) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (forall ((?v3 Int)) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (= (f34 ?v1 ?v4) f1))) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S21) (?v1 S16) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (forall ((?v3 S17)) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (= (f20 ?v1 ?v4) f1))) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S16) (?v1 S28) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (forall ((?v3 S18)) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (= (f38 ?v1 ?v4) f1))) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S15) (?v1 S26) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (forall ((?v3 Int)) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (= (f34 ?v1 ?v4) f1))) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S16)) (=> (= (f306 ?v0) f1) (=> (= (f41 ?v1 ?v2) f1) (=> (forall ((?v3 S17)) (=> (= (f41 ?v3 ?v2) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v2) f1)))) false))) false))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S28)) (=> (= (f307 ?v0) f1) (=> (= (f182 ?v1 ?v2) f1) (=> (forall ((?v3 S18)) (=> (= (f182 ?v3 ?v2) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v2) f1)))) false))) false))))) +(assert (forall ((?v0 S6) (?v1 S8) (?v2 S21)) (=> (= (f314 ?v0) f1) (=> (= (f44 ?v1 ?v2) f1) (=> (forall ((?v3 S8)) (=> (= (f44 ?v3 ?v2) f1) (=> (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v2) f1)))) false))) false))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 S26)) (=> (= (f312 ?v0) f1) (=> (= (f179 ?v1 ?v2) f1) (=> (forall ((?v3 Int)) (=> (= (f179 ?v3 ?v2) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v2) f1)))) false))) false))))) +(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (forall ((?v1 S16)) (=> (forall ((?v2 S17)) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v0) f1) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))) (forall ((?v2 S17)) (= (f20 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (forall ((?v1 S28)) (=> (forall ((?v2 S18)) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v0) f1) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))) (forall ((?v2 S18)) (= (f38 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S15)) (=> (= (f312 ?v0) f1) (forall ((?v1 S26)) (=> (forall ((?v2 Int)) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v0) f1) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))) (forall ((?v2 Int)) (= (f34 ?v1 ?v2) f1))))))) +(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f321 (f322 ?v0)) f1)))) +(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f323 (f324 ?v0)) f1)))) +(assert (= f303 (f325 f319))) +(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 f319)) f1) (< (f154 f155 ?v0) (f154 f155 ?v1))))) +(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f306 (f326 ?v0)) f1)))) +(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f307 (f325 ?v0)) f1)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 ?v2) f1) (= (f44 ?v_0 (f326 ?v2)) f1))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 ?v2) f1) (= (f41 ?v_0 (f325 ?v2)) f1))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 ?v2) f1) (= (f37 ?v_0 (f327 ?v2)) f1))))) +(assert (forall ((?v0 S16)) (=> (= (f305 ?v0) f1) (= (f325 ?v0) ?v0)))) +(assert (forall ((?v0 S16)) (= (f305 (f325 ?v0)) f1))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0))) (=> (= (f44 (f25 ?v_0 ?v1) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v2) f1) (= (f44 (f25 ?v_0 ?v3) (f326 ?v2)) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0))) (=> (= (f41 (f21 ?v_0 ?v1) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v2) f1) (= (f41 (f21 ?v_0 ?v3) (f325 ?v2)) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0))) (=> (= (f37 (f8 ?v_0 ?v1) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v2) f1) (= (f37 (f8 ?v_0 ?v3) (f327 ?v2)) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0)) (?v_1 (f326 ?v2))) (=> (= (f44 (f25 ?v_0 ?v1) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v_1) f1) (= (f44 (f25 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0)) (?v_1 (f325 ?v2))) (=> (= (f41 (f21 ?v_0 ?v1) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v_1) f1) (= (f41 (f21 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f327 ?v2))) (=> (= (f37 (f8 ?v_0 ?v1) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v_1) f1) (= (f37 (f8 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 S8) (?v1 S21)) (=> (= (f44 ?v0 ?v1) f1) (= (f44 ?v0 (f326 ?v1)) f1)))) +(assert (forall ((?v0 S17) (?v1 S16)) (=> (= (f41 ?v0 ?v1) f1) (= (f41 ?v0 (f325 ?v1)) f1)))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_1 (f26 f27 ?v0)) (?v_0 (f326 ?v2))) (=> (= (f44 (f25 ?v_1 ?v1) ?v_0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v_0) f1) (= (f44 (f25 ?v_1 ?v3) ?v_0) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_1 (f22 f23 ?v0)) (?v_0 (f325 ?v2))) (=> (= (f41 (f21 ?v_1 ?v1) ?v_0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v_0) f1) (= (f41 (f21 ?v_1 ?v3) ?v_0) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_1 (f9 f10 ?v0)) (?v_0 (f327 ?v2))) (=> (= (f37 (f8 ?v_1 ?v1) ?v_0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v_0) f1) (= (f37 (f8 ?v_1 ?v3) ?v_0) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0)) (?v_1 (f326 ?v2))) (=> (= (f44 (f25 ?v_0 ?v1) ?v_1) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v2) f1) (= (f44 (f25 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0)) (?v_1 (f325 ?v2))) (=> (= (f41 (f21 ?v_0 ?v1) ?v_1) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v2) f1) (= (f41 (f21 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f327 ?v2))) (=> (= (f37 (f8 ?v_0 ?v1) ?v_1) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v2) f1) (= (f37 (f8 ?v_0 ?v3) ?v_1) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 (f326 ?v2)) f1) (=> (=> (= (f44 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v3) (f326 ?v2)) f1) (=> (= (f44 (f25 (f26 f27 ?v3) ?v1) ?v2) f1) false))) false)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 (f325 ?v2)) f1) (=> (=> (= (f41 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v3) (f325 ?v2)) f1) (=> (= (f41 (f21 (f22 f23 ?v3) ?v1) ?v2) f1) false))) false)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 (f327 ?v2)) f1) (=> (=> (= (f37 ?v_0 ?v2) f1) false) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v3) (f327 ?v2)) f1) (=> (= (f37 (f8 (f9 f10 ?v3) ?v1) ?v2) f1) false))) false)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 (f326 ?v2)) f1) (=> (=> (= (f44 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v3) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v3) ?v1) (f326 ?v2)) f1) false))) false)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 (f325 ?v2)) f1) (=> (=> (= (f41 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v3) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v3) ?v1) (f325 ?v2)) f1) false))) false)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 (f327 ?v2)) f1) (=> (=> (= (f37 ?v_0 ?v2) f1) false) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v3) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v3) ?v1) (f327 ?v2)) f1) false))) false)))))) +(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (forall ((?v3 S17)) (not (= (f44 (f25 (f26 f27 ?v3) ?v3) (f326 ?v0)) f1))) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2)))))) +(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (forall ((?v3 S18)) (not (= (f41 (f21 (f22 f23 ?v3) ?v3) (f325 ?v0)) f1))) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2)))))) +(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (forall ((?v3 Int)) (not (= (f37 (f8 (f9 f10 ?v3) ?v3) (f327 ?v0)) f1))) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2)))))) +(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f321 (f328 ?v0)) f1)))) +(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f323 (f329 ?v0)) f1)))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S21) (?v5 S29)) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f326 ?v4)) f1) (=> (forall ((?v6 S18) (?v7 S18)) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v6) ?v7)) ?v4) f1) (= (f38 (f39 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 S18) (?v7 S18) (?v8 S18) (?v9 S18)) (let ((?v_0 (f21 (f22 f23 ?v6) ?v7))) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) ?v_0) (f326 ?v4)) f1) (=> (= (f44 (f25 (f26 f27 ?v_0) (f21 (f22 f23 ?v8) ?v9)) ?v4) f1) (=> (= (f38 (f39 ?v5 ?v6) ?v7) f1) (= (f38 (f39 ?v5 ?v8) ?v9) f1)))))) (= (f38 (f39 ?v5 ?v2) ?v3) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S6) (?v5 S30)) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f330 ?v4)) f1) (=> (forall ((?v6 S17) (?v7 S17)) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v6) ?v7)) ?v4) f1) (= (f20 (f42 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 S17) (?v7 S17) (?v8 S17) (?v9 S17)) (let ((?v_0 (f25 (f26 f27 ?v6) ?v7))) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) ?v_0) (f330 ?v4)) f1) (=> (= (f30 (f12 (f13 f14 ?v_0) (f25 (f26 f27 ?v8) ?v9)) ?v4) f1) (=> (= (f20 (f42 ?v5 ?v6) ?v7) f1) (= (f20 (f42 ?v5 ?v8) ?v9) f1)))))) (= (f20 (f42 ?v5 ?v2) ?v3) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S11) (?v5 S27)) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) (f8 (f9 f10 ?v2) ?v3)) (f331 ?v4)) f1) (=> (forall ((?v6 Int) (?v7 Int)) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) (f8 (f9 f10 ?v6) ?v7)) ?v4) f1) (= (f34 (f35 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 Int) (?v7 Int) (?v8 Int) (?v9 Int)) (let ((?v_0 (f8 (f9 f10 ?v6) ?v7))) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) ?v_0) (f331 ?v4)) f1) (=> (= (f33 (f16 (f17 f18 ?v_0) (f8 (f9 f10 ?v8) ?v9)) ?v4) f1) (=> (= (f34 (f35 ?v5 ?v6) ?v7) f1) (= (f34 (f35 ?v5 ?v8) ?v9) f1)))))) (= (f34 (f35 ?v5 ?v2) ?v3) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S16)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v1) (f326 ?v2)) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v1) ?v2) f1) (= (f20 ?v3 ?v4) f1))) (=> (forall ((?v4 S17) (?v5 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v5) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v5) ?v1) (f326 ?v2)) f1) (=> (= (f20 ?v3 ?v5) f1) (= (f20 ?v3 ?v4) f1))))) (= (f20 ?v3 ?v0) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S28)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 ?v2)) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v1) ?v2) f1) (= (f38 ?v3 ?v4) f1))) (=> (forall ((?v4 S18) (?v5 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v5) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v5) ?v1) (f325 ?v2)) f1) (=> (= (f38 ?v3 ?v5) f1) (= (f38 ?v3 ?v4) f1))))) (= (f38 ?v3 ?v0) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S26)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v1) (f327 ?v2)) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v1) ?v2) f1) (= (f34 ?v3 ?v4) f1))) (=> (forall ((?v4 Int) (?v5 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v5) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v5) ?v1) (f327 ?v2)) f1) (=> (= (f34 ?v3 ?v5) f1) (= (f34 ?v3 ?v4) f1))))) (= (f34 ?v3 ?v0) f1)))))) +(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S16)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v1) (f326 ?v2)) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v4) ?v2) f1) (= (f20 ?v3 ?v4) f1))) (=> (forall ((?v4 S17) (?v5 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v4) (f326 ?v2)) f1) (=> (= (f44 (f25 (f26 f27 ?v4) ?v5) ?v2) f1) (=> (= (f20 ?v3 ?v4) f1) (= (f20 ?v3 ?v5) f1))))) (= (f20 ?v3 ?v1) f1)))))) +(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S28)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 ?v2)) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v4) ?v2) f1) (= (f38 ?v3 ?v4) f1))) (=> (forall ((?v4 S18) (?v5 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v4) (f325 ?v2)) f1) (=> (= (f41 (f21 (f22 f23 ?v4) ?v5) ?v2) f1) (=> (= (f38 ?v3 ?v4) f1) (= (f38 ?v3 ?v5) f1))))) (= (f38 ?v3 ?v1) f1)))))) +(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S26)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v1) (f327 ?v2)) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v4) ?v2) f1) (= (f34 ?v3 ?v4) f1))) (=> (forall ((?v4 Int) (?v5 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v4) (f327 ?v2)) f1) (=> (= (f37 (f8 (f9 f10 ?v4) ?v5) ?v2) f1) (=> (= (f34 ?v3 ?v4) f1) (= (f34 ?v3 ?v5) f1))))) (= (f34 ?v3 ?v1) f1)))))) +(assert (forall ((?v0 S18)) (= (f160 f315 (f154 f155 ?v0)) ?v0))) +(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f154 f155 (f160 f315 ?v0)) ?v0)))) +(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f154 f155 (f160 f315 ?v0)) 0)))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/red-exp.smt2 b/test/regress/regress1/nl/red-exp.smt2 new file mode 100644 index 000000000..5dc5258e2 --- /dev/null +++ b/test/regress/regress1/nl/red-exp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) + +(declare-fun a () Real) +(declare-fun b () Real) + +(assert (or (= a (* b b)) (and (= a 9) (= b 3)))) +(assert (not (= (* a a) (* b b b b)))) +(check-sat) diff --git a/test/regress/regress1/nl/rewriting-sums.smt2 b/test/regress/regress1/nl/rewriting-sums.smt2 new file mode 100644 index 000000000..ca2edf024 --- /dev/null +++ b/test/regress/regress1/nl/rewriting-sums.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NIA) +(set-info :status unsat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) + + +(assert (or (= x 5) (= x 7) (= x 9))) + +(assert (or (= y (+ x 1)) (= y (+ x 2)))) + +(assert (or (= z (+ y 5)) (= z (+ y 10)))) + +(assert (> (* z z) 1000000000)) + +(check-sat) diff --git a/test/regress/regress1/nl/shifting.smt2 b/test/regress/regress1/nl/shifting.smt2 new file mode 100644 index 000000000..320c92d58 --- /dev/null +++ b/test/regress/regress1/nl/shifting.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: sat +(set-logic QF_NIRA) +(set-info :status sat) +(declare-fun pi () Real) + +(assert (and (< 3.0 pi) (< pi 3.5))) + +(declare-fun y () Real) +(assert (and (<= (- pi) y) (<= y pi))) + +(declare-fun s () Int) + +(declare-fun z () Real) + +(assert (= z (* 2 pi s))) + +(assert (> z 60)) + +(check-sat) diff --git a/test/regress/regress1/nl/shifting2.smt2 b/test/regress/regress1/nl/shifting2.smt2 new file mode 100644 index 000000000..c5e805c50 --- /dev/null +++ b/test/regress/regress1/nl/shifting2.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NIRA) +(set-info :status unsat) +(declare-fun pi () Real) + +(assert (and (< 3.0 pi) (< pi 3.5))) + +(declare-fun y () Real) +(assert (and (< (- pi) y) (< y pi))) + +(declare-fun s () Int) + +(declare-fun z () Real) + +(assert (= z (+ y (* 2 pi s)))) + +(assert (and (< (- pi) z) (< z pi))) + +(assert (not (= z y))) + +(check-sat) diff --git a/test/regress/regress1/nl/siegel-nl-bases.smt2 b/test/regress/regress1/nl/siegel-nl-bases.smt2 deleted file mode 100644 index cf6e3ab5e..000000000 --- a/test/regress/regress1/nl/siegel-nl-bases.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -; COMMAND-LINE: --nl-ext -; EXPECT: unsat -(set-logic QF_NIA) -(declare-const n Int) -(declare-const i1 Int) -(declare-const i2 Int) -(declare-const j1 Int) -(declare-const j2 Int) -(assert (>= n 0)) -(assert (not (= i1 i2))) -(assert (<= 0 i1)) -(assert (<= i1 j1)) -(assert (< j1 n)) -(assert (<= 0 i2)) -(assert (<= i2 j2)) -(assert (< j2 n)) -(assert (or - (= (+ (* i1 n) j1) (+ (* i2 n) j2)) - (= (+ (* i1 n) j1) (+ (* j2 n) i2)) - (= (+ (* j1 n) i1) (+ (* i2 n) j2)) - (= (+ (* j1 n) i1) (+ (* j2 n) i2)))) -(check-sat) diff --git a/test/regress/regress1/nl/simple-mono-unsat.smt2 b/test/regress/regress1/nl/simple-mono-unsat.smt2 new file mode 100644 index 000000000..b82b7ad7c --- /dev/null +++ b/test/regress/regress1/nl/simple-mono-unsat.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) + +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) + +(assert (or (= a 4) (= a 3))) + +(assert (> b 0)) +(assert (> c 0)) + +(assert (< (* a b c d d) 0)) + +(check-sat) diff --git a/test/regress/regress1/nl/simple-mono.smt2 b/test/regress/regress1/nl/simple-mono.smt2 new file mode 100644 index 000000000..3d4adad28 --- /dev/null +++ b/test/regress/regress1/nl/simple-mono.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) + + +(assert (> z 0)) +(assert (> x y)) + +;(assert (not (> (* x z) (* y z)))) +(assert (< (* x z) (* y z))) + + +(check-sat) diff --git a/test/regress/regress1/nl/sin-compare-across-phase.smt2 b/test/regress/regress1/nl/sin-compare-across-phase.smt2 new file mode 100644 index 000000000..f5d7fe32d --- /dev/null +++ b/test/regress/regress1/nl/sin-compare-across-phase.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (< (sin 3.1) (sin 3.3))) +(check-sat) diff --git a/test/regress/regress1/nl/sin-compare.smt2 b/test/regress/regress1/nl/sin-compare.smt2 new file mode 100644 index 000000000..790d7037f --- /dev/null +++ b/test/regress/regress1/nl/sin-compare.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) +(check-sat) diff --git a/test/regress/regress1/nl/sin-init-tangents.smt2 b/test/regress/regress1/nl/sin-init-tangents.smt2 new file mode 100644 index 000000000..e71ab231f --- /dev/null +++ b/test/regress/regress1/nl/sin-init-tangents.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(assert (or (> (sin 0.8) 0.9) (< (sin (- 0.7)) (- 0.75)) (= (sin 3.0) 0.8))) +(check-sat) diff --git a/test/regress/regress1/nl/sin-sign.smt2 b/test/regress/regress1/nl/sin-sign.smt2 new file mode 100644 index 000000000..9b05a3d52 --- /dev/null +++ b/test/regress/regress1/nl/sin-sign.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) +(check-sat) diff --git a/test/regress/regress1/nl/sin-sym2.smt2 b/test/regress/regress1/nl/sin-sym2.smt2 new file mode 100644 index 000000000..2e5d4eac2 --- /dev/null +++ b/test/regress/regress1/nl/sin-sym2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (and (< 0.0 x) (< x 1.0) (< 0.0 y) (< y 1.0))) +(assert (= (+ (sin x) (sin y)) 0.0)) +(assert (not (= (+ x y) 0.0))) +(check-sat) diff --git a/test/regress/regress1/nl/sin1-lb.smt2 b/test/regress/regress1/nl/sin1-lb.smt2 new file mode 100644 index 000000000..f8070cdb8 --- /dev/null +++ b/test/regress/regress1/nl/sin1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 1) 0.842)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2 new file mode 100644 index 000000000..d6275c6e8 --- /dev/null +++ b/test/regress/regress1/nl/sin1-sat.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 1) 0.84)) +(assert (< (sin 1) 0.85)) +(assert (< (- x (sin 1)) 0.000001)) +(assert (< (- (sin 1) x) 0.000001)) + +(check-sat) diff --git a/test/regress/regress1/nl/sin1-ub.smt2 b/test/regress/regress1/nl/sin1-ub.smt2 new file mode 100644 index 000000000..47d322a77 --- /dev/null +++ b/test/regress/regress1/nl/sin1-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 1) 0.8414)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress1/nl/sin2-lb.smt2 b/test/regress/regress1/nl/sin2-lb.smt2 new file mode 100644 index 000000000..686708230 --- /dev/null +++ b/test/regress/regress1/nl/sin2-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 2) 0.96)) +(assert (= x (sin 2))) + +(check-sat) diff --git a/test/regress/regress1/nl/sin2-ub.smt2 b/test/regress/regress1/nl/sin2-ub.smt2 new file mode 100644 index 000000000..51c9eb8a9 --- /dev/null +++ b/test/regress/regress1/nl/sin2-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 2) 0.901)) +(assert (= x (sin 2))) + +(check-sat) diff --git a/test/regress/regress1/nl/sqrt-problem-1.smt2 b/test/regress/regress1/nl/sqrt-problem-1.smt2 new file mode 100644 index 000000000..e74af3a2d --- /dev/null +++ b/test/regress/regress1/nl/sqrt-problem-1.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --nl-ext-tplanes +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun X () Real) +(declare-fun |sqrt{10}| () Real) +(declare-fun |sqrt{8}| () Real) +(assert (let ((.def_48 (<= X (to_real 300)))) +(let ((.def_47 (<= (to_real (- 300)) X))) +(let ((.def_49 (and .def_47 .def_48))) +(let ((.def_44 (<= |sqrt{10}| (to_real 300)))) +(let ((.def_43 (<= (to_real (- 300)) |sqrt{10}|))) +(let ((.def_45 (and .def_43 .def_44))) +(let ((.def_40 (<= |sqrt{8}| (to_real 300)))) +(let ((.def_39 (<= (to_real (- 300)) |sqrt{8}|))) +(let ((.def_41 (and .def_39 .def_40))) +(let ((.def_35 (<= (to_real 0) |sqrt{8}|))) +(let ((.def_31 (* |sqrt{8}| |sqrt{8}|))) +(let ((.def_33 (= .def_31 (to_real 3)))) +(let ((.def_29 (<= (to_real 0) |sqrt{10}|))) +(let ((.def_26 (* |sqrt{10}| |sqrt{10}|))) +(let ((.def_27 (= X .def_26))) +(let ((.def_21 (<= X (to_real 2)))) +(let ((.def_19 (<= (to_real 0) X))) +(let ((.def_22 (and .def_19 .def_21))) +(let ((.def_23 (not .def_22))) +(let ((.def_11 (+ |sqrt{10}| |sqrt{8}|))) +(let ((.def_15 (<= (/ 63 20) .def_11))) +(let ((.def_16 (not .def_15))) +(let ((.def_24 (or .def_16 .def_23))) +(let ((.def_25 (not .def_24))) +(let ((.def_28 (and .def_25 .def_27))) +(let ((.def_30 (and .def_28 .def_29))) +(let ((.def_34 (and .def_30 .def_33))) +(let ((.def_36 (and .def_34 .def_35))) +(let ((.def_42 (and .def_36 .def_41))) +(let ((.def_46 (and .def_42 .def_45))) +(let ((.def_50 (and .def_46 .def_49))) +.def_50)))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/sugar-ident-2.smt2 b/test/regress/regress1/nl/sugar-ident-2.smt2 new file mode 100644 index 000000000..84c224715 --- /dev/null +++ b/test/regress/regress1/nl/sugar-ident-2.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(declare-fun x5 () Real) + +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) + +(assert (= a2 (and (> (sin 1.0) 0.0) (> (cot 1.0) (/ (cos 1.0) (sin 1.0)))))) +(assert (= a7 (> (* (sec 1.0) (cos 1.0)) 1.0))) + +(assert (or +a2 +a7 +)) + +(check-sat) diff --git a/test/regress/regress1/nl/sugar-ident-3.smt2 b/test/regress/regress1/nl/sugar-ident-3.smt2 new file mode 100644 index 000000000..ab50bcb1d --- /dev/null +++ b/test/regress/regress1/nl/sugar-ident-3.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun a6 () Bool) +(assert (= a6 (> (* (csc 1.0) (sin 1.0)) 1.0))) +(assert a6) +(check-sat) diff --git a/test/regress/regress1/nl/sugar-ident.smt2 b/test/regress/regress1/nl/sugar-ident.smt2 new file mode 100644 index 000000000..95dbbc5fc --- /dev/null +++ b/test/regress/regress1/nl/sugar-ident.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x1 () Real) +(declare-fun x2 () Real) +(declare-fun x3 () Real) +(declare-fun x4 () Real) +(declare-fun x5 () Real) + +(declare-fun a1 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) + +(assert (= a1 (not (= (sin (arcsin x1)) x1)))) +(assert (= a3 (< (arccos x3) 0))) +(assert (= a4 (> (arctan x4) 1.8))) + +(assert (or a1 a3 a4)) + +(check-sat) diff --git a/test/regress/regress1/nl/tan-rewrite2.smt2 b/test/regress/regress1/nl/tan-rewrite2.smt2 new file mode 100644 index 000000000..af39f7559 --- /dev/null +++ b/test/regress/regress1/nl/tan-rewrite2.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) + + +(assert (= (tan x) (sin x))) +(assert (> (cos x) 0)) +(assert (not (= (cos x) 1))) +(assert (not (= (sin x) 0))) + +(check-sat) diff --git a/test/regress/regress1/nl/zero-subset.smt2 b/test/regress/regress1/nl/zero-subset.smt2 new file mode 100644 index 000000000..a8ce65b02 --- /dev/null +++ b/test/regress/regress1/nl/zero-subset.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) +(declare-fun e () Real) + +(assert (= (* a b c d) 0)) + +(assert (not (= (* a b c d e) 0))) + +(check-sat) |