NO
Rewrite Rules:
   [ f(?x,f(?y,?z)) -> f(f(?x,?y),f(?x,?z)),
     f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)),
     f(f(?x,?y),f(?y,?z)) -> ?y ]
Apply Direct Methods...
Inner CPs:
   [ f(?x,f(f(?x_1,?z_1),f(?y_1,?z_1))) = f(f(?x,f(?x_1,?y_1)),f(?x,?z_1)),
     f(?x,?y_2) = f(f(?x,f(?x_2,?y_2)),f(?x,f(?y_2,?z_2))),
     f(f(f(?x,?y),f(?x,?z)),?z_1) = f(f(?x,?z_1),f(f(?y,?z),?z_1)),
     f(?y_2,?z_1) = f(f(f(?x_2,?y_2),?z_1),f(f(?y_2,?z_2),?z_1)),
     f(f(f(?x,?y),f(?x,?z)),f(f(?y,?z),?z_2)) = f(?y,?z),
     f(f(?x_2,?x),f(f(?x,?y),f(?x,?z))) = ?x,
     f(f(f(?x_1,?z_1),f(?y_1,?z_1)),f(?z_1,?z_2)) = ?z_1,
     f(f(?x_2,f(?x_1,?y_1)),f(f(?x_1,?z_1),f(?y_1,?z_1))) = f(?x_1,?y_1),
     f(?x_1,f(f(?x,?y),f(?x,?z))) = f(f(?x_1,?x),f(?x_1,f(?y,?z))),
     f(f(f(?x,?z),f(?y,?z)),?z_1) = f(f(f(?x,?y),?z_1),f(?z,?z_1)),
     f(?y,f(f(?y,?z),?z_1)) = f(?y,?z),
     f(f(?x_1,f(?x,?y)),?y) = f(?x,?y) ]
Outer CPs:
   [ f(f(f(?x_1,?y_1),?y),f(f(?x_1,?y_1),?z)) = f(f(?x_1,f(?y,?z)),f(?y_1,f(?y,?z))),
     f(f(f(?x_2,?y),?y),f(f(?x_2,?y),?z)) = ?y,
     f(f(?x_1,f(?y_1,?z_2)),f(?y_1,f(?y_1,?z_2))) = ?y_1 ]
unknown Terminating
not Left-Linear, not Right-Linear
unknown Gomi&Oyamaguchi&Ohta
check Non-Confluence...Find Non-Joinable CP reducts: <?y, f(?x,?y)> from f(f(f(?x_1,?x),?y),f(f(?x,?y),f(?y,?z)))
Not Confluent
Direct Methods: not CR

Final result: not CR
15.trs: NO (360 msec.)