summaryrefslogtreecommitdiff
path: root/ocaml-binary-annot/testsuite/tests/misc-kb
diff options
context:
space:
mode:
Diffstat (limited to 'ocaml-binary-annot/testsuite/tests/misc-kb')
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/Makefile6
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/equations.ml115
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/equations.mli32
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/kb.ml188
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/kb.mli29
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.ml82
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.reference5460
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/orderings.ml99
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/orderings.mli31
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/terms.ml137
-rw-r--r--ocaml-binary-annot/testsuite/tests/misc-kb/terms.mli31
11 files changed, 6210 insertions, 0 deletions
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/Makefile b/ocaml-binary-annot/testsuite/tests/misc-kb/Makefile
new file mode 100644
index 0000000000..b5f5eaec97
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/Makefile
@@ -0,0 +1,6 @@
+MODULES=terms equations orderings kb
+MAIN_MODULE=kbmain
+ADD_COMPFLAGS=-w a
+
+include ../../makefiles/Makefile.one
+include ../../makefiles/Makefile.common
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/equations.ml b/ocaml-binary-annot/testsuite/tests/misc-kb/equations.ml
new file mode 100644
index 0000000000..3feeada7c7
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/equations.ml
@@ -0,0 +1,115 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: equations.ml 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+(****************** Equation manipulations *************)
+
+open Terms
+
+type rule =
+ { number: int;
+ numvars: int;
+ lhs: term;
+ rhs: term }
+
+(* standardizes an equation so its variables are 1,2,... *)
+
+let mk_rule num m n =
+ let all_vars = union (vars m) (vars n) in
+ let counter = ref 0 in
+ let subst =
+ List.map (fun v -> incr counter; (v, Var !counter)) (List.rev all_vars) in
+ { number = num;
+ numvars = !counter;
+ lhs = substitute subst m;
+ rhs = substitute subst n }
+
+
+(* checks that rules are numbered in sequence and returns their number *)
+
+let check_rules rules =
+ let counter = ref 0 in
+ List.iter (fun r -> incr counter;
+ if r.number <> !counter
+ then failwith "Rule numbers not in sequence")
+ rules;
+ !counter
+
+
+let pretty_rule rule =
+ print_int rule.number; print_string " : ";
+ pretty_term rule.lhs; print_string " = "; pretty_term rule.rhs;
+ print_newline()
+
+
+let pretty_rules rules = List.iter pretty_rule rules
+
+(****************** Rewriting **************************)
+
+(* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M.
+ With sigma = matching L M, we define the image of M by eq as sigma(R) *)
+let reduce l m r =
+ substitute (matching l m) r
+
+(* Test whether m can be reduced by l, i.e. m contains an instance of l. *)
+
+let can_match l m =
+ try let _ = matching l m in true
+ with Failure _ -> false
+
+let rec reducible l m =
+ can_match l m ||
+ (match m with
+ | Term(_,sons) -> List.exists (reducible l) sons
+ | _ -> false)
+
+(* Top-level rewriting with multiple rules. *)
+
+let rec mreduce rules m =
+ match rules with
+ [] -> failwith "mreduce"
+ | rule::rest ->
+ try
+ reduce rule.lhs m rule.rhs
+ with Failure _ ->
+ mreduce rest m
+
+
+(* One step of rewriting in leftmost-outermost strategy,
+ with multiple rules. Fails if no redex is found *)
+
+let rec mrewrite1 rules m =
+ try
+ mreduce rules m
+ with Failure _ ->
+ match m with
+ Var n -> failwith "mrewrite1"
+ | Term(f, sons) -> Term(f, mrewrite1_sons rules sons)
+
+and mrewrite1_sons rules = function
+ [] -> failwith "mrewrite1"
+ | son::rest ->
+ try
+ mrewrite1 rules son :: rest
+ with Failure _ ->
+ son :: mrewrite1_sons rules rest
+
+
+(* Iterating rewrite1. Returns a normal form. May loop forever *)
+
+let rec mrewrite_all rules m =
+ try
+ mrewrite_all rules (mrewrite1 rules m)
+ with Failure _ ->
+ m
+
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/equations.mli b/ocaml-binary-annot/testsuite/tests/misc-kb/equations.mli
new file mode 100644
index 0000000000..665b739ed4
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/equations.mli
@@ -0,0 +1,32 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: equations.mli 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+open Terms
+
+type rule =
+ { number: int;
+ numvars: int;
+ lhs: term;
+ rhs: term }
+
+val mk_rule: int -> term -> term -> rule
+val check_rules: rule list -> int
+val pretty_rule: rule -> unit
+val pretty_rules: rule list -> unit
+val reduce: term -> term -> term -> term
+val reducible: term -> term -> bool
+val mreduce: rule list -> term -> term
+val mrewrite1: rule list -> term -> term
+val mrewrite1_sons: rule list -> term list -> term list
+val mrewrite_all: rule list -> term -> term
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/kb.ml b/ocaml-binary-annot/testsuite/tests/misc-kb/kb.ml
new file mode 100644
index 0000000000..1e369bd1b5
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/kb.ml
@@ -0,0 +1,188 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: kb.ml 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+open Terms
+open Equations
+
+(****************** Critical pairs *********************)
+
+(* All (u,subst) such that N/u (&var) unifies with M,
+ with principal unifier subst *)
+
+let rec super m = function
+ Term(_,sons) as n ->
+ let rec collate n = function
+ [] -> []
+ | son::rest ->
+ List.map (fun (u, subst) -> (n::u, subst)) (super m son)
+ @ collate (n+1) rest in
+ let insides = collate 1 sons in
+ begin try
+ ([], unify m n) :: insides
+ with Failure _ ->
+ insides
+ end
+ | _ -> []
+
+
+(* Ex :
+let (m,_) = <<F(A,B)>>
+and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
+==> [[1],[2,Term ("B",[])]; x <- B
+ [2],[2,Term ("A",[]); 1,Term ("B",[])]] x <- A y <- B
+*)
+
+(* All (u,subst), u&[], such that n/u unifies with m *)
+
+let super_strict m = function
+ Term(_,sons) ->
+ let rec collate n = function
+ [] -> []
+ | son::rest ->
+ List.map (fun (u, subst) -> (n::u, subst)) (super m son)
+ @ collate (n+1) rest in
+ collate 1 sons
+ | _ -> []
+
+
+(* Critical pairs of l1=r1 with l2=r2 *)
+(* critical_pairs : term_pair -> term_pair -> term_pair list *)
+let critical_pairs (l1,r1) (l2,r2) =
+ let mk_pair (u,subst) =
+ substitute subst (replace l2 u r1), substitute subst r2 in
+ List.map mk_pair (super l1 l2)
+
+(* Strict critical pairs of l1=r1 with l2=r2 *)
+(* strict_critical_pairs : term_pair -> term_pair -> term_pair list *)
+let strict_critical_pairs (l1,r1) (l2,r2) =
+ let mk_pair (u,subst) =
+ substitute subst (replace l2 u r1), substitute subst r2 in
+ List.map mk_pair (super_strict l1 l2)
+
+
+(* All critical pairs of eq1 with eq2 *)
+let mutual_critical_pairs eq1 eq2 =
+ (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1)
+
+(* Renaming of variables *)
+
+let rename n (t1,t2) =
+ let rec ren_rec = function
+ Var k -> Var(k+n)
+ | Term(op,sons) -> Term(op, List.map ren_rec sons) in
+ (ren_rec t1, ren_rec t2)
+
+
+(************************ Completion ******************************)
+
+let deletion_message rule =
+ print_string "Rule ";print_int rule.number; print_string " deleted";
+ print_newline()
+
+
+(* Generate failure message *)
+let non_orientable (m,n) =
+ pretty_term m; print_string " = "; pretty_term n; print_newline()
+
+
+let rec partition p = function
+ [] -> ([], [])
+ | x::l -> let (l1, l2) = partition p l in
+ if p x then (x::l1, l2) else (l1, x::l2)
+
+
+let rec get_rule n = function
+ [] -> raise Not_found
+ | r::l -> if n = r.number then r else get_rule n l
+
+
+(* Improved Knuth-Bendix completion procedure *)
+
+let kb_completion greater =
+ let rec kbrec j rules =
+ let rec process failures (k,l) eqs =
+(****
+ print_string "***kb_completion "; print_int j; print_newline();
+ pretty_rules rules;
+ List.iter non_orientable failures;
+ print_int k; print_string " "; print_int l; print_newline();
+ List.iter non_orientable eqs;
+***)
+ match eqs with
+ [] ->
+ if k<l then next_criticals failures (k+1,l) else
+ if l<j then next_criticals failures (1,l+1) else
+ begin match failures with
+ [] -> rules (* successful completion *)
+ | _ -> print_string "Non-orientable equations :"; print_newline();
+ List.iter non_orientable failures;
+ failwith "kb_completion"
+ end
+ | (m,n)::eqs ->
+ let m' = mrewrite_all rules m
+ and n' = mrewrite_all rules n
+ and enter_rule(left,right) =
+ let new_rule = mk_rule (j+1) left right in
+ pretty_rule new_rule;
+ let left_reducible rule = reducible left rule.lhs in
+ let (redl,irredl) = partition left_reducible rules in
+ List.iter deletion_message redl;
+ let right_reduce rule =
+ mk_rule rule.number rule.lhs
+ (mrewrite_all (new_rule::rules) rule.rhs) in
+ let irreds = List.map right_reduce irredl in
+ let eqs' = List.map (fun rule -> (rule.lhs, rule.rhs)) redl in
+ kbrec (j+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures) in
+(***
+ print_string "--- Considering "; non_orientable (m', n');
+***)
+ if m' = n' then process failures (k,l) eqs else
+ if greater(m',n') then enter_rule(m',n') else
+ if greater(n',m') then enter_rule(n',m') else
+ process ((m',n')::failures) (k,l) eqs
+
+ and next_criticals failures (k,l) =
+(****
+ print_string "***next_criticals ";
+ print_int k; print_string " "; print_int l ; print_newline();
+****)
+ try
+ let rl = get_rule l rules in
+ let el = (rl.lhs, rl.rhs) in
+ if k=l then
+ process failures (k,l)
+ (strict_critical_pairs el (rename rl.numvars el))
+ else
+ try
+ let rk = get_rule k rules in
+ let ek = (rk.lhs, rk.rhs) in
+ process failures (k,l)
+ (mutual_critical_pairs el (rename rl.numvars ek))
+ with Not_found -> next_criticals failures (k+1,l)
+ with Not_found -> next_criticals failures (1,l+1)
+ in process
+ in kbrec
+
+
+(* complete_rules is assumed locally confluent, and checked Noetherian with
+ ordering greater, rules is any list of rules *)
+
+let kb_complete greater complete_rules rules =
+ let n = check_rules complete_rules
+ and eqs = List.map (fun rule -> (rule.lhs, rule.rhs)) rules in
+ let completed_rules =
+ kb_completion greater n complete_rules [] (n,n) eqs in
+ print_string "Canonical set found :"; print_newline();
+ pretty_rules (List.rev completed_rules)
+
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/kb.mli b/ocaml-binary-annot/testsuite/tests/misc-kb/kb.mli
new file mode 100644
index 0000000000..bd02de4baa
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/kb.mli
@@ -0,0 +1,29 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: kb.mli 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+open Terms
+open Equations
+
+val super: term -> term -> (int list * (int * term) list) list
+val super_strict: term -> term -> (int list * (int * term) list) list
+val critical_pairs: term * term -> term * term -> (term * term) list
+val strict_critical_pairs: term * term -> term * term -> (term * term) list
+val mutual_critical_pairs: term * term -> term * term -> (term * term) list
+val rename: int -> term * term -> term * term
+val deletion_message: rule -> unit
+val non_orientable: term * term -> unit
+val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
+val get_rule: int -> rule list -> rule
+val kb_completion: (term * term -> bool) -> int -> rule list -> (term * term) list -> int * int -> (term * term) list -> rule list
+val kb_complete: (term * term -> bool) -> rule list -> rule list -> unit
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.ml b/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.ml
new file mode 100644
index 0000000000..7d9e5baf19
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.ml
@@ -0,0 +1,82 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: kbmain.ml 7017 2005-08-12 09:22:04Z xleroy $ *)
+
+open Terms
+open Equations
+open Orderings
+open Kb
+
+(****
+let group_rules = [
+ { number = 1; numvars = 1;
+ lhs = Term("*", [Term("U",[]); Var 1]); rhs = Var 1 };
+ { number = 2; numvars = 1;
+ lhs = Term("*", [Term("I",[Var 1]); Var 1]); rhs = Term("U",[]) };
+ { number = 3; numvars = 3;
+ lhs = Term("*", [Term("*", [Var 1; Var 2]); Var 3]);
+ rhs = Term("*", [Var 1; Term("*", [Var 2; Var 3])]) }
+]
+****)
+
+let geom_rules = [
+ { number = 1; numvars = 1;
+ lhs = Term ("*",[(Term ("U",[])); (Var 1)]);
+ rhs = Var 1 };
+ { number = 2; numvars = 1;
+ lhs = Term ("*",[(Term ("I",[(Var 1)])); (Var 1)]);
+ rhs = Term ("U",[]) };
+ { number = 3; numvars = 3;
+ lhs = Term ("*",[(Term ("*",[(Var 1); (Var 2)])); (Var 3)]);
+ rhs = Term ("*",[(Var 1); (Term ("*",[(Var 2); (Var 3)]))]) };
+ { number = 4; numvars = 0;
+ lhs = Term ("*",[(Term ("A",[])); (Term ("B",[]))]);
+ rhs = Term ("*",[(Term ("B",[])); (Term ("A",[]))]) };
+ { number = 5; numvars = 0;
+ lhs = Term ("*",[(Term ("C",[])); (Term ("C",[]))]);
+ rhs = Term ("U",[]) };
+ { number = 6; numvars = 0;
+ lhs = Term("*",
+ [(Term ("C",[]));
+ (Term ("*",[(Term ("A",[])); (Term ("I",[(Term ("C",[]))]))]))]);
+ rhs = Term ("I",[(Term ("A",[]))]) };
+ { number = 7; numvars = 0;
+ lhs = Term("*",
+ [(Term ("C",[]));
+ (Term ("*",[(Term ("B",[])); (Term ("I",[(Term ("C",[]))]))]))]);
+ rhs = Term ("B",[]) }
+]
+
+let group_rank = function
+ "U" -> 0
+ | "*" -> 1
+ | "I" -> 2
+ | "B" -> 3
+ | "C" -> 4
+ | "A" -> 5
+ | _ -> assert false
+
+let group_precedence op1 op2 =
+ let r1 = group_rank op1
+ and r2 = group_rank op2 in
+ if r1 = r2 then Equal else
+ if r1 > r2 then Greater else NotGE
+
+let group_order = rpo group_precedence lex_ext
+
+let greater pair =
+ match group_order pair with Greater -> true | _ -> false
+
+let _ =
+ for i = 1 to 20 do kb_complete greater [] geom_rules done
+
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.reference b/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.reference
new file mode 100644
index 0000000000..2789a669bb
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/kbmain.reference
@@ -0,0 +1,5460 @@
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
+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)
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.ml b/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.ml
new file mode 100644
index 0000000000..2f3ee97352
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.ml
@@ -0,0 +1,99 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: orderings.ml 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+(*********************** Recursive Path Ordering ****************************)
+
+open Terms
+
+type ordering =
+ Greater
+ | Equal
+ | NotGE
+
+let ge_ord order pair = match order pair with NotGE -> false | _ -> true
+and gt_ord order pair = match order pair with Greater -> true | _ -> false
+and eq_ord order pair = match order pair with Equal -> true | _ -> false
+
+
+let rec rem_eq equiv x = function
+ [] -> failwith "rem_eq"
+ | y::l -> if equiv (x,y) then l else y :: rem_eq equiv x l
+
+
+let diff_eq equiv (x,y) =
+ let rec diffrec = function
+ ([],_) as p -> p
+ | (h::t, y) -> try
+ diffrec (t, rem_eq equiv h y)
+ with Failure _ ->
+ let (x',y') = diffrec (t,y) in (h::x',y') in
+ if List.length x > List.length y then diffrec(y,x) else diffrec(x,y)
+
+
+(* Multiset extension of order *)
+
+let mult_ext order = function
+ Term(_,sons1), Term(_,sons2) ->
+ begin match diff_eq (eq_ord order) (sons1,sons2) with
+ ([],[]) -> Equal
+ | (l1,l2) ->
+ if List.for_all
+ (fun n -> List.exists (fun m -> gt_ord order (m,n)) l1) l2
+ then Greater else NotGE
+ end
+ | _ -> failwith "mult_ext"
+
+
+(* Lexicographic extension of order *)
+
+let lex_ext order = function
+ (Term(_,sons1) as m), (Term(_,sons2) as n) ->
+ let rec lexrec = function
+ ([] , []) -> Equal
+ | ([] , _ ) -> NotGE
+ | ( _ , []) -> Greater
+ | (x1::l1, x2::l2) ->
+ match order (x1,x2) with
+ Greater -> if List.for_all (fun n' -> gt_ord order (m,n')) l2
+ then Greater else NotGE
+ | Equal -> lexrec (l1,l2)
+ | NotGE -> if List.exists (fun m' -> ge_ord order (m',n)) l1
+ then Greater else NotGE in
+ lexrec (sons1, sons2)
+ | _ -> failwith "lex_ext"
+
+
+(* Recursive path ordering *)
+
+let rpo op_order ext =
+ let rec rporec (m,n) =
+ if m = n then Equal else
+ match m with
+ Var vm -> NotGE
+ | Term(op1,sons1) ->
+ match n with
+ Var vn ->
+ if occurs vn m then Greater else NotGE
+ | Term(op2,sons2) ->
+ match (op_order op1 op2) with
+ Greater ->
+ if List.for_all (fun n' -> gt_ord rporec (m,n')) sons2
+ then Greater else NotGE
+ | Equal ->
+ ext rporec (m,n)
+ | NotGE ->
+ if List.exists (fun m' -> ge_ord rporec (m',n)) sons1
+ then Greater else NotGE
+ in rporec
+
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.mli b/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.mli
new file mode 100644
index 0000000000..b68ceda3d0
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/orderings.mli
@@ -0,0 +1,31 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: orderings.mli 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+open Terms
+
+type ordering =
+ Greater
+ | Equal
+ | NotGE
+
+val ge_ord: ('a -> ordering) -> 'a -> bool
+val gt_ord: ('a -> ordering) -> 'a -> bool
+val eq_ord: ('a -> ordering) -> 'a -> bool
+val rem_eq: ('a * 'b -> bool) -> 'a -> 'b list -> 'b list
+val diff_eq: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * 'a list
+val mult_ext: (term * term -> ordering) -> term * term -> ordering
+val lex_ext: (term * term -> ordering) -> term * term -> ordering
+val rpo: (string -> string -> ordering) ->
+ ((term * term -> ordering) -> term * term -> ordering) ->
+ term * term -> ordering
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/terms.ml b/ocaml-binary-annot/testsuite/tests/misc-kb/terms.ml
new file mode 100644
index 0000000000..1b182f7561
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/terms.ml
@@ -0,0 +1,137 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: terms.ml 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+(****************** Term manipulations *****************)
+
+type term =
+ Var of int
+ | Term of string * term list
+
+let rec union l1 l2 =
+ match l1 with
+ [] -> l2
+ | a::r -> if List.mem a l2 then union r l2 else a :: union r l2
+
+
+let rec vars = function
+ Var n -> [n]
+ | Term(_,l) -> vars_of_list l
+and vars_of_list = function
+ [] -> []
+ | t::r -> union (vars t) (vars_of_list r)
+
+
+let rec substitute subst = function
+ Term(oper,sons) -> Term(oper, List.map (substitute subst) sons)
+ | Var(n) as t -> try List.assoc n subst with Not_found -> t
+
+
+(* Term replacement: replace M u N is M[u<-N]. *)
+
+let rec replace m u n =
+ match (u, m) with
+ [], _ -> n
+ | i::u, Term(oper, sons) -> Term(oper, replace_nth i sons u n)
+ | _ -> failwith "replace"
+
+and replace_nth i sons u n =
+ match sons with
+ s::r -> if i = 1
+ then replace s u n :: r
+ else s :: replace_nth (i-1) r u n
+ | [] -> failwith "replace_nth"
+
+
+(* Term matching. *)
+
+let matching term1 term2 =
+ let rec match_rec subst t1 t2 =
+ match (t1, t2) with
+ Var v, _ ->
+ if List.mem_assoc v subst then
+ if t2 = List.assoc v subst then subst else failwith "matching"
+ else
+ (v, t2) :: subst
+ | Term(op1,sons1), Term(op2,sons2) ->
+ if op1 = op2
+ then List.fold_left2 match_rec subst sons1 sons2
+ else failwith "matching"
+ | _ -> failwith "matching" in
+ match_rec [] term1 term2
+
+
+(* A naive unification algorithm. *)
+
+let compsubst subst1 subst2 =
+ (List.map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1
+
+
+let rec occurs n = function
+ Var m -> m = n
+ | Term(_,sons) -> List.exists (occurs n) sons
+
+
+let rec unify term1 term2 =
+ match (term1, term2) with
+ Var n1, _ ->
+ if term1 = term2 then []
+ else if occurs n1 term2 then failwith "unify"
+ else [n1, term2]
+ | term1, Var n2 ->
+ if occurs n2 term1 then failwith "unify"
+ else [n2, term1]
+ | Term(op1,sons1), Term(op2,sons2) ->
+ if op1 = op2 then
+ List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1)
+ (substitute s t2)) s)
+ [] sons1 sons2
+ else failwith "unify"
+
+
+(* We need to print terms with variables independently from input terms
+ obtained by parsing. We give arbitrary names v1,v2,... to their variables.
+*)
+
+let infixes = ["+";"*"]
+
+let rec pretty_term = function
+ Var n ->
+ print_string "v"; print_int n
+ | Term (oper,sons) ->
+ if List.mem oper infixes then begin
+ match sons with
+ [s1;s2] ->
+ pretty_close s1; print_string oper; pretty_close s2
+ | _ ->
+ failwith "pretty_term : infix arity <> 2"
+ end else begin
+ print_string oper;
+ match sons with
+ [] -> ()
+ | t::lt -> print_string "(";
+ pretty_term t;
+ List.iter (fun t -> print_string ","; pretty_term t) lt;
+ print_string ")"
+ end
+
+and pretty_close = function
+ Term(oper, _) as m ->
+ if List.mem oper infixes then begin
+ print_string "("; pretty_term m; print_string ")"
+ end else
+ pretty_term m
+ | m ->
+ pretty_term m
+
+
diff --git a/ocaml-binary-annot/testsuite/tests/misc-kb/terms.mli b/ocaml-binary-annot/testsuite/tests/misc-kb/terms.mli
new file mode 100644
index 0000000000..a71e139c63
--- /dev/null
+++ b/ocaml-binary-annot/testsuite/tests/misc-kb/terms.mli
@@ -0,0 +1,31 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the Q Public License version 1.0. *)
+(* *)
+(***********************************************************************)
+
+(* $Id: terms.mli 2553 1999-11-17 18:59:06Z xleroy $ *)
+
+type term =
+ Var of int
+ | Term of string * term list
+
+val union: 'a list -> 'a list -> 'a list
+val vars: term -> int list
+val vars_of_list: term list -> int list
+val substitute: (int * term) list -> term -> term
+val replace: term -> int list -> term -> term
+val replace_nth: int -> term list -> int list -> term -> term list
+val matching: term -> term -> (int * term) list
+val compsubst: (int * term) list -> (int * term) list -> (int * term) list
+val occurs: int -> term -> bool
+val unify: term -> term -> (int * term) list
+val infixes: string list
+val pretty_term: term -> unit
+val pretty_close: term -> unit
View Lorry Controller Status