MAYBE
Trs:
 {                         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(cons(te(a), sortSu(t))))) -> sortSu(cons(te(a), 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(cons(te(a), sortSu(s))), sortSu(t))) -> sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t))))),
                                                                                                                  sortSu(circ(sortSu(id()), sortSu(s))) -> sortSu(s),
                                                                                            sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) -> sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u))))),
                                                                                                                  sortSu(circ(sortSu(s), sortSu(id()))) -> sortSu(s),
                                                                                                                         te(subst(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(msubst(te(a), sortSu(id()))) -> te(a)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open