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