Input TRS:
    1: sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t)))))
    2: sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t)))))
    3: sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t)))))
    4: sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))
    5: sortSu(circ(sortSu(s),sortSu(id()))) -> sortSu(s)
    6: sortSu(circ(sortSu(id()),sortSu(s))) -> sortSu(s)
    7: 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)))
    8: te(subst(te(a),sortSu(id()))) -> te(a)
    9: te(msubst(te(a),sortSu(id()))) -> te(a)
    10: te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> #sortSu(cons(te(a),sortSu(circ(sortSu(s),sortSu(t)))))
   #2: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> #sortSu(circ(sortSu(s),sortSu(t)))
   #3: #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)))
   #4: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift()),sortSu(t))),sortSu(u))))) -> #sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t)))))
   #5: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift()),sortSu(t))),sortSu(u))))) -> #sortSu(circ(sortSu(s),sortSu(t)))
   #6: #te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> #te(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t)))))
   #7: #te(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> #sortSu(circ(sortSu(s),sortSu(t)))
   #8: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> #sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t)))))
   #9: #sortSu(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> #sortSu(circ(sortSu(s),sortSu(t)))
   #10: #sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> #sortSu(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t)))))
   #11: #sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> #te(msubst(te(a),sortSu(t)))
   #12: #sortSu(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> #sortSu(circ(sortSu(s),sortSu(t)))
   #13: #sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> #sortSu(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u)))))
   #14: #sortSu(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> #sortSu(circ(sortSu(t),sortSu(u)))
Number of SCCs: 1, DPs: 10, edges: 64
	SCC { #2 #3 #5..7 #9 #11..14 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
sortSu(x1)	weight: max{0, 118196 + x1}
   sop(x1)	weight: 0
  #te(x1)	weight: max{0, (- (/ 1 4)) + x1}
#sortSu(x1)	weight: max{0, -23639 + x1}
  lift()	weight: (/ 1 4)
msubst(x1,x2)	weight: max{0, (/ 1087407 4) + x2 + x1}
 subst(x1,x2)	weight: max{0, 283671 + x1}
    te(x1)	weight: max{0, -283671 + x1}
  cons(x1,x2)	weight: max{0, (/ 638259 2) + x1, 59098 + x2}
    id()	weight: (/ 1 4)
  circ(x1,x2)	weight: max{0, (- (/ 520061 4)) + x2 + x1}
    Usable rules: { 1..10 }
    Removed DPs: #2 #3 #5 #7 #9 #11 #12 #14
Number of SCCs: 2, DPs: 2, edges: 2
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
sortSu(x1)	weight: (/ 1 4)
   sop(x1)	weight: (/ 1 4)
  #te(x1)	weight: x1
#sortSu(x1)	weight: (/ 1 2)
  lift()	weight: 0
msubst(x1,x2)	weight: x1
 subst(x1,x2)	weight: x1 + x2
    te(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4)
    id()	weight: 0
  circ(x1,x2)	weight: (/ 1 4)
    Usable rules: { 1..10 }
    Removed DPs: #6
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #13 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
sortSu(x1)	status: [x1]	precedence above: sop msubst te cons
   sop(x1)	status: []	precedence above: sortSu msubst te cons
  #te(x1)	status: []	precedence above:
#sortSu(x1)	status: [x1]	precedence above:
  lift()	status: []	precedence above:
msubst(x1,x2)	status: []	precedence above: te cons
 subst(x1,x2)	status: [x2,x1]	precedence above:
    te(x1)	status: []	precedence above: msubst cons
  cons(x1,x2)	status: []	precedence above: msubst te
    id()	status: []	precedence above:
  circ(x1,x2)	status: [x1,x2]	precedence above: sortSu sop msubst te cons
    Usable rules: { 1..7 }
    Removed DPs: #13
Number of SCCs: 0, DPs: 0, edges: 0
YES