Input TRS: 1: f(a(),g(y),z) -> f(a(),y,g(y)) 2: f(b(),g(y),z) -> f(a(),y,z) 3: a() -> b() e1: f(x,y,z) ->= f(x,y,g(z)) [relative] Weak rule e1 calls a strict rule