regression/kitkbjul9.ok

   1 1 : U*v1 = v1
   2 2 : I(v1)*v1 = U
   3 3 : (v3*v2)*v1 = v3*(v2*v1)
   4 4 : A*B = B*A
   5 5 : C*C = U
   6 6 : I(A) = C*(A*I(C))
   7 7 : C*(B*I(C)) = B
   8 8 : I(v2)*(v2*v1) = v1
   9 9 : A*(B*v1) = B*(A*v1)
  10 10 : C*(C*v1) = v1
  11 11 : C*(A*(I(C)*A)) = U
  12 12 : C*(B*(I(C)*v1)) = B*v1
  13 13 : I(U)*v1 = v1
  14 14 : I(I(v1))*U = v1
  15 15 : I(v3*v2)*(v3*(v2*v1)) = v1
  16 16 : C*(A*(I(C)*(B*A))) = B
  17 17 : I(C)*U = C
  18 18 : C*(A*(I(C)*(A*v1))) = v1
  19 19 : I(C)*B = B*I(C)
  20 20 : I(I(v2))*v1 = v2*v1
  21 Rule 14 deleted
  22 21 : v1*U = v1
  23 Rule 17 deleted
  24 22 : I(C) = C
  25 Rule 19 deleted
  26 Rule 18 deleted
  27 Rule 16 deleted
  28 Rule 12 deleted
  29 Rule 11 deleted
  30 Rule 7 deleted
  31 23 : C*B = B*C
  32 24 : C*(A*(C*(A*v1))) = v1
  33 25 : C*(A*(C*(B*A))) = B
  34 26 : C*(B*(C*v1)) = B*v1
  35 27 : C*(A*(C*A)) = U
  36 28 : C*(B*C) = B
  37 29 : C*(A*(C*(B*(A*v1)))) = B*v1
  38 30 : I(I(v2*v1)*v2) = v1
  39 31 : I(v2*I(v1))*v2 = v1
  40 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1
  41 33 : I(v1*A)*(v1*(B*A)) = B
  42 34 : I(v1*C)*v1 = C
  43 35 : I(v3*I(v2))*(v3*v1) = v2*v1
  44 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1
  45 37 : I(v2*C)*(v2*v1) = C*v1
  46 38 : v1*I(v1) = U
  47 39 : I(C*(A*C))*v1 = A*v1
  48 40 : v2*(I(v2)*v1) = v1
  49 41 : I(U) = U
  50 Rule 13 deleted
  51 42 : I(I(v1)) = v1
  52 Rule 20 deleted
  53 43 : C*(B*v1) = B*(C*v1)
  54 Rule 29 deleted
  55 Rule 28 deleted
  56 Rule 26 deleted
  57 Rule 25 deleted
  58 44 : A*(C*(A*v1)) = C*v1
  59 Rule 24 deleted
  60 45 : A*(C*A) = C
  61 Rule 27 deleted
  62 46 : v2*(I(v1*v2)*v1) = U
  63 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1
  64 48 : I(I(B*A)*A) = B
  65 49 : v3*(I(v2*v3)*(v2*v1)) = v1
  66 50 : I(I(v2)*I(v1)) = v1*v2
  67 51 : I(I(B*(A*v1))*A) = B*v1
  68 52 : I(I(v1)*C) = C*v1
  69 53 : I(v2*I(v1*v2)) = v1
  70 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1
  71 55 : I(v1*(C*(A*C)))*v1 = A
  72 56 : v2*I(I(v1)*v2) = v1
  73 57 : I(v3*(I(v2*v1)*v2))*v3 = v1
  74 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1
  75 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B
  76 60 : I(v2*(v1*C))*(v2*v1) = C
  77 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1
  78 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1
  79 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1
  80 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1
  81 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1
  82 66 : I(I(B)*A)*A = B
  83 67 : I(A*A)*(B*(A*A)) = B
  84 68 : v1*(I(A*v1)*(B*A)) = B
  85 69 : I(I(v1*A)*(v1*B))*B = A
  86 70 : v1*I(C*v1) = C
  87 71 : I(A*I(v1))*(B*A) = v1*B
  88 72 : I(C*I(v1)) = v1*C
  89 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1
  90 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1)
  91 75 : v3*(I(I(v2)*v3)*v1) = v2*v1
  92 76 : I(I(B*I(v1))*A)*(v1*A) = B
  93 77 : I(v1*A)*(v1*(B*(B*A))) = B*B
  94 78 : I(I(B)*A)*(A*v1) = B*v1
  95 79 : I(A*A)*(B*(A*(A*v1))) = B*v1
  96 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1)
  97 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1
  98 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1
  99 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1
 100 84 : I(A*C)*(B*A) = B*C
 101 85 : I(A*C)*(B*(A*v1)) = B*(C*v1)
 102 86 : v2*(I(C*v2)*v1) = C*v1
 103 87 : I(I(B*C)*A)*(C*A) = B
 104 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1
 105 89 : v2*(v1*I(v2*v1)) = U
 106 90 : B*(A*I(B)) = A
 107 91 : I(v2*v1)*v2 = I(v1)
 108 Rule 64 deleted
 109 Rule 57 deleted
 110 Rule 55 deleted
 111 Rule 46 deleted
 112 Rule 34 deleted
 113 Rule 31 deleted
 114 Rule 30 deleted
 115 92 : I(C*(A*C)) = A
 116 Rule 39 deleted
 117 93 : I(v3*(v2*v1))*(v3*v2) = I(v1)
 118 Rule 60 deleted
 119 Rule 54 deleted
 120 Rule 47 deleted
 121 94 : I(v2*I(v1)) = v1*I(v2)
 122 Rule 83 deleted
 123 Rule 76 deleted
 124 Rule 74 deleted
 125 Rule 72 deleted
 126 Rule 71 deleted
 127 Rule 53 deleted
 128 Rule 50 deleted
 129 Rule 35 deleted
 130 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1
 131 96 : I(v1*(I(B)*A))*(v1*A) = B
 132 97 : I(v1*A)*(v1*B) = B*(C*(A*C))
 133 Rule 82 deleted
 134 Rule 69 deleted
 135 98 : I(v1*C) = C*I(v1)
 136 Rule 88 deleted
 137 Rule 87 deleted
 138 Rule 85 deleted
 139 Rule 84 deleted
 140 Rule 52 deleted
 141 Rule 37 deleted
 142 99 : v3*(v2*(I(v3*v2)*v1)) = v1
 143 100 : B*(A*(I(B)*v1)) = A*v1
 144 101 : I(v3*v2)*(v3*v1) = I(v2)*v1
 145 Rule 97 deleted
 146 Rule 96 deleted
 147 Rule 95 deleted
 148 Rule 93 deleted
 149 Rule 80 deleted
 150 Rule 77 deleted
 151 Rule 73 deleted
 152 Rule 65 deleted
 153 Rule 63 deleted
 154 Rule 62 deleted
 155 Rule 61 deleted
 156 Rule 59 deleted
 157 Rule 58 deleted
 158 Rule 49 deleted
 159 Rule 36 deleted
 160 Rule 33 deleted
 161 Rule 32 deleted
 162 Rule 15 deleted
 163 102 : B*(C*I(B)) = C
 164 103 : B*(C*(I(B)*v1)) = C*v1
 165 104 : B*(I(B*A)*A) = U
 166 105 : B*(I(B*A)*(A*v1)) = v1
 167 106 : I(B*A)*A = I(B)
 168 Rule 104 deleted
 169 Rule 48 deleted
 170 107 : B*(v1*(I(B*(A*v1))*A)) = U
 171 108 : I(I(B*(B*A))*A) = B*B
 172 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1
 173 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1)
 174 111 : I(I(B)*A) = B*(C*(A*C))
 175 Rule 78 deleted
 176 Rule 66 deleted
 177 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1)))
 178 Rule 110 deleted
 179 Rule 108 deleted
 180 Rule 51 deleted
 181 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1
 182 114 : v1*I(C*(A*(C*v1))) = A
 183 115 : I(I(v2)*v1) = I(v1)*v2
 184 Rule 113 deleted
 185 Rule 112 deleted
 186 Rule 111 deleted
 187 Rule 75 deleted
 188 Rule 56 deleted
 189 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B
 190 117 : I(A*v1)*(B*A) = I(v1)*B
 191 Rule 116 deleted
 192 Rule 68 deleted
 193 118 : v2*(v1*I(C*(v2*v1))) = C
 194 119 : I(C*v1) = I(v1)*C
 195 Rule 118 deleted
 196 Rule 114 deleted
 197 Rule 92 deleted
 198 Rule 86 deleted
 199 Rule 70 deleted
 200 120 : v1*(I(A*(C*v1))*C) = A
 201 121 : I(A*A)*(B*(B*(A*A))) = B*B
 202 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1)
 203 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1)))
 204 Rule 79 deleted
 205 Rule 67 deleted
 206 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1
 207 125 : v1*(I(A*v1)*(B*(B*A))) = B*B
 208 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1)
 209 Rule 124 deleted
 210 Rule 123 deleted
 211 Rule 81 deleted
 212 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U
 213 128 : v2*I(v1*v2) = I(v1)
 214 Rule 89 deleted
 215 129 : A*I(B) = I(B)*A
 216 Rule 90 deleted
 217 130 : I(v2*v1) = I(v1)*I(v2)
 218 Rule 128 deleted
 219 Rule 127 deleted
 220 Rule 126 deleted
 221 Rule 125 deleted
 222 Rule 122 deleted
 223 Rule 121 deleted
 224 Rule 120 deleted
 225 Rule 119 deleted
 226 Rule 117 deleted
 227 Rule 115 deleted
 228 Rule 109 deleted
 229 Rule 107 deleted
 230 Rule 106 deleted
 231 Rule 105 deleted
 232 Rule 101 deleted
 233 Rule 99 deleted
 234 Rule 98 deleted
 235 Rule 94 deleted
 236 Rule 91 deleted
 237 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1
 238 132 : B*(C*(A*(C*(I(B)*A)))) = U
 239 133 : C*(A*(C*(I(B)*A))) = I(B)
 240 Rule 132 deleted
 241 134 : A*(I(B)*v1) = I(B)*(A*v1)
 242 Rule 100 deleted
 243 135 : C*I(B) = I(B)*C
 244 Rule 102 deleted
 245 136 : C*(I(B)*v1) = I(B)*(C*v1)
 246 Rule 133 deleted
 247 Rule 131 deleted
 248 Rule 103 deleted
 249 Canonical set found :
 250 1 : U*v1 = v1
 251 2 : I(v1)*v1 = U
 252 3 : (v3*v2)*v1 = v3*(v2*v1)
 253 4 : A*B = B*A
 254 5 : C*C = U
 255 6 : I(A) = C*(A*C)
 256 8 : I(v2)*(v2*v1) = v1
 257 9 : A*(B*v1) = B*(A*v1)
 258 10 : C*(C*v1) = v1
 259 21 : v1*U = v1
 260 22 : I(C) = C
 261 23 : C*B = B*C
 262 38 : v1*I(v1) = U
 263 40 : v2*(I(v2)*v1) = v1
 264 41 : I(U) = U
 265 42 : I(I(v1)) = v1
 266 43 : C*(B*v1) = B*(C*v1)
 267 44 : A*(C*(A*v1)) = C*v1
 268 45 : A*(C*A) = C
 269 129 : A*I(B) = I(B)*A
 270 130 : I(v2*v1) = I(v1)*I(v2)
 271 134 : A*(I(B)*v1) = I(B)*(A*v1)
 272 135 : C*I(B) = I(B)*C
 273 136 : C*(I(B)*v1) = I(B)*(C*v1)
 274 1 : U*v1 = v1
 275 2 : I(v1)*v1 = U
 276 3 : (v3*v2)*v1 = v3*(v2*v1)
 277 4 : A*B = B*A
 278 5 : C*C = U
 279 6 : I(A) = C*(A*I(C))
 280 7 : C*(B*I(C)) = B
 281 8 : I(v2)*(v2*v1) = v1
 282 9 : A*(B*v1) = B*(A*v1)
 283 10 : C*(C*v1) = v1
 284 11 : C*(A*(I(C)*A)) = U
 285 12 : C*(B*(I(C)*v1)) = B*v1
 286 13 : I(U)*v1 = v1
 287 14 : I(I(v1))*U = v1
 288 15 : I(v3*v2)*(v3*(v2*v1)) = v1
 289 16 : C*(A*(I(C)*(B*A))) = B
 290 17 : I(C)*U = C
 291 18 : C*(A*(I(C)*(A*v1))) = v1
 292 19 : I(C)*B = B*I(C)
 293 20 : I(I(v2))*v1 = v2*v1
 294 Rule 14 deleted
 295 21 : v1*U = v1
 296 Rule 17 deleted
 297 22 : I(C) = C
 298 Rule 19 deleted
 299 Rule 18 deleted
 300 Rule 16 deleted
 301 Rule 12 deleted
 302 Rule 11 deleted
 303 Rule 7 deleted
 304 23 : C*B = B*C
 305 24 : C*(A*(C*(A*v1))) = v1
 306 25 : C*(A*(C*(B*A))) = B
 307 26 : C*(B*(C*v1)) = B*v1
 308 27 : C*(A*(C*A)) = U
 309 28 : C*(B*C) = B
 310 29 : C*(A*(C*(B*(A*v1)))) = B*v1
 311 30 : I(I(v2*v1)*v2) = v1
 312 31 : I(v2*I(v1))*v2 = v1
 313 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1
 314 33 : I(v1*A)*(v1*(B*A)) = B
 315 34 : I(v1*C)*v1 = C
 316 35 : I(v3*I(v2))*(v3*v1) = v2*v1
 317 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1
 318 37 : I(v2*C)*(v2*v1) = C*v1
 319 38 : v1*I(v1) = U
 320 39 : I(C*(A*C))*v1 = A*v1
 321 40 : v2*(I(v2)*v1) = v1
 322 41 : I(U) = U
 323 Rule 13 deleted
 324 42 : I(I(v1)) = v1
 325 Rule 20 deleted
 326 43 : C*(B*v1) = B*(C*v1)
 327 Rule 29 deleted
 328 Rule 28 deleted
 329 Rule 26 deleted
 330 Rule 25 deleted
 331 44 : A*(C*(A*v1)) = C*v1
 332 Rule 24 deleted
 333 45 : A*(C*A) = C
 334 Rule 27 deleted
 335 46 : v2*(I(v1*v2)*v1) = U
 336 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1
 337 48 : I(I(B*A)*A) = B
 338 49 : v3*(I(v2*v3)*(v2*v1)) = v1
 339 50 : I(I(v2)*I(v1)) = v1*v2
 340 51 : I(I(B*(A*v1))*A) = B*v1
 341 52 : I(I(v1)*C) = C*v1
 342 53 : I(v2*I(v1*v2)) = v1
 343 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1
 344 55 : I(v1*(C*(A*C)))*v1 = A
 345 56 : v2*I(I(v1)*v2) = v1
 346 57 : I(v3*(I(v2*v1)*v2))*v3 = v1
 347 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1
 348 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B
 349 60 : I(v2*(v1*C))*(v2*v1) = C
 350 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1
 351 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1
 352 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1
 353 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1
 354 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1
 355 66 : I(I(B)*A)*A = B
 356 67 : I(A*A)*(B*(A*A)) = B
 357 68 : v1*(I(A*v1)*(B*A)) = B
 358 69 : I(I(v1*A)*(v1*B))*B = A
 359 70 : v1*I(C*v1) = C
 360 71 : I(A*I(v1))*(B*A) = v1*B
 361 72 : I(C*I(v1)) = v1*C
 362 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1
 363 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1)
 364 75 : v3*(I(I(v2)*v3)*v1) = v2*v1
 365 76 : I(I(B*I(v1))*A)*(v1*A) = B
 366 77 : I(v1*A)*(v1*(B*(B*A))) = B*B
 367 78 : I(I(B)*A)*(A*v1) = B*v1
 368 79 : I(A*A)*(B*(A*(A*v1))) = B*v1
 369 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1)
 370 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1
 371 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1
 372 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1
 373 84 : I(A*C)*(B*A) = B*C
 374 85 : I(A*C)*(B*(A*v1)) = B*(C*v1)
 375 86 : v2*(I(C*v2)*v1) = C*v1
 376 87 : I(I(B*C)*A)*(C*A) = B
 377 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1
 378 89 : v2*(v1*I(v2*v1)) = U
 379 90 : B*(A*I(B)) = A
 380 91 : I(v2*v1)*v2 = I(v1)
 381 Rule 64 deleted
 382 Rule 57 deleted
 383 Rule 55 deleted
 384 Rule 46 deleted
 385 Rule 34 deleted
 386 Rule 31 deleted
 387 Rule 30 deleted
 388 92 : I(C*(A*C)) = A
 389 Rule 39 deleted
 390 93 : I(v3*(v2*v1))*(v3*v2) = I(v1)
 391 Rule 60 deleted
 392 Rule 54 deleted
 393 Rule 47 deleted
 394 94 : I(v2*I(v1)) = v1*I(v2)
 395 Rule 83 deleted
 396 Rule 76 deleted
 397 Rule 74 deleted
 398 Rule 72 deleted
 399 Rule 71 deleted
 400 Rule 53 deleted
 401 Rule 50 deleted
 402 Rule 35 deleted
 403 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1
 404 96 : I(v1*(I(B)*A))*(v1*A) = B
 405 97 : I(v1*A)*(v1*B) = B*(C*(A*C))
 406 Rule 82 deleted
 407 Rule 69 deleted
 408 98 : I(v1*C) = C*I(v1)
 409 Rule 88 deleted
 410 Rule 87 deleted
 411 Rule 85 deleted
 412 Rule 84 deleted
 413 Rule 52 deleted
 414 Rule 37 deleted
 415 99 : v3*(v2*(I(v3*v2)*v1)) = v1
 416 100 : B*(A*(I(B)*v1)) = A*v1
 417 101 : I(v3*v2)*(v3*v1) = I(v2)*v1
 418 Rule 97 deleted
 419 Rule 96 deleted
 420 Rule 95 deleted
 421 Rule 93 deleted
 422 Rule 80 deleted
 423 Rule 77 deleted
 424 Rule 73 deleted
 425 Rule 65 deleted
 426 Rule 63 deleted
 427 Rule 62 deleted
 428 Rule 61 deleted
 429 Rule 59 deleted
 430 Rule 58 deleted
 431 Rule 49 deleted
 432 Rule 36 deleted
 433 Rule 33 deleted
 434 Rule 32 deleted
 435 Rule 15 deleted
 436 102 : B*(C*I(B)) = C
 437 103 : B*(C*(I(B)*v1)) = C*v1
 438 104 : B*(I(B*A)*A) = U
 439 105 : B*(I(B*A)*(A*v1)) = v1
 440 106 : I(B*A)*A = I(B)
 441 Rule 104 deleted
 442 Rule 48 deleted
 443 107 : B*(v1*(I(B*(A*v1))*A)) = U
 444 108 : I(I(B*(B*A))*A) = B*B
 445 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1
 446 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1)
 447 111 : I(I(B)*A) = B*(C*(A*C))
 448 Rule 78 deleted
 449 Rule 66 deleted
 450 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1)))
 451 Rule 110 deleted
 452 Rule 108 deleted
 453 Rule 51 deleted
 454 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1
 455 114 : v1*I(C*(A*(C*v1))) = A
 456 115 : I(I(v2)*v1) = I(v1)*v2
 457 Rule 113 deleted
 458 Rule 112 deleted
 459 Rule 111 deleted
 460 Rule 75 deleted
 461 Rule 56 deleted
 462 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B
 463 117 : I(A*v1)*(B*A) = I(v1)*B
 464 Rule 116 deleted
 465 Rule 68 deleted
 466 118 : v2*(v1*I(C*(v2*v1))) = C
 467 119 : I(C*v1) = I(v1)*C
 468 Rule 118 deleted
 469 Rule 114 deleted
 470 Rule 92 deleted
 471 Rule 86 deleted
 472 Rule 70 deleted
 473 120 : v1*(I(A*(C*v1))*C) = A
 474 121 : I(A*A)*(B*(B*(A*A))) = B*B
 475 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1)
 476 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1)))
 477 Rule 79 deleted
 478 Rule 67 deleted
 479 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1
 480 125 : v1*(I(A*v1)*(B*(B*A))) = B*B
 481 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1)
 482 Rule 124 deleted
 483 Rule 123 deleted
 484 Rule 81 deleted
 485 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U
 486 128 : v2*I(v1*v2) = I(v1)
 487 Rule 89 deleted
 488 129 : A*I(B) = I(B)*A
 489 Rule 90 deleted
 490 130 : I(v2*v1) = I(v1)*I(v2)
 491 Rule 128 deleted
 492 Rule 127 deleted
 493 Rule 126 deleted
 494 Rule 125 deleted
 495 Rule 122 deleted
 496 Rule 121 deleted
 497 Rule 120 deleted
 498 Rule 119 deleted
 499 Rule 117 deleted
 500 Rule 115 deleted
 501 Rule 109 deleted
 502 Rule 107 deleted
 503 Rule 106 deleted
 504 Rule 105 deleted
 505 Rule 101 deleted
 506 Rule 99 deleted
 507 Rule 98 deleted
 508 Rule 94 deleted
 509 Rule 91 deleted
 510 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1
 511 132 : B*(C*(A*(C*(I(B)*A)))) = U
 512 133 : C*(A*(C*(I(B)*A))) = I(B)
 513 Rule 132 deleted
 514 134 : A*(I(B)*v1) = I(B)*(A*v1)
 515 Rule 100 deleted
 516 135 : C*I(B) = I(B)*C
 517 Rule 102 deleted
 518 136 : C*(I(B)*v1) = I(B)*(C*v1)
 519 Rule 133 deleted
 520 Rule 131 deleted
 521 Rule 103 deleted
 522 Canonical set found :
 523 1 : U*v1 = v1
 524 2 : I(v1)*v1 = U
 525 3 : (v3*v2)*v1 = v3*(v2*v1)
 526 4 : A*B = B*A
 527 5 : C*C = U
 528 6 : I(A) = C*(A*C)
 529 8 : I(v2)*(v2*v1) = v1
 530 9 : A*(B*v1) = B*(A*v1)
 531 10 : C*(C*v1) = v1
 532 21 : v1*U = v1
 533 22 : I(C) = C
 534 23 : C*B = B*C
 535 38 : v1*I(v1) = U
 536 40 : v2*(I(v2)*v1) = v1
 537 41 : I(U) = U
 538 42 : I(I(v1)) = v1
 539 43 : C*(B*v1) = B*(C*v1)
 540 44 : A*(C*(A*v1)) = C*v1
 541 45 : A*(C*A) = C
 542 129 : A*I(B) = I(B)*A
 543 130 : I(v2*v1) = I(v1)*I(v2)
 544 134 : A*(I(B)*v1) = I(B)*(A*v1)
 545 135 : C*I(B) = I(B)*C
 546 136 : C*(I(B)*v1) = I(B)*(C*v1)
 547 1 : U*v1 = v1
 548 2 : I(v1)*v1 = U
 549 3 : (v3*v2)*v1 = v3*(v2*v1)
 550 4 : A*B = B*A
 551 5 : C*C = U
 552 6 : I(A) = C*(A*I(C))
 553 7 : C*(B*I(C)) = B
 554 8 : I(v2)*(v2*v1) = v1
 555 9 : A*(B*v1) = B*(A*v1)
 556 10 : C*(C*v1) = v1
 557 11 : C*(A*(I(C)*A)) = U
 558 12 : C*(B*(I(C)*v1)) = B*v1
 559 13 : I(U)*v1 = v1
 560 14 : I(I(v1))*U = v1
 561 15 : I(v3*v2)*(v3*(v2*v1)) = v1
 562 16 : C*(A*(I(C)*(B*A))) = B
 563 17 : I(C)*U = C
 564 18 : C*(A*(I(C)*(A*v1))) = v1
 565 19 : I(C)*B = B*I(C)
 566 20 : I(I(v2))*v1 = v2*v1
 567 Rule 14 deleted
 568 21 : v1*U = v1
 569 Rule 17 deleted
 570 22 : I(C) = C
 571 Rule 19 deleted
 572 Rule 18 deleted
 573 Rule 16 deleted
 574 Rule 12 deleted
 575 Rule 11 deleted
 576 Rule 7 deleted
 577 23 : C*B = B*C
 578 24 : C*(A*(C*(A*v1))) = v1
 579 25 : C*(A*(C*(B*A))) = B
 580 26 : C*(B*(C*v1)) = B*v1
 581 27 : C*(A*(C*A)) = U
 582 28 : C*(B*C) = B
 583 29 : C*(A*(C*(B*(A*v1)))) = B*v1
 584 30 : I(I(v2*v1)*v2) = v1
 585 31 : I(v2*I(v1))*v2 = v1
 586 32 : I(v4*(v3*v2))*(v4*(v3*(v2*v1))) = v1
 587 33 : I(v1*A)*(v1*(B*A)) = B
 588 34 : I(v1*C)*v1 = C
 589 35 : I(v3*I(v2))*(v3*v1) = v2*v1
 590 36 : I(v2*A)*(v2*(B*(A*v1))) = B*v1
 591 37 : I(v2*C)*(v2*v1) = C*v1
 592 38 : v1*I(v1) = U
 593 39 : I(C*(A*C))*v1 = A*v1
 594 40 : v2*(I(v2)*v1) = v1
 595 41 : I(U) = U
 596 Rule 13 deleted
 597 42 : I(I(v1)) = v1
 598 Rule 20 deleted
 599 43 : C*(B*v1) = B*(C*v1)
 600 Rule 29 deleted
 601 Rule 28 deleted
 602 Rule 26 deleted
 603 Rule 25 deleted
 604 44 : A*(C*(A*v1)) = C*v1
 605 Rule 24 deleted
 606 45 : A*(C*A) = C
 607 Rule 27 deleted
 608 46 : v2*(I(v1*v2)*v1) = U
 609 47 : I(I(v3*(v2*v1))*(v3*v2)) = v1
 610 48 : I(I(B*A)*A) = B
 611 49 : v3*(I(v2*v3)*(v2*v1)) = v1
 612 50 : I(I(v2)*I(v1)) = v1*v2
 613 51 : I(I(B*(A*v1))*A) = B*v1
 614 52 : I(I(v1)*C) = C*v1
 615 53 : I(v2*I(v1*v2)) = v1
 616 54 : I(v3*(v2*I(v1)))*(v3*v2) = v1
 617 55 : I(v1*(C*(A*C)))*v1 = A
 618 56 : v2*I(I(v1)*v2) = v1
 619 57 : I(v3*(I(v2*v1)*v2))*v3 = v1
 620 58 : I(v5*(v4*(v3*v2)))*(v5*(v4*(v3*(v2*v1)))) = v1
 621 59 : I(v2*(v1*A))*(v2*(v1*(B*A))) = B
 622 60 : I(v2*(v1*C))*(v2*v1) = C
 623 61 : I(v4*(v3*I(v2)))*(v4*(v3*v1)) = v2*v1
 624 62 : I(v3*(v2*A))*(v3*(v2*(B*(A*v1)))) = B*v1
 625 63 : I(v3*(v2*C))*(v3*(v2*v1)) = C*v1
 626 64 : I(v4*(I(v3*v2)*v3))*(v4*v1) = v2*v1
 627 65 : v4*(I(v3*(v2*v4))*(v3*(v2*v1))) = v1
 628 66 : I(I(B)*A)*A = B
 629 67 : I(A*A)*(B*(A*A)) = B
 630 68 : v1*(I(A*v1)*(B*A)) = B
 631 69 : I(I(v1*A)*(v1*B))*B = A
 632 70 : v1*I(C*v1) = C
 633 71 : I(A*I(v1))*(B*A) = v1*B
 634 72 : I(C*I(v1)) = v1*C
 635 73 : I(v2*(C*(A*C)))*(v2*v1) = A*v1
 636 74 : I(A*I(v2))*(B*(A*v1)) = v2*(B*v1)
 637 75 : v3*(I(I(v2)*v3)*v1) = v2*v1
 638 76 : I(I(B*I(v1))*A)*(v1*A) = B
 639 77 : I(v1*A)*(v1*(B*(B*A))) = B*B
 640 78 : I(I(B)*A)*(A*v1) = B*v1
 641 79 : I(A*A)*(B*(A*(A*v1))) = B*v1
 642 80 : I(v2*A)*(v2*(B*(B*(A*v1)))) = B*(B*v1)
 643 81 : v2*(I(A*v2)*(B*(A*v1))) = B*v1
 644 82 : I(I(v2*A)*(v2*B))*(B*v1) = A*v1
 645 83 : I(I(B*I(v2))*A)*(v2*(A*v1)) = B*v1
 646 84 : I(A*C)*(B*A) = B*C
 647 85 : I(A*C)*(B*(A*v1)) = B*(C*v1)
 648 86 : v2*(I(C*v2)*v1) = C*v1
 649 87 : I(I(B*C)*A)*(C*A) = B
 650 88 : I(I(B*C)*A)*(C*(A*v1)) = B*v1
 651 89 : v2*(v1*I(v2*v1)) = U
 652 90 : B*(A*I(B)) = A
 653 91 : I(v2*v1)*v2 = I(v1)
 654 Rule 64 deleted
 655 Rule 57 deleted
 656 Rule 55 deleted
 657 Rule 46 deleted
 658 Rule 34 deleted
 659 Rule 31 deleted
 660 Rule 30 deleted
 661 92 : I(C*(A*C)) = A
 662 Rule 39 deleted
 663 93 : I(v3*(v2*v1))*(v3*v2) = I(v1)
 664 Rule 60 deleted
 665 Rule 54 deleted
 666 Rule 47 deleted
 667 94 : I(v2*I(v1)) = v1*I(v2)
 668 Rule 83 deleted
 669 Rule 76 deleted
 670 Rule 74 deleted
 671 Rule 72 deleted
 672 Rule 71 deleted
 673 Rule 53 deleted
 674 Rule 50 deleted
 675 Rule 35 deleted
 676 95 : I(v2*(I(B)*A))*(v2*(A*v1)) = B*v1
 677 96 : I(v1*(I(B)*A))*(v1*A) = B
 678 97 : I(v1*A)*(v1*B) = B*(C*(A*C))
 679 Rule 82 deleted
 680 Rule 69 deleted
 681 98 : I(v1*C) = C*I(v1)
 682 Rule 88 deleted
 683 Rule 87 deleted
 684 Rule 85 deleted
 685 Rule 84 deleted
 686 Rule 52 deleted
 687 Rule 37 deleted
 688 99 : v3*(v2*(I(v3*v2)*v1)) = v1
 689 100 : B*(A*(I(B)*v1)) = A*v1
 690 101 : I(v3*v2)*(v3*v1) = I(v2)*v1
 691 Rule 97 deleted
 692 Rule 96 deleted
 693 Rule 95 deleted
 694 Rule 93 deleted
 695 Rule 80 deleted
 696 Rule 77 deleted
 697 Rule 73 deleted
 698 Rule 65 deleted
 699 Rule 63 deleted
 700 Rule 62 deleted
 701 Rule 61 deleted
 702 Rule 59 deleted
 703 Rule 58 deleted
 704 Rule 49 deleted
 705 Rule 36 deleted
 706 Rule 33 deleted
 707 Rule 32 deleted
 708 Rule 15 deleted
 709 102 : B*(C*I(B)) = C
 710 103 : B*(C*(I(B)*v1)) = C*v1
 711 104 : B*(I(B*A)*A) = U
 712 105 : B*(I(B*A)*(A*v1)) = v1
 713 106 : I(B*A)*A = I(B)
 714 Rule 104 deleted
 715 Rule 48 deleted
 716 107 : B*(v1*(I(B*(A*v1))*A)) = U
 717 108 : I(I(B*(B*A))*A) = B*B
 718 109 : B*(v2*(I(B*(A*v2))*(A*v1))) = v1
 719 110 : I(I(B*(B*(A*v1)))*A) = B*(B*v1)
 720 111 : I(I(B)*A) = B*(C*(A*C))
 721 Rule 78 deleted
 722 Rule 66 deleted
 723 112 : I(I(B*v1)*A) = B*(C*(A*(C*v1)))
 724 Rule 110 deleted
 725 Rule 108 deleted
 726 Rule 51 deleted
 727 113 : v3*(v2*I(I(v1)*(v3*v2))) = v1
 728 114 : v1*I(C*(A*(C*v1))) = A
 729 115 : I(I(v2)*v1) = I(v1)*v2
 730 Rule 113 deleted
 731 Rule 112 deleted
 732 Rule 111 deleted
 733 Rule 75 deleted
 734 Rule 56 deleted
 735 116 : v2*(v1*(I(A*(v2*v1))*(B*A))) = B
 736 117 : I(A*v1)*(B*A) = I(v1)*B
 737 Rule 116 deleted
 738 Rule 68 deleted
 739 118 : v2*(v1*I(C*(v2*v1))) = C
 740 119 : I(C*v1) = I(v1)*C
 741 Rule 118 deleted
 742 Rule 114 deleted
 743 Rule 92 deleted
 744 Rule 86 deleted
 745 Rule 70 deleted
 746 120 : v1*(I(A*(C*v1))*C) = A
 747 121 : I(A*A)*(B*(B*(A*A))) = B*B
 748 122 : I(A*A)*(B*(B*(A*(A*v1)))) = B*(B*v1)
 749 123 : I(A*A)*(B*(A*v1)) = B*(C*(A*(C*v1)))
 750 Rule 79 deleted
 751 Rule 67 deleted
 752 124 : v3*(v2*(I(A*(v3*v2))*(B*(A*v1)))) = B*v1
 753 125 : v1*(I(A*v1)*(B*(B*A))) = B*B
 754 126 : I(A*v2)*(B*(A*v1)) = I(v2)*(B*v1)
 755 Rule 124 deleted
 756 Rule 123 deleted
 757 Rule 81 deleted
 758 127 : v3*(v2*(v1*I(v3*(v2*v1)))) = U
 759 128 : v2*I(v1*v2) = I(v1)
 760 Rule 89 deleted
 761 129 : A*I(B) = I(B)*A
 762 Rule 90 deleted
 763 130 : I(v2*v1) = I(v1)*I(v2)
 764 Rule 128 deleted
 765 Rule 127 deleted
 766 Rule 126 deleted
 767 Rule 125 deleted
 768 Rule 122 deleted
 769 Rule 121 deleted
 770 Rule 120 deleted
 771 Rule 119 deleted
 772 Rule 117 deleted
 773 Rule 115 deleted
 774 Rule 109 deleted
 775 Rule 107 deleted
 776 Rule 106 deleted
 777 Rule 105 deleted
 778 Rule 101 deleted
 779 Rule 99 deleted
 780 Rule 98 deleted
 781 Rule 94 deleted
 782 Rule 91 deleted
 783 131 : B*(C*(A*(C*(I(B)*(A*v1))))) = v1
 784 132 : B*(C*(A*(C*(I(B)*A)))) = U
 785 133 : C*(A*(C*(I(B)*A))) = I(B)
 786 Rule 132 deleted
 787 134 : A*(I(B)*v1) = I(B)*(A*v1)
 788 Rule 100 deleted
 789 135 : C*I(B) = I(B)*C
 790 Rule 102 deleted
 791 136 : C*(I(B)*v1) = I(B)*(C*v1)
 792 Rule 133 deleted
 793 Rule 131 deleted
 794 Rule 103 deleted
 795 Canonical set found :
 796 1 : U*v1 = v1
 797 2 : I(v1)*v1 = U
 798 3 : (v3*v2)*v1 = v3*(v2*v1)
 799 4 : A*B = B*A
 800 5 : C*C = U
 801 6 : I(A) = C*(A*C)
 802 8 : I(v2)*(v2*v1) = v1
 803 9 : A*(B*v1) = B*(A*v1)
 804 10 : C*(C*v1) = v1
 805 21 : v1*U = v1
 806 22 : I(C) = C
 807 23 : C*B = B*C
 808 38 : v1*I(v1) = U
 809 40 : v2*(I(v2)*v1) = v1
 810 41 : I(U) = U
 811 42 : I(I(v1)) = v1
 812 43 : C*(B*v1) = B*(C*v1)
 813 44 : A*(C*(A*v1)) = C*v1
 814 45 : A*(C*A) = C
 815 129 : A*I(B) = I(B)*A
 816 130 : I(v2*v1) = I(v1)*I(v2)
 817 134 : A*(I(B)*v1) = I(B)*(A*v1)
 818 135 : C*I(B) = I(B)*C
 819 136 : C*(I(B)*v1) = I(B)*(C*v1)