MAYBE

Problem:
 active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
 active(g(b())) -> mark(c())
 active(b()) -> mark(c())
 mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
 mark(g(X)) -> active(g(mark(X)))
 mark(b()) -> active(b())
 mark(c()) -> active(c())
 f(mark(X1),X2,X3) -> f(X1,X2,X3)
 f(X1,mark(X2),X3) -> f(X1,X2,X3)
 f(X1,X2,mark(X3)) -> f(X1,X2,X3)
 f(active(X1),X2,X3) -> f(X1,X2,X3)
 f(X1,active(X2),X3) -> f(X1,X2,X3)
 f(X1,X2,active(X3)) -> f(X1,X2,X3)
 g(mark(X)) -> g(X)
 g(active(X)) -> g(X)

Proof:
 DP Processor:
  DPs:
   active#(f(X,g(X),Y)) -> f#(Y,Y,Y)
   active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y))
   active#(g(b())) -> mark#(c())
   active#(b()) -> mark#(c())
   mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3))
   mark#(g(X)) -> mark#(X)
   mark#(g(X)) -> g#(mark(X))
   mark#(g(X)) -> active#(g(mark(X)))
   mark#(b()) -> active#(b())
   mark#(c()) -> active#(c())
   f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
   f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
   f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
   f#(active(X1),X2,X3) -> f#(X1,X2,X3)
   f#(X1,active(X2),X3) -> f#(X1,X2,X3)
   f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
   g#(mark(X)) -> g#(X)
   g#(active(X)) -> g#(X)
  TRS:
   active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
   active(g(b())) -> mark(c())
   active(b()) -> mark(c())
   mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
   mark(g(X)) -> active(g(mark(X)))
   mark(b()) -> active(b())
   mark(c()) -> active(c())
   f(mark(X1),X2,X3) -> f(X1,X2,X3)
   f(X1,mark(X2),X3) -> f(X1,X2,X3)
   f(X1,X2,mark(X3)) -> f(X1,X2,X3)
   f(active(X1),X2,X3) -> f(X1,X2,X3)
   f(X1,active(X2),X3) -> f(X1,X2,X3)
   f(X1,X2,active(X3)) -> f(X1,X2,X3)
   g(mark(X)) -> g(X)
   g(active(X)) -> g(X)
  EDG Processor:
   DPs:
    active#(f(X,g(X),Y)) -> f#(Y,Y,Y)
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y))
    active#(g(b())) -> mark#(c())
    active#(b()) -> mark#(c())
    mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3))
    mark#(g(X)) -> mark#(X)
    mark#(g(X)) -> g#(mark(X))
    mark#(g(X)) -> active#(g(mark(X)))
    mark#(b()) -> active#(b())
    mark#(c()) -> active#(c())
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    g#(mark(X)) -> g#(X)
    g#(active(X)) -> g#(X)
   TRS:
    active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
    active(g(b())) -> mark(c())
    active(b()) -> mark(c())
    mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
    mark(g(X)) -> active(g(mark(X)))
    mark(b()) -> active(b())
    mark(c()) -> active(c())
    f(mark(X1),X2,X3) -> f(X1,X2,X3)
    f(X1,mark(X2),X3) -> f(X1,X2,X3)
    f(X1,X2,mark(X3)) -> f(X1,X2,X3)
    f(active(X1),X2,X3) -> f(X1,X2,X3)
    f(X1,active(X2),X3) -> f(X1,X2,X3)
    f(X1,X2,active(X3)) -> f(X1,X2,X3)
    g(mark(X)) -> g(X)
    g(active(X)) -> g(X)
   graph:
    g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X)
    g#(mark(X)) -> g#(X) -> g#(active(X)) -> g#(X)
    g#(active(X)) -> g#(X) -> g#(mark(X)) -> g#(X)
    g#(active(X)) -> g#(X) -> g#(active(X)) -> g#(X)
    mark#(b()) -> active#(b()) ->
    active#(b()) -> mark#(c())
    mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) ->
    active#(f(X,g(X),Y)) -> f#(Y,Y,Y)
    mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3)) ->
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y))
    mark#(g(X)) -> g#(mark(X)) -> g#(mark(X)) -> g#(X)
    mark#(g(X)) -> g#(mark(X)) -> g#(active(X)) -> g#(X)
    mark#(g(X)) -> mark#(X) -> mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3))
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X)
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X))
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X)))
    mark#(g(X)) -> mark#(X) -> mark#(b()) -> active#(b())
    mark#(g(X)) -> mark#(X) -> mark#(c()) -> active#(c())
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(f(X,g(X),Y)) -> f#(Y,Y,Y)
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(b())) -> mark#(c())
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(active(X1),X2,X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(mark(X1),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#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(X1,active(X2),X3) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(active(X1),X2,X3) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(X1,active(X2),X3) -> f#(X1,X2,X3)
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3) ->
    f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
    active#(b()) -> mark#(c()) -> mark#(c()) -> active#(c())
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) ->
    mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3))
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) ->
    mark#(g(X)) -> mark#(X)
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) ->
    mark#(g(X)) -> g#(mark(X))
    active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y)) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(g(b())) -> mark#(c()) -> mark#(c()) -> active#(c())
   SCC Processor:
    #sccs: 3
    #rules: 12
    #arcs: 60/324
    DPs:
     f#(mark(X1),X2,X3) -> f#(X1,X2,X3)
     f#(X1,X2,active(X3)) -> f#(X1,X2,X3)
     f#(X1,active(X2),X3) -> f#(X1,X2,X3)
     f#(active(X1),X2,X3) -> f#(X1,X2,X3)
     f#(X1,X2,mark(X3)) -> f#(X1,X2,X3)
     f#(X1,mark(X2),X3) -> f#(X1,X2,X3)
    TRS:
     active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
     active(g(b())) -> mark(c())
     active(b()) -> mark(c())
     mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
     mark(g(X)) -> active(g(mark(X)))
     mark(b()) -> active(b())
     mark(c()) -> active(c())
     f(mark(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,mark(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,mark(X3)) -> f(X1,X2,X3)
     f(active(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,active(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,active(X3)) -> f(X1,X2,X3)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
    Open
    
    DPs:
     mark#(f(X1,X2,X3)) -> active#(f(X1,X2,X3))
     active#(f(X,g(X),Y)) -> mark#(f(Y,Y,Y))
     mark#(g(X)) -> active#(g(mark(X)))
     mark#(g(X)) -> mark#(X)
    TRS:
     active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
     active(g(b())) -> mark(c())
     active(b()) -> mark(c())
     mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
     mark(g(X)) -> active(g(mark(X)))
     mark(b()) -> active(b())
     mark(c()) -> active(c())
     f(mark(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,mark(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,mark(X3)) -> f(X1,X2,X3)
     f(active(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,active(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,active(X3)) -> f(X1,X2,X3)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
    Open
    
    DPs:
     g#(mark(X)) -> g#(X)
     g#(active(X)) -> g#(X)
    TRS:
     active(f(X,g(X),Y)) -> mark(f(Y,Y,Y))
     active(g(b())) -> mark(c())
     active(b()) -> mark(c())
     mark(f(X1,X2,X3)) -> active(f(X1,X2,X3))
     mark(g(X)) -> active(g(mark(X)))
     mark(b()) -> active(b())
     mark(c()) -> active(c())
     f(mark(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,mark(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,mark(X3)) -> f(X1,X2,X3)
     f(active(X1),X2,X3) -> f(X1,X2,X3)
     f(X1,active(X2),X3) -> f(X1,X2,X3)
     f(X1,X2,active(X3)) -> f(X1,X2,X3)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
    Open