MAYBE
Time: 4.984081
TRS:
 {   mark f(X1, X2, X3) -> active f(X1, mark X2, X3),
               mark c() -> active c(),
               mark b() -> active b(),
     f(X1, X2, mark 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, active X2, X3) -> f(X1, X2, X3),
     f(mark X1, X2, X3) -> f(X1, X2, X3),
   f(active X1, X2, X3) -> f(X1, X2, X3),
  active f(b(), X, c()) -> mark f(X, c(), X),
             active c() -> mark b()}
 DP:
  DP:
   {   mark# f(X1, X2, X3) -> mark# X2,
       mark# f(X1, X2, X3) -> f#(X1, mark X2, X3),
       mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3),
                 mark# c() -> active# c(),
                 mark# b() -> active# b(),
       f#(X1, X2, mark 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, active X2, X3) -> f#(X1, X2, X3),
       f#(mark X1, X2, X3) -> f#(X1, X2, X3),
     f#(active X1, X2, X3) -> f#(X1, X2, X3),
    active# f(b(), X, c()) -> mark# f(X, c(), X),
    active# f(b(), X, c()) -> f#(X, c(), X),
               active# c() -> mark# b()}
  TRS:
  {   mark f(X1, X2, X3) -> active f(X1, mark X2, X3),
                mark c() -> active c(),
                mark b() -> active b(),
      f(X1, X2, mark 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, active X2, X3) -> f(X1, X2, X3),
      f(mark X1, X2, X3) -> f(X1, X2, X3),
    f(active X1, X2, X3) -> f(X1, X2, X3),
   active f(b(), X, c()) -> mark f(X, c(), X),
              active c() -> mark b()}
  EDG:
   {(active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3))
    (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3))
    (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> mark# X2)
    (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#(mark 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, mark 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, mark 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#(mark 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, mark 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, mark 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#(mark 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, mark 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#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (active# f(b(), X, c()) -> f#(X, c(), X), f#(active X1, X2, X3) -> f#(X1, X2, X3))
    (active# f(b(), X, c()) -> f#(X, c(), X), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, active X3) -> f#(X1, X2, X3))
    (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (mark# c() -> active# c(), active# c() -> mark# b())
    (active# c() -> mark# b(), mark# b() -> active# b())
    (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2)
    (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3))
    (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3))
    (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> active# c())
    (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b())
    (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#(X1, X2, active 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, active 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#(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#(X1, X2, mark 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, 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, active 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, 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, 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#(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, active X2, 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#(active X1, X2, X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3))
    (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X))
    (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> f#(X, c(), X))}
   STATUS:
    arrows: 0.704082
    SCCS (2):
     Scc:
      {   mark# f(X1, X2, X3) -> mark# X2,
          mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3),
       active# f(b(), X, c()) -> mark# f(X, c(), X)}
     Scc:
      {  f#(X1, X2, mark 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, active X2, X3) -> f#(X1, X2, X3),
         f#(mark X1, X2, X3) -> f#(X1, X2, X3),
       f#(active X1, X2, X3) -> f#(X1, X2, X3)}
     
     SCC (3):
      Strict:
       {   mark# f(X1, X2, X3) -> mark# X2,
           mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3),
        active# f(b(), X, c()) -> mark# f(X, c(), X)}
      Weak:
      {   mark f(X1, X2, X3) -> active f(X1, mark X2, X3),
                    mark c() -> active c(),
                    mark b() -> active b(),
          f(X1, X2, mark 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, active X2, X3) -> f(X1, X2, X3),
          f(mark X1, X2, X3) -> f(X1, X2, X3),
        f(active X1, X2, X3) -> f(X1, X2, X3),
       active f(b(), X, c()) -> mark f(X, c(), X),
                  active c() -> mark b()}
      Open
     
     
     
     
     
     SCC (6):
      Strict:
       {  f#(X1, X2, mark 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, active X2, X3) -> f#(X1, X2, X3),
          f#(mark X1, X2, X3) -> f#(X1, X2, X3),
        f#(active X1, X2, X3) -> f#(X1, X2, X3)}
      Weak:
      {   mark f(X1, X2, X3) -> active f(X1, mark X2, X3),
                    mark c() -> active c(),
                    mark b() -> active b(),
          f(X1, X2, mark 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, active X2, X3) -> f(X1, X2, X3),
          f(mark X1, X2, X3) -> f(X1, X2, X3),
        f(active X1, X2, X3) -> f(X1, X2, X3),
       active f(b(), X, c()) -> mark f(X, c(), X),
                  active c() -> mark b()}
      Open