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