MAYBE

Problem:
 active(f(x)) -> mark(x)
 top(active(c())) -> top(mark(c()))
 top(mark(x)) -> top(check(x))
 check(f(x)) -> f(check(x))
 check(x) -> start(match(f(X()),x))
 match(f(x),f(y)) -> f(match(x,y))
 match(X(),x) -> proper(x)
 proper(c()) -> ok(c())
 proper(f(x)) -> f(proper(x))
 f(ok(x)) -> ok(f(x))
 start(ok(x)) -> found(x)
 f(found(x)) -> found(f(x))
 top(found(x)) -> top(active(x))
 active(f(x)) -> f(active(x))
 f(mark(x)) -> mark(f(x))

Proof:
 DP Processor:
  DPs:
   top#(active(c())) -> top#(mark(c()))
   top#(mark(x)) -> check#(x)
   top#(mark(x)) -> top#(check(x))
   check#(f(x)) -> check#(x)
   check#(f(x)) -> f#(check(x))
   check#(x) -> f#(X())
   check#(x) -> match#(f(X()),x)
   check#(x) -> start#(match(f(X()),x))
   match#(f(x),f(y)) -> match#(x,y)
   match#(f(x),f(y)) -> f#(match(x,y))
   match#(X(),x) -> proper#(x)
   proper#(f(x)) -> proper#(x)
   proper#(f(x)) -> f#(proper(x))
   f#(ok(x)) -> f#(x)
   f#(found(x)) -> f#(x)
   top#(found(x)) -> active#(x)
   top#(found(x)) -> top#(active(x))
   active#(f(x)) -> active#(x)
   active#(f(x)) -> f#(active(x))
   f#(mark(x)) -> f#(x)
  TRS:
   active(f(x)) -> mark(x)
   top(active(c())) -> top(mark(c()))
   top(mark(x)) -> top(check(x))
   check(f(x)) -> f(check(x))
   check(x) -> start(match(f(X()),x))
   match(f(x),f(y)) -> f(match(x,y))
   match(X(),x) -> proper(x)
   proper(c()) -> ok(c())
   proper(f(x)) -> f(proper(x))
   f(ok(x)) -> ok(f(x))
   start(ok(x)) -> found(x)
   f(found(x)) -> found(f(x))
   top(found(x)) -> top(active(x))
   active(f(x)) -> f(active(x))
   f(mark(x)) -> mark(f(x))
  Usable Rule Processor:
   DPs:
    top#(active(c())) -> top#(mark(c()))
    top#(mark(x)) -> check#(x)
    top#(mark(x)) -> top#(check(x))
    check#(f(x)) -> check#(x)
    check#(f(x)) -> f#(check(x))
    check#(x) -> f#(X())
    check#(x) -> match#(f(X()),x)
    check#(x) -> start#(match(f(X()),x))
    match#(f(x),f(y)) -> match#(x,y)
    match#(f(x),f(y)) -> f#(match(x,y))
    match#(X(),x) -> proper#(x)
    proper#(f(x)) -> proper#(x)
    proper#(f(x)) -> f#(proper(x))
    f#(ok(x)) -> f#(x)
    f#(found(x)) -> f#(x)
    top#(found(x)) -> active#(x)
    top#(found(x)) -> top#(active(x))
    active#(f(x)) -> active#(x)
    active#(f(x)) -> f#(active(x))
    f#(mark(x)) -> f#(x)
   TRS:
    check(f(x)) -> f(check(x))
    check(x) -> start(match(f(X()),x))
    f(ok(x)) -> ok(f(x))
    f(found(x)) -> found(f(x))
    f(mark(x)) -> mark(f(x))
    start(ok(x)) -> found(x)
    match(f(x),f(y)) -> f(match(x,y))
    match(X(),x) -> proper(x)
    proper(c()) -> ok(c())
    proper(f(x)) -> f(proper(x))
    active(f(x)) -> mark(x)
    active(f(x)) -> f(active(x))
   EDG Processor:
    DPs:
     top#(active(c())) -> top#(mark(c()))
     top#(mark(x)) -> check#(x)
     top#(mark(x)) -> top#(check(x))
     check#(f(x)) -> check#(x)
     check#(f(x)) -> f#(check(x))
     check#(x) -> f#(X())
     check#(x) -> match#(f(X()),x)
     check#(x) -> start#(match(f(X()),x))
     match#(f(x),f(y)) -> match#(x,y)
     match#(f(x),f(y)) -> f#(match(x,y))
     match#(X(),x) -> proper#(x)
     proper#(f(x)) -> proper#(x)
     proper#(f(x)) -> f#(proper(x))
     f#(ok(x)) -> f#(x)
     f#(found(x)) -> f#(x)
     top#(found(x)) -> active#(x)
     top#(found(x)) -> top#(active(x))
     active#(f(x)) -> active#(x)
     active#(f(x)) -> f#(active(x))
     f#(mark(x)) -> f#(x)
    TRS:
     check(f(x)) -> f(check(x))
     check(x) -> start(match(f(X()),x))
     f(ok(x)) -> ok(f(x))
     f(found(x)) -> found(f(x))
     f(mark(x)) -> mark(f(x))
     start(ok(x)) -> found(x)
     match(f(x),f(y)) -> f(match(x,y))
     match(X(),x) -> proper(x)
     proper(c()) -> ok(c())
     proper(f(x)) -> f(proper(x))
     active(f(x)) -> mark(x)
     active(f(x)) -> f(active(x))
    graph:
     proper#(f(x)) -> proper#(x) -> proper#(f(x)) -> proper#(x)
     proper#(f(x)) -> proper#(x) -> proper#(f(x)) -> f#(proper(x))
     proper#(f(x)) -> f#(proper(x)) -> f#(ok(x)) -> f#(x)
     proper#(f(x)) -> f#(proper(x)) -> f#(found(x)) -> f#(x)
     proper#(f(x)) -> f#(proper(x)) -> f#(mark(x)) -> f#(x)
     match#(X(),x) -> proper#(x) -> proper#(f(x)) -> proper#(x)
     match#(X(),x) -> proper#(x) -> proper#(f(x)) -> f#(proper(x))
     match#(f(x),f(y)) -> match#(x,y) ->
     match#(f(x),f(y)) -> match#(x,y)
     match#(f(x),f(y)) -> match#(x,y) ->
     match#(f(x),f(y)) -> f#(match(x,y))
     match#(f(x),f(y)) -> match#(x,y) ->
     match#(X(),x) -> proper#(x)
     match#(f(x),f(y)) -> f#(match(x,y)) -> f#(ok(x)) -> f#(x)
     match#(f(x),f(y)) -> f#(match(x,y)) ->
     f#(found(x)) -> f#(x)
     match#(f(x),f(y)) -> f#(match(x,y)) -> f#(mark(x)) -> f#(x)
     f#(found(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
     f#(found(x)) -> f#(x) -> f#(found(x)) -> f#(x)
     f#(found(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
     f#(ok(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
     f#(ok(x)) -> f#(x) -> f#(found(x)) -> f#(x)
     f#(ok(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
     f#(mark(x)) -> f#(x) -> f#(ok(x)) -> f#(x)
     f#(mark(x)) -> f#(x) -> f#(found(x)) -> f#(x)
     f#(mark(x)) -> f#(x) -> f#(mark(x)) -> f#(x)
     check#(f(x)) -> f#(check(x)) -> f#(ok(x)) -> f#(x)
     check#(f(x)) -> f#(check(x)) -> f#(found(x)) -> f#(x)
     check#(f(x)) -> f#(check(x)) -> f#(mark(x)) -> f#(x)
     check#(f(x)) -> check#(x) -> check#(f(x)) -> check#(x)
     check#(f(x)) -> check#(x) -> check#(f(x)) -> f#(check(x))
     check#(f(x)) -> check#(x) -> check#(x) -> f#(X())
     check#(f(x)) -> check#(x) -> check#(x) -> match#(f(X()),x)
     check#(f(x)) -> check#(x) -> check#(x) -> start#(match(f(X()),x))
     check#(x) -> match#(f(X()),x) -> match#(f(x),f(y)) -> match#(x,y)
     check#(x) -> match#(f(X()),x) ->
     match#(f(x),f(y)) -> f#(match(x,y))
     top#(found(x)) -> top#(active(x)) ->
     top#(active(c())) -> top#(mark(c()))
     top#(found(x)) -> top#(active(x)) ->
     top#(mark(x)) -> check#(x)
     top#(found(x)) -> top#(active(x)) ->
     top#(mark(x)) -> top#(check(x))
     top#(found(x)) -> top#(active(x)) ->
     top#(found(x)) -> active#(x)
     top#(found(x)) -> top#(active(x)) ->
     top#(found(x)) -> top#(active(x))
     top#(found(x)) -> active#(x) -> active#(f(x)) -> active#(x)
     top#(found(x)) -> active#(x) -> active#(f(x)) -> f#(active(x))
     top#(mark(x)) -> check#(x) -> check#(f(x)) -> check#(x)
     top#(mark(x)) -> check#(x) -> check#(f(x)) -> f#(check(x))
     top#(mark(x)) -> check#(x) -> check#(x) -> f#(X())
     top#(mark(x)) -> check#(x) -> check#(x) -> match#(f(X()),x)
     top#(mark(x)) -> check#(x) ->
     check#(x) -> start#(match(f(X()),x))
     top#(mark(x)) -> top#(check(x)) -> top#(mark(x)) -> check#(x)
     top#(mark(x)) -> top#(check(x)) ->
     top#(mark(x)) -> top#(check(x))
     top#(mark(x)) -> top#(check(x)) -> top#(found(x)) -> active#(x)
     top#(mark(x)) -> top#(check(x)) ->
     top#(found(x)) -> top#(active(x))
     top#(active(c())) -> top#(mark(c())) ->
     top#(mark(x)) -> check#(x)
     top#(active(c())) -> top#(mark(c())) ->
     top#(mark(x)) -> top#(check(x))
     active#(f(x)) -> f#(active(x)) -> f#(ok(x)) -> f#(x)
     active#(f(x)) -> f#(active(x)) -> f#(found(x)) -> f#(x)
     active#(f(x)) -> f#(active(x)) -> f#(mark(x)) -> f#(x)
     active#(f(x)) -> active#(x) -> active#(f(x)) -> active#(x)
     active#(f(x)) -> active#(x) -> active#(f(x)) -> f#(active(x))
    Restore Modifier:
     DPs:
      top#(active(c())) -> top#(mark(c()))
      top#(mark(x)) -> check#(x)
      top#(mark(x)) -> top#(check(x))
      check#(f(x)) -> check#(x)
      check#(f(x)) -> f#(check(x))
      check#(x) -> f#(X())
      check#(x) -> match#(f(X()),x)
      check#(x) -> start#(match(f(X()),x))
      match#(f(x),f(y)) -> match#(x,y)
      match#(f(x),f(y)) -> f#(match(x,y))
      match#(X(),x) -> proper#(x)
      proper#(f(x)) -> proper#(x)
      proper#(f(x)) -> f#(proper(x))
      f#(ok(x)) -> f#(x)
      f#(found(x)) -> f#(x)
      top#(found(x)) -> active#(x)
      top#(found(x)) -> top#(active(x))
      active#(f(x)) -> active#(x)
      active#(f(x)) -> f#(active(x))
      f#(mark(x)) -> f#(x)
     TRS:
      active(f(x)) -> mark(x)
      top(active(c())) -> top(mark(c()))
      top(mark(x)) -> top(check(x))
      check(f(x)) -> f(check(x))
      check(x) -> start(match(f(X()),x))
      match(f(x),f(y)) -> f(match(x,y))
      match(X(),x) -> proper(x)
      proper(c()) -> ok(c())
      proper(f(x)) -> f(proper(x))
      f(ok(x)) -> ok(f(x))
      start(ok(x)) -> found(x)
      f(found(x)) -> found(f(x))
      top(found(x)) -> top(active(x))
      active(f(x)) -> f(active(x))
      f(mark(x)) -> mark(f(x))
     SCC Processor:
      #sccs: 6
      #rules: 10
      #arcs: 55/400
      DPs:
       top#(found(x)) -> top#(active(x))
       top#(mark(x)) -> top#(check(x))
       top#(active(c())) -> top#(mark(c()))
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open
      
      DPs:
       active#(f(x)) -> active#(x)
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open
      
      DPs:
       check#(f(x)) -> check#(x)
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open
      
      DPs:
       match#(f(x),f(y)) -> match#(x,y)
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open
      
      DPs:
       proper#(f(x)) -> proper#(x)
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open
      
      DPs:
       f#(mark(x)) -> f#(x)
       f#(found(x)) -> f#(x)
       f#(ok(x)) -> f#(x)
      TRS:
       active(f(x)) -> mark(x)
       top(active(c())) -> top(mark(c()))
       top(mark(x)) -> top(check(x))
       check(f(x)) -> f(check(x))
       check(x) -> start(match(f(X()),x))
       match(f(x),f(y)) -> f(match(x,y))
       match(X(),x) -> proper(x)
       proper(c()) -> ok(c())
       proper(f(x)) -> f(proper(x))
       f(ok(x)) -> ok(f(x))
       start(ok(x)) -> found(x)
       f(found(x)) -> found(f(x))
       top(found(x)) -> top(active(x))
       active(f(x)) -> f(active(x))
       f(mark(x)) -> mark(f(x))
      Open