f(a1(),x) -> x f(a2(),x) -> x f(a3(),x) -> x f(x,i1(x)) -> a1() i1(a3()) -> a1() i1(a2()) -> a1() i1(a1()) -> a1() f(f(x,y),z) -> f(x,f(y,z)) f(x,f(i1(x),y)) -> y f(x,a1()) -> i1(i1(x)) f(i1(i1(x)),y) -> f(x,y) f(i1(x),f(x,y)) -> y i3(x) -> f(i1(x),a3()) i1(i1(i1(x))) -> i1(x) i2(x) -> f(i1(x),a2()) i1(f(x,y)) -> f(i1(y),i1(x))