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))
    7: topA(i,N1(x),y) ->= topA(1(),T1(x),y)
    8: topB(i,x,N2(y)) ->= topB(0(),x,T2(y))
    9: topA(i,S1(x),y) ->= topA(i,N1(x),y)
    10: topB(i,x,S2(y)) ->= topB(i,x,N2(y))
    11: topB(i,N1(x),T2(y)) ->= topB(i,N1(x),S2(y))
    12: topB(1(),T1(x),T2(y)) ->= topB(1(),T1(x),S2(y))
    13: topA(i,N1(x),y) ->= topA(i,N1(C(x)),y)
    14: topB(i,x,N2(y)) ->= topB(i,x,N2(C(y)))
    15: topA(i,T1(x),y) ->= topA(i,T1(x),y)
    16: topB(i,x,T2(y)) ->= topB(i,x,T2(y))
    17: topB(i,x,S2(y)) ->= topB(i,x,S2(D(y)))
Removing trivial weak rule 16.
Removing trivial weak rule 15.
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5 7 9 6 2
     1()	weight: (/ 1 16)
    T1(x1)	weight: (/ 1 16) + x1
  topB(x1,x2,x3)	weight: x3 + 2 * x2 + 2 * x1
    S1(x1)	weight: (/ 1 4) + x1
    T2(x1)	weight: (/ 1 16) + x1
     D(x1)	weight: x1
     C(x1)	weight: x1
     0()	weight: 0
  topA(x1,x2,x3)	weight: (/ 1 16) + x3 + 2 * x2 + 2 * x1
    N2(x1)	weight: (/ 1 16) + x1
    N1(x1)	weight: (/ 3 16) + x1
    S2(x1)	weight: (/ 1 16) + x1
Number of strict rules: 0
YES