--- a/src/HOL/SMT/Examples/cert/z3_linarith_10.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#2 := false
-#6 := 5::int
-#4 := 2::int
-#5 := (+ 2::int 2::int)
-#7 := (= #5 5::int)
-#8 := (not #7)
-#9 := (not #8)
-#48 := (iff #9 false)
-#1 := true
-#43 := (not true)
-#46 := (iff #43 false)
-#47 := [rewrite]: #46
-#44 := (iff #9 #43)
-#41 := (iff #8 true)
-#36 := (not false)
-#39 := (iff #36 true)
-#40 := [rewrite]: #39
-#37 := (iff #8 #36)
-#34 := (iff #7 false)
-#26 := 4::int
-#29 := (= 4::int 5::int)
-#32 := (iff #29 false)
-#33 := [rewrite]: #32
-#30 := (iff #7 #29)
-#27 := (= #5 4::int)
-#28 := [rewrite]: #27
-#31 := [monotonicity #28]: #30
-#35 := [trans #31 #33]: #34
-#38 := [monotonicity #35]: #37
-#42 := [trans #38 #40]: #41
-#45 := [monotonicity #42]: #44
-#49 := [trans #45 #47]: #48
-#25 := [asserted]: #9
-[mp #25 #49]: false
-unsat