We consider the following Problem:

  Strict Trs:
    {  circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
     , circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t))
     , circ(cons(lift(), s), cons(lift(), t)) ->
       cons(lift(), circ(s, t))
     , circ(circ(s, t), u) -> circ(s, circ(t, u))
     , circ(s, id()) -> s
     , circ(id(), s) -> s
     , circ(cons(lift(), s), circ(cons(lift(), t), u)) ->
       circ(cons(lift(), circ(s, t)), u)
     , subst(a, id()) -> a
     , msubst(a, id()) -> a
     , msubst(msubst(a, s), t) -> msubst(a, circ(s, t))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
  Arguments of following rules are not normal-forms:
  {circ(cons(lift(), s), circ(cons(lift(), t), u)) ->
   circ(cons(lift(), circ(s, t)), u)}
  
  All above mentioned rules can be savely removed.
  
  We consider the following Problem:
  
    Strict Trs:
      {  circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
       , circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t))
       , circ(cons(lift(), s), cons(lift(), t)) ->
         cons(lift(), circ(s, t))
       , circ(circ(s, t), u) -> circ(s, circ(t, u))
       , circ(s, id()) -> s
       , circ(id(), s) -> s
       , subst(a, id()) -> a
       , msubst(a, id()) -> a
       , msubst(msubst(a, s), t) -> msubst(a, circ(s, t))}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^2))
  
  Proof:
    We consider the following Problem:
    
      Strict Trs:
        {  circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t))
         , circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t))
         , circ(cons(lift(), s), cons(lift(), t)) ->
           cons(lift(), circ(s, t))
         , circ(circ(s, t), u) -> circ(s, circ(t, u))
         , circ(s, id()) -> s
         , circ(id(), s) -> s
         , subst(a, id()) -> a
         , msubst(a, id()) -> a
         , msubst(msubst(a, s), t) -> msubst(a, circ(s, t))}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^2))
    
    Proof:
      The following argument positions are usable:
        Uargs(circ) = {2}, Uargs(cons) = {1, 2}, Uargs(msubst) = {2},
        Uargs(subst) = {}
      We have the following restricted  polynomial interpretation:
      Interpretation Functions:
       [circ](x1, x2) = 1 + 2*x1 + x1*x2 + x1^2 + x2
       [cons](x1, x2) = 2 + x1 + x2
       [msubst](x1, x2) = 2 + 3*x1 + x1*x2 + x1^2 + 2*x2
       [lift]() = 3
       [id]() = 3
       [subst](x1, x2) = 1 + x1

Hurray, we answered YES(?,O(n^2))