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