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())
    7: topA(i,N1(),y) ->= topA(1(),T1(),y)
    8: topB(i,x,N2()) ->= topB(0(),x,T2())
    9: topA(i,S1(),y) ->= topA(i,N1(),y)
    10: topB(i,x,S2()) ->= topB(i,x,N2())
    11: topB(i,N1(),T2()) ->= topB(i,N1(),S2())
    12: topB(1(),T1(),T2()) ->= topB(1(),T1(),S2())
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5 7 9 6 2
     1()	weight: (/ 65213 4)
    T1()	weight: (/ 234849 4)
  topB(x1,x2,x3)	weight: x3 + x2 + x1
    S1()	weight: (/ 150033 2)
    T2()	weight: (/ 1 4)
     0()	weight: 0
  topA(x1,x2,x3)	weight: (/ 1 4) + x3 + x2 + x1
    N2()	weight: (/ 1 4)
    N1()	weight: 75016
    S2()	weight: (/ 1 4)
Number of strict rules: 0
YES