ceta_v1.17: REJECTED
termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.1: error below the monotonic reduction pair (with usable rules) processor
  1.1.1.1: error below the monotonic reduction pair processor
   1.1.1.1.1: error below the monotonic reduction pair processor
    1.1.1.1.1.1: error below the monotonic reduction pair processor
     1.1.1.1.1.1.1: error when applying the reduction pair processor to switch from
      dependency pairs:
      top#(ok(X)) -> top#(active(X))
      top#(mark(X)) -> top#(proper(X))
      rewrite system:
      proper(nats) -> ok(nats)
      proper(adx(X)) -> adx(proper(X))
      proper(zeros) -> ok(zeros)
      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
      proper(0) -> ok(0)
      proper(incr(X)) -> incr(proper(X))
      proper(s(X)) -> s(proper(X))
      proper(hd(X)) -> hd(proper(X))
      proper(tl(X)) -> tl(proper(X))
      tl(mark(X)) -> mark(tl(X))
      tl(ok(X)) -> ok(tl(X))
      hd(mark(X)) -> mark(hd(X))
      hd(ok(X)) -> ok(hd(X))
      s(ok(X)) -> ok(s(X))
      incr(mark(X)) -> mark(incr(X))
      incr(ok(X)) -> ok(incr(X))
      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
      adx(mark(X)) -> mark(adx(X))
      adx(ok(X)) -> ok(adx(X))
      active(zeros) -> mark(cons(0, zeros))
      active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
      active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
      active(adx(X)) -> adx(active(X))
      active(incr(X)) -> incr(active(X))
      active(hd(X)) -> hd(active(X))
      active(tl(X)) -> tl(active(X))
      
      to the DP problem
      dependency pairs:
      top#(ok(X)) -> top#(active(X))
      rewrite system:
      proper(nats) -> ok(nats)
      proper(adx(X)) -> adx(proper(X))
      proper(zeros) -> ok(zeros)
      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
      proper(0) -> ok(0)
      proper(incr(X)) -> incr(proper(X))
      proper(s(X)) -> s(proper(X))
      proper(hd(X)) -> hd(proper(X))
      proper(tl(X)) -> tl(proper(X))
      tl(mark(X)) -> mark(tl(X))
      tl(ok(X)) -> ok(tl(X))
      hd(mark(X)) -> mark(hd(X))
      hd(ok(X)) -> ok(hd(X))
      s(ok(X)) -> ok(s(X))
      incr(mark(X)) -> mark(incr(X))
      incr(ok(X)) -> ok(incr(X))
      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
      adx(mark(X)) -> mark(adx(X))
      adx(ok(X)) -> ok(adx(X))
      active(zeros) -> mark(cons(0, zeros))
      active(incr(cons(X, Y))) -> mark(cons(s(X), incr(Y)))
      active(adx(cons(X, Y))) -> mark(incr(cons(X, adx(Y))))
      active(adx(X)) -> adx(active(X))
      active(incr(X)) -> incr(active(X))
      active(hd(X)) -> hd(active(X))
      active(tl(X)) -> tl(active(X))
      
      could not apply the reduction pair processor with the following
      Argument Filter: 
      pi(top#/1) = [1]
      pi(ok/1) = 1
      pi(active/1) = 1
      pi(mark/1) = [1]
      pi(proper/1) = 1
      pi(zeros/0) = []
      pi(cons/2) = [1]
      pi(0/0) = []
      pi(incr/1) = [1]
      pi(s/1) = []
      pi(adx/1) = [1]
      pi(hd/1) = [1]
      pi(tl/1) = 1
      pi(nats/0) = []
      
      LPO with the following precedence
      precedence(top#[1]) = 0
      precedence(mark[1]) = 3
      precedence(zeros[0]) = 5
      precedence(cons[2]) = 2
      precedence(0[0]) = 4
      precedence(incr[1]) = 3
      precedence(s[1]) = 1
      precedence(adx[1]) = 6
      precedence(hd[1]) = 3
      precedence(nats[0]) = 7
      
      precedence(_) = 0
      
      problem when orienting TRS
      could not orient active(incr(cons(X, Y))) >= mark(cons(s(X), incr(Y)))
      pi( active(incr(cons(X, Y))) ) = incr(cons(X))
      pi( mark(cons(s(X), incr(Y))) ) = mark(cons(s))
      could not orient incr(cons(X)) >=LPO mark(cons(s))