src/HOL/SMT_Examples/SMT_Examples.certs2

-3aa17d1c77bc1a92bca05df291d11d81c645a931 6 0
-unsat
-((set-logic AUFLIA)
-(proof
-(let ((@x30 (rewrite (= (not true) false))))
-(mp (asserted (not true)) @x30 false))))
-
 572677daa32981bf8212986300f1362edf42a0c1 7 0
 unsat
 ((set-logic AUFLIA)
 (proof
 (let ((@x36 (monotonicity (rewrite (= (or p$ (not p$)) true)) (= (not (or p$ (not p$))) (not true)))))
 (let ((@x40 (trans @x36 (rewrite (= (not true) false)) (= (not (or p$ (not p$))) false))))
 (mp (asserted (not (or p$ (not p$)))) @x40 false)))))
+
+3aa17d1c77bc1a92bca05df291d11d81c645a931 6 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let ((@x30 (rewrite (= (not true) false))))
+(mp (asserted (not true)) @x30 false))))
 
 dfd95b23f80baacb2acdc442487bd8121f072035 9 0
 unsat
 ((set-logic AUFLIA)
 (proof

 (let ((@x52 (trans @x48 (rewrite (= (< 5 8) true)) (= (< 5 (ite (<= 3 8) 8 3)) true))))
 (let ((@x55 (monotonicity @x52 (= (not (< 5 (ite (<= 3 8) 8 3))) (not true)))))
 (let ((@x59 (trans @x55 (rewrite (= (not true) false)) (= (not (< 5 (ite (<= 3 8) 8 3))) false))))
 (mp (asserted (not (< 5 (ite (<= 3 8) 8 3)))) @x59 false)))))))))
 
-2d63144daf211d89368e355b9b23a3b5118b7ba9 88 0
+6b0b089fbe179e8a27509c818f9a5e6847ac6bf2 88 0
 unsat
 ((set-logic AUFLIRA)
 (proof
 (let ((?x44 (* (- 1.0) x$)))
 (let (($x83 (>= x$ 0.0)))

 (let ((@x62 (monotonicity (rewrite (= (< a$ 0.0) (not $x58))) (= (not (< a$ 0.0)) (not (not $x58))))))
 (let ((@x66 (trans @x62 (rewrite (= (not (not $x58)) $x58)) (= (not (< a$ 0.0)) $x58))))
 (let ((@x67 (mp (asserted (not (< a$ 0.0))) @x66 $x58)))
 ((_ th-lemma arith farkas 7 3/2 1) @x67 @x52 @x40 false)))))))))))))))))
 
-b9f61649fae66ac195bf2593181f9d76c958bfe2 22 0
+3a6df2b095b936aac9a1d533e306f2d31b4fb44e 22 0
 unsat
 ((set-logic AUFLIA)
 (proof
 (let (($x38 (not false)))
 (let (($x34 (<= 0 x$)))

 (let ((@x428 (monotonicity (rewrite (= $x57 (not $x422))) (= (not $x57) (not (not $x422))))))
 (let ((@x432 (trans @x428 (rewrite (= (not (not $x422)) $x422)) (= (not $x57) $x422))))
 (let ((@x433 (mp (not-or-elim @x205 (not $x57)) @x432 $x422)))
 (unit-resolution @x433 @x488 (mp @x478 @x480 $x44) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-fbc59441c65d9a844da44405d06d138b55c5d187 933 0
+32286f9c5e71eb2b15c18f86f04c80931e2e307b 933 0
 unsat
 ((set-logic AUFLIA)
 (proof
 (let (($x91 (= x1$ x10$)))
 (let (($x582 (not $x91)))

 (let ((@x52 (trans (monotonicity @x45 (= $x34 (or false $x43))) (rewrite (= (or false $x43) $x43)) (= $x34 $x43))))
 (let ((@x59 (trans (monotonicity @x45 @x52 (= $x35 (or $x43 $x43))) (rewrite (= (or $x43 $x43) $x43)) (= $x35 $x43))))
 (let ((@x62 (monotonicity @x59 (= $x36 (not $x43)))))
 (mp (asserted $x36) (trans @x62 @x71 (= $x36 false)) false))))))))))))))))))
 
