MAYBE

Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(tail(cons(X,XS))) -> mark(XS)
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(tail(X)) -> tail(active(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 tail(mark(X)) -> mark(tail(X))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(tail(X)) -> tail(proper(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 tail(ok(X)) -> ok(tail(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(cons(X1,X2)) -> active#(X1)
   active#(cons(X1,X2)) -> cons#(active(X1),X2)
   active#(tail(X)) -> active#(X)
   active#(tail(X)) -> tail#(active(X))
   cons#(mark(X1),X2) -> cons#(X1,X2)
   tail#(mark(X)) -> tail#(X)
   proper#(cons(X1,X2)) -> proper#(X2)
   proper#(cons(X1,X2)) -> proper#(X1)
   proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
   proper#(tail(X)) -> proper#(X)
   proper#(tail(X)) -> tail#(proper(X))
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   tail#(ok(X)) -> tail#(X)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(tail(cons(X,XS))) -> mark(XS)
   active(cons(X1,X2)) -> cons(active(X1),X2)
   active(tail(X)) -> tail(active(X))
   cons(mark(X1),X2) -> mark(cons(X1,X2))
   tail(mark(X)) -> mark(tail(X))
   proper(zeros()) -> ok(zeros())
   proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(tail(X)) -> tail(proper(X))
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   tail(ok(X)) -> ok(tail(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  Usable Rule Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(tail(X)) -> active#(X)
    active#(tail(X)) -> tail#(active(X))
    cons#(mark(X1),X2) -> cons#(X1,X2)
    tail#(mark(X)) -> tail#(X)
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X)
    proper#(tail(X)) -> tail#(proper(X))
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    tail#(ok(X)) -> tail#(X)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(tail(cons(X,XS))) -> mark(XS)
    active(cons(X1,X2)) -> cons(active(X1),X2)
    active(tail(X)) -> tail(active(X))
    cons(mark(X1),X2) -> mark(cons(X1,X2))
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    tail(mark(X)) -> mark(tail(X))
    tail(ok(X)) -> ok(tail(X))
    proper(zeros()) -> ok(zeros())
    proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(tail(X)) -> tail(proper(X))
   ADG Processor:
    DPs:
     active#(zeros()) -> cons#(0(),zeros())
     active#(cons(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(tail(X)) -> active#(X)
     active#(tail(X)) -> tail#(active(X))
     cons#(mark(X1),X2) -> cons#(X1,X2)
     tail#(mark(X)) -> tail#(X)
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(tail(X)) -> proper#(X)
     proper#(tail(X)) -> tail#(proper(X))
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     tail#(ok(X)) -> tail#(X)
     top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X))
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     tail(ok(X)) -> ok(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
    graph:
     top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
     top#(ok(X)) -> top#(active(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
     top#(ok(X)) -> active#(X) -> active#(zeros()) -> cons#(0(),zeros())
     top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
     top#(ok(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     top#(ok(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
     top#(ok(X)) -> active#(X) ->
     active#(tail(X)) -> tail#(active(X))
     top#(mark(X)) -> top#(proper(X)) ->
     top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> top#(proper(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
     top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     top#(mark(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(tail(X)) -> tail#(proper(X))
     proper#(tail(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(tail(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(tail(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(tail(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
     proper#(tail(X)) -> proper#(X) ->
     proper#(tail(X)) -> tail#(proper(X))
     proper#(tail(X)) -> tail#(proper(X)) ->
     tail#(mark(X)) -> tail#(X)
     proper#(tail(X)) -> tail#(proper(X)) ->
     tail#(ok(X)) -> tail#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(tail(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(tail(X)) -> tail#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(tail(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(tail(X)) -> tail#(proper(X))
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     tail#(ok(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
     tail#(ok(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X)
     tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
     tail#(mark(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X)
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     active#(tail(X)) -> tail#(active(X)) ->
     tail#(mark(X)) -> tail#(X)
     active#(tail(X)) -> tail#(active(X)) -> tail#(ok(X)) -> tail#(X)
     active#(tail(X)) -> active#(X) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(tail(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(tail(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(tail(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
     active#(tail(X)) -> active#(X) ->
     active#(tail(X)) -> tail#(active(X))
     active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(tail(X)) -> active#(X)
     active#(cons(X1,X2)) -> active#(X1) -> active#(tail(X)) -> tail#(active(X))
    Restore Modifier:
     DPs:
      active#(zeros()) -> cons#(0(),zeros())
      active#(cons(X1,X2)) -> active#(X1)
      active#(cons(X1,X2)) -> cons#(active(X1),X2)
      active#(tail(X)) -> active#(X)
      active#(tail(X)) -> tail#(active(X))
      cons#(mark(X1),X2) -> cons#(X1,X2)
      tail#(mark(X)) -> tail#(X)
      proper#(cons(X1,X2)) -> proper#(X2)
      proper#(cons(X1,X2)) -> proper#(X1)
      proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
      proper#(tail(X)) -> proper#(X)
      proper#(tail(X)) -> tail#(proper(X))
      cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
      tail#(ok(X)) -> tail#(X)
      top#(mark(X)) -> proper#(X)
      top#(mark(X)) -> top#(proper(X))
      top#(ok(X)) -> active#(X)
      top#(ok(X)) -> top#(active(X))
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(tail(cons(X,XS))) -> mark(XS)
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(tail(X)) -> tail(active(X))
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      tail(mark(X)) -> mark(tail(X))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(tail(X)) -> tail(proper(X))
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      tail(ok(X)) -> ok(tail(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     SCC Processor:
      #sccs: 5
      #rules: 11
      #arcs: 59/324
      DPs:
       top#(ok(X)) -> top#(active(X))
       top#(mark(X)) -> top#(proper(X))
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
      Open
      
      DPs:
       proper#(tail(X)) -> proper#(X)
       proper#(cons(X1,X2)) -> proper#(X1)
       proper#(cons(X1,X2)) -> proper#(X2)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
      Open
      
      DPs:
       active#(tail(X)) -> active#(X)
       active#(cons(X1,X2)) -> active#(X1)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
      Open
      
      DPs:
       cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
       cons#(mark(X1),X2) -> cons#(X1,X2)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
      Open
      
      DPs:
       tail#(ok(X)) -> tail#(X)
       tail#(mark(X)) -> tail#(X)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
      Open