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(a4,y) -> y
        f(a5,y) -> y
        f(a6,y) -> y
        f(a7,y) -> y
        f(a8,y) -> y
        f(a9,y) -> y
        f(a10,y) -> y
        f(a11,y) -> y
        f(a12,y) -> y
        f(x,i3(x)) -> a3
        i3(a1) -> a3
        i3(a2) -> a3
        i3(a3) -> a3
        i3(a4) -> a3
        i3(a5) -> a3
        i3(a6) -> a3
        i3(a7) -> a3
        i3(a8) -> a3
        i3(a9) -> a3
        i3(a10) -> a3
        i3(a11) -> a3
        i3(a12) -> a3
        f(x,f(i3(x),z)) -> z
        i3(i3(x)) -> f(x,a3)
        f(i3(x),f(x,z)) -> z
        i1(x) -> f(i3(x),a1)
        i2(x) -> f(i3(x),a2)
        f(i3(x),a3) -> i3(x)
        i4(x) -> f(i3(x),a4)
        i5(x) -> f(i3(x),a5)
        i6(x) -> f(i3(x),a6)
        i7(x) -> f(i3(x),a7)
        i8(x) -> f(i3(x),a8)
        i9(x) -> f(i3(x),a9)
        i10(x) -> f(i3(x),a10)
        i11(x) -> f(i3(x),a11)
        i12(x) -> f(i3(x),a12)
        i3(f(y,x)) -> f(i3(x),i3(y))
        
)