src/HOL/SMT_Examples/SMT_Examples.certs

--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Sep 26 07:56:54 2016 +0200
@@ -6057,3 +6057,579 @@
 (let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
 (mp (asserted $x32) @x42 false))))))))
 
+0b997744cf42fde45b98a34c933b0698332e657f 113 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x228 (mod x$ 2)))
+(let ((?x262 (* (- 1) ?x228)))
+(let ((?x31 (modulo$ x$ 2)))
+(let ((?x263 (+ ?x31 ?x262)))
+(let (($x280 (>= ?x263 0)))
+(let (($x264 (= ?x263 0)))
+(let (($x205 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (modulo$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9))
+))
+(let (($x181 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x136 (mod ?v0 ?v1)))
+(let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?v1 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?v1 0)))
+(let ((?x175 (ite $x78 ?v0 ?x170)))
+(let ((?x135 (modulo$ ?v0 ?v1)))
+(= ?x135 ?x175))))))))))) :qid k!9))
+))
+(let ((?x136 (mod ?1 ?0)))
+(let ((?x93 (* (- 1) ?0)))
+(let ((?x90 (* (- 1) ?1)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let (($x111 (<= ?0 0)))
+(let ((?x170 (ite $x111 ?x150 ?x136)))
+(let (($x78 (= ?0 0)))
+(let ((?x175 (ite $x78 ?1 ?x170)))
+(let ((?x135 (modulo$ ?1 ?0)))
+(let (($x178 (= ?x135 ?x175)))
+(let (($x142 (forall ((?v0 Int) (?v1 Int) )(! (let (($x78 (= ?v1 0)))
+(let ((?x140 (ite $x78 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x135 (modulo$ ?v0 ?v1)))
+(= ?x135 ?x140)))) :qid k!9))
+))
+(let (($x164 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x93 (* (- 1) ?v1)))
+(let ((?x90 (* (- 1) ?v0)))
+(let ((?x144 (mod ?x90 ?x93)))
+(let ((?x150 (* (- 1) ?x144)))
+(let ((?x136 (mod ?v0 ?v1)))
+(let (($x79 (< 0 ?v1)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let (($x78 (= ?v1 0)))
+(let ((?x158 (ite $x78 ?v0 ?x155)))
+(let ((?x135 (modulo$ ?v0 ?v1)))
+(= ?x135 ?x158))))))))))) :qid k!9))
+))
+(let ((@x169 (monotonicity (rewrite (= (< 0 ?0) (not $x111))) (= (ite (< 0 ?0) ?x136 ?x150) (ite (not $x111) ?x136 ?x150)))))
+(let ((@x174 (trans @x169 (rewrite (= (ite (not $x111) ?x136 ?x150) ?x170)) (= (ite (< 0 ?0) ?x136 ?x150) ?x170))))
+(let ((@x177 (monotonicity @x174 (= (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150)) ?x175))))
+(let ((@x180 (monotonicity @x177 (= (= ?x135 (ite $x78 ?1 (ite (< 0 ?0) ?x136 ?x150))) $x178))))
+(let (($x79 (< 0 ?0)))
+(let ((?x155 (ite $x79 ?x136 ?x150)))
+(let ((?x158 (ite $x78 ?1 ?x155)))
+(let (($x161 (= ?x135 ?x158)))
+(let (($x162 (= (= ?x135 (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))))) $x161)))
+(let ((@x146 (monotonicity (rewrite (= (- ?1) ?x90)) (rewrite (= (- ?0) ?x93)) (= (mod (- ?1) (- ?0)) ?x144))))
+(let ((@x154 (trans (monotonicity @x146 (= (- (mod (- ?1) (- ?0))) (- ?x144))) (rewrite (= (- ?x144) ?x150)) (= (- (mod (- ?1) (- ?0))) ?x150))))
+(let ((@x157 (monotonicity @x154 (= (ite $x79 ?x136 (- (mod (- ?1) (- ?0)))) ?x155))))
+(let ((@x160 (monotonicity @x157 (= (ite $x78 ?1 (ite $x79 ?x136 (- (mod (- ?1) (- ?0))))) ?x158))))
+(let ((@x185 (trans (quant-intro (monotonicity @x160 $x162) (= $x142 $x164)) (quant-intro @x180 (= $x164 $x181)) (= $x142 $x181))))
+(let ((@x196 (mp~ (mp (asserted $x142) @x185 $x181) (nnf-pos (refl (~ $x178 $x178)) (~ $x181 $x181)) $x181)))
+(let ((@x210 (mp @x196 (quant-intro (refl (= $x178 $x178)) (= $x181 $x205)) $x205)))
+(let (($x270 (or (not $x205) $x264)))
+(let ((?x225 (* (- 1) 2)))
+(let ((?x224 (* (- 1) x$)))
+(let ((?x226 (mod ?x224 ?x225)))
+(let ((?x227 (* (- 1) ?x226)))
+(let (($x223 (<= 2 0)))
+(let ((?x229 (ite $x223 ?x227 ?x228)))
+(let (($x222 (= 2 0)))
+(let ((?x230 (ite $x222 x$ ?x229)))
+(let (($x231 (= ?x31 ?x230)))
+(let ((@x244 (monotonicity (monotonicity (rewrite (= ?x225 (- 2))) (= ?x226 (mod ?x224 (- 2)))) (= ?x227 (* (- 1) (mod ?x224 (- 2)))))))
+(let ((@x247 (monotonicity (rewrite (= $x223 false)) @x244 (= ?x229 (ite false (* (- 1) (mod ?x224 (- 2))) ?x228)))))
+(let ((@x251 (trans @x247 (rewrite (= (ite false (* (- 1) (mod ?x224 (- 2))) ?x228) ?x228)) (= ?x229 ?x228))))
+(let ((@x254 (monotonicity (rewrite (= $x222 false)) @x251 (= ?x230 (ite false x$ ?x228)))))
+(let ((@x261 (monotonicity (trans @x254 (rewrite (= (ite false x$ ?x228) ?x228)) (= ?x230 ?x228)) (= $x231 (= ?x31 ?x228)))))
+(let ((@x274 (monotonicity (trans @x261 (rewrite (= (= ?x31 ?x228) $x264)) (= $x231 $x264)) (= (or (not $x205) $x231) $x270))))
+(let ((@x277 (trans @x274 (rewrite (= $x270 $x270)) (= (or (not $x205) $x231) $x270))))
+(let ((@x278 (mp ((_ quant-inst x$ 2) (or (not $x205) $x231)) @x277 $x270)))
+(let ((@x332 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x264) $x280)) (unit-resolution @x278 @x210 $x264) $x280)))
+(let (($x305 (>= ?x228 0)))
+(let (($x64 (>= ?x31 0)))
+(let (($x67 (not $x64)))
+(let (($x36 (not (<= (+ x$ 1) (+ x$ (+ (* 2 ?x31) 1))))))
+(let ((@x69 (monotonicity (rewrite (= (>= (* 2 ?x31) 0) $x64)) (= (not (>= (* 2 ?x31) 0)) $x67))))
+(let ((?x32 (* 2 ?x31)))
+(let ((?x47 (+ 1 x$ ?x32)))
+(let (($x52 (<= (+ 1 x$) ?x47)))
+(let (($x55 (not $x52)))
+(let ((@x63 (monotonicity (rewrite (= $x52 (>= ?x32 0))) (= $x55 (not (>= ?x32 0))))))
+(let ((@x46 (monotonicity (rewrite (= (+ ?x32 1) (+ 1 ?x32))) (= (+ x$ (+ ?x32 1)) (+ x$ (+ 1 ?x32))))))
+(let ((@x51 (trans @x46 (rewrite (= (+ x$ (+ 1 ?x32)) ?x47)) (= (+ x$ (+ ?x32 1)) ?x47))))
+(let ((@x54 (monotonicity (rewrite (= (+ x$ 1) (+ 1 x$))) @x51 (= (<= (+ x$ 1) (+ x$ (+ ?x32 1))) $x52))))
+(let ((@x73 (trans (monotonicity @x54 (= $x36 $x55)) (trans @x63 @x69 (= $x55 $x67)) (= $x36 $x67))))
+(let ((@x74 (mp (asserted $x36) @x73 $x67)))
+((_ th-lemma arith farkas -1 1 1) @x74 (unit-resolution ((_ th-lemma arith) (or false $x305)) (true-axiom true) $x305) @x332 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+2e67f9e254b2a35a9d35027c6e63de01bc5086bd 112 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x224 (mod x$ 2)))
+(let (($x318 (>= ?x224 2)))
+(let (($x319 (not $x318)))
+(let ((?x258 (* (- 1) ?x224)))
+(let ((?x29 (modulo$ x$ 2)))
+(let ((?x259 (+ ?x29 ?x258)))
+(let (($x275 (<= ?x259 0)))
+(let (($x260 (= ?x259 0)))
+(let (($x201 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (modulo$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!9))
+))
+(let (($x177 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x132 (mod ?v0 ?v1)))
+(let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?v1 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?v1 0)))
+(let ((?x171 (ite $x74 ?v0 ?x166)))
+(let ((?x131 (modulo$ ?v0 ?v1)))
+(= ?x131 ?x171))))))))))) :qid k!9))
+))
+(let ((?x132 (mod ?1 ?0)))
+(let ((?x89 (* (- 1) ?0)))
+(let ((?x86 (* (- 1) ?1)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let (($x107 (<= ?0 0)))
+(let ((?x166 (ite $x107 ?x146 ?x132)))
+(let (($x74 (= ?0 0)))
+(let ((?x171 (ite $x74 ?1 ?x166)))
+(let ((?x131 (modulo$ ?1 ?0)))
+(let (($x174 (= ?x131 ?x171)))
+(let (($x138 (forall ((?v0 Int) (?v1 Int) )(! (let (($x74 (= ?v1 0)))
+(let ((?x136 (ite $x74 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x131 (modulo$ ?v0 ?v1)))
+(= ?x131 ?x136)))) :qid k!9))
+))
+(let (($x160 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x89 (* (- 1) ?v1)))
+(let ((?x86 (* (- 1) ?v0)))
+(let ((?x140 (mod ?x86 ?x89)))
+(let ((?x146 (* (- 1) ?x140)))
+(let ((?x132 (mod ?v0 ?v1)))
+(let (($x75 (< 0 ?v1)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let (($x74 (= ?v1 0)))
+(let ((?x154 (ite $x74 ?v0 ?x151)))
+(let ((?x131 (modulo$ ?v0 ?v1)))
+(= ?x131 ?x154))))))))))) :qid k!9))
+))
+(let ((@x165 (monotonicity (rewrite (= (< 0 ?0) (not $x107))) (= (ite (< 0 ?0) ?x132 ?x146) (ite (not $x107) ?x132 ?x146)))))
+(let ((@x170 (trans @x165 (rewrite (= (ite (not $x107) ?x132 ?x146) ?x166)) (= (ite (< 0 ?0) ?x132 ?x146) ?x166))))
+(let ((@x173 (monotonicity @x170 (= (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146)) ?x171))))
+(let ((@x176 (monotonicity @x173 (= (= ?x131 (ite $x74 ?1 (ite (< 0 ?0) ?x132 ?x146))) $x174))))
+(let (($x75 (< 0 ?0)))
+(let ((?x151 (ite $x75 ?x132 ?x146)))
+(let ((?x154 (ite $x74 ?1 ?x151)))
+(let (($x157 (= ?x131 ?x154)))
+(let (($x158 (= (= ?x131 (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))))) $x157)))
+(let ((@x142 (monotonicity (rewrite (= (- ?1) ?x86)) (rewrite (= (- ?0) ?x89)) (= (mod (- ?1) (- ?0)) ?x140))))
+(let ((@x150 (trans (monotonicity @x142 (= (- (mod (- ?1) (- ?0))) (- ?x140))) (rewrite (= (- ?x140) ?x146)) (= (- (mod (- ?1) (- ?0))) ?x146))))
+(let ((@x153 (monotonicity @x150 (= (ite $x75 ?x132 (- (mod (- ?1) (- ?0)))) ?x151))))
+(let ((@x156 (monotonicity @x153 (= (ite $x74 ?1 (ite $x75 ?x132 (- (mod (- ?1) (- ?0))))) ?x154))))
+(let ((@x181 (trans (quant-intro (monotonicity @x156 $x158) (= $x138 $x160)) (quant-intro @x176 (= $x160 $x177)) (= $x138 $x177))))
+(let ((@x192 (mp~ (mp (asserted $x138) @x181 $x177) (nnf-pos (refl (~ $x174 $x174)) (~ $x177 $x177)) $x177)))
+(let ((@x206 (mp @x192 (quant-intro (refl (= $x174 $x174)) (= $x177 $x201)) $x201)))
+(let (($x266 (or (not $x201) $x260)))
+(let ((?x221 (* (- 1) 2)))
+(let ((?x220 (* (- 1) x$)))
+(let ((?x222 (mod ?x220 ?x221)))
+(let ((?x223 (* (- 1) ?x222)))
+(let (($x219 (<= 2 0)))
+(let ((?x225 (ite $x219 ?x223 ?x224)))
+(let (($x218 (= 2 0)))
+(let ((?x226 (ite $x218 x$ ?x225)))
+(let (($x227 (= ?x29 ?x226)))
+(let ((@x240 (monotonicity (monotonicity (rewrite (= ?x221 (- 2))) (= ?x222 (mod ?x220 (- 2)))) (= ?x223 (* (- 1) (mod ?x220 (- 2)))))))
+(let ((@x243 (monotonicity (rewrite (= $x219 false)) @x240 (= ?x225 (ite false (* (- 1) (mod ?x220 (- 2))) ?x224)))))
+(let ((@x247 (trans @x243 (rewrite (= (ite false (* (- 1) (mod ?x220 (- 2))) ?x224) ?x224)) (= ?x225 ?x224))))
+(let ((@x250 (monotonicity (rewrite (= $x218 false)) @x247 (= ?x226 (ite false x$ ?x224)))))
+(let ((@x257 (monotonicity (trans @x250 (rewrite (= (ite false x$ ?x224) ?x224)) (= ?x226 ?x224)) (= $x227 (= ?x29 ?x224)))))
+(let ((@x270 (monotonicity (trans @x257 (rewrite (= (= ?x29 ?x224) $x260)) (= $x227 $x260)) (= (or (not $x201) $x227) $x266))))
+(let ((@x273 (trans @x270 (rewrite (= $x266 $x266)) (= (or (not $x201) $x227) $x266))))
+(let ((@x274 (mp ((_ quant-inst x$ 2) (or (not $x201) $x227)) @x273 $x266)))
+(let ((@x331 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x260) $x275)) (unit-resolution @x274 @x206 $x260) $x275)))
+(let (($x63 (>= ?x29 2)))
+(let ((?x37 (* 2 ?x29)))
+(let (($x56 (>= ?x37 3)))
+(let (($x46 (< (+ x$ ?x37) (+ 3 x$))))
+(let (($x49 (not $x46)))
+(let ((@x58 (monotonicity (rewrite (= $x46 (not $x56))) (= $x49 (not (not $x56))))))
+(let ((@x67 (trans (trans @x58 (rewrite (= (not (not $x56)) $x56)) (= $x49 $x56)) (rewrite (= $x56 $x63)) (= $x49 $x63))))
+(let ((@x42 (monotonicity (rewrite (= (+ ?x29 ?x29) ?x37)) (= (+ x$ (+ ?x29 ?x29)) (+ x$ ?x37)))))
+(let ((@x48 (monotonicity @x42 (rewrite (= (+ x$ 3) (+ 3 x$))) (= (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)) $x46))))
+(let ((@x51 (monotonicity @x48 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x49))))
+(let ((@x69 (trans @x51 @x67 (= (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3))) $x63))))
+(let ((@x70 (mp (asserted (not (< (+ x$ (+ ?x29 ?x29)) (+ x$ 3)))) @x69 $x63)))
+((_ th-lemma arith farkas -1 1 1) @x70 @x331 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+b6d44e20599d4862894eecfa4c98fcb043a6336d 348 0
+unsat
+((set-logic <null>)
+(proof
+(let ((?x96 (map$ uu$ xs$)))
+(let ((?x97 (eval_dioph$ ks$ ?x96)))
+(let ((?x424 (+ l$ ?x97)))
+(let ((?x425 (mod ?x424 2)))
+(let (($x482 (>= ?x425 2)))
+(let (($x564 (not $x482)))
+(let ((@x26 (true-axiom true)))
+(let ((?x369 (* (- 1) l$)))
+(let ((?x93 (eval_dioph$ ks$ xs$)))
+(let ((?x678 (+ ?x93 ?x369)))
+(let (($x679 (<= ?x678 0)))
+(let (($x95 (= ?x93 l$)))
+(let ((?x110 (* (- 1) ?x97)))
+(let ((?x111 (+ l$ ?x110)))
+(let ((?x114 (divide$ ?x111 2)))
+(let ((?x101 (map$ uua$ xs$)))
+(let ((?x102 (eval_dioph$ ks$ ?x101)))
+(let (($x117 (= ?x102 ?x114)))
+(let (($x282 (not $x117)))
+(let ((?x99 (modulo$ l$ 2)))
+(let ((?x98 (modulo$ ?x97 2)))
+(let (($x100 (= ?x98 ?x99)))
+(let (($x281 (not $x100)))
+(let (($x283 (or $x281 $x282)))
+(let (($x465 (>= ?x425 0)))
+(let ((?x496 (* (- 2) ?x102)))
+(let ((?x497 (+ ?x93 ?x110 ?x496)))
+(let (($x504 (<= ?x497 0)))
+(let (($x498 (= ?x497 0)))
+(let (($x304 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :pattern ( (eval_dioph$ ?v0 (map$ uua$ ?v1)) ) :qid k!19))
+))
+(let (($x85 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?v0 (map$ uu$ ?v1))) (* (- 2) (eval_dioph$ ?v0 (map$ uua$ ?v1))))))
+(= ?x83 0))) :qid k!19))
+))
+(let ((?x45 (eval_dioph$ ?1 ?0)))
+(let ((?x83 (+ ?x45 (* (- 1) (eval_dioph$ ?1 (map$ uu$ ?0))) (* (- 2) (eval_dioph$ ?1 (map$ uua$ ?0))))))
+(let (($x79 (= ?x83 0)))
+(let (($x58 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x56 (+ (* (eval_dioph$ ?v0 (map$ uua$ ?v1)) 2) ?x48)))
+(= ?x56 ?x45)))) :qid k!19))
+))
+(let (($x74 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (let ((?x45 (eval_dioph$ ?v0 ?v1)))
+(let ((?x54 (eval_dioph$ ?v0 (map$ uua$ ?v1))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?v0 (map$ uu$ ?v1))))
+(let ((?x66 (+ ?x48 ?x60)))
+(= ?x66 ?x45)))))) :qid k!19))
+))
+(let ((?x54 (eval_dioph$ ?1 (map$ uua$ ?0))))
+(let ((?x60 (* 2 ?x54)))
+(let ((?x48 (eval_dioph$ ?1 (map$ uu$ ?0))))
+(let ((?x66 (+ ?x48 ?x60)))
+(let (($x71 (= ?x66 ?x45)))
+(let ((@x65 (monotonicity (rewrite (= (* ?x54 2) ?x60)) (= (+ (* ?x54 2) ?x48) (+ ?x60 ?x48)))))
+(let ((@x70 (trans @x65 (rewrite (= (+ ?x60 ?x48) ?x66)) (= (+ (* ?x54 2) ?x48) ?x66))))
+(let ((@x76 (quant-intro (monotonicity @x70 (= (= (+ (* ?x54 2) ?x48) ?x45) $x71)) (= $x58 $x74))))
+(let ((@x89 (trans @x76 (quant-intro (rewrite (= $x71 $x79)) (= $x74 $x85)) (= $x58 $x85))))
+(let ((@x270 (mp~ (mp (asserted $x58) @x89 $x85) (nnf-pos (refl (~ $x79 $x79)) (~ $x85 $x85)) $x85)))
+(let ((@x309 (mp @x270 (quant-intro (refl (= $x79 $x79)) (= $x85 $x304)) $x304)))
+(let (($x502 (or (not $x304) $x498)))
+(let ((@x503 ((_ quant-inst ks$ xs$) $x502)))
+(let ((@x795 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x504)) (unit-resolution @x503 @x309 $x498) $x504)))
+(let (($x815 (not $x679)))
+(let (($x680 (>= ?x678 0)))
+(let ((?x592 (mod ?x97 2)))
+(let ((?x619 (* (- 1) ?x592)))
+(let ((?x511 (mod l$ 2)))
+(let ((?x538 (* (- 1) ?x511)))
+(let ((?x776 (* (- 1) ?x102)))
+(let ((?x759 (+ l$ ?x98 ?x776 ?x538 (* (- 1) (div l$ 2)) ?x619 (* (- 1) (div ?x97 2)))))
+(let (($x760 (>= ?x759 1)))
+(let (($x747 (not $x760)))
+(let ((?x674 (* (- 1) ?x99)))
+(let ((?x675 (+ ?x98 ?x674)))
+(let (($x676 (<= ?x675 0)))
+(let (($x284 (not $x283)))
+(let ((@x493 (hypothesis $x284)))
+(let ((@x781 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x676)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x676)))
+(let ((?x670 (* (- 1) ?x114)))
+(let ((?x671 (+ ?x102 ?x670)))
+(let (($x673 (>= ?x671 0)))
+(let ((@x787 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x673)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x673)))
+(let ((?x557 (div l$ 2)))
+(let ((?x570 (* (- 2) ?x557)))
+(let ((?x571 (+ l$ ?x538 ?x570)))
+(let (($x576 (<= ?x571 0)))
+(let (($x569 (= ?x571 0)))
+(let ((@x568 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x576)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x576)))
+(let ((?x620 (+ ?x98 ?x619)))
+(let (($x635 (<= ?x620 0)))
+(let (($x621 (= ?x620 0)))
+(let (($x318 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (modulo$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :pattern ( (modulo$ ?v0 ?v1) ) :qid k!22))
+))
+(let (($x245 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x200 (mod ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?v1 0)))
+(let ((?x239 (ite $x143 ?v0 ?x234)))
+(let ((?x199 (modulo$ ?v0 ?v1)))
+(= ?x199 ?x239))))))))))) :qid k!22))
+))
+(let ((?x200 (mod ?1 ?0)))
+(let ((?x157 (* (- 1) ?0)))
+(let ((?x154 (* (- 1) ?1)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let (($x175 (<= ?0 0)))
+(let ((?x234 (ite $x175 ?x214 ?x200)))
+(let (($x143 (= ?0 0)))
+(let ((?x239 (ite $x143 ?1 ?x234)))
+(let ((?x199 (modulo$ ?1 ?0)))
+(let (($x242 (= ?x199 ?x239)))
+(let (($x206 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0)))
+(let ((?x204 (ite $x143 ?v0 (ite (< 0 ?v1) (mod ?v0 ?v1) (- (mod (- ?v0) (- ?v1)))))))
+(let ((?x199 (modulo$ ?v0 ?v1)))
+(= ?x199 ?x204)))) :qid k!22))
+))
+(let (($x228 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x208 (mod ?x154 ?x157)))
+(let ((?x214 (* (- 1) ?x208)))
+(let ((?x200 (mod ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let (($x143 (= ?v1 0)))
+(let ((?x222 (ite $x143 ?v0 ?x219)))
+(let ((?x199 (modulo$ ?v0 ?v1)))
+(= ?x199 ?x222))))))))))) :qid k!22))
+))
+(let ((@x233 (monotonicity (rewrite (= (< 0 ?0) (not $x175))) (= (ite (< 0 ?0) ?x200 ?x214) (ite (not $x175) ?x200 ?x214)))))
+(let ((@x238 (trans @x233 (rewrite (= (ite (not $x175) ?x200 ?x214) ?x234)) (= (ite (< 0 ?0) ?x200 ?x214) ?x234))))
+(let ((@x241 (monotonicity @x238 (= (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214)) ?x239))))
+(let ((@x244 (monotonicity @x241 (= (= ?x199 (ite $x143 ?1 (ite (< 0 ?0) ?x200 ?x214))) $x242))))
+(let (($x144 (< 0 ?0)))
+(let ((?x219 (ite $x144 ?x200 ?x214)))
+(let ((?x222 (ite $x143 ?1 ?x219)))
+(let (($x225 (= ?x199 ?x222)))
+(let (($x226 (= (= ?x199 (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))))) $x225)))
+(let ((@x210 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (mod (- ?1) (- ?0)) ?x208))))
+(let ((@x218 (trans (monotonicity @x210 (= (- (mod (- ?1) (- ?0))) (- ?x208))) (rewrite (= (- ?x208) ?x214)) (= (- (mod (- ?1) (- ?0))) ?x214))))
+(let ((@x221 (monotonicity @x218 (= (ite $x144 ?x200 (- (mod (- ?1) (- ?0)))) ?x219))))
+(let ((@x224 (monotonicity @x221 (= (ite $x143 ?1 (ite $x144 ?x200 (- (mod (- ?1) (- ?0))))) ?x222))))
+(let ((@x249 (trans (quant-intro (monotonicity @x224 $x226) (= $x206 $x228)) (quant-intro @x244 (= $x228 $x245)) (= $x206 $x245))))
+(let ((@x280 (mp~ (mp (asserted $x206) @x249 $x245) (nnf-pos (refl (~ $x242 $x242)) (~ $x245 $x245)) $x245)))
+(let ((@x323 (mp @x280 (quant-intro (refl (= $x242 $x242)) (= $x245 $x318)) $x318)))
+(let (($x545 (not $x318)))
+(let (($x626 (or $x545 $x621)))
+(let ((?x359 (* (- 1) 2)))
+(let ((?x590 (mod ?x110 ?x359)))
+(let ((?x591 (* (- 1) ?x590)))
+(let (($x357 (<= 2 0)))
+(let ((?x593 (ite $x357 ?x591 ?x592)))
+(let (($x356 (= 2 0)))
+(let ((?x594 (ite $x356 ?x97 ?x593)))
+(let (($x595 (= ?x98 ?x594)))
+(let ((@x601 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x590 (mod ?x110 (- 2)))) (= ?x591 (* (- 1) (mod ?x110 (- 2)))))))
+(let ((@x368 (rewrite (= $x357 false))))
+(let ((@x604 (monotonicity @x368 @x601 (= ?x593 (ite false (* (- 1) (mod ?x110 (- 2))) ?x592)))))
+(let ((@x608 (trans @x604 (rewrite (= (ite false (* (- 1) (mod ?x110 (- 2))) ?x592) ?x592)) (= ?x593 ?x592))))
+(let ((@x366 (rewrite (= $x356 false))))
+(let ((@x615 (trans (monotonicity @x366 @x608 (= ?x594 (ite false ?x97 ?x592))) (rewrite (= (ite false ?x97 ?x592) ?x592)) (= ?x594 ?x592))))
+(let ((@x625 (trans (monotonicity @x615 (= $x595 (= ?x98 ?x592))) (rewrite (= (= ?x98 ?x592) $x621)) (= $x595 $x621))))
+(let ((@x633 (trans (monotonicity @x625 (= (or $x545 $x595) $x626)) (rewrite (= $x626 $x626)) (= (or $x545 $x595) $x626))))
+(let ((@x634 (mp ((_ quant-inst (eval_dioph$ ks$ ?x96) 2) (or $x545 $x595)) @x633 $x626)))
+(let ((@x431 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x635)) (unit-resolution @x634 @x323 $x621) $x635)))
+(let ((?x637 (div ?x97 2)))
+(let ((?x650 (* (- 2) ?x637)))
+(let ((?x651 (+ ?x97 ?x619 ?x650)))
+(let (($x656 (<= ?x651 0)))
+(let (($x649 (= ?x651 0)))
+(let ((@x661 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x656)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x656)))
+(let ((?x539 (+ ?x99 ?x538)))
+(let (($x555 (<= ?x539 0)))
+(let (($x540 (= ?x539 0)))
+(let (($x546 (or $x545 $x540)))
+(let ((?x506 (mod ?x369 ?x359)))
+(let ((?x507 (* (- 1) ?x506)))
+(let ((?x512 (ite $x357 ?x507 ?x511)))
+(let ((?x513 (ite $x356 l$ ?x512)))
+(let (($x514 (= ?x99 ?x513)))
+(let ((@x520 (monotonicity (monotonicity (rewrite (= ?x359 (- 2))) (= ?x506 (mod ?x369 (- 2)))) (= ?x507 (* (- 1) (mod ?x369 (- 2)))))))
+(let ((@x523 (monotonicity @x368 @x520 (= ?x512 (ite false (* (- 1) (mod ?x369 (- 2))) ?x511)))))
+(let ((@x527 (trans @x523 (rewrite (= (ite false (* (- 1) (mod ?x369 (- 2))) ?x511) ?x511)) (= ?x512 ?x511))))
+(let ((@x534 (trans (monotonicity @x366 @x527 (= ?x513 (ite false l$ ?x511))) (rewrite (= (ite false l$ ?x511) ?x511)) (= ?x513 ?x511))))
+(let ((@x544 (trans (monotonicity @x534 (= $x514 (= ?x99 ?x511))) (rewrite (= (= ?x99 ?x511) $x540)) (= $x514 $x540))))
+(let ((@x553 (trans (monotonicity @x544 (= (or $x545 $x514) $x546)) (rewrite (= $x546 $x546)) (= (or $x545 $x514) $x546))))
+(let ((@x554 (mp ((_ quant-inst l$ 2) (or $x545 $x514)) @x553 $x546)))
+(let ((@x668 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x555)) (unit-resolution @x554 @x323 $x540) $x555)))
+(let ((?x361 (div ?x111 2)))
+(let ((?x395 (* (- 1) ?x361)))
+(let ((?x396 (+ ?x114 ?x395)))
+(let (($x414 (>= ?x396 0)))
+(let (($x397 (= ?x396 0)))
+(let (($x311 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :pattern ( (divide$ ?v0 ?v1) ) :qid k!21))
+))
+(let (($x193 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x145 (div ?v0 ?v1)))
+(let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let (($x175 (<= ?v1 0)))
+(let ((?x182 (ite $x175 ?x160 ?x145)))
+(let (($x143 (= ?v1 0)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 (ite $x143 0 ?x182)))))))))) :qid k!21))
+))
+(let ((?x141 (divide$ ?1 ?0)))
+(let (($x190 (= ?x141 (ite $x143 0 (ite $x175 (div ?x154 ?x157) (div ?1 ?0))))))
+(let (($x152 (forall ((?v0 Int) (?v1 Int) )(! (let (($x143 (= ?v1 0)))
+(let ((?x150 (ite $x143 0 (ite (< 0 ?v1) (div ?v0 ?v1) (div (- ?v0) (- ?v1))))))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x150)))) :qid k!21))
+))
+(let (($x172 (forall ((?v0 Int) (?v1 Int) )(! (let ((?x157 (* (- 1) ?v1)))
+(let ((?x154 (* (- 1) ?v0)))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?v0 ?v1)))
+(let (($x144 (< 0 ?v1)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let (($x143 (= ?v1 0)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let ((?x141 (divide$ ?v0 ?v1)))
+(= ?x141 ?x166)))))))))) :qid k!21))
+))
+(let ((?x160 (div ?x154 ?x157)))
+(let ((?x145 (div ?1 ?0)))
+(let ((?x163 (ite $x144 ?x145 ?x160)))
+(let ((?x166 (ite $x143 0 ?x163)))
+(let (($x169 (= ?x141 ?x166)))
+(let ((@x181 (monotonicity (rewrite (= $x144 (not $x175))) (= ?x163 (ite (not $x175) ?x145 ?x160)))))
+(let ((@x186 (trans @x181 (rewrite (= (ite (not $x175) ?x145 ?x160) (ite $x175 ?x160 ?x145))) (= ?x163 (ite $x175 ?x160 ?x145)))))
+(let ((@x192 (monotonicity (monotonicity @x186 (= ?x166 (ite $x143 0 (ite $x175 ?x160 ?x145)))) (= $x169 $x190))))
+(let (($x170 (= (= ?x141 (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0))))) $x169)))
+(let ((@x162 (monotonicity (rewrite (= (- ?1) ?x154)) (rewrite (= (- ?0) ?x157)) (= (div (- ?1) (- ?0)) ?x160))))
+(let ((@x168 (monotonicity (monotonicity @x162 (= (ite $x144 ?x145 (div (- ?1) (- ?0))) ?x163)) (= (ite $x143 0 (ite $x144 ?x145 (div (- ?1) (- ?0)))) ?x166))))
+(let ((@x197 (trans (quant-intro (monotonicity @x168 $x170) (= $x152 $x172)) (quant-intro @x192 (= $x172 $x193)) (= $x152 $x193))))
+(let ((@x275 (mp~ (mp (asserted $x152) @x197 $x193) (nnf-pos (refl (~ $x190 $x190)) (~ $x193 $x193)) $x193)))
+(let ((@x316 (mp @x275 (quant-intro (refl (= $x190 $x190)) (= $x193 $x311)) $x311)))
+(let (($x403 (or (not $x311) $x397)))
+(let ((?x358 (* (- 1) ?x111)))
+(let ((?x360 (div ?x358 ?x359)))
+(let ((?x362 (ite $x357 ?x360 ?x361)))
+(let ((?x363 (ite $x356 0 ?x362)))
+(let (($x364 (= ?x114 ?x363)))
+(let ((@x374 (rewrite (= ?x359 (- 2)))))
+(let ((@x377 (monotonicity (rewrite (= ?x358 (+ ?x369 ?x97))) @x374 (= ?x360 (div (+ ?x369 ?x97) (- 2))))))
+(let ((@x380 (monotonicity @x368 @x377 (= ?x362 (ite false (div (+ ?x369 ?x97) (- 2)) ?x361)))))
+(let ((@x384 (trans @x380 (rewrite (= (ite false (div (+ ?x369 ?x97) (- 2)) ?x361) ?x361)) (= ?x362 ?x361))))
+(let ((@x391 (trans (monotonicity @x366 @x384 (= ?x363 (ite false 0 ?x361))) (rewrite (= (ite false 0 ?x361) ?x361)) (= ?x363 ?x361))))
+(let ((@x401 (trans (monotonicity @x391 (= $x364 (= ?x114 ?x361))) (rewrite (= (= ?x114 ?x361) $x397)) (= $x364 $x397))))
+(let ((@x410 (trans (monotonicity @x401 (= (or (not $x311) $x364) $x403)) (rewrite (= $x403 $x403)) (= (or (not $x311) $x364) $x403))))
+(let ((@x411 (mp ((_ quant-inst (+ l$ ?x110) 2) (or (not $x311) $x364)) @x410 $x403)))
+(let ((@x485 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x414)) (unit-resolution @x411 @x316 $x397) $x414)))
+(let ((?x436 (* (- 1) ?x425)))
+(let ((?x435 (* (- 2) ?x361)))
+(let ((?x437 (+ l$ ?x110 ?x435 ?x436)))
+(let (($x442 (<= ?x437 0)))
+(let (($x434 (= ?x437 0)))
+(let ((@x745 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x442)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x442)))
+(let ((@x746 ((_ th-lemma arith farkas 1 -2 -2 -2 1 1 1 1 1 1) @x745 @x485 (hypothesis $x673) (hypothesis $x760) (hypothesis $x676) @x668 @x661 @x431 @x568 (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false)))
+(let ((@x788 (unit-resolution (lemma @x746 (or $x747 (not $x673) (not $x676))) @x787 @x781 $x747)))
+(let (($x677 (>= ?x675 0)))
+(let ((@x812 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x281 $x677)) (unit-resolution (def-axiom (or $x283 $x100)) @x493 $x100) $x677)))
+(let (($x577 (>= ?x571 0)))
+(let ((@x778 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x569) $x577)) (unit-resolution ((_ th-lemma arith) (or false $x569)) @x26 $x569) $x577)))
+(let (($x556 (>= ?x539 0)))
+(let ((@x645 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x540) $x556)) (unit-resolution @x554 @x323 $x540) $x556)))
+(let (($x636 (>= ?x620 0)))
+(let ((@x652 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x621) $x636)) (unit-resolution @x634 @x323 $x621) $x636)))
+(let (($x505 (>= ?x497 0)))
+(let ((@x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x498) $x505)) (unit-resolution @x503 @x309 $x498) $x505)))
+(let (($x657 (>= ?x651 0)))
+(let ((@x581 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x649) $x657)) (unit-resolution ((_ th-lemma arith) (or false $x649)) @x26 $x649) $x657)))
+(let ((@x582 ((_ th-lemma arith farkas -1/2 -1/2 -1/2 1/2 -1/2 -1/2 -1/2 1) @x581 (hypothesis $x677) @x488 (hypothesis (not $x680)) @x652 @x645 @x778 (hypothesis $x747) false)))
+(let ((@x813 (unit-resolution (lemma @x582 (or $x680 (not $x677) $x760)) @x812 @x788 $x680)))
+(let (($x134 (not $x95)))
+(let (($x290 (= $x95 $x283)))
+(let ((@x289 (monotonicity (rewrite (= (and $x100 $x117) $x284)) (= (= $x134 (and $x100 $x117)) (= $x134 $x284)))))
+(let ((@x294 (trans @x289 (rewrite (= (= $x134 $x284) $x290)) (= (= $x134 (and $x100 $x117)) $x290))))
+(let (($x120 (and $x100 $x117)))
+(let (($x135 (= $x134 $x120)))
+(let (($x107 (= $x95 (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))))))
+(let (($x108 (not $x107)))
+(let ((@x116 (monotonicity (rewrite (= (- l$ ?x97) ?x111)) (= (divide$ (- l$ ?x97) 2) ?x114))))
+(let ((@x122 (monotonicity (monotonicity @x116 (= (= ?x102 (divide$ (- l$ ?x97) 2)) $x117)) (= (and $x100 (= ?x102 (divide$ (- l$ ?x97) 2))) $x120))))
+(let ((@x130 (trans (monotonicity @x122 (= $x107 (= $x95 $x120))) (rewrite (= (= $x95 $x120) (= $x95 $x120))) (= $x107 (= $x95 $x120)))))
+(let ((@x139 (trans (monotonicity @x130 (= $x108 (not (= $x95 $x120)))) (rewrite (= (not (= $x95 $x120)) $x135)) (= $x108 $x135))))
+(let ((@x295 (mp (mp (asserted $x108) @x139 $x135) @x294 $x290)))
+(let ((@x344 (unit-resolution (def-axiom (or $x134 $x283 (not $x290))) @x295 (or $x134 $x283))))
+(let ((@x819 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x95 $x815 (not $x680))) (unit-resolution @x344 @x493 $x134) (or $x815 (not $x680)))))
+(let (($x672 (<= ?x671 0)))
+(let ((@x823 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x282 $x672)) (unit-resolution (def-axiom (or $x283 $x117)) @x493 $x117) $x672)))
+(let (($x413 (<= ?x396 0)))
+(let ((@x802 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x397) $x413)) (unit-resolution @x411 @x316 $x397) $x413)))
+(let (($x443 (>= ?x437 0)))
+(let ((@x826 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x434) $x443)) (unit-resolution ((_ th-lemma arith) (or false $x434)) @x26 $x434) $x443)))
+(let ((@x827 ((_ th-lemma arith farkas 1 -2 -2 1 -1 1) @x826 @x802 @x823 (unit-resolution @x819 @x813 $x815) @x795 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) false)))
+(let ((@x828 (lemma @x827 $x283)))
+(let ((@x340 (unit-resolution (def-axiom (or $x95 $x284 (not $x290))) @x295 (or $x95 $x284))))
+(let ((@x584 (unit-resolution @x340 @x828 $x95)))
+(let (($x807 (not $x672)))
+(let ((@x888 ((_ th-lemma arith assign-bounds 1 -1/2 -1/2 1/2 -1/2) (or $x673 (not $x413) (not $x465) (not $x443) (not $x504) (not $x680)))))
+(let ((@x889 (unit-resolution @x888 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x680)) @x584 $x680) @x802 @x826 (unit-resolution ((_ th-lemma arith) (or false $x465)) @x26 $x465) @x795 $x673)))
+(let ((@x728 (monotonicity (symm @x584 (= l$ ?x93)) (= ?x99 (modulo$ ?x93 2)))))
+(let ((?x499 (modulo$ ?x93 2)))
+(let (($x500 (= ?x499 ?x98)))
+(let (($x297 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :pattern ( (eval_dioph$ ?v0 (map$ uu$ ?v1)) ) :qid k!18))
+))
+(let (($x51 (forall ((?v0 Int_list$) (?v1 Int_list$) )(! (= (modulo$ (eval_dioph$ ?v0 ?v1) 2) (modulo$ (eval_dioph$ ?v0 (map$ uu$ ?v1)) 2)) :qid k!18))
+))
+(let (($x50 (= (modulo$ ?x45 2) (modulo$ ?x48 2))))
+(let ((@x265 (mp~ (asserted $x51) (nnf-pos (refl (~ $x50 $x50)) (~ $x51 $x51)) $x51)))
+(let ((@x302 (mp @x265 (quant-intro (refl (= $x50 $x50)) (= $x51 $x297)) $x297)))
+(let (($x464 (or (not $x297) $x500)))
+(let ((@x578 ((_ quant-inst ks$ xs$) $x464)))
+(let ((@x748 (trans (symm (unit-resolution @x578 @x302 $x500) (= ?x98 ?x499)) (symm @x728 (= ?x499 ?x99)) $x100)))
+(let ((@x891 (unit-resolution (unit-resolution (def-axiom (or $x284 $x281 $x282)) @x828 $x283) (lemma (unit-resolution (hypothesis $x281) @x748 false) $x100) $x282)))
+(let ((@x895 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x117 $x807 (not $x673))) @x891 (or $x807 (not $x673)))))
+((_ th-lemma arith farkas -2 -2 1 -1 1 1) (unit-resolution @x895 @x889 $x807) @x485 @x745 @x488 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x134 $x679)) @x584 $x679) (unit-resolution ((_ th-lemma arith) (or false $x564)) @x26 $x564) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+