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