Input TRS:
    1: app(nil(),YS) -> YS
    2: app(cons(X,XS),YS) -> cons(X,n__app(activate(XS),YS))
    3: from(X) -> cons(X,n__from(n__s(X)))
    4: zWadr(nil(),YS) -> nil()
    5: zWadr(XS,nil()) -> nil()
    6: zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,n__nil())),n__zWadr(activate(XS),activate(YS)))
    7: prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L)))
    8: app(X1,X2) -> n__app(X1,X2)
    9: from(X) -> n__from(X)
    10: s(X) -> n__s(X)
    11: nil() -> n__nil()
    12: zWadr(X1,X2) -> n__zWadr(X1,X2)
    13: prefix(X) -> n__prefix(X)
    14: activate(n__app(X1,X2)) -> app(activate(X1),activate(X2))
    15: activate(n__from(X)) -> from(activate(X))
    16: activate(n__s(X)) -> s(activate(X))
    17: activate(n__nil()) -> nil()
    18: activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(X2))
    19: activate(n__prefix(X)) -> prefix(activate(X))
    20: activate(X) -> X
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #app(cons(X,XS),YS) -> #activate(XS)
   #2: #zWadr(cons(X,XS),cons(Y,YS)) -> #app(Y,cons(X,n__nil()))
   #3: #zWadr(cons(X,XS),cons(Y,YS)) -> #activate(XS)
   #4: #zWadr(cons(X,XS),cons(Y,YS)) -> #activate(YS)
   #5: #activate(n__app(X1,X2)) -> #app(activate(X1),activate(X2))
   #6: #activate(n__app(X1,X2)) -> #activate(X1)
   #7: #activate(n__app(X1,X2)) -> #activate(X2)
   #8: #prefix(L) -> #nil()
   #9: #activate(n__nil()) -> #nil()
   #10: #activate(n__prefix(X)) -> #prefix(activate(X))
   #11: #activate(n__prefix(X)) -> #activate(X)
   #12: #activate(n__s(X)) -> #s(activate(X))
   #13: #activate(n__s(X)) -> #activate(X)
   #14: #activate(n__from(X)) -> #from(activate(X))
   #15: #activate(n__from(X)) -> #activate(X)
   #16: #activate(n__zWadr(X1,X2)) -> #zWadr(activate(X1),activate(X2))
   #17: #activate(n__zWadr(X1,X2)) -> #activate(X1)
   #18: #activate(n__zWadr(X1,X2)) -> #activate(X2)
Number of SCCs: 1, DPs: 13, edges: 95
	SCC { #1..7 #11 #13 #15..18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
     s(x1)	weight: x1
n__prefix(x1)	weight: (/ 3 8) + x1
activate(x1)	weight: x1
n__from(x1)	weight: (/ 1 4) + x1
#activate(x1)	weight: (/ 1 16) + x1
prefix(x1)	weight: (/ 3 8) + x1
#zWadr(x1,x2)	weight: max{(/ 1 16) + x2, (/ 7 16) + x1}
 zWadr(x1,x2)	weight: max{x2, (/ 3 8) + x1}
n__nil()	weight: (/ 1 8)
n__zWadr(x1,x2)	weight: max{x2, (/ 3 8) + x1}
  n__s(x1)	weight: x1
  from(x1)	weight: (/ 1 4) + x1
n__app(x1,x2)	weight: max{(/ 1 16) + x2, x1}
   #s(x1)	weight: 0
   nil()	weight: (/ 1 8)
#prefix(x1)	weight: 0
 #nil()	weight: 0
 #app(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 16) + x1}
#from(x1)	weight: 0
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
   app(x1,x2)	weight: max{(/ 1 16) + x2, x1}
    Usable rules: { 1..20 }
    Removed DPs: #2 #3 #7 #11 #15 #17
Number of SCCs: 1, DPs: 7, edges: 27
	SCC { #1 #4..6 #13 #16 #18 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4) + x1
n__prefix(x1)	weight: (/ 1 4)
activate(x1)	weight: x1
n__from(x1)	weight: (/ 1 4)
#activate(x1)	weight: x1
prefix(x1)	weight: (/ 1 4)
#zWadr(x1,x2)	weight: x2
 zWadr(x1,x2)	weight: x2
n__nil()	weight: 0
n__zWadr(x1,x2)	weight: x2
  n__s(x1)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4)
n__app(x1,x2)	weight: (/ 1 2) + x1 + x2
   #s(x1)	weight: 0
   nil()	weight: 0
#prefix(x1)	weight: 0
 #nil()	weight: 0
 #app(x1,x2)	weight: (/ 1 4) + x1
#from(x1)	weight: 0
  cons(x1,x2)	weight: x2
   app(x1,x2)	weight: (/ 1 2) + x1 + x2
    Usable rules: { 1..20 }
    Removed DPs: #1 #5 #6 #13
Number of SCCs: 1, DPs: 3, edges: 5
	SCC { #4 #16 #18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     s(x1)	weight: max{0, (- (/ 1 16)) + x1}
n__prefix(x1)	weight: max{0, (/ 3 8) + x1}
activate(x1)	weight: max{0, x1}
n__from(x1)	weight: max{0, (/ 1 4) + x1}
#activate(x1)	weight: max{0, (/ 1 4) + x1}
prefix(x1)	weight: max{0, (/ 3 8) + x1}
#zWadr(x1,x2)	weight: max{0, (/ 3 8) + x2}
 zWadr(x1,x2)	weight: max{0, (/ 1 2) + x1, (/ 1 8) + x2}
n__nil()	weight: (/ 1 16)
n__zWadr(x1,x2)	weight: max{0, (/ 1 2) + x1, (/ 1 8) + x2}
  n__s(x1)	weight: max{0, (- (/ 1 16)) + x1}
  from(x1)	weight: max{0, (/ 1 4) + x1}
n__app(x1,x2)	weight: max{0, (/ 1 16) + x1, (/ 13 16) + x2}
   #s(x1)	weight: 0
   nil()	weight: (/ 1 16)
#prefix(x1)	weight: 0
 #nil()	weight: 0
 #app(x1,x2)	weight: 0
#from(x1)	weight: 0
  cons(x1,x2)	weight: max{0, (- (/ 5 16)) + x1, (- (/ 1 8)) + x2}
   app(x1,x2)	weight: max{0, (/ 1 16) + x1, (/ 13 16) + x2}
    Usable rules: { 1..20 }
    Removed DPs: #18
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #4 #16 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE