products/sources/formale sprachen/Isabelle/HOL/SMT_Examples/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: subset_algebra_def.prf   Sprache: Lisp

rahmenlose Ansicht.certs DruckansichtHaskell {Haskell[358] Ada[539] Abap[606]}Entwicklung

c6761b6a026c6bf2d28c35e9faf633fc441c84c5 45 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x44 (id$ x$)))
(let (($x46 (= ?x44 x$)))
(let (($x73 (not $x46)))
(let (($x47 (id$a true)))
(let (($x510 (forall ((?v0 Bool) )(! (let (($x33 (id$a ?v0)))
(= $x33 ?v0)) :pattern ( (id$a ?v0) ) :qid k!9))
))
(let (($x40 (forall ((?v0 Bool) )(! (let (($x33 (id$a ?v0)))
(= $x33 ?v0)) :qid k!9))
))
(let ((@x514 (quant-intro (refl (= (= (id$a ?0) ?0) (= (id$a ?0) ?0))) (= $x40 $x510))))
(let ((@x69 (nnf-pos (refl (~ (= (id$a ?0) ?0) (= (id$a ?0) ?0))) (~ $x40 $x40))))
(let (($x35 (forall ((?v0 Bool) )(! (let (($x33 (id$a ?v0)))
(= $x33 ?v0)) :qid k!9))
))
(let ((@x42 (quant-intro (rewrite (= (= (id$a ?0) ?0) (= (id$a ?0) ?0))) (= $x35 $x40))))
(let ((@x515 (mp (mp~ (mp (asserted $x35) @x42 $x40) @x69 $x40) @x514 $x510)))
(let (($x87 (or (not $x510) $x47)))
(let ((@x176 (monotonicity (rewrite (= (= $x47 true) $x47)) (= (or (not $x510) (= $x47 true)) $x87))))
(let ((@x179 (trans @x176 (rewrite (= $x87 $x87)) (= (or (not $x510) (= $x47 true)) $x87))))
(let ((@x495 (unit-resolution (mp ((_ quant-inst true) (or (not $x510) (= $x47 true))) @x179 $x87) @x515 (hypothesis (not $x47)) false)))
(let (($x71 (or $x73 (not $x47))))
(let ((@x79 (monotonicity (rewrite (= (and $x46 $x47) (not $x71))) (= (not (and $x46 $x47)) (not (not $x71))))))
(let ((@x83 (trans @x79 (rewrite (= (not (not $x71)) $x71)) (= (not (and $x46 $x47)) $x71))))
(let (($x54 (and $x46 $x47)))
(let (($x57 (not $x54)))
(let ((@x56 (monotonicity (rewrite (= (= $x47 true) $x47)) (= (and $x46 (= $x47 true)) $x54))))
(let ((@x62 (mp (asserted (not (and $x46 (= $x47 true)))) (monotonicity @x56 (= (not (and $x46 (= $x47 true))) $x57)) $x57)))
(let ((@x84 (mp @x62 @x83 $x71)))
(let (($x503 (forall ((?v0 A$) )(! (let ((?x28 (id$ ?v0)))
(= ?x28 ?v0)) :pattern ( (id$ ?v0) ) :qid k!8))
))
(let (($x30 (forall ((?v0 A$) )(! (let ((?x28 (id$ ?v0)))
(= ?x28 ?v0)) :qid k!8))
))
(let ((@x507 (quant-intro (refl (= (= (id$ ?0) ?0) (= (id$ ?0) ?0))) (= $x30 $x503))))
(let ((@x64 (nnf-pos (refl (~ (= (id$ ?0) ?0) (= (id$ ?0) ?0))) (~ $x30 $x30))))
(let ((@x508 (mp (mp~ (asserted $x30) @x64 $x30) @x507 $x503)))
(let (($x163 (or (not $x503) $x46)))
(let ((@x496 ((_ quant-inst x$) $x163)))
(unit-resolution @x496 @x508 (unit-resolution @x84 (lemma @x495 $x47) $x73) false)))))))))))))))))))))))))))))))))

23f5eb3b530a4577da2f8947333286ff70ed557f 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x29 (exists ((?v0 A$) )(! (g$ ?v0) :qid k!7))
))
(let (($x30 (f$ $x29)))
(let (($x31 (=> $x30 true)))
(let (($x32 (not $x31)))
(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
(mp (asserted $x32) @x42 false))))))))

174a4beaccbbd473470bdf78d1dd5655decaaf38 51 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x61 (fun_app$ f$ i$)))
(let ((?x57 (fun_upd$ f$ i1$ v1$)))
(let ((?x59 (fun_upd$ ?x57 i2$ v2$)))
(let ((?x60 (fun_app$ ?x59 i$)))
(let (($x62 (= ?x60 ?x61)))
(let ((?x189 (fun_app$ ?x57 i$)))
(let (($x197 (= ?x189 ?x61)))
(let (($x196 (= ?x189 v1$)))
(let (($x49 (= i$ i1$)))
(let (($x476 (ite $x49 $x196 $x197)))
(let (($x524 (forall ((?v0 A_b_fun$) (?v1 A$) (?v2 B$) (?v3 A$) )(! (let (($x41 (= ?v3 ?v1)))
(ite $x41 (= (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3) ?v2) (= (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3) (fun_app$ ?v0 ?v3)))) :pattern ( (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3) ) :qid k!16))
))
(let (($x94 (forall ((?v0 A_b_fun$) (?v1 A$) (?v2 B$) (?v3 A$) )(! (let (($x41 (= ?v3 ?v1)))
(ite $x41 (= (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3) ?v2) (= (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3) (fun_app$ ?v0 ?v3)))) :qid k!16))
))
(let (($x41 (= ?0 ?2)))
(let (($x89 (ite $x41 (= (fun_app$ (fun_upd$ ?3 ?2 ?1) ?0) ?1) (= (fun_app$ (fun_upd$ ?3 ?2 ?1) ?0) (fun_app$ ?3 ?0)))))
(let (($x45 (forall ((?v0 A_b_fun$) (?v1 A$) (?v2 B$) (?v3 A$) )(! (let ((?x40 (fun_app$ (fun_upd$ ?v0 ?v1 ?v2) ?v3)))
(= ?x40 (ite (= ?v3 ?v1) ?v2 (fun_app$ ?v0 ?v3)))) :qid k!16))
))
(let ((?x40 (fun_app$ (fun_upd$ ?3 ?2 ?1) ?0)))
(let (($x44 (= ?x40 (ite $x41 ?1 (fun_app$ ?3 ?0)))))
(let ((@x82 (mp~ (asserted $x45) (nnf-pos (refl (~ $x44 $x44)) (~ $x45 $x45)) $x45)))
(let ((@x97 (mp @x82 (quant-intro (rewrite (= $x44 $x89)) (= $x45 $x94)) $x94)))
(let ((@x529 (mp @x97 (quant-intro (refl (= $x89 $x89)) (= $x94 $x524)) $x524)))
(let (($x163 (not $x524)))
(let (($x478 (or $x163 $x476)))
(let ((@x479 ((_ quant-inst f$ i1$ v1$ i$) $x478)))
(let (($x50 (not $x49)))
(let (($x52 (= i$ i2$)))
(let (($x53 (not $x52)))
(let (($x54 (and $x50 $x53)))
(let ((@x72 (monotonicity (rewrite (= (=> $x54 $x62) (or (not $x54) $x62))) (= (not (=> $x54 $x62)) (not (or (not $x54) $x62))))))
(let ((@x73 (not-or-elim (mp (asserted (not (=> $x54 $x62))) @x72 (not (or (not $x54) $x62))) $x54)))
(let ((@x74 (and-elim @x73 $x50)))
(let ((@x313 (unit-resolution (def-axiom (or (not $x476) $x49 $x197)) @x74 (or (not $x476) $x197))))
(let (($x192 (= ?x60 ?x189)))
(let (($x188 (= ?x60 v2$)))
(let (($x171 (ite $x52 $x188 $x192)))
(let (($x293 (or $x163 $x171)))
(let ((@x503 ((_ quant-inst (fun_upd$ f$ i1$ v1$) i2$ v2$ i$) $x293)))
(let ((@x76 (and-elim @x73 $x53)))
(let ((@x458 (unit-resolution (def-axiom (or (not $x171) $x52 $x192)) @x76 (or (not $x171) $x192))))
(let ((@x462 (trans (unit-resolution @x458 (unit-resolution @x503 @x529 $x171) $x192) (unit-resolution @x313 (unit-resolution @x479 @x529 $x476) $x197) $x62)))
(let ((@x78 (not-or-elim (mp (asserted (not (=> $x54 $x62))) @x72 (not (or (not $x54) $x62))) (not $x62))))
(unit-resolution @x78 @x462 false)))))))))))))))))))))))))))))))))))))))))))

3aa17d1c77bc1a92bca05df291d11d81c645a931 6 0
unsat
((set-logic AUFLIA)
(proof
(let ((@x30 (rewrite (= (not true) false))))
(mp (asserted (not true)) @x30 false))))

feaa6ef662dd489cf55f86209489c2992ff08d28 46 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x61 (fun_app$a le$ 3)))
(let (($x63 (fun_app$ ?x61 42)))
(let (($x75 (not $x63)))
(let (($x59 (= le$ uu$)))
(let ((@x73 (monotonicity (rewrite (= (=> $x59 $x63) (or (not $x59) $x63))) (= (not (=> $x59 $x63)) (not (or (not $x59) $x63))))))
(let ((@x74 (not-or-elim (mp (asserted (not (=> $x59 $x63))) @x73 (not (or (not $x59) $x63))) $x59)))
(let ((@x482 (monotonicity (symm @x74 (= uu$ le$)) (= (fun_app$a uu$ 3) ?x61))))
(let ((@x484 (symm (monotonicity @x482 (= (fun_app$ (fun_app$a uu$ 3) 42) $x63)) (= $x63 (fun_app$ (fun_app$a uu$ 3) 42)))))
(let ((@x472 (monotonicity @x484 (= $x75 (not (fun_app$ (fun_app$a uu$ 3) 42))))))
(let ((@x77 (not-or-elim (mp (asserted (not (=> $x59 $x63))) @x73 (not (or (not $x59) $x63))) $x75)))
(let ((?x79 (fun_app$a uu$ 3)))
(let (($x168 (fun_app$ ?x79 42)))
(let (($x52 (forall ((?v0 Int) (?v1 Int) )(! (let (($x46 (<= (+ ?v0 (* (- 1) ?v1)) 0)))
(let (($x31 (fun_app$ (fun_app$a uu$ ?v0) ?v1)))
(= $x31 $x46))) :pattern ( (fun_app$ (fun_app$a uu$ ?v0) ?v1) ) :qid k!10))
))
(let (($x46 (<= (+ ?1 (* (- 1) ?0)) 0)))
(let (($x31 (fun_app$ (fun_app$a uu$ ?1) ?0)))
(let (($x49 (= $x31 $x46)))
(let (($x35 (forall ((?v0 Int) (?v1 Int) )(! (let (($x32 (<= ?v0 ?v1)))
(let (($x31 (fun_app$ (fun_app$a uu$ ?v0) ?v1)))
(= $x31 $x32))) :pattern ( (fun_app$ (fun_app$a uu$ ?v0) ?v1) ) :qid k!10))
))
(let (($x40 (forall ((?v0 Int) (?v1 Int) )(! (let (($x32 (<= ?v0 ?v1)))
(let (($x31 (fun_app$ (fun_app$a uu$ ?v0) ?v1)))
(= $x31 $x32))) :pattern ( (fun_app$ (fun_app$a uu$ ?v0) ?v1) ) :qid k!10))
))
(let ((@x51 (monotonicity (rewrite (= (<= ?1 ?0) $x46)) (= (= $x31 (<= ?1 ?0)) $x49))))
(let ((@x42 (quant-intro (rewrite (= (= $x31 (<= ?1 ?0)) (= $x31 (<= ?1 ?0)))) (= $x35 $x40))))
(let ((@x57 (mp (asserted $x35) (trans @x42 (quant-intro @x51 (= $x40 $x52)) (= $x35 $x52)) $x52)))
(let ((@x78 (mp~ @x57 (nnf-pos (refl (~ $x49 $x49)) (~ $x52 $x52)) $x52)))
(let (($x134 (or (not $x52) $x168)))
(let (($x137 (= (or (not $x52) (= $x168 (<= (+ 3 (* (- 1) 42)) 0))) $x134)))
(let ((?x169 (* (- 1) 42)))
(let ((?x170 (+ 3 ?x169)))
(let (($x160 (<= ?x170 0)))
(let (($x171 (= $x168 $x160)))
(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)))))))))))))))))))))))))))))))))))

60f1b32e9c6a2229b64c85dcfb0bde9c2bd5433a 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x29 (forall ((?v0 A$) )(! (g$ ?v0) :qid k!7))
))
(let (($x30 (f$ $x29)))
(let (($x31 (=> $x30 true)))
(let (($x32 (not $x31)))
(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
(mp (asserted $x32) @x42 false))))))))

