-
Notifications
You must be signed in to change notification settings - Fork 3
/
fol_canonicalization_test.txt
108 lines (106 loc) · 6.06 KB
/
fol_canonicalization_test.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
f(a) & g(a); f(a) & g(a);
f(a) & ~g(a); f(a) & ~g(a);
f(a) & f(a); f(a);
f(a) & g(a) & h(a); f(a) & g(a) & h(a);
g(a) & (f(a) & h(a)); f(a) & g(a) & h(a);
f(a) => f(a); T;
f(a) | (h(a) | g(a)); f(a) | g(a) | h(a);
?[X]:(f(X) & g(X)); ?[X]:(f(X) & g(X));
![X]:(f(a) & f(X)); f(a) & ![X]:f(X);
?[X]:(f(X) | f(a)); f(a) | ?[X]:f(X);
![X]:(g(b) & f(a)); f(a) & g(b);
?[X]:(f(a) => f(X)); f(a) => ?[X]:f(X);
?[X]:(f(a) => ~f(X)); f(a) => ?[X]:~f(X);
![X]:(f(X) => f(a)); f(a) | ![X]:~f(X);
?[X,Y]:(f(X) => f(Y)); ?[Y]:f(Y) | ?[X]:~f(X);
~~f(a); f(a);
![X]:f(a); f(a);
![X]:(~f(a) & f(X)); ![X]:f(X) & ~f(a);
~![X]:~f(a); f(a);
~f(a) & (f(a) & g(a)); F;
F & (f(a) & g(a)); F;
F | (f(a) & g(a)); f(a) & g(a);
T & (f(a) & g(a)); f(a) & g(a);
T | (f(a) & g(a)); T;
f(a) <=> f(a); T;
(f(a) & g(a)) | T; T;
f(a) => ~f(a); ~f(a);
F => f(a); T;
a=a; T;
a=b; F;
h(a) & ~k(a) & ~g(a) & f(a) & f(b); f(a) & f(b) & h(a) & ~g(a) & ~k(a);
(f(a) & g(b)) | (h(c) & ~(i(d) => i(d))); f(a) & g(b);
f(a) <=> (g(b) <=> (~(h(c) => h(c)) <=> ~(h(d) => h(d)))); f(a) <=> g(b);
f(a) <=> (g(b) <=> (~(h(c) => h(c)) <=> (~(h(d) => h(d)) <=> F))); ~(f(a) <=> g(b));
(f(a) <=> g(b)) <=> (~(h(c) => h(c)) <=> (~(h(d) => h(d)) <=> F)); ~(f(a) <=> g(b));
![X,Y]:(f(a) | f(X) | f(Y)); f(a) | ![X]:f(X);
?[X,Y,Z]:![U,V]:(f(a) & f(X) & f(Y) & f(Z) & (f(U) => f(V))); f(a) & (![V]:f(V) | ![U]:~f(U)) & ?[X]:f(X);
~~f(a) & f(a) & (~~![X]:g(a) | ?[Y,Z]:~g(a)); f(a);
![X]:(f(a) | (f(b) & (f(c) | (f(d) & f(X))))); f(a) | (f(b) & (f(c) | (f(d) & ![X]:f(X))));
(f(a) & g(b)) => (f(c) | h(d)); (f(a) & g(b)) => (f(c) | h(d));
?[Y]:(f(a) | (f(b) => (f(c) | f(Y)))); f(a) | (f(b) => (f(c) | ?[Y]:f(Y)));
?[Y]:(f(a) | (f(b) & (f(c) | f(Y)))); f(a) | (f(b) & (f(c) | ?[Y]:f(Y)));
?[Y]:(f(a) | (f(b) | (f(c) | f(Y)))); f(a) | f(b) | f(c) | ?[Y]:f(Y);
?[Y]:(f(a) | (g(Y) | (f(c) | f(Y)))); f(a) | f(c) | ?[Y]:(f(Y) | g(Y));
?[Y]:(f(a) | (g(Y) & (f(c) | f(d)))); f(a) | ((f(c) | f(d)) & ?[Y]:g(Y));
![X]:(~(f(a) => f(X)) => f(c)); f(c) | (f(a) => ![X]:f(X));
(f(a) & g(a)) & (f(a) & ~g(a)); F;
(~f(a) & ~g(a)) & (~f(a) & g(a)); F;
(f(a) & g(a)) & (g(a) & f(a)); f(a) & g(a);
(h(a) & f(a)) & (g(a) & f(a)); f(a) & g(a) & h(a);
(f(a) <=> g(a)) <=> (f(a) <=> (f(a) <=> ~g(a))); ~f(a);
((f(a) <=> ~g(a)) <=> f(a)) <=> (f(a) <=> g(a)); ~f(a);
(~f(a) <=> ~g(a)) <=> (~f(a) <=> (~f(a) <=> ~g(a))); ~f(a);
(f(a) => g(a)) => (h(b) => g(b)); (h(b) & (f(a) => g(a))) => g(b);
(~f(a) => ~g(a)) => (~h(b) => ~g(b)); ((~f(a) => ~g(a)) & ~h(b)) => ~g(b);
![X]:((~f(a) => ~g(a)) => (~h(X) => ~g(X))); (~f(a) => ~g(a)) => ![X]:(~h(X) => ~g(X));
?[X]:(~f(a) => (f(X) & ~f(X))); f(a);
?[X]:((f(X) | ~f(X)) => ~f(a)); ~f(a);
((~f(a) <=> ~h(a)) <=> ~g(a)) <=> (f(a) <=> g(a)); ~h(a);
(f(a) <=> g(a)) <=> ((~f(b) <=> ~h(a)) <=> ~g(b)); f(a) <=> g(a) <=> ~f(b) <=> ~g(b) <=> ~h(a);
?[X]:((f(X) & ~f(a)) => (~f(X) | f(X))); T;
f(a) | (g(b) => (f(a) | (g(b) => f(a)))); f(a) | (g(b) => f(a));
f(a) | (g(b) => (f(a) | f(b) | (g(b) => (~h(a) | ~g(b))))); f(a) | (g(b) => (f(a) | f(b) | ~g(b) | ~h(a)));
g(a) => (f(a) | f(b) | (g(b) => (~h(a) | ~g(b)))); (g(a) & g(b)) => (f(a) | f(b) | ~g(b) | ~h(a));
g(a) => (f(a) | f(b) | (~g(b) => (h(a) | g(b)))); (g(a) & ~g(b)) => (f(a) | f(b) | g(b) | h(a));
(f(a) <=> f(b)) <=> (g(a) <=> ~f(b)); ~(f(a) <=> g(a));
(f(a) <=> g(a)) <=> (~f(a) <=> ~g(a)); T;
((f(a) <=> g(a)) <=> ~h(a)) <=> ((~f(a) <=> ~g(a)) <=> h(a)); F;
(f(a) | g(b)) | (~f(a) | h(c)); T;
(f(a) <=> F) <=> ~f(a); T;
(f(a) <=> a = b) <=> ~f(a); T;
(f(a) <=> ~(a = a)) <=> ~f(a); T;
(f(a) <=> g(b)) <=> ~f(a); ~g(b);
f(a) <=> f(a) <=> f(a); f(a);
(f(a) & g(b)) & ~f(a); F;
(f(a) | g(b)) | ~f(a); T;
((f(a) <=> g(b)) <=> g(c)) <=> ~f(a); ~(g(b) <=> g(c));
~f(a) <=> (f(a) <=> g(b)); ~g(b);
~f(a) & (f(a) & g(b)); F;
~f(a) | (f(a) | g(b)); T;
~f(a) <=> ((f(a) <=> g(b)) <=> g(c)); ~(g(b) <=> g(c));
~(f(a) <=> ![X]:g(X)) => (f(a) <=> ![X]:g(X)); f(a) <=> ![X]:g(X);
(f(a) <=> ![X]:g(X)) => ~(f(a) <=> ![X]:g(X)); ~(f(a) <=> ![X]:g(X));
~(f(a) <=> ![X]:g(X)) => ~(f(b) <=> ![X]:g(X)); ~(f(a) <=> ![X]:g(X)) => ~(f(b) <=> ![X]:g(X));
~(f(a) <=> g(b)) & (g(a) <=> f(a)); (f(a) <=> g(a)) & ~(f(a) <=> g(b));
~(f(a) <=> g(b)) & ~(g(a) <=> f(a)); ~(f(a) <=> g(a)) & ~(f(a) <=> g(b));
~(a=a <=> f(a) <=> g(b)) & ~(g(a) <=> f(a)); ~(f(a) <=> g(a)) & ~(f(a) <=> g(b));
(~f(a) & ~g(b)) => (~f(a) | ~h(c)); T;
~f(a) => (f(a) => ~h(c)); T;
(~f(a) & ~g(b)) => (f(a) => ~h(c)); T;
?[X]:(f(a) & ~?[Y]:~f(Y) & ~f(X)); F;
?[X]:(a=a & ~?[Y]:~f(Y) & ~f(X)); F;
?[X]:(f(a) | ~?[Y]:~f(Y) | ~f(X)); T;
?[X]:(f(a) => (g(X) & ~f(X))); f(a) => ?[X]:(g(X) & ~f(X));
?[X]:(f(a) => (b=X & ~f(X))); f(a) => ?[X]:(X=b & ~f(X));
?[X]:(f(a) => (X=b & ~f(X))); f(a) => ?[X]:(X=b & ~f(X));
![X]:((f(X) & g(X)) => f(a)); f(a) | ![X]:~(f(X) & g(X));
![X]:(~(f(X) & g(X)) => f(a)); f(a) | ![X]:(f(X) & g(X));
![X]:(~(f(X) & g(X)) => (f(a) | ~![Y]:(f(Y) & g(Y)))); T;
?[X]:(f(a) => (g(X) | ~?[Y]:(g(Y) | ~f(Y)) | ~f(X))); T;
g(a) => (f(a) | f(b) | h(c) | (g(c) <=> f(c)) | (~g(b) => (h(a) | g(b)))); (g(a) & ~g(b)) => (f(a) | f(b) | g(b) | h(a) | h(c) | (f(c) <=> g(c)));
g(a) => (f(a) | f(b) | h(c) | (g(c) <=> f(c)) | (~g(b) => (h(a) | g(b))) | (~g(b) => (h(a) | g(c)))); (g(a) & ~g(b)) => (f(a) | f(b) | g(b) | g(c) | h(a) | h(c) | (f(c) <=> g(c)));
g(a) => (h(c) | (g(c) <=> f(c)) | (~g(b) => (h(a) | g(b) | ![X]:f(X) | ![X]:g(X)))); (g(a) & ~g(b)) => (g(b) | h(a) | h(c) | (f(c) <=> g(c)) | ![X]:f(X) | ![X]:g(X));
g(a) => (f(a) | f(b) | h(c) | (g(c) <=> f(c)) | (~g(b) => (~f(a) | g(b)))); T;
g(a) => (f(a) | f(b) | h(c) | (f(c) => (f(a) | g(b))) | (~f(c) => (f(a) | g(b)))); T;
![X]:((f(X) & g(X)) => (f(a) | h(X) | ~![Y]:((f(Y) & g(Y)) => h(Y)))); T;