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
   |0|()	weight: 0
    T1(x1)	weight: (/ 135813 4) + x1
  topB(x1,x2,x3)	weight: x3 + x2 + x1
    S1(x1)	weight: (/ 67909 2) + x1
    T2(x1)	weight: (/ 122449 4) + x1
     D(x1)	weight: x1
     C(x1)	weight: x1
   |1|()	weight: (/ 1 4)
  topA(x1,x2,x3)	weight: (/ 1 4) + x3 + x2 + x1
    N2(x1)	weight: (/ 122449 4) + x1
    N1(x1)	weight: 33954 + x1
    S2(x1)	weight: (/ 122449 4) + x1
Number of strict rules: 0
YES