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_prop_08
changeset 33010 39f73a59e855 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_prop_08	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,22 @@
+(benchmark Isabelle
+:extrasorts ( T1)
+:extrapreds (
+  (up_1)
+  (up_2)
+  (up_3)
+  (up_4)
+  (up_5)
+  (up_6)
+  (up_8)
+  (up_9)
+  (up_7)
+ )
+:assumption (or up_1 (or up_2 (or up_3 up_4)))
+:assumption (or up_5 (or up_6 (and up_1 up_4)))
+:assumption (or (not (or up_1 (and up_3 (not up_3)))) up_2)
+:assumption (or (not (and up_2 (or up_7 (not up_7)))) up_3)
+:assumption (or (not (or up_4 false)) up_3)
+:assumption (not (or up_3 (and (not up_8) (or up_8 (and up_9 (not up_9))))))
+:assumption (not false)
+:formula true
+)
isabelle