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
   |0|()	weight: 0
    T1()	weight: (/ 80649 4)
  topB(x1,x2,x3)	weight: 2 * x3 + x2 + x1
    S1()	weight: (/ 40327 2)
    T2()	weight: (/ 1 4)
   |1|()	weight: (/ 1 4)
  topA(x1,x2,x3)	weight: (/ 1 4) + 2 * x3 + x2 + x1
    N2()	weight: (/ 1 4)
    N1()	weight: 20163
    S2()	weight: (/ 1 4)
Number of strict rules: 0
YES