EQUATIONS: f(f(x,y),z) = f(x,f(y,z)) f(a1(),y) = y f(a2(),y) = y f(x,i1(x)) = a1() f(x,i2(x)) = a2() COMPLETE TRS: RULES: f(f(x,y),z) -> f(x,f(y,z)) f(a2(),y) -> y f(x,i1(x)) -> i1(a2()) f(i1(a2()),x) -> x i1(i1(a2())) -> i1(a2()) f(x,i1(a2())) -> i1(i1(x)) f(i1(x),f(x,y)) -> y i1(i1(i1(x))) -> i1(x) f(i1(i1(x)),y) -> f(x,y) a1() -> i1(a2()) f(y,f(i1(y),x)) -> x i2(x) -> f(i1(x),a2()) i1(f(y,x)) -> f(i1(x),i1(y)) SUCCESS MaxTRS: 2 Search time: 0.95 seconds