ocaml/test/Results/kb.out

1 : U*v1 = v1
2 : I(v1)*v1 = U
3 : (v3*v2)*v1 = v3*(v2*v1)
4 : A*B = B*A
5 : C*C = U
6 : I(A) = C*(A*I(C))
7 : C*(B*I(C)) = B
8 : I(v2)*(v2*v1) = v1
9 : A*(B*v1) = B*(A*v1)
10 : C*(C*v1) = v1
11 : C*(A*(I(C)*A)) = U
12 : C*(B*(I(C)*v1)) = B*v1
13 : I(U)*v1 = v1
14 : I(I(v1))*U = v1
15 : I(v3*v2)*(v3*(v2*v1)) = v1
16 : C*(A*(I(C)*(B*A))) = B
17 : I(C)*U = C
18 : C*(A*(I(C)*(A*v1))) = v1
19 : I(C)*B = B*I(C)
20 : I(I(v2))*v1 = v2*v1
Rule 14 deleted
21 : v1*U = v1
Rule 17 deleted
22 : I(C) = C
Rule 19 deleted
Rule 18 deleted
Rule 16 deleted
Rule 12 deleted
Rule 11 deleted
Rule 7 deleted
23 : C*B = B*C
24 : C*(A*(C*(A*v1))) = v1
25 : C*(A*(C*(B*A))) = B
26 : C*(B*(C*v1)) = B*v1
27 : C*(A*(C*A)) = U
28 : C*(B*C) = B
29 : C*(A*(C*(B*(A*v1)))) = B*v1
30 : I(I(v2*v1)*v2) = v1
31 : I(v2*I(v1))*v2 = v1
32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1
33 : I(v1*A)*(v1*(B*A)) = B
34 : I(v1*C)*v1 = C
35 : I(v3*I(v2))*(v3*v1) = v2*v1
36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1
37 : I(v2*C)*(v2*v1) = C*v1
38 : v1*I(v1) = U
39 : I(C*(A*C))*v1 = A*v1
40 : v2*(I(v2)*v1) = v1
41 : I(U) = U
Rule 13 deleted
42 : I(I(v1)) = v1
Rule 20 deleted
43 : C*(B*v1) = B*(C*v1)
Rule 29 deleted
Rule 28 deleted
Rule 26 deleted
Rule 25 deleted
44 : A*(C*(A*v1)) = C*v1
Rule 24 deleted
45 : A*(C*A) = C
Rule 27 deleted
46 : v2*(I(v1*v2)*v1) = U
47 : I(I(v3*(v2*v1))*(v3*v2)) = v1
48 : I(I(B*A)*A) = B
49 : v3*(I(v2*v3)*(v2*v1)) = v1
50 : I(I(v1)*I(v2)) = v2*v1
51 : I(I(B*(A*v1))*A) = B*v1
52 : I(I(v1)*C) = C*v1
53 : I(v2*I(v1*v2)) = v1
54 : I(v3*(v2*I(v1)))*(v3*v2) = v1
55 : I(v1*(C*(A*C)))*v1 = A
56 : v2*I(I(v1)*v2) = v1
57 : I(v2*(I(v3*v1)*v3))*v2 = v1
58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1
59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B
60 : I(v2*(v1*C))*(v2*v1) = C
61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1
62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1
63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1
64 : I(v3*(I(v4*v2)*v4))*(v3*v1) = v2*v1
65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1
66 : I(I(B)*A)*A = B
67 : I(A*A)*(B*(A*A)) = B
68 : v1*(I(A*v1)*(B*A)) = B
69 : I(I(v1*A)*(v1*B))*B = A
70 : v1*I(C*v1) = C
71 : I(A*I(v1))*(B*A) = v1*B
72 : I(C*I(v1)) = v1*C
73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1
74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1)
75 : v3*(I(I(v2)*v3)*v1) = v2*v1
76 : I(I(B*I(v1))*A)*(v1*A) = B
77 : I(v1*A)*(v1*(B*(B*A))) = B*B
78 : I(I(B)*A)*(A*v1) = B*v1
79 : I(A*A)*(B*(A*(A*v1))) = B*v1
80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1)
81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1
82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1
83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1
84 : I(A*C)*(B*A) = B*C
85 : I(A*C)*(B*(A*v1)) = B*(C*v1)
86 : v2*(I(C*v2)*v1) = C*v1
87 : I(I(B*C)*A)*(C*A) = B
88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1
89 : v2*(v1*I(v2*v1)) = U
90 : B*(A*I(B)) = A
91 : I(v2*v1)*v2 = I(v1)
Rule 64 deleted
Rule 57 deleted
Rule 55 deleted
Rule 46 deleted
Rule 34 deleted
Rule 31 deleted
Rule 30 deleted
92 : I(C*(A*C)) = A
Rule 39 deleted
93 : I(v3*(v2*v1))*(v3*v2) = I(v1)
Rule 60 deleted
Rule 54 deleted
Rule 47 deleted
94 : I(v1*I(v2)) = v2*I(v1)
Rule 83 deleted
Rule 76 deleted
Rule 74 deleted
Rule 72 deleted
Rule 71 deleted
Rule 53 deleted
Rule 50 deleted
Rule 35 deleted
95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1
96 : I(v1*(I(B)*A))*(v1*A) = B
97 : I(v1*A)*(v1*B) = B*(C*(A*C))
Rule 82 deleted
Rule 69 deleted
98 : I(v1*C) = C*I(v1)
Rule 88 deleted
Rule 87 deleted
Rule 85 deleted
Rule 84 deleted
Rule 52 deleted
Rule 37 deleted
99 : v3*(v2*(I(v3*v2)*v1)) = v1
100 : B*(A*(I(B)*v1)) = A*v1
101 : I(v3*v2)*(v3*v1) = I(v2)*v1
Rule 97 deleted
Rule 96 deleted
Rule 95 deleted
Rule 93 deleted
Rule 80 deleted
Rule 77 deleted
Rule 73 deleted
Rule 65 deleted
Rule 63 deleted
Rule 62 deleted
Rule 61 deleted
Rule 59 deleted
Rule 58 deleted
Rule 49 deleted
Rule 36 deleted
Rule 33 deleted
Rule 32 deleted
Rule 15 deleted
102 : B*(C*I(B)) = C
103 : B*(C*(I(B)*v1)) = C*v1
104 : B*(I(B*A)*A) = U
105 : B*(I(B*A)*(A*v1)) = v1
106 : I(B*A)*A = I(B)
Rule 104 deleted
Rule 48 deleted
107 : B*(v1*(I(B*(A*v1))*A)) = U
108 : I(I(B*(B*A))*A) = B*B
109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1
110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1)
111 : I(I(B)*A) = B*(C*(A*C))
Rule 78 deleted
Rule 66 deleted
112 : I(I(B*v1)*A) = B*(C*(A*(C*v1)))
Rule 110 deleted
Rule 108 deleted
Rule 51 deleted
113 : v3*(v2*I(I(v1)*(v3*v2))) = v1
114 : v1*I(C*(A*(C*v1))) = A
115 : I(I(v1)*v2) = I(v2)*v1
Rule 113 deleted
Rule 112 deleted
Rule 111 deleted
Rule 75 deleted
Rule 56 deleted
116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B
117 : I(A*v1)*(B*A) = I(v1)*B
Rule 116 deleted
Rule 68 deleted
118 : v2*(v1*I(C*(v2*v1))) = C
119 : I(C*v1) = I(v1)*C
Rule 118 deleted
Rule 114 deleted
Rule 92 deleted
Rule 86 deleted
Rule 70 deleted
120 : v1*(I(A*(C*v1))*C) = A
121 : I(A*A)*(B*(B*(A*A))) = B*B
122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1)
123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1)))
Rule 79 deleted
Rule 67 deleted
124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1
125 : v1*(I(A*v1)*(B*(B*A))) = B*B
126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1)
Rule 124 deleted
Rule 123 deleted
Rule 81 deleted
127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U
128 : v2*I(v1*v2) = I(v1)
Rule 89 deleted
129 : A*I(B) = I(B)*A
Rule 90 deleted
130 : I(v1*v2) = I(v2)*I(v1)
Rule 128 deleted
Rule 127 deleted
Rule 126 deleted
Rule 125 deleted
Rule 122 deleted
Rule 121 deleted
Rule 120 deleted
Rule 119 deleted
Rule 117 deleted
Rule 115 deleted
Rule 109 deleted
Rule 107 deleted
Rule 106 deleted
Rule 105 deleted
Rule 101 deleted
Rule 99 deleted
Rule 98 deleted
Rule 94 deleted
Rule 91 deleted
131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1
132 : B*(C*(A*(C*(I(B)*A)))) = U
133 : C*(A*(C*(I(B)*A))) = I(B)
Rule 132 deleted
134 : A*(I(B)*v1) = I(B)*(A*v1)
Rule 100 deleted
135 : C*I(B) = I(B)*C
Rule 102 deleted
136 : C*(I(B)*v1) = I(B)*(C*v1)
Rule 133 deleted
Rule 131 deleted
Rule 103 deleted
Canonical set found :
1 : U*v1 = v1
2 : I(v1)*v1 = U
3 : (v3*v2)*v1 = v3*(v2*v1)
4 : A*B = B*A
5 : C*C = U
6 : I(A) = C*(A*C)
8 : I(v2)*(v2*v1) = v1
9 : A*(B*v1) = B*(A*v1)
10 : C*(C*v1) = v1
21 : v1*U = v1
22 : I(C) = C
23 : C*B = B*C
38 : v1*I(v1) = U
40 : v2*(I(v2)*v1) = v1
41 : I(U) = U
42 : I(I(v1)) = v1
43 : C*(B*v1) = B*(C*v1)
44 : A*(C*(A*v1)) = C*v1
45 : A*(C*A) = C
129 : A*I(B) = I(B)*A
130 : I(v1*v2) = I(v2)*I(v1)
134 : A*(I(B)*v1) = I(B)*(A*v1)
135 : C*I(B) = I(B)*C
136 : C*(I(B)*v1) = I(B)*(C*v1)