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

Named_Thms is not scalable;

#2 := false
#5 := 3::int
#6 := 8::int
#7 := (<= 3::int 8::int)
#8 := (ite #7 8::int 3::int)
#4 := 5::int
#9 := (< 5::int #8)
#10 := (not #9)
#50 := (iff #10 false)
#1 := true
#45 := (not true)
#48 := (iff #45 false)
#49 := [rewrite]: #48
#46 := (iff #10 #45)
#43 := (iff #9 true)
#38 := (< 5::int 8::int)
#41 := (iff #38 true)
#42 := [rewrite]: #41
#39 := (iff #9 #38)
#36 := (= #8 8::int)
#31 := (ite true 8::int 3::int)
#34 := (= #31 8::int)
#35 := [rewrite]: #34
#32 := (= #8 #31)
#29 := (iff #7 true)
#30 := [rewrite]: #29
#33 := [monotonicity #30]: #32
#37 := [trans #33 #35]: #36
#40 := [monotonicity #37]: #39
#44 := [trans #40 #42]: #43
#47 := [monotonicity #44]: #46
#51 := [trans #47 #49]: #50
#26 := [asserted]: #10
[mp #26 #51]: false
unsat