-d2037888c28cf52f7a45f66288246169de6f14ad 113 0
+faae12ee7efe4347f92e42776a0e0e57a624319c 113 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x228 (mod x$ 2)))
 (let ((?x262 (* (- 1) ?x228)))

 (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) @x337 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-29e336c1b1dbb5e85401e6a2954560661ff3cadc 112 0
+57f344c9e787868c98d1e622f158c445c1899c96 112 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x224 (mod x$ 2)))
 (let (($x318 (>= ?x224 2)))

 (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 @x336 (unit-resolution ((_ th-lemma arith) (or false $x319)) (true-axiom true) $x319) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-5bcedd8db3cccf5f1df2ef7ad1ca5e39c817a6f4 32 0
+3938db798ebafb55191dcdaf83a8615d1d59c0c3 32 0
 unsat
 ((set-logic <null>)
 (proof
 (let (($x28 (= x$ 0.0)))
 (let (($x29 (not $x28)))

 (let (($x102 (>= x$ 0.0)))
 (let (($x100 (>= ?x47 0.0)))
 (let ((@x117 (unit-resolution ((_ th-lemma arith assign-bounds 1) (or $x102 (not $x100))) (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x95) $x100)) @x98 $x100) $x102)))
 (unit-resolution ((_ th-lemma arith triangle-eq) (or $x28 (not $x101) (not $x102))) @x117 @x110 @x30 false))))))))))))))))))))))))))))))
 
-97186805a3315ef9a1cc4847a2e19a6d09c77915 236 0
+353c8b65ed1b98772a89ffdae52f1cfae628dd6a 236 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x410 (div n$ 2)))
 (let ((?x704 (* (- 1) ?x410)))

 (let ((@x40 (monotonicity (rewrite (= (ite $x31 false true) (not $x31))) (= $x33 (not (not $x31))))))
 (let ((@x60 (trans (trans @x40 (rewrite (= (not (not $x31)) $x31)) (= $x33 $x31)) (quant-intro @x55 (= $x31 $x56)) (= $x33 $x56))))
 (let ((@x66 (mp~ (mp (asserted $x33) @x60 $x56) (nnf-pos (refl (~ $x53 $x53)) (~ $x56 $x56)) $x56)))
 (unit-resolution @x66 @x464 false)))))))))))))))))))))))))
 
-a8cb4a130675f119ab8ba11cbe3a15041f18d2c6 62 0
+a02ae6c9688537bbe4c3be0d3dcebbc703417864 62 0
 unsat
 ((set-logic AUFLIA)
 (declare-fun ?v0!1 () Int)
 (declare-fun z3name!0 () Bool)
 (proof

 (let ((@x126 (monotonicity @x109 @x123 (~ (and $x89 (or z3name!0 $x90)) (and $x89 $x121)))))
 (let ((@x131 (and-elim (mp~ @x93 @x126 (and $x89 $x121)) $x89)))
 (let ((@x515 (unit-resolution (def-axiom (or z3name!0 $x220)) (unit-resolution @x131 @x238 $x88) $x220)))
 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x220) (>= ?x96 3))) @x515 @x245 false))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-9e0e67e5bd5078ab683d440f1a73c518a403be1b 39 0
+9853592ad3514c1450e40271884a9f21f57ff85b 39 0
 unsat
 ((set-logic AUFLIA)
 (proof
 (let (($x38 (exists ((?v0 Int) (?v1 Int) (?v2 Int) )(let ((?x33 (- 6)))
 (let ((?x34 (* ?x33 ?v1)))

 (let (($x101 (<= ?v2!0 0)))
 (let (($x102 (not $x101)))
 (let ((@x117 (and-elim (not-or-elim @x112 (and $x100 $x102)) $x102)))
 ((_ th-lemma arith farkas 1 1 1) @x117 @x116 @x118 false)))))))))))))))))))))))))))))))))))
 
-0d380fa4e68ab250e8351813b95695943794f02d 46 0
+9201a8009730b821ad6a3a2b64598e50ab5748ca 46 0
 unsat
 ((set-logic AUFLIRA)
 (declare-fun ?v1!1 () Int)
 (declare-fun ?v2!0 () Real)
 (proof

 (let ((@x74 (not-or-elim @x70 $x64)))
 (let (($x65 (not $x64)))
 (let (($x62 (<= ?v1!0 0)))
 (let ((@x73 (not-or-elim @x70 $x62)))
 (unit-resolution (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x65 (not $x62))) @x73 $x65) @x74 false))))))))))))))))))
+
+d98ad8f668dead6f610669a52351ea0176a811b0 26 0
+unsat
+((set-logic <null>)
+(proof
+(let (($x58 (<= b$ 0)))
+(let (($x62 (or (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))) (not $x58))))
+(let (($x65 (not $x62)))
+(let (($x35 (not (=> (and (< 0 a$) (< 0 (* a$ b$))) (< 0 b$)))))
+(let (($x33 (< 0 b$)))
+(let (($x38 (or (not (and (< 0 a$) (< 0 (* a$ b$)))) $x33)))
+(let (($x56 (= (not (and (< 0 a$) (< 0 (* a$ b$)))) (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))))))
+(let ((?x30 (* a$ b$)))
+(let (($x48 (<= ?x30 0)))
+(let (($x49 (not $x48)))
+(let (($x44 (<= a$ 0)))
+(let (($x45 (not $x44)))
+(let (($x52 (and $x45 $x49)))
+(let (($x32 (and (< 0 a$) (< 0 ?x30))))
+(let ((@x54 (monotonicity (rewrite (= (< 0 a$) $x45)) (rewrite (= (< 0 ?x30) $x49)) (= $x32 $x52))))
+(let ((@x64 (monotonicity (monotonicity @x54 $x56) (rewrite (= $x33 (not $x58))) (= $x38 $x62))))
+(let ((@x43 (monotonicity (rewrite (= (=> $x32 $x33) $x38)) (= $x35 (not $x38)))))
+(let ((@x69 (trans @x43 (monotonicity @x64 (= (not $x38) $x65)) (= $x35 $x65))))
+(let ((@x74 (not-or-elim (mp (asserted $x35) @x69 $x65) $x58)))
+(let ((@x72 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x45)))
+(let ((@x73 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x49)))
+((_ th-lemma arith farkas 1 1 1) @x73 @x72 @x74 false))))))))))))))))))))))))
 
 271390ea915947de195c2202e30f90bb84689d60 26 0
 unsat
 ((set-logic <null>)
 (proof

 (let ((@x51 (trans @x46 (rewrite (= (+ (+ 1 x$) y$) (+ 1 x$ y$))) (= ?x32 (+ 1 x$ y$)))))
 (let ((@x60 (trans (monotonicity @x51 (= ?x33 (* a$ (+ 1 x$ y$)))) @x58 (= ?x33 (+ a$ ?x34 (* a$ y$))))))
 (let ((@x88 (monotonicity (trans (monotonicity @x60 @x78 $x80) (rewrite $x82) (= $x38 true)) (= $x39 (not true)))))
 (let ((@x92 (trans @x88 (rewrite (= (not true) false)) (= $x39 false))))
 (mp (asserted $x39) @x92 false))))))))))))))))))))))))
-
-d98ad8f668dead6f610669a52351ea0176a811b0 26 0
-unsat
-((set-logic <null>)
-(proof
-(let (($x58 (<= b$ 0)))
-(let (($x62 (or (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))) (not $x58))))
-(let (($x65 (not $x62)))
-(let (($x35 (not (=> (and (< 0 a$) (< 0 (* a$ b$))) (< 0 b$)))))
-(let (($x33 (< 0 b$)))
-(let (($x38 (or (not (and (< 0 a$) (< 0 (* a$ b$)))) $x33)))
-(let (($x56 (= (not (and (< 0 a$) (< 0 (* a$ b$)))) (not (and (not (<= a$ 0)) (not (<= (* a$ b$) 0)))))))
-(let ((?x30 (* a$ b$)))
-(let (($x48 (<= ?x30 0)))
-(let (($x49 (not $x48)))
-(let (($x44 (<= a$ 0)))
-(let (($x45 (not $x44)))
-(let (($x52 (and $x45 $x49)))
-(let (($x32 (and (< 0 a$) (< 0 ?x30))))
-(let ((@x54 (monotonicity (rewrite (= (< 0 a$) $x45)) (rewrite (= (< 0 ?x30) $x49)) (= $x32 $x52))))
-(let ((@x64 (monotonicity (monotonicity @x54 $x56) (rewrite (= $x33 (not $x58))) (= $x38 $x62))))
-(let ((@x43 (monotonicity (rewrite (= (=> $x32 $x33) $x38)) (= $x35 (not $x38)))))
-(let ((@x69 (trans @x43 (monotonicity @x64 (= (not $x38) $x65)) (= $x35 $x65))))
-(let ((@x74 (not-or-elim (mp (asserted $x35) @x69 $x65) $x58)))
-(let ((@x72 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x45)))
-(let ((@x73 (and-elim (not-or-elim (mp (asserted $x35) @x69 $x65) $x52) $x49)))
-((_ th-lemma arith farkas 1 1 1) @x73 @x72 @x74 false))))))))))))))))))))))))
 
 b216c79478e44396acca3654b76845499fc18a04 23 0
 unsat
 ((set-logic <null>)
 (proof

 (let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
 (let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
 (let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
 (mp (asserted $x33) @x53 false)))))))))))
 
