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

reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)

#2 := false
#4 := 3::real
#5 := (= 3::real 3::real)
#6 := (not #5)
#30 := (iff #6 false)
#1 := true
#25 := (not true)
#28 := (iff #25 false)
#29 := [rewrite]: #28
#26 := (iff #6 #25)
#23 := (iff #5 true)
#24 := [rewrite]: #23
#27 := [monotonicity #24]: #26
#31 := [trans #27 #29]: #30
#22 := [asserted]: #6
[mp #22 #31]: false
unsat