9cdd1051dbf4e0648f71536fbc74bbab8e0e744e 75 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x78 (cons$ 2 nil$)))
(let ((?x79 (cons$ 1 ?x78)))
(let ((?x74 (cons$ 1 nil$)))
(let ((?x75 (cons$ 0 ?x74)))
(let ((?x76 (map$ uu$ ?x75)))
(let (($x80 (= ?x76 ?x79)))
(let ((?x185 (map$ uu$ ?x74)))
(let ((?x189 (map$ uu$ nil$)))
(let ((?x188 (fun_app$ uu$ 1)))
(let ((?x160 (cons$ ?x188 ?x189)))
(let (($x290 (= ?x185 ?x160)))
(let (($x521 (forall ((?v0 Int_int_fun$) (?v1 Int) (?v2 Int_list$) )(! (= (map$ ?v0 (cons$ ?v1 ?v2)) (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))) :pattern ( (map$ ?v0 (cons$ ?v1 ?v2)) ) :pattern ( (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2)) ) :qid k!13))
))
(let (($x72 (forall ((?v0 Int_int_fun$) (?v1 Int) (?v2 Int_list$) )(! (= (map$ ?v0 (cons$ ?v1 ?v2)) (cons$ (fun_app$ ?v0 ?v1) (map$ ?v0 ?v2))) :qid k!13))
))
(let (($x71 (= (map$ ?2 (cons$ ?1 ?0)) (cons$ (fun_app$ ?2 ?1) (map$ ?2 ?0)))))
(let ((@x97 (mp~ (asserted $x72) (nnf-pos (refl (~ $x71 $x71)) (~ $x72 $x72)) $x72)))
(let ((@x526 (mp @x97 (quant-intro (refl (= $x71 $x71)) (= $x72 $x521)) $x521)))
(let (($x173 (or (not $x521) $x290)))
(let ((@x506 ((_ quant-inst uu$ 1 nil$) $x173)))
(let (($x492 (= ?x189 nil$)))
(let (($x513 (forall ((?v0 Int_int_fun$) )(! (= (map$ ?v0 nil$) nil$) :pattern ( (map$ ?v0 nil$) ) :qid k!12))
))
(let (($x61 (forall ((?v0 Int_int_fun$) )(! (= (map$ ?v0 nil$) nil$) :qid k!12))
))
(let ((@x515 (refl (= (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
(let ((@x83 (refl (~ (= (map$ ?0 nil$) nil$) (= (map$ ?0 nil$) nil$)))))
(let ((@x518 (mp (mp~ (asserted $x61) (nnf-pos @x83 (~ $x61 $x61)) $x61) (quant-intro @x515 (= $x61 $x513)) $x513)))
(let (($x495 (or (not $x513) $x492)))
(let ((@x496 ((_ quant-inst uu$) $x495)))
(let (($x136 (= ?x188 2)))
(let (($x51 (forall ((?v0 Int) )(! (= (+ ?v0 (* (- 1) (fun_app$ uu$ ?v0))) (- 1)) :pattern ( (fun_app$ uu$ ?v0) ) :qid k!11))
))
(let (($x47 (= (+ ?0 (* (- 1) (fun_app$ uu$ ?0))) (- 1))))
(let (($x34 (forall ((?v0 Int) )(! (let ((?x29 (fun_app$ uu$ ?v0)))
(= ?x29 (+ ?v0 1))) :pattern ( (fun_app$ uu$ ?v0) ) :qid k!11))
))
(let (($x42 (forall ((?v0 Int) )(! (let ((?x29 (fun_app$ uu$ ?v0)))
(= ?x29 (+ 1 ?v0))) :pattern ( (fun_app$ uu$ ?v0) ) :qid k!11))
))
(let ((@x53 (quant-intro (rewrite (= (= (fun_app$ uu$ ?0) (+ 1 ?0)) $x47)) (= $x42 $x51))))
(let ((?x29 (fun_app$ uu$ ?0)))
(let (($x39 (= ?x29 (+ 1 ?0))))
(let ((@x41 (monotonicity (rewrite (= (+ ?0 1) (+ 1 ?0))) (= (= ?x29 (+ ?0 1)) $x39))))
(let ((@x56 (mp (asserted $x34) (trans (quant-intro @x41 (= $x34 $x42)) @x53 (= $x34 $x51)) $x51)))
(let ((@x85 (mp~ @x56 (nnf-pos (refl (~ $x47 $x47)) (~ $x51 $x51)) $x51)))
(let (($x145 (not $x51)))
(let (($x499 (or $x145 $x136)))
(let ((@x498 (rewrite (= (= (+ 1 (* (- 1) ?x188)) (- 1)) $x136))))
(let ((@x204 (monotonicity @x498 (= (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1))) $x499))))
(let ((@x207 (trans @x204 (rewrite (= $x499 $x499)) (= (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1))) $x499))))
(let ((@x104 (mp ((_ quant-inst 1) (or $x145 (= (+ 1 (* (- 1) ?x188)) (- 1)))) @x207 $x499)))
(let ((@x191 (monotonicity (symm (unit-resolution @x104 @x85 $x136) (= 2 ?x188)) (symm (unit-resolution @x496 @x518 $x492) (= nil$ ?x189)) (= ?x78 ?x160))))
(let ((@x473 (trans @x191 (symm (unit-resolution @x506 @x526 $x290) (= ?x160 ?x185)) (= ?x78 ?x185))))
(let ((?x182 (fun_app$ uu$ 0)))
(let (($x163 (= ?x182 1)))
(let (($x487 (or $x145 $x163)))
(let ((@x501 (monotonicity (rewrite (= (+ 0 (* (- 1) ?x182)) (* (- 1) ?x182))) (= (= (+ 0 (* (- 1) ?x182)) (- 1)) (= (* (- 1) ?x182) (- 1))))))
(let ((@x503 (trans @x501 (rewrite (= (= (* (- 1) ?x182) (- 1)) $x163)) (= (= (+ 0 (* (- 1) ?x182)) (- 1)) $x163))))
(let ((@x151 (monotonicity @x503 (= (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1))) $x487))))
(let ((@x490 (trans @x151 (rewrite (= $x487 $x487)) (= (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1))) $x487))))
(let ((@x491 (mp ((_ quant-inst 0) (or $x145 (= (+ 0 (* (- 1) ?x182)) (- 1)))) @x490 $x487)))
(let ((@x478 (monotonicity (symm (unit-resolution @x491 @x85 $x163) (= 1 ?x182)) @x473 (= ?x79 (cons$ ?x182 ?x185)))))
(let ((?x186 (cons$ ?x182 ?x185)))
(let (($x187 (= ?x76 ?x186)))
(let (($x504 (or (not $x521) $x187)))
(let ((@x505 ((_ quant-inst uu$ 0 (cons$ 1 nil$)) $x504)))
(let ((@x466 (trans (unit-resolution @x505 @x526 $x187) (symm @x478 (= ?x186 ?x79)) $x80)))
(let (($x81 (not $x80)))
(let ((@x82 (asserted $x81)))
(unit-resolution @x82 @x466 false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

40c61a0200976d6203302a7343af5b7ad1e6ce36 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x29 (forall ((?v0 A$) )(! (p$ ?v0) :qid k!6))
))
(let (($x30 (not $x29)))
(let (($x31 (or $x29 $x30)))
(let (($x32 (not $x31)))
(let ((@x42 (trans (monotonicity (rewrite (= $x31 true)) (= $x32 (not true))) (rewrite (= (not true) false)) (= $x32 false))))
(mp (asserted $x32) @x42 false))))))))

f17a5e4d5f1a5a93fbc847f858c7c845c29d8349 109 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x75 (dec_10$ 4)))
(let ((?x76 (* 4 ?x75)))
(let ((?x77 (dec_10$ ?x76)))
(let (($x79 (= ?x77 6)))
(let (($x150 (<= ?x75 4)))
(let (($x174 (= ?x75 4)))
(let (($x513 (forall ((?v0 Int) )(! (let (($x55 (>= ?v0 10)))
(ite $x55 (= (dec_10$ ?v0) (dec_10$ (+ (- 10) ?v0))) (= (dec_10$ ?v0) ?v0))) :pattern ( (dec_10$ ?v0) ) :qid k!5))
))
(let (($x92 (forall ((?v0 Int) )(! (let (($x55 (>= ?v0 10)))
(ite $x55 (= (dec_10$ ?v0) (dec_10$ (+ (- 10) ?v0))) (= (dec_10$ ?v0) ?v0))) :qid k!5))
))
(let (($x55 (>= ?0 10)))
(let (($x87 (ite $x55 (= (dec_10$ ?0) (dec_10$ (+ (- 10) ?0))) (= (dec_10$ ?0) ?0))))
(let (($x68 (forall ((?v0 Int) )(! (let ((?x38 (+ (- 10) ?v0)))
(let ((?x41 (dec_10$ ?x38)))
(let (($x55 (>= ?v0 10)))
(let ((?x60 (ite $x55 ?x41 ?v0)))
(let ((?x28 (dec_10$ ?v0)))
(= ?x28 ?x60)))))) :qid k!5))
))
(let ((?x38 (+ (- 10) ?0)))
(let ((?x41 (dec_10$ ?x38)))
(let ((?x60 (ite $x55 ?x41 ?0)))
(let ((?x28 (dec_10$ ?0)))
(let (($x65 (= ?x28 ?x60)))
(let (($x35 (forall ((?v0 Int) )(! (let ((?x28 (dec_10$ ?v0)))
(= ?x28 (ite (< ?v0 10) ?v0 (dec_10$ (- ?v0 10))))) :qid k!5))
))
(let (($x50 (forall ((?v0 Int) )(! (let ((?x38 (+ (- 10) ?v0)))
(let ((?x41 (dec_10$ ?x38)))
(let (($x30 (< ?v0 10)))
(let ((?x44 (ite $x30 ?v0 ?x41)))
(let ((?x28 (dec_10$ ?v0)))
(= ?x28 ?x44)))))) :qid k!5))
))
(let ((@x59 (monotonicity (rewrite (= (< ?0 10) (not $x55))) (= (ite (< ?0 10) ?0 ?x41) (ite (not $x55) ?0 ?x41)))))
(let ((@x64 (trans @x59 (rewrite (= (ite (not $x55) ?0 ?x41) ?x60)) (= (ite (< ?0 10) ?0 ?x41) ?x60))))
(let ((@x67 (monotonicity @x64 (= (= ?x28 (ite (< ?0 10) ?0 ?x41)) $x65))))
(let (($x30 (< ?0 10)))
(let ((?x44 (ite $x30 ?0 ?x41)))
(let (($x47 (= ?x28 ?x44)))
(let ((@x43 (monotonicity (rewrite (= (- ?0 10) ?x38)) (= (dec_10$ (- ?0 10)) ?x41))))
(let ((@x49 (monotonicity (monotonicity @x43 (= (ite $x30 ?0 (dec_10$ (- ?0 10))) ?x44)) (= (= ?x28 (ite $x30 ?0 (dec_10$ (- ?0 10)))) $x47))))
(let ((@x72 (trans (quant-intro @x49 (= $x35 $x50)) (quant-intro @x67 (= $x50 $x68)) (= $x35 $x68))))
(let ((@x86 (mp~ (mp (asserted $x35) @x72 $x68) (nnf-pos (refl (~ $x65 $x65)) (~ $x68 $x68)) $x68)))
(let ((@x95 (mp @x86 (quant-intro (rewrite (= $x65 $x87)) (= $x68 $x92)) $x92)))
(let ((@x518 (mp @x95 (quant-intro (refl (= $x87 $x87)) (= $x92 $x513)) $x513)))
(let (($x501 (not $x513)))
(let (($x163 (or $x501 $x174)))
(let ((?x97 (+ (- 10) 4)))
(let ((?x183 (dec_10$ ?x97)))
(let (($x184 (= ?x75 ?x183)))
(let (($x96 (>= 4 10)))
(let (($x185 (ite $x96 $x184 $x174)))
(let ((@x172 (monotonicity (monotonicity (rewrite (= ?x97 (- 6))) (= ?x183 (dec_10$ (- 6)))) (= $x184 (= ?x75 (dec_10$ (- 6)))))))
(let ((@x507 (monotonicity (rewrite (= $x96 false)) @x172 (= $x185 (ite false (= ?x75 (dec_10$ (- 6))) $x174)))))
(let ((@x511 (trans @x507 (rewrite (= (ite false (= ?x75 (dec_10$ (- 6))) $x174) $x174)) (= $x185 $x174))))
(let ((@x148 (trans (monotonicity @x511 (= (or $x501 $x185) $x163)) (rewrite (= $x163 $x163)) (= (or $x501 $x185) $x163))))
(let ((@x149 (mp ((_ quant-inst 4) (or $x501 $x185)) @x148 $x163)))
(let ((@x438 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x174) $x150)) (unit-resolution @x149 @x518 $x174) $x150)))
(let (($x151 (>= ?x75 4)))
(let ((@x428 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x174) $x151)) (unit-resolution @x149 @x518 $x174) $x151)))
(let ((?x489 (+ (- 10) ?x76)))
(let ((?x490 (dec_10$ ?x489)))
(let ((?x448 (* (- 1) ?x490)))
(let ((?x449 (+ ?x76 ?x448)))
(let (($x444 (<= ?x449 10)))
(let (($x292 (= ?x449 10)))
(let ((?x455 (+ (- 20) ?x76)))
(let ((?x458 (dec_10$ ?x455)))
(let (($x461 (= ?x490 ?x458)))
(let (($x310 (>= ?x75 5)))
(let (($x450 (ite $x310 $x461 $x292)))
(let (($x453 (or $x501 $x450)))
(let (($x470 (= ?x490 ?x489)))
(let ((?x467 (+ (- 10) ?x489)))
(let ((?x468 (dec_10$ ?x467)))
(let (($x469 (= ?x490 ?x468)))
(let (($x466 (>= ?x489 10)))
(let (($x471 (ite $x466 $x469 $x470)))
(let ((@x463 (monotonicity (monotonicity (rewrite (= ?x467 ?x455)) (= ?x468 ?x458)) (= $x469 $x461))))
(let ((@x452 (monotonicity (rewrite (= $x466 $x310)) @x463 (rewrite (= $x470 $x292)) (= $x471 $x450))))
(let ((@x442 (trans (monotonicity @x452 (= (or $x501 $x471) $x453)) (rewrite (= $x453 $x453)) (= (or $x501 $x471) $x453))))
(let ((@x443 (mp ((_ quant-inst (+ (- 10) ?x76)) (or $x501 $x471)) @x442 $x453)))
(let (($x346 (not $x310)))
(let ((@x418 (unit-resolution (def-axiom (or (not $x450) $x310 $x292)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x346 (not $x150))) @x438 $x346) (or (not $x450) $x292))))
(let ((@x422 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x292) $x444)) (unit-resolution @x418 (unit-resolution @x443 @x518 $x450) $x292) $x444)))
(let (($x336 (>= ?x449 10)))
(let ((@x410 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x292) $x336)) (unit-resolution @x418 (unit-resolution @x443 @x518 $x450) $x292) $x336)))
(let (($x491 (= ?x77 ?x490)))
(let ((?x499 (* (- 1) ?x77)))
(let ((?x485 (+ ?x76 ?x499)))
(let (($x497 (= ?x485 0)))
(let (($x131 (>= ?x75 3)))
(let (($x486 (ite $x131 $x491 $x497)))
(let (($x205 (or $x501 $x486)))
(let ((@x204 (monotonicity (rewrite (= (>= ?x76 10) $x131)) (rewrite (= (= ?x77 ?x76) $x497)) (= (ite (>= ?x76 10) $x491 (= ?x77 ?x76)) $x486))))
(let ((@x479 (monotonicity @x204 (= (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76))) $x205))))
(let ((@x212 (trans @x479 (rewrite (= $x205 $x205)) (= (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76))) $x205))))
(let ((@x481 (mp ((_ quant-inst (* 4 ?x75)) (or $x501 (ite (>= ?x76 10) $x491 (= ?x77 ?x76)))) @x212 $x205)))
(let ((@x397 (unit-resolution (def-axiom (or (not $x486) (not $x131) $x491)) (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x131 (not $x151))) @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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

db184ed715734759b60f9bdc99290a92283563f5 64 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x108 (collect$ uu$)))
(let ((?x109 (sup$ ?x108)))
(let (($x117 (less_eq$ ?x109 ?x109)))
(let (($x118 (not $x117)))
(let ((@x119 (asserted $x118)))
(let ((?x111 (collect$ uua$)))
(let ((?x112 (sup$ ?x111)))
(let (($x115 (less_eq$ ?x112 ?x109)))
(let ((@x116 (asserted $x115)))
(let (($x113 (less_eq$ ?x109 ?x112)))
(let ((@x114 (asserted $x113)))
(let (($x578 (forall ((?v0 A$) (?v1 A$) (?v2 A$) )(! (let (($x97 (less_eq$ ?v0 ?v2)))
(let (($x95 (less_eq$ ?v1 ?v2)))
(let (($x138 (not $x95)))
(let (($x93 (less_eq$ ?v0 ?v1)))
(let (($x137 (not $x93)))
(or $x137 $x138 $x97)))))) :pattern ( (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2) ) :qid k!17))
))
(let (($x156 (forall ((?v0 A$) (?v1 A$) (?v2 A$) )(! (let (($x97 (less_eq$ ?v0 ?v2)))
(let (($x95 (less_eq$ ?v1 ?v2)))
(let (($x138 (not $x95)))
(let (($x93 (less_eq$ ?v0 ?v1)))
(let (($x137 (not $x93)))
(or $x137 $x138 $x97)))))) :qid k!17))
))
(let ((@x583 (trans (rewrite (= $x156 $x578)) (rewrite (= $x578 $x578)) (= $x156 $x578))))
(let (($x105 (forall ((?v0 A$) (?v1 A$) (?v2 A$) )(! (let (($x97 (less_eq$ ?v0 ?v2)))
(let (($x95 (less_eq$ ?v1 ?v2)))
(let (($x93 (less_eq$ ?v0 ?v1)))
(let (($x96 (and $x93 $x95)))
(let (($x101 (not $x96)))
(or $x101 $x97)))))) :qid k!17))
))
(let (($x97 (less_eq$ ?2 ?0)))
(let (($x95 (less_eq$ ?1 ?0)))
(let (($x138 (not $x95)))
(let (($x93 (less_eq$ ?2 ?1)))
(let (($x137 (not $x93)))
(let (($x151 (or $x137 $x138 $x97)))
(let (($x96 (and $x93 $x95)))
(let (($x101 (not $x96)))
(let (($x102 (or $x101 $x97)))
(let ((@x143 (monotonicity (rewrite (= $x96 (not (or $x137 $x138)))) (= $x101 (not (not (or $x137 $x138)))))))
(let ((@x147 (trans @x143 (rewrite (= (not (not (or $x137 $x138))) (or $x137 $x138))) (= $x101 (or $x137 $x138)))))
(let ((@x155 (trans (monotonicity @x147 (= $x102 (or (or $x137 $x138) $x97))) (rewrite (= (or (or $x137 $x138) $x97) $x151)) (= $x102 $x151))))
(let (($x99 (forall ((?v0 A$) (?v1 A$) (?v2 A$) )(! (let (($x97 (less_eq$ ?v0 ?v2)))
(let (($x95 (less_eq$ ?v1 ?v2)))
(let (($x93 (less_eq$ ?v0 ?v1)))
(let (($x96 (and $x93 $x95)))
(=> $x96 $x97))))) :qid k!17))
))
(let ((@x110 (mp (asserted $x99) (quant-intro (rewrite (= (=> $x96 $x97) $x102)) (= $x99 $x105)) $x105)))
(let ((@x159 (mp (mp~ @x110 (nnf-pos (refl (~ $x102 $x102)) (~ $x105 $x105)) $x105) (quant-intro @x155 (= $x105 $x156)) $x156)))
(let ((@x584 (mp @x159 @x583 $x578)))
(let (($x247 (not $x115)))
(let (($x160 (not $x113)))
(let (($x251 (not $x578)))
(let (($x252 (or $x251 $x160 $x247 $x117)))
(let ((@x570 (mp ((_ quant-inst (sup$ ?x108) (sup$ ?x111) (sup$ ?x108)) (or $x251 (or $x160 $x247 $x117))) (rewrite (= (or $x251 (or $x160 $x247 $x117)) $x252)) $x252)))
(unit-resolution @x570 @x584 @x114 @x116 @x119 false)))))))))))))))))))))))))))))))))))))))

4e8ab14f236ad601aa67494ca8ea18b2ba6a1a79 25 0
unsat
((set-logic AUFLIA)
(proof
(let (($x142 (pred$e 1)))
(let (($x144 (not $x142)))
(let ((@x145 (asserted $x144)))
(let (($x615 (forall ((?v0 Int) )(! (pred$e ?v0) :pattern ( (pred$e ?v0) ) :qid k!29))
))
(let (($x138 (forall ((?v0 Int) )(! (pred$e ?v0) :qid k!29))
))
(let (($x127 (forall ((?v0 Int) )(! (let (($x125 (or (pred$d (cons$d ?v0 nil$d)) (not (pred$d (cons$d ?v0 nil$d))))))
(let (($x119 (pred$e ?v0)))
(and $x119 $x125))) :qid k!29))
))
(let (($x119 (pred$e ?0)))
(let (($x125 (or (pred$d (cons$d ?0 nil$d)) (not (pred$d (cons$d ?0 nil$d))))))
(let (($x126 (and $x119 $x125)))
(let ((@x133 (monotonicity (rewrite (= $x125 true)) (= $x126 (and $x119 true)))))
(let ((@x140 (quant-intro (trans @x133 (rewrite (= (and $x119 true) $x119)) (= $x126 $x119)) (= $x127 $x138))))
(let ((@x170 (mp~ (mp (asserted $x127) @x140 $x138) (nnf-pos (refl (~ $x119 $x119)) (~ $x138 $x138)) $x138)))
(let ((@x620 (mp @x170 (quant-intro (refl (= $x119 $x119)) (= $x138 $x615)) $x615)))
(let (($x257 (or (not $x615) $x142)))
(let ((@x258 ((_ quant-inst 1) $x257)))
(unit-resolution @x258 @x620 @x145 false))))))))))))))))))

b4b100f728c8f0d6f96483e4de44e248cc4be1aa 101 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x124 (some$a true)))
(let ((?x125 (g$b ?x124)))
(let ((?x122 (some$ 3)))
(let ((?x123 (g$ ?x122)))
(let (($x126 (= ?x123 ?x125)))
(let ((?x269 (cons$a true nil$a)))
(let ((?x270 (g$c ?x269)))
(let (($x587 (= ?x125 ?x270)))
(let (($x604 (forall ((?v0 Bool) )(! (= (g$b (some$a ?v0)) (g$c (cons$a ?v0 nil$a))) :pattern ( (some$a ?v0) ) :pattern ( (cons$a ?v0 nil$a) ) :qid k!33))
))
(let (($x43 (forall ((?v0 Bool) )(! (= (g$b (some$a ?v0)) (g$c (cons$a ?v0 nil$a))) :qid k!33))
))
(let (($x42 (= (g$b (some$a ?0)) (g$c (cons$a ?0 nil$a)))))
(let ((@x160 (mp~ (asserted $x43) (nnf-pos (refl (~ $x42 $x42)) (~ $x43 $x43)) $x43)))
(let ((@x609 (mp @x160 (quant-intro (refl (= $x42 $x42)) (= $x43 $x604)) $x604)))
(let (($x254 (or (not $x604) $x587)))
(let ((@x255 ((_ quant-inst true) $x254)))
(let ((?x227 (size$ ?x269)))
(let (($x569 (= ?x270 ?x227)))
(let (($x612 (forall ((?v0 Bool_list$) )(! (let ((?x61 (size$ ?v0)))
(let ((?x60 (g$c ?v0)))
(= ?x60 ?x61))) :pattern ( (g$c ?v0) ) :pattern ( (size$ ?v0) ) :qid k!38))
))
(let (($x63 (forall ((?v0 Bool_list$) )(! (let ((?x61 (size$ ?v0)))
(let ((?x60 (g$c ?v0)))
(= ?x60 ?x61))) :qid k!38))
))
(let ((@x616 (quant-intro (refl (= (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (= $x63 $x612))))
(let ((@x142 (nnf-pos (refl (~ (= (g$c ?0) (size$ ?0)) (= (g$c ?0) (size$ ?0)))) (~ $x63 $x63))))
(let ((@x617 (mp (mp~ (asserted $x63) @x142 $x63) @x616 $x612)))
(let (($x571 (or (not $x612) $x569)))
(let ((@x572 ((_ quant-inst (cons$a true nil$a)) $x571)))
(let ((?x89 (suc$ zero$)))
(let ((?x105 (size$ nil$a)))
(let ((?x233 (plus$ ?x105 ?x89)))
(let (($x570 (= ?x227 ?x233)))
(let (($x657 (forall ((?v0 Bool) (?v1 Bool_list$) )(! (= (size$ (cons$a ?v0 ?v1)) (plus$ (size$ ?v1) (suc$ zero$))) :pattern ( (cons$a ?v0 ?v1) ) :qid k!46))
))
(let (($x114 (forall ((?v0 Bool) (?v1 Bool_list$) )(! (= (size$ (cons$a ?v0 ?v1)) (plus$ (size$ ?v1) (suc$ zero$))) :qid k!46))
))
(let (($x113 (= (size$ (cons$a ?1 ?0)) (plus$ (size$ ?0) ?x89))))
(let ((@x173 (mp~ (asserted $x114) (nnf-pos (refl (~ $x113 $x113)) (~ $x114 $x114)) $x114)))
(let ((@x662 (mp @x173 (quant-intro (refl (= $x113 $x113)) (= $x114 $x657)) $x657)))
(let (($x576 (or (not $x657) $x570)))
(let ((@x213 ((_ quant-inst true nil$a) $x576)))
(let ((?x108 (size$a nil$)))
(let (($x109 (= ?x108 zero$)))
(let ((@x110 (asserted $x109)))
(let (($x106 (= ?x105 zero$)))
(let ((@x107 (asserted $x106)))
(let ((@x287 (monotonicity (trans @x107 (symm @x110 (= zero$ ?x108)) (= ?x105 ?x108)) (= ?x233 (plus$ ?x108 ?x89)))))
(let ((?x246 (plus$ ?x108 ?x89)))
(let ((?x256 (cons$ 3 nil$)))
(let ((?x588 (size$a ?x256)))
(let (($x584 (= ?x588 ?x246)))
(let (($x664 (forall ((?v0 Int) (?v1 Int_list$) )(! (= (size$a (cons$ ?v0 ?v1)) (plus$ (size$a ?v1) (suc$ zero$))) :pattern ( (cons$ ?v0 ?v1) ) :qid k!47))
))
(let (($x119 (forall ((?v0 Int) (?v1 Int_list$) )(! (= (size$a (cons$ ?v0 ?v1)) (plus$ (size$a ?v1) (suc$ zero$))) :qid k!47))
))
(let (($x118 (= (size$a (cons$ ?1 ?0)) (plus$ (size$a ?0) ?x89))))
(let ((@x178 (mp~ (asserted $x119) (nnf-pos (refl (~ $x118 $x118)) (~ $x119 $x119)) $x119)))
(let ((@x669 (mp @x178 (quant-intro (refl (= $x118 $x118)) (= $x119 $x664)) $x664)))
(let (($x231 (or (not $x664) $x584)))
(let ((@x232 ((_ quant-inst 3 nil$) $x231)))
(let ((?x267 (g$a ?x256)))
(let (($x592 (= ?x267 ?x588)))
(let (($x620 (forall ((?v0 Int_list$) )(! (let ((?x67 (size$a ?v0)))
(let ((?x66 (g$a ?v0)))
(= ?x66 ?x67))) :pattern ( (g$a ?v0) ) :pattern ( (size$a ?v0) ) :qid k!39))
))
(let (($x69 (forall ((?v0 Int_list$) )(! (let ((?x67 (size$a ?v0)))
(let ((?x66 (g$a ?v0)))
(= ?x66 ?x67))) :qid k!39))
))
(let ((@x622 (refl (= (= (g$a ?0) (size$a ?0)) (= (g$a ?0) (size$a ?0))))))
(let ((@x129 (nnf-pos (refl (~ (= (g$a ?0) (size$a ?0)) (= (g$a ?0) (size$a ?0)))) (~ $x69 $x69))))
(let ((@x625 (mp (mp~ (asserted $x69) @x129 $x69) (quant-intro @x622 (= $x69 $x620)) $x620)))
(let (($x248 (or (not $x620) $x592)))
(let ((@x585 ((_ quant-inst (cons$ 3 nil$)) $x248)))
(let (($x268 (= ?x123 ?x267)))
(let (($x596 (forall ((?v0 Int) )(! (= (g$ (some$ ?v0)) (g$a (cons$ ?v0 nil$))) :pattern ( (some$ ?v0) ) :pattern ( (cons$ ?v0 nil$) ) :qid k!32))
))
(let (($x34 (forall ((?v0 Int) )(! (= (g$ (some$ ?v0)) (g$a (cons$ ?v0 nil$))) :qid k!32))
))
(let (($x33 (= (g$ (some$ ?0)) (g$a (cons$ ?0 nil$)))))
(let ((@x157 (mp~ (asserted $x34) (nnf-pos (refl (~ $x33 $x33)) (~ $x34 $x34)) $x34)))
(let ((@x601 (mp @x157 (quant-intro (refl (= $x33 $x33)) (= $x34 $x596)) $x596)))
(let (($x250 (or (not $x596) $x268)))
(let ((@x586 ((_ quant-inst 3) $x250)))
(let ((@x275 (trans (unit-resolution @x586 @x601 $x268) (unit-resolution @x585 @x625 $x592) (= ?x123 ?x588))))
(let ((@x280 (trans (trans @x275 (unit-resolution @x232 @x669 $x584) (= ?x123 ?x246)) (symm @x287 (= ?x246 ?x233)) (= ?x123 ?x233))))
(let ((@x558 (trans @x280 (symm (unit-resolution @x213 @x662 $x570) (= ?x233 ?x227)) (= ?x123 ?x227))))
(let ((@x560 (trans @x558 (symm (unit-resolution @x572 @x617 $x569) (= ?x227 ?x270)) (= ?x123 ?x270))))
(let ((@x546 (trans @x560 (symm (unit-resolution @x255 @x609 $x587) (= ?x270 ?x125)) $x126)))
(let (($x127 (not $x126)))
(let ((@x128 (asserted $x127)))
(unit-resolution @x128 @x546 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)))))

dfd95b23f80baacb2acdc442487bd8121f072035 9 0
unsat
((set-logic AUFLIA)
(proof
(let ((@x36 (monotonicity (rewrite (= (and p$ true) p$)) (= (= (and p$ true) p$) (= p$ p$)))))
(let ((@x40 (trans @x36 (rewrite (= (= p$ p$) true)) (= (= (and p$ true) p$) true))))
(let ((@x43 (monotonicity @x40 (= (not (= (and p$ true) p$)) (not true)))))
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= (and p$ true) p$)) false))))
(mp (asserted (not (= (and p$ true) p$))) @x47 false)))))))

8d6b87f1242925c8eefb2ec3e8ab8eefcd64e572 13 0
unsat
((set-logic AUFLIA)
(proof
(let (($x33 (not (=> (and (or p$ q$) (not p$)) q$))))
(let (($x37 (= (=> (and (or p$ q$) (not p$)) q$) (or (not (and (or p$ q$) (not p$))) q$))))
(let ((@x41 (monotonicity (rewrite $x37) (= $x33 (not (or (not (and (or p$ q$) (not p$))) q$))))))
(let ((@x44 (mp (asserted $x33) @x41 (not (or (not (and (or p$ q$) (not p$))) q$)))))
(let ((@x45 (and-elim (not-or-elim @x44 (and (or p$ q$) (not p$))) (not p$))))
(let ((@x54 (monotonicity (iff-false @x45 (= p$ false)) (iff-false (not-or-elim @x44 (not q$)) (= q$ false)) (= (or p$ q$) (or false false)))))
(let ((@x58 (trans @x54 (rewrite (= (or false false) false)) (= (or p$ q$) false))))
(let (($x29 (or p$ q$)))
(mp (and-elim (not-or-elim @x44 (and $x29 (not p$))) $x29) @x58 false)))))))))))

dfb7aeab4f33cdf91b335d72ad619dbd0d65fb62 23 0
unsat
((set-logic AUFLIA)
(proof
(let (($x33 (and p1$ p3$)))
(let (($x32 (and p3$ p2$)))
(let (($x34 (or $x32 $x33)))
(let (($x35 (=> p1$ $x34)))
(let (($x36 (or $x35 p1$)))
(let (($x29 (and p1$ p2$)))
(let (($x31 (or $x29 p3$)))
(let (($x37 (=> $x31 $x36)))
(let (($x38 (not $x37)))
(let (($x40 (not p1$)))
(let (($x41 (or $x40 $x34)))
(let (($x44 (or $x41 p1$)))
(let (($x50 (not $x31)))
(let (($x51 (or $x50 $x44)))
(let (($x56 (not $x51)))
(let ((@x67 (trans (monotonicity (rewrite (= $x51 true)) (= $x56 (not true))) (rewrite (= (not true) false)) (= $x56 false))))
(let ((@x49 (monotonicity (monotonicity (rewrite (= $x35 $x41)) (= $x36 $x44)) (= $x37 (=> $x31 $x44)))))
(let ((@x58 (monotonicity (trans @x49 (rewrite (= (=> $x31 $x44) $x51)) (= $x37 $x51)) (= $x38 $x56))))
(mp (asserted $x38) (trans @x58 @x67 (= $x38 false)) false)))))))))))))))))))))

a021a5fec5486f23204e54770f9c04c64baf7e25 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x32 (and c$ d$)))
(let (($x29 (and a$ b$)))
(let (($x33 (or $x29 $x32)))
(let (($x34 (=> $x33 $x33)))
(let (($x35 (not $x34)))
(let ((@x45 (trans (monotonicity (rewrite (= $x34 true)) (= $x35 (not true))) (rewrite (= (not true) false)) (= $x35 false))))
(mp (asserted $x35) @x45 false)))))))))

3efca8956be216e9acda1b32436ba8f01358d35e 24 0
unsat
((set-logic AUFLIA)
(proof
(let (($x28 (= p$ p$)))
(let (($x29 (= $x28 p$)))
(let (($x30 (= $x29 p$)))
(let (($x31 (= $x30 p$)))
(let (($x32 (= $x31 p$)))
(let (($x33 (= $x32 p$)))
(let (($x34 (= $x33 p$)))
(let (($x35 (= $x34 p$)))
(let (($x36 (= $x35 p$)))
(let (($x37 (not $x36)))
(let ((@x40 (rewrite (= $x28 true))))
(let ((@x45 (rewrite (= (= true p$) p$))))
(let ((@x47 (trans (monotonicity @x40 (= $x29 (= true p$))) @x45 (= $x29 p$))))
(let ((@x53 (monotonicity (trans (monotonicity @x47 (= $x30 $x28)) @x40 (= $x30 true)) (= $x31 (= true p$)))))
(let ((@x59 (trans (monotonicity (trans @x53 @x45 (= $x31 p$)) (= $x32 $x28)) @x40 (= $x32 true))))
(let ((@x63 (trans (monotonicity @x59 (= $x33 (= true p$))) @x45 (= $x33 p$))))
(let ((@x69 (monotonicity (trans (monotonicity @x63 (= $x34 $x28)) @x40 (= $x34 true)) (= $x35 (= true p$)))))
(let ((@x75 (trans (monotonicity (trans @x69 @x45 (= $x35 p$)) (= $x36 $x28)) @x40 (= $x36 true))))
(let ((@x82 (trans (monotonicity @x75 (= $x37 (not true))) (rewrite (= (not true) false)) (= $x37 false))))
(mp (asserted $x37) @x82 false))))))))))))))))))))))

143f46ba7acb4b0a8f67b0de474b0a249f30985b 27 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x38 (symm_f$ b$ a$)))
(let ((?x37 (symm_f$ a$ b$)))
(let (($x39 (= ?x37 ?x38)))
(let (($x52 (not $x39)))
(let ((@x47 (monotonicity (rewrite (= (= a$ a$) true)) (= (and (= a$ a$) $x39) (and true $x39)))))
(let ((@x51 (trans @x47 (rewrite (= (and true $x39) $x39)) (= (and (= a$ a$) $x39) $x39))))
(let ((@x57 (mp (asserted (not (and (= a$ a$) $x39))) (monotonicity @x51 (= (not (and (= a$ a$) $x39)) $x52)) $x52)))
(let (($x480 (forall ((?v0 A$) (?v1 A$) )(! (let ((?x30 (symm_f$ ?v1 ?v0)))
(let ((?x29 (symm_f$ ?v0 ?v1)))
(= ?x29 ?x30))) :pattern ( (symm_f$ ?v0 ?v1) ) :pattern ( (symm_f$ ?v1 ?v0) ) :qid k!8))
))
(let (($x32 (forall ((?v0 A$) (?v1 A$) )(! (let ((?x30 (symm_f$ ?v1 ?v0)))
(let ((?x29 (symm_f$ ?v0 ?v1)))
(= ?x29 ?x30))) :qid k!8))
))
(let ((?x30 (symm_f$ ?0 ?1)))
(let ((?x29 (symm_f$ ?1 ?0)))
(let (($x31 (= ?x29 ?x30)))
(let ((@x60 (mp~ (asserted $x32) (nnf-pos (refl (~ $x31 $x31)) (~ $x32 $x32)) $x32)))
(let ((@x485 (mp @x60 (quant-intro (refl (= $x31 $x31)) (= $x32 $x480)) $x480)))
(let (($x149 (or (not $x480) $x39)))
(let ((@x61 ((_ quant-inst a$ b$) $x149)))
(unit-resolution @x61 @x485 @x57 false)))))))))))))))))))

d600888ef4325a32ff87997035fed7a7c01e4767 39 0
unsat
((set-logic AUFLIA)
(proof
(let (($x100 (not d$)))
(let (($x45 (not c$)))
(let (($x112 (or p$ (and q$ (not q$)))))
(let (($x113 (and (not p$) $x112)))
(let (($x114 (or c$ $x113)))
(let (($x115 (not $x114)))
(let ((@x121 (monotonicity (rewrite (= (and q$ (not q$)) false)) (= $x112 (or p$ false)))))
(let ((@x128 (monotonicity (trans @x121 (rewrite (= (or p$ false) p$)) (= $x112 p$)) (= $x113 (and (not p$) p$)))))
(let ((@x132 (trans @x128 (rewrite (= (and (not p$) p$) false)) (= $x113 false))))
(let ((@x139 (trans (monotonicity @x132 (= $x114 (or c$ false))) (rewrite (= (or c$ false) c$)) (= $x114 c$))))
(let ((@x153 (iff-false (mp (asserted $x115) (monotonicity @x139 (= $x115 $x45)) $x45) (= c$ false))))
(let ((@x147 (trans (monotonicity @x153 (= (or $x100 c$) (or $x100 false))) (rewrite (= (or $x100 false) $x100)) (= (or $x100 c$) $x100))))
(let (($x103 (or $x100 c$)))
(let ((@x102 (monotonicity (rewrite (= (or d$ false) d$)) (= (not (or d$ false)) $x100))))
(let ((@x108 (mp (asserted (or (not (or d$ false)) c$)) (monotonicity @x102 (= (or (not (or d$ false)) c$) $x103)) $x103)))
(let (($x87 (not b$)))
(let ((@x164 (trans (monotonicity @x153 (= (or $x87 c$) (or $x87 false))) (rewrite (= (or $x87 false) $x87)) (= (or $x87 c$) $x87))))
(let (($x90 (or $x87 c$)))
(let ((@x82 (monotonicity (rewrite (= (or x$ (not x$)) true)) (= (and b$ (or x$ (not x$))) (and b$ true)))))
(let ((@x86 (trans @x82 (rewrite (= (and b$ true) b$)) (= (and b$ (or x$ (not x$))) b$))))
(let ((@x92 (monotonicity (monotonicity @x86 (= (not (and b$ (or x$ (not x$)))) $x87)) (= (or (not (and b$ (or x$ (not x$)))) c$) $x90))))
(let ((@x95 (mp (asserted (or (not (and b$ (or x$ (not x$)))) c$)) @x92 $x90)))
(let (($x64 (not a$)))
(let ((@x170 (monotonicity (iff-false (mp @x95 @x164 $x87) (= b$ false)) (= (or $x64 b$) (or $x64 false)))))
(let ((@x174 (trans @x170 (rewrite (= (or $x64 false) $x64)) (= (or $x64 b$) $x64))))
(let (($x67 (or $x64 b$)))
(let ((@x59 (monotonicity (rewrite (= (and c$ $x45) false)) (= (or a$ (and c$ $x45)) (or a$ false)))))
(let ((@x63 (trans @x59 (rewrite (= (or a$ false) a$)) (= (or a$ (and c$ $x45)) a$))))
(let ((@x69 (monotonicity (monotonicity @x63 (= (not (or a$ (and c$ $x45))) $x64)) (= (or (not (or a$ (and c$ $x45))) b$) $x67))))
(let ((@x175 (mp (mp (asserted (or (not (or a$ (and c$ $x45))) b$)) @x69 $x67) @x174 $x64)))
(let ((@x198 (monotonicity (iff-false @x175 (= a$ false)) (iff-false (mp @x95 @x164 $x87) (= b$ false)) @x153 (iff-false (mp @x108 @x147 $x100) (= d$ false)) (= (or a$ b$ c$ d$) (or false false false false)))))
(let ((@x202 (trans @x198 (rewrite (= (or false false false false) false)) (= (or a$ b$ c$ d$) false))))
(let (($x37 (or a$ b$ c$ d$)))
(let ((@x40 (mp (asserted (or a$ (or b$ (or c$ d$)))) (rewrite (= (or a$ (or b$ (or c$ d$))) $x37)) $x37)))
(mp @x40 @x202 false)))))))))))))))))))))))))))))))))))))

a6dd135a0c109f49b36d7266dc7a6becc640e496 637 0
unsat
((set-logic AUFLIA)
(proof
(let (($x397 (not x38$)))
(let (($x553 (not x51$)))
(let (($x657 (not x25$)))
(let (($x610 (not x56$)))
(let (($x538 (not x17$)))
(let ((@x897 (hypothesis $x538)))
(let (($x482 (not x45$)))
(let (($x609 (not x22$)))
(let (($x453 (not x11$)))
(let ((@x815 (hypothesis $x453)))
(let (($x667 (not x27$)))
(let (($x638 (not x58$)))
(let (($x567 (not x52$)))
(let ((@x756 (hypothesis $x567)))
(let (($x509 (not x47$)))
(let (($x637 (not x24$)))
(let (($x566 (not x19$)))
(let (($x294 (or x24$ x53$)))
(let ((@x774 (monotonicity (iff-false (asserted (not x59$)) (= x59$ false)) (= (or x59$ x24$ x53$) (or false x24$ x53$)))))
(let ((@x778 (trans @x774 (rewrite (= (or false x24$ x53$) $x294)) (= (or x59$ x24$ x53$) $x294))))
(let (($x303 (or x59$ x24$ x53$)))
(let ((@x306 (mp (asserted (or x59$ $x294)) (rewrite (= (or x59$ $x294) $x303)) $x303)))
(let ((@x779 (mp @x306 @x778 $x294)))
(let ((@x1181 (unit-resolution @x779 (unit-resolution (asserted (or $x637 $x638)) (hypothesis x58$) $x637) x53$)))
(let (($x580 (not x53$)))
(let (($x581 (or $x580 $x566)))
(let ((@x582 (asserted $x581)))
(let ((@x1182 (unit-resolution @x582 @x1181 $x566)))
(let (($x496 (not x46$)))
(let (($x583 (or $x580 $x509)))
(let ((@x584 (asserted $x583)))
(let ((@x1183 (unit-resolution @x584 @x1181 $x509)))
(let (($x438 (not x41$)))
(let (($x363 (not x4$)))
(let (($x347 (not x2$)))
(let (($x336 (not x31$)))
(let (($x623 (not x23$)))
(let (($x645 (or $x638 $x623)))
(let ((@x646 (asserted $x645)))
(let ((@x974 (hypothesis $x509)))
(let ((@x757 (hypothesis $x566)))
(let ((@x853 (hypothesis $x397)))
(let (($x410 (not x8$)))
(let (($x355 (not x3$)))
(let (($x467 (not x12$)))
(let ((@x882 (hypothesis $x467)))
(let ((@x845 (hypothesis $x347)))
(let (($x356 (not x33$)))
(let (($x481 (not x13$)))
(let (($x424 (not x9$)))
(let ((@x728 (hypothesis x41$)))
(let (($x439 (or $x438 $x424)))
(let ((@x440 (asserted $x439)))
(let ((@x922 (unit-resolution @x440 @x728 $x424)))
(let (($x364 (not x34$)))
(let (($x72 (or x35$ x4$)))
(let ((@x77 (asserted $x72)))
(let ((@x994 (unit-resolution @x77 (unit-resolution (asserted (or $x438 (not x35$))) @x728 (not x35$)) x4$)))
(let (($x365 (or $x363 $x364)))
(let ((@x366 (asserted $x365)))
(let ((@x999 (unit-resolution @x366 @x994 $x364)))
(let (($x396 (not x7$)))
(let (($x414 (or $x410 $x396)))
(let ((@x415 (asserted $x414)))
(let (($x348 (not x32$)))
(let ((@x942 (hypothesis $x355)))
(let (($x64 (or x3$ x33$ x2$)))
(let ((@x67 (mp (asserted (or x3$ (or x33$ x2$))) (rewrite (= (or x3$ (or x33$ x2$)) $x64)) $x64)))
(let ((@x1048 (unit-resolution @x67 (unit-resolution (asserted (or $x410 $x356)) (hypothesis x8$) $x356) @x942 x2$)))
(let (($x349 (or $x347 $x348)))
(let ((@x350 (asserted $x349)))
(let (($x105 (or x7$ x38$ x6$ x32$)))
(let ((@x108 (mp (asserted (or x7$ (or x38$ (or x6$ x32$)))) (rewrite (= (or x7$ (or x38$ (or x6$ x32$))) $x105)) $x105)))
(let ((@x842 (unit-resolution @x108 (unit-resolution @x350 @x1048 $x348) (unit-resolution @x415 (hypothesis x8$) $x396) @x853 x6$)))
(let (($x701 (or x1$ x31$)))
(let ((@x700 (monotonicity (iff-false (asserted (not x0$)) (= x0$ false)) (= (or x1$ x31$ x0$) (or x1$ x31$ false)))))
(let ((@x705 (trans @x700 (rewrite (= (or x1$ x31$ false) $x701)) (= (or x1$ x31$ x0$) $x701))))
(let (($x46 (or x1$ x31$ x0$)))
(let ((@x49 (mp (asserted (or x1$ (or x31$ x0$))) (rewrite (= (or x1$ (or x31$ x0$)) $x46)) $x46)))
(let ((@x706 (mp @x49 @x705 $x701)))
(let ((@x1002 (unit-resolution @x706 (unit-resolution (asserted (or $x347 (not x1$))) @x1048 (not x1$)) x31$)))
(let (($x382 (not x6$)))
(let (($x388 (or $x382 $x336)))
(let ((@x389 (asserted $x388)))
(let ((@x1011 (lemma (unit-resolution @x389 @x1002 @x842 false) (or $x410 x38$ x3$))))
(let ((@x952 (unit-resolution @x1011 (unit-resolution (asserted (or $x363 $x355)) @x994 $x355) @x853 $x410)))
(let (($x125 (or x9$ x40$ x8$ x34$)))
(let ((@x128 (mp (asserted (or x9$ (or x40$ (or x8$ x34$)))) (rewrite (= (or x9$ (or x40$ (or x8$ x34$))) $x125)) $x125)))
(let (($x425 (not x40$)))
(let (($x505 (or $x496 $x425)))
(let ((@x506 (asserted $x505)))
(let ((@x868 (unit-resolution @x506 (unit-resolution @x128 @x952 @x999 @x922 x40$) $x496)))
(let (($x239 (or x19$ x52$ x18$ x46$)))
(let ((@x242 (mp (asserted (or x19$ (or x52$ (or x18$ x46$)))) (rewrite (= (or x19$ (or x52$ (or x18$ x46$))) $x239)) $x239)))
(let (($x411 (not x39$)))
(let ((@x992 (unit-resolution @x67 (unit-resolution (asserted (or $x363 $x355)) @x994 $x355) @x845 x33$)))
(let (($x420 (or $x411 $x356)))
(let ((@x421 (asserted $x420)))
(let (($x507 (or $x481 $x425)))
(let ((@x508 (asserted $x507)))
(let ((@x1036 (unit-resolution @x508 (unit-resolution @x128 @x952 @x999 @x922 x40$) $x481)))
(let (($x172 (or x13$ x45$ x12$ x39$)))
(let ((@x175 (mp (asserted (or x13$ (or x45$ (or x12$ x39$)))) (rewrite (= (or x13$ (or x45$ (or x12$ x39$))) $x172)) $x172)))
(let ((@x1037 (unit-resolution @x175 @x1036 @x882 (unit-resolution @x421 @x992 $x411) x45$)))
(let (($x552 (not x18$)))
(let (($x558 (or $x552 $x482)))
(let ((@x559 (asserted $x558)))
(let ((@x1080 (unit-resolution @x559 @x1037 (unit-resolution @x242 @x868 @x757 @x756 x18$) false)))
(let ((@x1051 (unit-resolution (lemma @x1080 (or $x438 x12$ x19$ x52$ x2$ x38$)) @x845 @x757 @x756 @x882 @x853 $x438)))
(let (($x190 (or x47$ x14$ x41$)))
(let ((@x193 (mp (asserted (or x47$ (or x14$ x41$))) (rewrite (= (or x47$ (or x14$ x41$)) $x190)) $x190)))
(let ((@x732 (unit-resolution @x193 @x1051 @x974 x14$)))
(let (($x495 (not x14$)))
(let (($x499 (or $x495 $x481)))
(let ((@x500 (asserted $x499)))
(let ((@x941 (unit-resolution @x242 (unit-resolution (asserted (or $x495 $x496)) @x732 $x496) @x757 @x756 x18$)))
(let ((@x991 (unit-resolution @x175 (unit-resolution @x559 @x941 $x482) @x882 (unit-resolution @x500 @x732 $x481) x39$)))
(let (($x367 (or $x363 $x355)))
(let ((@x368 (asserted $x367)))
(let ((@x980 (unit-resolution @x368 (unit-resolution @x67 (unit-resolution @x421 @x991 $x356) @x845 x3$) $x363)))
(let (($x369 (or $x364 $x355)))
(let ((@x370 (asserted $x369)))
(let ((@x878 (unit-resolution @x370 (unit-resolution @x67 (unit-resolution @x421 @x991 $x356) @x845 x3$) $x364)))
(let ((@x879 (unit-resolution @x128 @x878 (unit-resolution (asserted (or $x495 $x425)) @x732 $x425) (unit-resolution (asserted (or $x410 $x411)) @x991 $x410) x9$)))
(let (($x371 (not x35$)))
(let (($x443 (or $x424 $x371)))
(let ((@x444 (asserted $x443)))
(let ((@x912 (lemma (unit-resolution @x444 @x879 (unit-resolution @x77 @x980 x35$) false) (or x2$ x12$ x19$ x52$ x47$ x38$))))
(let ((@x1091 (unit-resolution @x912 @x882 @x757 @x756 @x974 @x853 x2$)))
(let (($x359 (or $x355 $x347)))
(let ((@x360 (asserted $x359)))
(let ((@x784 (unit-resolution @x706 (unit-resolution (asserted (or $x347 (not x1$))) @x1091 (not x1$)) x31$)))
(let ((@x808 (unit-resolution @x108 (unit-resolution @x389 @x784 $x382) (unit-resolution @x350 @x1091 $x348) @x853 x7$)))
(let (($x418 (or $x411 $x396)))
(let ((@x419 (asserted $x418)))
(let ((@x913 (hypothesis $x410)))
(let ((@x931 (unit-resolution @x193 (unit-resolution @x500 (hypothesis x13$) $x495) @x974 x41$)))
(let ((@x867 (unit-resolution @x128 (unit-resolution @x440 @x931 $x424) (unit-resolution @x508 (hypothesis x13$) $x425) @x913 x34$)))
--> --------------------

--> maximum size reached

--> --------------------

[ Seitenstruktur0.443Drucken  ]