diff options
Diffstat (limited to 'test/Results/kb.out')
-rw-r--r-- | test/Results/kb.out | 273 |
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) |