Input TRS:
    1: topB(i,N1(x),y) -> topA(1(),T1(x),y)
    2: topA(i,x,N2(y)) -> topB(0(),x,T2(y))
    3: topB(i,S1(x),y) -> topA(i,N1(x),y)
    4: topA(i,x,S2(y)) -> topB(i,x,N2(y))
    5: topA(i,N1(x),T2(y)) -> topB(i,N1(x),S2(y))
    6: topA(1(),T1(x),T2(y)) -> topB(1(),T1(x),S2(y))
   e1: topA(i,N1(x),y) ->= topA(1(),T1(x),y)	[relative]
   e2: topB(i,x,N2(y)) ->= topB(0(),x,T2(y))	[relative]
   e3: topA(i,S1(x),y) ->= topA(i,N1(x),y)	[relative]
   e4: topB(i,x,S2(y)) ->= topB(i,x,N2(y))	[relative]
   e5: topB(i,N1(x),T2(y)) ->= topB(i,N1(x),S2(y))	[relative]
   e6: topB(1(),T1(x),T2(y)) ->= topB(1(),T1(x),S2(y))	[relative]
   e7: topA(i,N1(x),y) ->= topA(i,N1(C(x)),y)	[relative]
   e8: topB(i,x,N2(y)) ->= topB(i,x,N2(C(y)))	[relative]
   e9: topA(i,T1(x),y) ->= topA(i,T1(x),y)	[relative]
   e10: topB(i,x,T2(y)) ->= topB(i,x,T2(y))	[relative]
   e11: topB(i,x,S2(y)) ->= topB(i,x,S2(D(y)))	[relative]
Removing trivial relative rule e9.
Removing trivial relative rule e10.
Dependency Pairs:
   #1: # topA(i,x,N2(y)) -> # topB(0(),x,T2(y))
   #2: # topA(1(),T1(x),T2(y)) -> # topB(1(),T1(x),S2(y))
   #3: # topB(i,x,S2(y)) -> # topB(i,x,N2(y))	[relative]
   #4: # topB(i,x,N2(y)) -> # topB(i,x,N2(C(y)))	[relative]
   #5: # topA(i,S1(x),y) -> # topA(i,N1(x),y)	[relative]
   #6: # topB(i,N1(x),T2(y)) -> # topB(i,N1(x),S2(y))	[relative]
   #7: # topB(i,x,S2(y)) -> # topB(i,x,S2(D(y)))	[relative]
   #8: # topB(1(),T1(x),T2(y)) -> # topB(1(),T1(x),S2(y))	[relative]
   #9: # topA(i,N1(x),y) -> # topA(i,N1(C(x)),y)	[relative]
   #10: # topA(i,N1(x),T2(y)) -> # topB(i,N1(x),S2(y))
   #11: # topB(i,S1(x),y) -> # topA(i,N1(x),y)
   #12: # topB(i,N1(x),y) -> # topA(1(),T1(x),y)
   #13: # topB(i,x,N2(y)) -> # topB(0(),x,T2(y))	[relative]
   #14: # topA(i,N1(x),y) -> # topA(1(),T1(x),y)	[relative]
   #15: # topA(i,x,S2(y)) -> # topB(i,x,N2(y))
Number of SCCs: 1
  SCC { #1..4 #6 #7 #9..15 }
    POLO(Sum)... removes: #1 #2 #10 #11 #12 #14 #15
	I(1) = 1
	I(T1) = 0
	I(S1) = max(x1 + 9, 0)
	I(T2) = 0
	I(# topB) = max(x1 + x2 + x3 - 2, 0)
	I(D) = 1
	I(C) = max(x1 - 1, 0)
	I(0) = 0
	I(# topA) = max(x1 + x2 + x3 + 1, 0)
	I(N2) = 0
	I(N1) = 5
	I(S2) = 0
    USABLE RULES: { }
Number of SCCs: 2
  SCC { #9 }
    POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat2b... failed.