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