ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.1: error when applying the reduction pair processor to remove from the DP problem
  pairs:
  
  a__app#(nil, YS) -> mark#(YS)
  a__app#(cons(X, XS), YS) -> mark#(X)
  a__from#(X) -> mark#(X)
  a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark(Y), cons(mark(X), nil))
  a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark#(Y)
  a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark#(X)
  mark#(app(X1, X2)) -> a__app#(mark(X1), mark(X2))
  mark#(app(X1, X2)) -> mark#(X1)
  mark#(app(X1, X2)) -> mark#(X2)
  mark#(from(X)) -> a__from#(mark(X))
  mark#(from(X)) -> mark#(X)
  mark#(zWadr(X1, X2)) -> a__zWadr#(mark(X1), mark(X2))
  mark#(zWadr(X1, X2)) -> mark#(X1)
  mark#(zWadr(X1, X2)) -> mark#(X2)
  mark#(prefix(X)) -> mark#(X)
  mark#(cons(X1, X2)) -> mark#(X1)
  mark#(s(X)) -> mark#(X)
  rules:
  
  a__app(nil, YS) -> mark(YS)
  a__app(cons(X, XS), YS) -> cons(mark(X), app(XS, YS))
  a__app(X1, X2) -> app(X1, X2)
  a__from(X) -> cons(mark(X), from(s(X)))
  a__from(X) -> from(X)
  a__prefix(L) -> cons(nil, zWadr(L, prefix(L)))
  a__prefix(X) -> prefix(X)
  a__zWadr(nil, YS) -> nil
  a__zWadr(XS, nil) -> nil
  a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
  a__zWadr(X1, X2) -> zWadr(X1, X2)
  mark(app(X1, X2)) -> a__app(mark(X1), mark(X2))
  mark(from(X)) -> a__from(mark(X))
  mark(zWadr(X1, X2)) -> a__zWadr(mark(X1), mark(X2))
  mark(prefix(X)) -> a__prefix(mark(X))
  mark(nil) -> nil
  mark(cons(X1, X2)) -> cons(mark(X1), X2)
  mark(s(X)) -> s(mark(X))
  
   the pairs 
  a__app#(nil, YS) -> mark#(YS)
  a__app#(cons(X, XS), YS) -> mark#(X)
  a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark#(Y)
  a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark#(X)
  mark#(app(X1, X2)) -> a__app#(mark(X1), mark(X2))
  mark#(app(X1, X2)) -> mark#(X1)
  mark#(app(X1, X2)) -> mark#(X2)
  mark#(zWadr(X1, X2)) -> a__zWadr#(mark(X1), mark(X2))
  mark#(zWadr(X1, X2)) -> mark#(X1)
  mark#(zWadr(X1, X2)) -> mark#(X2)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(mark#) = [(epsilon,0),(1,0)]
  pi(a__app#) = [(epsilon,0),(1,2),(2,0)]
  pi(a__from#) = [(epsilon,0),(1,0)]
  pi(a__zWadr#) = [(epsilon,0),(1,0),(2,2)]
  polynomial interpretration over naturals with negative constants
  Pol(mark#(x_1)) = 1
  Pol(app(x_1, x_2)) = 1 + x_2 + x_1
  Pol(a__app#(x_1, x_2)) = 1
  Pol(mark(x_1)) = x_1
  Pol(nil) = 0
  Pol(from(x_1)) = x_1
  Pol(a__from#(x_1)) = 1
  Pol(zWadr(x_1, x_2)) = 1 + x_2 + x_1
  Pol(a__zWadr#(x_1, x_2)) = 1
  Pol(cons(x_1, x_2)) = x_1
  Pol(prefix(x_1)) = x_1
  Pol(s(x_1)) = x_1
  Pol(a__app(x_1, x_2)) = 1 + x_2 + x_1
  Pol(a__from(x_1)) = x_1
  Pol(a__zWadr(x_1, x_2)) = 1 + x_2 + x_1
  Pol(a__prefix(x_1)) = x_1
  problem when orienting DPs
  cannot orient pair a__from#(X) -> mark#(X) weakly:
  [(a__from#(X),0),(X,0)] >=mu [(mark#(X),0),(X,0)] could not be ensured