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, (/ 553739 8) + x1}
   sop(x1)	weight: max{0, (- (/ 276869 4)) + x1}
  #te(x1)	weight: max{0, (/ 181745 2) + x1}
#sortSu(x1)	weight: max{0, (/ 276869 4) + x1}
  lift()	weight: (/ 1 8)
msubst(x1,x2)	weight: max{0, (- (/ 726981 8)) + x2 + x1}
 subst(x1,x2)	weight: max{0, x1}
    te(x1)	weight: max{0, (/ 86621 4) + x1}
  cons(x1,x2)	weight: max{0, x1, (- (/ 190247 4)) + x2}
    id()	weight: (/ 1 8)
  circ(x1,x2)	weight: max{0, (- (/ 553739 4)) + x2 + x1}
    Usable rules: { 1..10 }
    Removed DPs: #2 #3 #5 #7 #9 #12
Number of SCCs: 2, DPs: 3, edges: 5
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
sortSu(x1)	weight: (/ 1 4)
   sop(x1)	weight: (/ 1 4)
  #te(x1)	weight: (/ 1 2) + x1
#sortSu(x1)	weight: 0
  lift()	weight: 0
msubst(x1,x2)	weight: x1
 subst(x1,x2)	weight: x1
    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: 2, edges: 4
	SCC { #13 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
sortSu(x1)	weight: (/ 1 8) + x1
   sop(x1)	weight: (/ 1 8)
  #te(x1)	weight: (/ 1 4) + x1
#sortSu(x1)	weight: x1
  lift()	weight: 0
msubst(x1,x2)	weight: x1
 subst(x1,x2)	weight: x1
    te(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: (/ 1 8)
    id()	weight: 0
  circ(x1,x2)	weight: x1 + x2
    Usable rules: { 1..10 }
    Removed DPs: #14
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 te cons
   sop(x1)	status: []	precedence above:
  #te(x1)	status: []	precedence above:
#sortSu(x1)	status: [x1]	precedence above:
  lift()	status: []	precedence above:
msubst(x1,x2)	status: []	precedence above: sortSu sop #te te cons circ
 subst(x1,x2)	status: [x1]	precedence above:
    te(x1)	status: []	precedence above: sop cons
  cons(x1,x2)	status: [x1]	precedence above: sop te
    id()	status: []	precedence above:
  circ(x1,x2)	status: [x1,x2]	precedence above: sortSu sop te cons
    Usable rules: { 1..10 }
    Removed DPs: #13
Number of SCCs: 0, DPs: 0, edges: 0
YES