6 |
6 |
7 theory Clausify |
7 theory Clausify |
8 imports Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 text {* Definitional CNF for goal *} |
|
12 |
|
13 (* FIXME: shouldn't need this *) |
11 (* FIXME: shouldn't need this *) |
14 declare [[unify_search_bound = 100]] |
12 declare [[unify_search_bound = 100]] |
15 declare [[unify_trace_bound = 100]] |
13 declare [[unify_trace_bound = 100]] |
16 |
14 |
|
15 text {* Definitional CNF for facts *} |
|
16 |
|
17 declare [[meson_max_clauses = 10]] |
|
18 |
|
19 axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
20 qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
|
21 |
|
22 declare [[metis_new_skolemizer = false]] |
|
23 |
|
24 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
25 by (metis qax) |
|
26 |
|
27 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
28 by (metisFT qax) |
|
29 |
|
30 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
|
31 by (metis qax) |
|
32 |
|
33 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
|
34 by (metisFT qax) |
|
35 |
|
36 declare [[metis_new_skolemizer]] |
|
37 |
|
38 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
39 by (metis qax) |
|
40 |
|
41 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
42 by (metisFT qax) |
|
43 |
|
44 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
|
45 by (metis qax) |
|
46 |
|
47 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
|
48 by (metisFT qax) |
|
49 |
|
50 declare [[meson_max_clauses = 60]] |
|
51 |
|
52 axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
53 rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or> |
|
54 (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or> |
|
55 (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> |
|
56 (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" |
|
57 |
|
58 declare [[metis_new_skolemizer = false]] |
|
59 |
|
60 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
61 by (metis rax) |
|
62 |
|
63 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
64 by (metisFT rax) |
|
65 |
|
66 declare [[metis_new_skolemizer]] |
|
67 |
|
68 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
69 by (metis rax) |
|
70 |
|
71 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
72 by (metisFT rax) |
|
73 |
|
74 text {* Definitional CNF for goal *} |
|
75 |
17 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
76 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
18 pax: "\<exists>b. \<forall>a. ((p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b))" |
77 pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)" |
19 |
78 |
20 declare [[metis_new_skolemizer = false]] |
79 declare [[metis_new_skolemizer = false]] |
21 |
80 |
22 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and> |
81 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and> |
23 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
82 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |