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]
Number of Rules: 8
Direct POLO(Sum) ...Direct Mat2b ... failed.
Dependency Pairs:
   #1: # o(d(x,y),z) -> # d(o(x,z),o(y,z))
   #2: # o(d(x,y),z) -> # o(x,z)
   #3: # o(d(x,y),z) -> # o(y,z)
   #4: # o(x,y) -> # d(y,x)	[relative]
   #5: # o(x,y) -> # d(x,y)	[relative]
   #6: # o(o(x,y),z) -> # o(x,o(y,z))
   #7: # o(o(x,y),z) -> # o(y,z)
   #8: # o(lambda(x),y) -> # lambda(o(x,d(1(),o(y,p()))))
   #9: # o(lambda(x),y) -> # o(x,d(1(),o(y,p())))
   #10: # o(lambda(x),y) -> # d(1(),o(y,p()))
   #11: # o(lambda(x),y) -> # o(y,p())
Number of SCCs: 1
  SCC { #2 #3 #6 #7 #9 #11 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... removes: #9 #11
	I(1) = 0
	I(d) = max(x1, x2)	sigma(d) = [2,1]
	I(lambda) = x1 + 4	sigma(lambda) = [1]
	I(# o) = x1 + x2 + 5	sigma(# o) = []
	I(o) = x1 + x2	sigma(o) = [1,2]
	I(p) = 0
    PREC: 1 > lambda > d > o > p > # o
    USABLE RULES: { 4 8 1 3 5 10 7 9 6 2 }
Number of SCCs: 1
  SCC { #2 #3 #6 #7 }
    POLO(Sum)... removes: #2 #3 #6 #7
	I(1) = 1
	I(d) = max(x1 + x2 + 2, 0)
	I(lambda) = max(x1 + 3, 0)
	I(# o) = max(x1 - 1, 0)
	I(o) = max(x1 + x2 + 2, 0)
	I(p) = 1
    USABLE RULES: { }
Number of SCCs: 0