Input TRS:
    1: comp(s,id()) -> s
    2: cons(one(),shift()) -> id()
    3: cons(comp(one(),s),comp(shift(),s)) -> s
    4: comp(one(),cons(s,t)) -> s
    5: comp(shift(),cons(s,t)) -> t
    6: comp(abs(s),t) -> abs(comp(s,cons(one(),comp(t,shift()))))
    7: comp(cons(s,t),u) -> cons(comp(s,u),comp(t,u))
    8: comp(id(),s) -> s
    9: comp(comp(s,t),u) -> comp(s,comp(t,u))
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #comp(abs(s),t) -> #comp(s,cons(one(),comp(t,shift())))
   #2: #comp(abs(s),t) -> #cons(one(),comp(t,shift()))
   #3: #comp(abs(s),t) -> #comp(t,shift())
   #4: #comp(comp(s,t),u) -> #comp(s,comp(t,u))
   #5: #comp(comp(s,t),u) -> #comp(t,u)
   #6: #comp(cons(s,t),u) -> #cons(comp(s,u),comp(t,u))
   #7: #comp(cons(s,t),u) -> #comp(s,u)
   #8: #comp(cons(s,t),u) -> #comp(t,u)
Number of SCCs: 1, DPs: 6, edges: 36
	SCC { #1 #3..5 #7 #8 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
#cons(x1,x2)	weight: 0
   one()	weight: 0
   abs(x1)	weight: max{0, (/ 1 4) + x1}
#comp(x1,x2)	weight: max{0, (/ 1 4) + x2 + x1}
  cons(x1,x2)	weight: max{0, x1, x2}
    id()	weight: 0
 shift()	weight: 0
  comp(x1,x2)	weight: max{0, x2 + x1}
    Usable rules: { 1..9 }
    Removed DPs: #1 #3
Number of SCCs: 1, DPs: 4, edges: 16
	SCC { #4 #5 #7 #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
   one()	weight: 0
   abs(x1)	weight: (/ 1 4) + x1
#comp(x1,x2)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
    id()	weight: 0
 shift()	weight: 0
  comp(x1,x2)	weight: (/ 1 4) + x1 + x2
    Usable rules: { }
    Removed DPs: #4 #5 #7 #8
Number of SCCs: 0, DPs: 0, edges: 0
YES