MAYBE
MAYBE
TRS:
 {
                                                                                                                  
  sortSu(circ(sortSu(s), sortSu(id()))) -> sortSu(s),
                                                                                                
  sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) ->
  sortSu(
        cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))
        )
  ),
                                 sortSu(
                                       circ(
                                           sortSu(
                                                 cons(sop(lift()), sortSu(s))
                                           ), sortSu(cons(te(a), sortSu(t)))
                                       )
                                 )
  -> sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t))))),
                           sortSu(
                                 circ(
                                     sortSu(cons(sop(lift()), sortSu(s))),
                                     sortSu(cons(sop(lift()), sortSu(t)))
                                 )
                           )
  -> sortSu(cons(sop(lift()), sortSu(circ(sortSu(s), sortSu(t))))),
  sortSu(
        circ(
            sortSu(cons(sop(lift()), sortSu(s))),
            sortSu(circ(sortSu(cons(sop(lift()), sortSu(t))), sortSu(u)))
        )
  ) ->
  sortSu(
        circ(
            sortSu(cons(sop(lift()), sortSu(circ(sortSu(s), sortSu(t))))),
            sortSu(u)
        )
  ),
                                                                                            
  sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) ->
  sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u))))),
                                                                                                                  
  sortSu(circ(sortSu(id()), sortSu(s))) -> sortSu(s),
                                                                                                                        
  te(msubst(te(a), sortSu(id()))) -> te(a),
                                                                                                    
  te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) ->
  te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t))))),
                                                                                                                         
  te(subst(te(a), sortSu(id()))) -> te(a)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                                                                                                                    
    sortSu(circ(sortSu(s), sortSu(id()))) -> sortSu(s),
                                                                                                  
    sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) ->
    sortSu(
          cons(
              te(msubst(te(a), sortSu(t))),
              sortSu(circ(sortSu(s), sortSu(t)))
          )
    ),
                                   sortSu(
                                         circ(
                                             sortSu(
                                                   cons(
                                                       sop(lift()), sortSu(s)
                                                   )
                                             ),
                                             sortSu(cons(te(a), sortSu(t)))
                                         )
                                   )
    -> sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t))))),
                             sortSu(
                                   circ(
                                       sortSu(cons(sop(lift()), sortSu(s))),
                                       sortSu(cons(sop(lift()), sortSu(t)))
                                   )
                             )
    -> sortSu(cons(sop(lift()), sortSu(circ(sortSu(s), sortSu(t))))),
    sortSu(
          circ(
              sortSu(cons(sop(lift()), sortSu(s))),
              sortSu(circ(sortSu(cons(sop(lift()), sortSu(t))), sortSu(u)))
          )
    ) ->
    sortSu(
          circ(
              sortSu(cons(sop(lift()), sortSu(circ(sortSu(s), sortSu(t))))),
              sortSu(u)
          )
    ),
                                                                                              
    sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) ->
    sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u))))),
                                                                                                                    
    sortSu(circ(sortSu(id()), sortSu(s))) -> sortSu(s),
                                                                                                                          
    te(msubst(te(a), sortSu(id()))) -> te(a),
                                                                                                      
    te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) ->
    te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t))))),
                                                                                                                           
    te(subst(te(a), sortSu(id()))) -> te(a)
   }
  Fail