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