summaryrefslogtreecommitdiff
path: root/test/Results/kb.out
diff options
context:
space:
mode:
Diffstat (limited to 'test/Results/kb.out')
-rw-r--r--test/Results/kb.out273
1 files changed, 0 insertions, 273 deletions
diff --git a/test/Results/kb.out b/test/Results/kb.out
deleted file mode 100644
index 758a0b4d60..0000000000
--- a/test/Results/kb.out
+++ /dev/null
@@ -1,273 +0,0 @@
-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)