Input TRS:
    1: o(lambda(x),y) -> lambda(o(x,d(1(),o(y,p()))))
    2: o(d(x,y),z) -> d(o(x,z),o(y,z))
    3: o(o(x,y),z) -> o(x,o(y,z))
    4: lambda(x) -> x
    5: o(x,y) -> x
    6: o(x,y) -> y
    7: d(x,y) -> x
    8: d(x,y) -> y
   e1: o(x,y) ->= d(x,y)	[relative]
   e2: o(x,y) ->= d(y,x)	[relative]
Weak rule e2 calls a strict rule