src/HOL/SMT/Examples/cert/z3_fol_01.proof

code cache without copy; tuned

#2 := false
decl up_1 :: (-> int bool)
decl ?x1!0 :: int
#54 := ?x1!0
#55 := (up_1 ?x1!0)
#58 := (not #55)
decl ?x2!1 :: int
#66 := ?x2!1
#67 := (up_1 ?x2!1)
#85 := (or #55 #67)
#88 := (not #85)
#91 := (and #55 #88)
#68 := (or #67 #55)
#69 := (not #68)
#63 := (not #58)
#75 := (and #63 #69)
#92 := (iff #75 #91)
#89 := (iff #69 #88)
#86 := (iff #68 #85)
#87 := [rewrite]: #86
#90 := [monotonicity #87]: #89
#83 := (iff #63 #55)
#84 := [rewrite]: #83
#93 := [monotonicity #84 #90]: #92
#6 := (:var 1 int)
#7 := (up_1 #6)
#4 := (:var 0 int)
#5 := (up_1 #4)
#29 := (or #5 #7)
#32 := (forall (vars (?x2 int)) #29)
#38 := (not #5)
#39 := (or #38 #32)
#44 := (forall (vars (?x1 int)) #39)
#47 := (not #44)
#78 := (~ #47 #75)
#56 := (or #5 #55)
#57 := (forall (vars (?x2 int)) #56)
#59 := (or #58 #57)
#60 := (not #59)
#76 := (~ #60 #75)
#70 := (not #57)
#71 := (~ #70 #69)
#72 := [sk]: #71
#64 := (~ #63 #63)
#65 := [refl]: #64
#77 := [nnf-neg #65 #72]: #76
#61 := (~ #47 #60)
#62 := [sk]: #61
#79 := [trans #62 #77]: #78
#8 := (or #7 #5)
#9 := (forall (vars (?x2 int)) #8)
#10 := (implies #5 #9)
#11 := (forall (vars (?x1 int)) #10)
#12 := (not #11)
#48 := (iff #12 #47)
#45 := (iff #11 #44)
#42 := (iff #10 #39)
#35 := (implies #5 #32)
#40 := (iff #35 #39)
#41 := [rewrite]: #40
#36 := (iff #10 #35)
#33 := (iff #9 #32)
#30 := (iff #8 #29)
#31 := [rewrite]: #30
#34 := [quant-intro #31]: #33
#37 := [monotonicity #34]: #36
#43 := [trans #37 #41]: #42
#46 := [quant-intro #43]: #45
#49 := [monotonicity #46]: #48
#28 := [asserted]: #12
#52 := [mp #28 #49]: #47
#80 := [mp~ #52 #79]: #75
#81 := [mp #80 #93]: #91
#94 := [and-elim #81]: #88
#95 := [not-or-elim #94]: #58
#82 := [and-elim #81]: #55
[unit-resolution #82 #95]: false
unsat