Input TRS:
    1: f(s(x),y) -> f(-(s(x),y),y)
   e1: +(0(),y) ->= y	[relative]
   e2: +(s(x),y) ->= s(+(x,y))	[relative]
   e3: -(x,0()) ->= x	[relative]
   e4: -(0(),y) ->= 0()	[relative]
   e5: -(s(x),s(y)) ->= -(x,y)	[relative]
   e6: f(x,y) ->= f(x,+(x,y))	[relative]
Number of Rules: 1
Direct POLO(Sum) ...Direct Mat2b ...Direct Mat3b ... failed.
Dependency Pairs:
   #1: # f(x,y) -> # f(x,+(x,y))	[relative]
   #2: # f(s(x),y) -> # f(-(s(x),y),y)
Number of SCCs: 1
  SCC { #1 #2 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat3b... failed.