Input TRS:
    1: s(a(x)) -> s(b(x))
    2: b(b(x)) -> a(x)
   e1: f(s(x),y) ->= f(x,s(y))	[relative]
   e2: s(a(x)) ->= a(s(x))	[relative]
   e3: s(b(x)) ->= b(s(x))	[relative]
   e4: a(s(x)) ->= s(a(x))	[relative]
   e5: b(s(x)) ->= s(b(x))	[relative]
Dependency Pairs:
   #1: # b(b(x)) -> # a(x)
   #2: # a(s(x)) -> # s(a(x))	[relative]
   #3: # a(s(x)) -> # a(x)	[relative]
   #4: # f(s(x),y) -> # f(x,s(y))	[relative]
   #5: # f(s(x),y) -> # s(y)	[relative]
   #6: # b(s(x)) -> # s(b(x))	[relative]
   #7: # b(s(x)) -> # b(x)	[relative]
   #8: # s(a(x)) -> # a(s(x))	[relative]
   #9: # s(a(x)) -> # s(x)	[relative]
   #10: # s(a(x)) -> # s(b(x))
   #11: # s(a(x)) -> # b(x)
   #12: # s(b(x)) -> # b(s(x))	[relative]
   #13: # s(b(x)) -> # s(x)	[relative]
Number of SCCs: 2
  SCC { #4 }
    POLO(Sum)... removes: #4
	I(a) = 0
	I(# a) = 0
	I(s) = max(x1 + 1, 0)
	I(b) = 0
	I(# s) = max(x1 - 1, 0)
	I(# f) = max(x1 + 1, 0)
	I(# b) = max(x1 - 1, 0)
    USABLE RULES: { }
Number of SCCs: 1
  SCC { #1..3 #6..13 }
    POLO(Sum)... removes: #1 #3 #7 #9 #10 #11 #13
	I(a) = max(x1 + 5, 0)
	I(# a) = max(x1 + 1, 0)
	I(s) = max(x1 + 6, 0)
	I(b) = max(x1 + 3, 0)
	I(# s) = max(x1 + 2, 0)
	I(# f) = max(x1 + 1, 0)
	I(# b) = max(x1 - 1, 0)
    USABLE RULES: { 4 1 3 5 6 2 }
Number of SCCs: 1
  SCC { #2 #6 #8 #12 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.