EQUATIONS: times(x,times(y,z)) = times(times(x,y),z) times(1(),1()) = 1() times(x,i(x)) = 1() g(times(x,y),y) = f(times(x,y),x) f(1(),y) = y COMPLETE TRS: RULES: times(x,i(x)) -> 1() f(1(),y) -> y i(1()) -> 1() i(i(x)) -> x times(i(x),x) -> 1() times(i(x),times(x,y)) -> y g(x,y) -> f(x,times(x,i(y))) times(times(x,y),z) -> times(x,times(y,z)) times(y,times(i(y),x)) -> x times(x,1()) -> x times(1(),x) -> x i(times(y,x)) -> times(i(x),i(y)) SUCCESS MaxTRS: 3 Search time: 0.90 seconds