src/HOL/SMT/Examples/cert/z3_hol_01

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_hol_01	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,18 @@
+(benchmark Isabelle
+:extrasorts ( T2 T3 T1)
+:extrafuns (
+  (uf_2 T1 T2 T3 T1)
+  (uf_1 T1 T2 T3)
+  (uf_6 T1)
+  (uf_3 T2)
+  (uf_4 T2)
+  (uf_5 T2)
+  (uf_7 T3)
+  (uf_8 T3)
+ )
+:assumption (forall (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2) (= (uf_1 (uf_2 ?x1 ?x2 ?x3) ?x4) (ite (= ?x4 ?x2) ?x3 (uf_1 ?x1 ?x4))))
+:assumption (forall (?x5 T1) (?x6 T2) (?x7 T3) (= (uf_1 (uf_2 ?x5 ?x6 ?x7) ?x6) ?x7))
+:assumption (and (not (= uf_3 uf_4)) (not (= uf_3 uf_5)))
+:assumption (not (= (uf_1 (uf_2 (uf_2 uf_6 uf_4 uf_7) uf_5 uf_8) uf_3) (uf_1 uf_6 uf_3)))
+:formula true
+)