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(v2)*I(v1)) = v1*v2 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(v3*(I(v2*v1)*v2))*v3 = 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(v4*(I(v3*v2)*v3))*(v4*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(v2*I(v1)) = v1*I(v2) 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(v2)*v1) = I(v1)*v2 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(v2*v1) = I(v1)*I(v2) 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(v2*v1) = I(v1)*I(v2) 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) 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(v2)*I(v1)) = v1*v2 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(v3*(I(v2*v1)*v2))*v3 = 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(v4*(I(v3*v2)*v3))*(v4*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(v2*I(v1)) = v1*I(v2) 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(v2)*v1) = I(v1)*v2 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(v2*v1) = I(v1)*I(v2) 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(v2*v1) = I(v1)*I(v2) 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) 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(v2)*I(v1)) = v1*v2 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(v3*(I(v2*v1)*v2))*v3 = 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(v4*(I(v3*v2)*v3))*(v4*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(v2*I(v1)) = v1*I(v2) 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(v2)*v1) = I(v1)*v2 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(v2*v1) = I(v1)*I(v2) 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(v2*v1) = I(v1)*I(v2) 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)