MAYBE

Problem:
 active(f(b(),c(),x)) -> mark(f(x,x,x))
 active(f(x,y,z)) -> f(x,y,active(z))
 active(d()) -> m(b())
 f(x,y,mark(z)) -> mark(f(x,y,z))
 active(d()) -> mark(c())
 proper(b()) -> ok(b())
 proper(c()) -> ok(c())
 proper(d()) -> ok(d())
 proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
 f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
 top(mark(x)) -> top(proper(x))
 top(ok(x)) -> top(active(x))

Proof:
 DP Processor:
  DPs:
   active#(f(b(),c(),x)) -> f#(x,x,x)
   active#(f(x,y,z)) -> active#(z)
   active#(f(x,y,z)) -> f#(x,y,active(z))
   f#(x,y,mark(z)) -> f#(x,y,z)
   proper#(f(x,y,z)) -> proper#(z)
   proper#(f(x,y,z)) -> proper#(y)
   proper#(f(x,y,z)) -> proper#(x)
   proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
   f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
   top#(mark(x)) -> proper#(x)
   top#(mark(x)) -> top#(proper(x))
   top#(ok(x)) -> active#(x)
   top#(ok(x)) -> top#(active(x))
  TRS:
   active(f(b(),c(),x)) -> mark(f(x,x,x))
   active(f(x,y,z)) -> f(x,y,active(z))
   active(d()) -> m(b())
   f(x,y,mark(z)) -> mark(f(x,y,z))
   active(d()) -> mark(c())
   proper(b()) -> ok(b())
   proper(c()) -> ok(c())
   proper(d()) -> ok(d())
   proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
   f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
   top(mark(x)) -> top(proper(x))
   top(ok(x)) -> top(active(x))
  TDG Processor:
   DPs:
    active#(f(b(),c(),x)) -> f#(x,x,x)
    active#(f(x,y,z)) -> active#(z)
    active#(f(x,y,z)) -> f#(x,y,active(z))
    f#(x,y,mark(z)) -> f#(x,y,z)
    proper#(f(x,y,z)) -> proper#(z)
    proper#(f(x,y,z)) -> proper#(y)
    proper#(f(x,y,z)) -> proper#(x)
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    top#(mark(x)) -> proper#(x)
    top#(mark(x)) -> top#(proper(x))
    top#(ok(x)) -> active#(x)
    top#(ok(x)) -> top#(active(x))
   TRS:
    active(f(b(),c(),x)) -> mark(f(x,x,x))
    active(f(x,y,z)) -> f(x,y,active(z))
    active(d()) -> m(b())
    f(x,y,mark(z)) -> mark(f(x,y,z))
    active(d()) -> mark(c())
    proper(b()) -> ok(b())
    proper(c()) -> ok(c())
    proper(d()) -> ok(d())
    proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
    f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
    top(mark(x)) -> top(proper(x))
    top(ok(x)) -> top(active(x))
   graph:
    top#(ok(x)) -> top#(active(x)) -> top#(ok(x)) -> top#(active(x))
    top#(ok(x)) -> top#(active(x)) -> top#(ok(x)) -> active#(x)
    top#(ok(x)) -> top#(active(x)) ->
    top#(mark(x)) -> top#(proper(x))
    top#(ok(x)) -> top#(active(x)) -> top#(mark(x)) -> proper#(x)
    top#(ok(x)) -> active#(x) -> active#(f(x,y,z)) -> f#(x,y,active(z))
    top#(ok(x)) -> active#(x) -> active#(f(x,y,z)) -> active#(z)
    top#(ok(x)) -> active#(x) -> active#(f(b(),c(),x)) -> f#(x,x,x)
    top#(mark(x)) -> top#(proper(x)) ->
    top#(ok(x)) -> top#(active(x))
    top#(mark(x)) -> top#(proper(x)) -> top#(ok(x)) -> active#(x)
    top#(mark(x)) -> top#(proper(x)) ->
    top#(mark(x)) -> top#(proper(x))
    top#(mark(x)) -> top#(proper(x)) -> top#(mark(x)) -> proper#(x)
    top#(mark(x)) -> proper#(x) ->
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
    top#(mark(x)) -> proper#(x) -> proper#(f(x,y,z)) -> proper#(x)
    top#(mark(x)) -> proper#(x) -> proper#(f(x,y,z)) -> proper#(y)
    top#(mark(x)) -> proper#(x) -> proper#(f(x,y,z)) -> proper#(z)
    proper#(f(x,y,z)) -> proper#(z) ->
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
    proper#(f(x,y,z)) -> proper#(z) ->
    proper#(f(x,y,z)) -> proper#(x)
    proper#(f(x,y,z)) -> proper#(z) ->
    proper#(f(x,y,z)) -> proper#(y)
    proper#(f(x,y,z)) -> proper#(z) ->
    proper#(f(x,y,z)) -> proper#(z)
    proper#(f(x,y,z)) -> proper#(y) ->
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
    proper#(f(x,y,z)) -> proper#(y) ->
    proper#(f(x,y,z)) -> proper#(x)
    proper#(f(x,y,z)) -> proper#(y) ->
    proper#(f(x,y,z)) -> proper#(y)
    proper#(f(x,y,z)) -> proper#(y) ->
    proper#(f(x,y,z)) -> proper#(z)
    proper#(f(x,y,z)) -> proper#(x) ->
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z))
    proper#(f(x,y,z)) -> proper#(x) ->
    proper#(f(x,y,z)) -> proper#(x)
    proper#(f(x,y,z)) -> proper#(x) ->
    proper#(f(x,y,z)) -> proper#(y)
    proper#(f(x,y,z)) -> proper#(x) ->
    proper#(f(x,y,z)) -> proper#(z)
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z)) ->
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    proper#(f(x,y,z)) -> f#(proper(x),proper(y),proper(z)) ->
    f#(x,y,mark(z)) -> f#(x,y,z)
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z) ->
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z) -> f#(x,y,mark(z)) -> f#(x,y,z)
    f#(x,y,mark(z)) -> f#(x,y,z) -> f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    f#(x,y,mark(z)) -> f#(x,y,z) -> f#(x,y,mark(z)) -> f#(x,y,z)
    active#(f(b(),c(),x)) -> f#(x,x,x) ->
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    active#(f(b(),c(),x)) -> f#(x,x,x) ->
    f#(x,y,mark(z)) -> f#(x,y,z)
    active#(f(x,y,z)) -> f#(x,y,active(z)) ->
    f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    active#(f(x,y,z)) -> f#(x,y,active(z)) ->
    f#(x,y,mark(z)) -> f#(x,y,z)
    active#(f(x,y,z)) -> active#(z) ->
    active#(f(x,y,z)) -> f#(x,y,active(z))
    active#(f(x,y,z)) -> active#(z) ->
    active#(f(x,y,z)) -> active#(z)
    active#(f(x,y,z)) -> active#(z) -> active#(f(b(),c(),x)) -> f#(x,x,x)
   SCC Processor:
    #sccs: 4
    #rules: 8
    #arcs: 40/169
    DPs:
     top#(ok(x)) -> top#(active(x))
     top#(mark(x)) -> top#(proper(x))
    TRS:
     active(f(b(),c(),x)) -> mark(f(x,x,x))
     active(f(x,y,z)) -> f(x,y,active(z))
     active(d()) -> m(b())
     f(x,y,mark(z)) -> mark(f(x,y,z))
     active(d()) -> mark(c())
     proper(b()) -> ok(b())
     proper(c()) -> ok(c())
     proper(d()) -> ok(d())
     proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
     f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
     top(mark(x)) -> top(proper(x))
     top(ok(x)) -> top(active(x))
    Open
    
    DPs:
     active#(f(x,y,z)) -> active#(z)
    TRS:
     active(f(b(),c(),x)) -> mark(f(x,x,x))
     active(f(x,y,z)) -> f(x,y,active(z))
     active(d()) -> m(b())
     f(x,y,mark(z)) -> mark(f(x,y,z))
     active(d()) -> mark(c())
     proper(b()) -> ok(b())
     proper(c()) -> ok(c())
     proper(d()) -> ok(d())
     proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
     f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
     top(mark(x)) -> top(proper(x))
     top(ok(x)) -> top(active(x))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     problem:
      DPs:
       
      TRS:
       active(f(b(),c(),x)) -> mark(f(x,x,x))
       active(f(x,y,z)) -> f(x,y,active(z))
       active(d()) -> m(b())
       f(x,y,mark(z)) -> mark(f(x,y,z))
       active(d()) -> mark(c())
       proper(b()) -> ok(b())
       proper(c()) -> ok(c())
       proper(d()) -> ok(d())
       proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
       f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
       top(mark(x)) -> top(proper(x))
       top(ok(x)) -> top(active(x))
     Qed
    
    DPs:
     proper#(f(x,y,z)) -> proper#(z)
     proper#(f(x,y,z)) -> proper#(y)
     proper#(f(x,y,z)) -> proper#(x)
    TRS:
     active(f(b(),c(),x)) -> mark(f(x,x,x))
     active(f(x,y,z)) -> f(x,y,active(z))
     active(d()) -> m(b())
     f(x,y,mark(z)) -> mark(f(x,y,z))
     active(d()) -> mark(c())
     proper(b()) -> ok(b())
     proper(c()) -> ok(c())
     proper(d()) -> ok(d())
     proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
     f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
     top(mark(x)) -> top(proper(x))
     top(ok(x)) -> top(active(x))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     problem:
      DPs:
       
      TRS:
       active(f(b(),c(),x)) -> mark(f(x,x,x))
       active(f(x,y,z)) -> f(x,y,active(z))
       active(d()) -> m(b())
       f(x,y,mark(z)) -> mark(f(x,y,z))
       active(d()) -> mark(c())
       proper(b()) -> ok(b())
       proper(c()) -> ok(c())
       proper(d()) -> ok(d())
       proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
       f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
       top(mark(x)) -> top(proper(x))
       top(ok(x)) -> top(active(x))
     Qed
    
    DPs:
     f#(x,y,mark(z)) -> f#(x,y,z)
     f#(ok(x),ok(y),ok(z)) -> f#(x,y,z)
    TRS:
     active(f(b(),c(),x)) -> mark(f(x,x,x))
     active(f(x,y,z)) -> f(x,y,active(z))
     active(d()) -> m(b())
     f(x,y,mark(z)) -> mark(f(x,y,z))
     active(d()) -> mark(c())
     proper(b()) -> ok(b())
     proper(c()) -> ok(c())
     proper(d()) -> ok(d())
     proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
     f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
     top(mark(x)) -> top(proper(x))
     top(ok(x)) -> top(active(x))
    Subterm Criterion Processor:
     simple projection:
      pi(f#) = 2
     problem:
      DPs:
       
      TRS:
       active(f(b(),c(),x)) -> mark(f(x,x,x))
       active(f(x,y,z)) -> f(x,y,active(z))
       active(d()) -> m(b())
       f(x,y,mark(z)) -> mark(f(x,y,z))
       active(d()) -> mark(c())
       proper(b()) -> ok(b())
       proper(c()) -> ok(c())
       proper(d()) -> ok(d())
       proper(f(x,y,z)) -> f(proper(x),proper(y),proper(z))
       f(ok(x),ok(y),ok(z)) -> ok(f(x,y,z))
       top(mark(x)) -> top(proper(x))
       top(ok(x)) -> top(active(x))
     Qed