+8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
+unsat
+((set-logic AUFLIA)
+(proof
+(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
+))
+(let (($x30 (ite $x29 true false)))
+(let (($x31 (f$ $x30)))
+(let (($x32 (=> $x31 true)))
+(let (($x33 (not $x32)))
+(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
+(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
+(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
+(mp (asserted $x33) @x53 false)))))))))))
+
 b221de9d8dbe279344ac85e2ada07f5722636ce5 46 0
 unsat
 ((set-logic AUFLIA)
 (proof
 (let ((?x61 (fun_app$a le$ 3)))

 (let ((@x158 (trans (monotonicity (rewrite (= ?x169 (- 42))) (= ?x170 (+ 3 (- 42)))) (rewrite (= (+ 3 (- 42)) (- 39))) (= ?x170 (- 39)))))
 (let ((@x497 (trans (monotonicity @x158 (= $x160 (<= (- 39) 0))) (rewrite (= (<= (- 39) 0) true)) (= $x160 true))))
 (let ((@x131 (trans (monotonicity @x497 (= $x171 (= $x168 true))) (rewrite (= (= $x168 true) $x168)) (= $x171 $x168))))
 (let ((@x478 (mp ((_ quant-inst 3 42) (or (not $x52) $x171)) (trans (monotonicity @x131 $x137) (rewrite (= $x134 $x134)) $x137) $x134)))
 (unit-resolution (unit-resolution @x478 @x78 $x168) (mp @x77 @x472 (not $x168)) false)))))))))))))))))))))))))))))))))))
-
-8b09776b03122aeacc9dd9526e1f0e5d41a07f14 14 0
-unsat
-((set-logic AUFLIA)
-(proof
-(let (($x29 (forall ((?v0 A$) )(g$ ?v0))
-))
-(let (($x30 (ite $x29 true false)))
-(let (($x31 (f$ $x30)))
-(let (($x32 (=> $x31 true)))
-(let (($x33 (not $x32)))
-(let ((@x42 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= $x31 (f$ $x29))) (= $x32 (=> (f$ $x29) true)))))
-(let ((@x46 (trans @x42 (rewrite (= (=> (f$ $x29) true) true)) (= $x32 true))))
-(let ((@x53 (trans (monotonicity @x46 (= $x33 (not true))) (rewrite (= (not true) false)) (= $x33 false))))
-(mp (asserted $x33) @x53 false)))))))))))
 
 5d3ccbcf168a634cad3952ad8f6d2798329d6a77 75 0
 unsat
 ((set-logic AUFLIA)
 (proof

 (let ((@x397 (unit-resolution (def-axiom (or (not $x486) (not $x131) $x491)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or (not $x151) $x131)) @x428 $x131) (unit-resolution @x481 @x518 $x486) $x491)))
 (let (($x80 (not $x79)))
 (let ((@x81 (asserted $x80)))
 (unit-resolution @x81 (trans @x397 ((_ th-lemma arith eq-propagate 1 1 -4 -4) @x410 @x422 @x428 @x438 (= ?x490 6)) $x79) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
-fa62bf7228a50eb8c663092f87f9af7c25feaffe 336 0
+640bb6103260f74026864b86c2301c00ea737ff0 336 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x99 (mod$ l$ 2)))
 (let ((?x96 (map$ uu$ xs$)))