MAYBE

Problem:
 active(f(a(),X,X)) -> mark(f(X,b(),b()))
 active(b()) -> mark(a())
 active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
 proper(a()) -> ok(a())
 proper(b()) -> ok(b())
 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(f(a(),X,X)) -> f#(X,b(),b())
   active#(f(X1,X2,X3)) -> active#(X2)
   active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
   f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
   proper#(f(X1,X2,X3)) -> proper#(X3)
   proper#(f(X1,X2,X3)) -> proper#(X2)
   proper#(f(X1,X2,X3)) -> proper#(X1)
   proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
   f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
   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(a(),X,X)) -> mark(f(X,b(),b()))
   active(b()) -> mark(a())
   active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
   f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
   proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
   proper(a()) -> ok(a())
   proper(b()) -> ok(b())
   f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  TDG Processor:
   DPs:
    active#(f(a(),X,X)) -> f#(X,b(),b())
    active#(f(X1,X2,X3)) -> active#(X2)
    active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    proper#(f(X1,X2,X3)) -> proper#(X3)
    proper#(f(X1,X2,X3)) -> proper#(X2)
    proper#(f(X1,X2,X3)) -> proper#(X1)
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    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(a(),X,X)) -> mark(f(X,b(),b()))
    active(b()) -> mark(a())
    active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
    f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
    proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
    proper(a()) -> ok(a())
    proper(b()) -> ok(b())
    f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
    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(X1,X2,X3)) -> f#(X1,active(X2),X3)
    top#(ok(X)) -> active#(X) -> active#(f(X1,X2,X3)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(f(a(),X,X)) -> f#(X,b(),b())
    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(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
    top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2,X3)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2,X3)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(f(X1,X2,X3)) -> proper#(X3)
    proper#(f(X1,X2,X3)) -> proper#(X3) ->
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
    proper#(f(X1,X2,X3)) -> proper#(X3) ->
    proper#(f(X1,X2,X3)) -> proper#(X1)
    proper#(f(X1,X2,X3)) -> proper#(X3) ->
    proper#(f(X1,X2,X3)) -> proper#(X2)
    proper#(f(X1,X2,X3)) -> proper#(X3) ->
    proper#(f(X1,X2,X3)) -> proper#(X3)
    proper#(f(X1,X2,X3)) -> proper#(X2) ->
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
    proper#(f(X1,X2,X3)) -> proper#(X2) ->
    proper#(f(X1,X2,X3)) -> proper#(X1)
    proper#(f(X1,X2,X3)) -> proper#(X2) ->
    proper#(f(X1,X2,X3)) -> proper#(X2)
    proper#(f(X1,X2,X3)) -> proper#(X2) ->
    proper#(f(X1,X2,X3)) -> proper#(X3)
    proper#(f(X1,X2,X3)) -> proper#(X1) ->
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
    proper#(f(X1,X2,X3)) -> proper#(X1) ->
    proper#(f(X1,X2,X3)) -> proper#(X1)
    proper#(f(X1,X2,X3)) -> proper#(X1) ->
    proper#(f(X1,X2,X3)) -> proper#(X2)
    proper#(f(X1,X2,X3)) -> proper#(X1) ->
    proper#(f(X1,X2,X3)) -> proper#(X3)
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) ->
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3) ->
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    active#(f(a(),X,X)) -> f#(X,b(),b()) ->
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    active#(f(a(),X,X)) -> f#(X,b(),b()) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) ->
    f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
    active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    active#(f(X1,X2,X3)) -> active#(X2) ->
    active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
    active#(f(X1,X2,X3)) -> active#(X2) ->
    active#(f(X1,X2,X3)) -> active#(X2)
    active#(f(X1,X2,X3)) -> active#(X2) -> active#(f(a(),X,X)) -> f#(X,b(),b())
   EDG Processor:
    DPs:
     active#(f(a(),X,X)) -> f#(X,b(),b())
     active#(f(X1,X2,X3)) -> active#(X2)
     active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     proper#(f(X1,X2,X3)) -> proper#(X3)
     proper#(f(X1,X2,X3)) -> proper#(X2)
     proper#(f(X1,X2,X3)) -> proper#(X1)
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
     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(a(),X,X)) -> mark(f(X,b(),b()))
     active(b()) -> mark(a())
     active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
     f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
     proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
     proper(a()) -> ok(a())
     proper(b()) -> ok(b())
     f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(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#(f(a(),X,X)) -> f#(X,b(),b())
     top#(ok(X)) -> active#(X) -> active#(f(X1,X2,X3)) -> active#(X2)
     top#(ok(X)) -> active#(X) ->
     active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
     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#(f(X1,X2,X3)) -> proper#(X3)
     top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2,X3)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2,X3)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) ->
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
     proper#(f(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X1,X2,X3)) -> proper#(X3)
     proper#(f(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X1,X2,X3)) -> proper#(X2)
     proper#(f(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X1,X2,X3)) -> proper#(X1)
     proper#(f(X1,X2,X3)) -> proper#(X3) ->
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
     proper#(f(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X1,X2,X3)) -> proper#(X3)
     proper#(f(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X1,X2,X3)) -> proper#(X2)
     proper#(f(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X1,X2,X3)) -> proper#(X1)
     proper#(f(X1,X2,X3)) -> proper#(X2) ->
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
     proper#(f(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X1,X2,X3)) -> proper#(X3)
     proper#(f(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X1,X2,X3)) -> proper#(X2)
     proper#(f(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X1,X2,X3)) -> proper#(X1)
     proper#(f(X1,X2,X3)) -> proper#(X1) ->
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3))
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) ->
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) ->
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3) ->
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3) ->
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
     active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) ->
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) ->
     f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
     active#(f(X1,X2,X3)) -> active#(X2) ->
     active#(f(a(),X,X)) -> f#(X,b(),b())
     active#(f(X1,X2,X3)) -> active#(X2) ->
     active#(f(X1,X2,X3)) -> active#(X2)
     active#(f(X1,X2,X3)) -> active#(X2) -> active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3)
    SCC Processor:
     #sccs: 4
     #rules: 8
     #arcs: 38/169
     DPs:
      top#(ok(X)) -> top#(active(X))
      top#(mark(X)) -> top#(proper(X))
     TRS:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      proper#(f(X1,X2,X3)) -> proper#(X1)
      proper#(f(X1,X2,X3)) -> proper#(X2)
      proper#(f(X1,X2,X3)) -> proper#(X3)
     TRS:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      active#(f(X1,X2,X3)) -> active#(X2)
     TRS:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      f#(ok(X1),ok(X2),ok(X3)) -> f#(X1,X2,X3)
      f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
     TRS:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open