-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathhol_canonicalization_test.txt
122 lines (119 loc) · 6.34 KB
/
hol_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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
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;
a=4; a=4;
4=a; a=4;
2=2; T;
size(S)=3; size(S)=3;
3=size(S); size(S)=3;
(f(a) & g(a)) | (~f(a) & g(a)); g(a);
~f(a) & g(a) & ~(f(a) & g(a)); g(a) & ~f(a);
(f(a) & g(a)) => f(a); T;
((f(a) & g(a)) => f(a)) => h(a); h(a);
f(a) => ((b=a) | (c=a) | (d=a)); ~f(a);
(^[x]:f(x))(y); f(y);
(^[x]:(f(a)=x))(f(a)); T;
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;
?[x]:(?[y]:f(y)); ?[x]:f(x);
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;