Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT/Examples/cert/z3_mono_01
changeset 33010 39f73a59e855 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_mono_01	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,58 @@
+(benchmark Isabelle
+:extrasorts ( T2 T13 T12 T11 T10 T9 T8 T7 T6 T5 T4 T1 T3)
+:extrafuns (
+  (uf_37 T13)
+  (uf_34 T12)
+  (uf_31 T11)
+  (uf_28 T10)
+  (uf_25 T9)
+  (uf_22 T8)
+  (uf_19 T7)
+  (uf_16 T6)
+  (uf_13 T5)
+  (uf_10 T4)
+  (uf_7 T1)
+  (uf_4 T3)
+  (uf_36 Int T13 T13)
+  (uf_33 T13 T12 T12)
+  (uf_30 T12 T11 T11)
+  (uf_27 T11 T10 T10)
+  (uf_24 T10 T9 T9)
+  (uf_21 T9 T8 T8)
+  (uf_18 T8 T7 T7)
+  (uf_15 T7 T6 T6)
+  (uf_12 T6 T5 T5)
+  (uf_9 T5 T4 T4)
+  (uf_6 T4 T1 T1)
+  (uf_3 T1 T3 T3)
+ )
+:extrapreds (
+  (up_35 Int)
+  (up_32 T13)
+  (up_29 T12)
+  (up_26 T11)
+  (up_23 T10)
+  (up_20 T9)
+  (up_17 T8)
+  (up_14 T7)
+  (up_11 T6)
+  (up_8 T5)
+  (up_5 T4)
+  (up_1 T1)
+  (up_2 T3)
+ )
+:assumption (forall (?x1 T1) (and (up_1 ?x1) (or (up_2 (uf_3 ?x1 uf_4)) (not (up_2 (uf_3 ?x1 uf_4))))))
+:assumption (forall (?x2 T4) (and (up_5 ?x2) (or (up_1 (uf_6 ?x2 uf_7)) (not (up_1 (uf_6 ?x2 uf_7))))))
+:assumption (forall (?x3 T5) (and (up_8 ?x3) (or (up_5 (uf_9 ?x3 uf_10)) (not (up_5 (uf_9 ?x3 uf_10))))))
+:assumption (forall (?x4 T6) (and (up_11 ?x4) (or (up_8 (uf_12 ?x4 uf_13)) (not (up_8 (uf_12 ?x4 uf_13))))))
+:assumption (forall (?x5 T7) (and (up_14 ?x5) (or (up_11 (uf_15 ?x5 uf_16)) (not (up_11 (uf_15 ?x5 uf_16))))))
+:assumption (forall (?x6 T8) (and (up_17 ?x6) (or (up_14 (uf_18 ?x6 uf_19)) (not (up_14 (uf_18 ?x6 uf_19))))))
+:assumption (forall (?x7 T9) (and (up_20 ?x7) (or (up_17 (uf_21 ?x7 uf_22)) (not (up_17 (uf_21 ?x7 uf_22))))))
+:assumption (forall (?x8 T10) (and (up_23 ?x8) (or (up_20 (uf_24 ?x8 uf_25)) (not (up_20 (uf_24 ?x8 uf_25))))))
+:assumption (forall (?x9 T11) (and (up_26 ?x9) (or (up_23 (uf_27 ?x9 uf_28)) (not (up_23 (uf_27 ?x9 uf_28))))))
+:assumption (forall (?x10 T12) (and (up_29 ?x10) (or (up_26 (uf_30 ?x10 uf_31)) (not (up_26 (uf_30 ?x10 uf_31))))))
+:assumption (forall (?x11 T13) (and (up_32 ?x11) (or (up_29 (uf_33 ?x11 uf_34)) (not (up_29 (uf_33 ?x11 uf_34))))))
+:assumption (forall (?x12 Int) (and (up_35 ?x12) (or (up_32 (uf_36 ?x12 uf_37)) (not (up_32 (uf_36 ?x12 uf_37))))))
+:assumption (not (up_35 1))
+:formula true
+)
isabelle