MAYBE
Time: 0.007410
TRS:
 {   mark f(X1, X2, X3) -> active f(mark 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# X1,
       mark# f(X1, X2, X3) -> mark# X3,
       mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3),
       mark# f(X1, X2, X3) -> active# f(mark 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(mark 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()}
  UR:
   {   mark f(X1, X2, X3) -> active f(mark 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(),
                  d(x, y) -> x,
                  d(x, y) -> y}
   EDG:
    {(mark# a() -> active# a(), active# c() -> mark# b())
     (mark# a() -> active# a(), active# c() -> mark# a())
     (mark# a() -> active# a(), active# f(a(), b(), X) -> f#(X, X, X))
     (mark# a() -> active# a(), active# f(a(), b(), X) -> mark# f(X, X, X))
     (mark# c() -> active# c(), active# c() -> mark# b())
     (mark# c() -> active# c(), active# c() -> mark# a())
     (mark# c() -> active# c(), active# f(a(), b(), X) -> f#(X, X, X))
     (mark# c() -> active# c(), active# f(a(), b(), X) -> mark# f(X, X, X))
     (active# c() -> mark# b(), mark# c() -> active# c())
     (active# c() -> mark# b(), mark# b() -> active# b())
     (active# c() -> mark# b(), mark# a() -> active# a())
     (active# c() -> mark# b(), mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3))
     (active# c() -> mark# b(), mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3))
     (active# c() -> mark# b(), mark# f(X1, X2, X3) -> mark# X3)
     (active# c() -> mark# b(), mark# f(X1, X2, X3) -> mark# X1)
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(active X1, X2, X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(X1, active X2, X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(X1, X2, active X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> mark# f(X, X, X), mark# c() -> active# c())
     (active# f(a(), b(), X) -> mark# f(X, X, X), mark# b() -> active# b())
     (active# f(a(), b(), X) -> mark# f(X, X, X), mark# a() -> active# a())
     (active# f(a(), b(), X) -> mark# f(X, X, X), mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3))
     (active# f(a(), b(), X) -> mark# f(X, X, X), mark# f(X1, X2, X3) -> f#(mark X1, X2, mark 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) -> mark# X1)
     (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))
     (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) -> f#(X, X, X), f#(X1, X2, mark X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, X2, active X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, mark X2, X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(X1, active X2, X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(mark X1, X2, X3) -> f#(X1, X2, X3))
     (active# f(a(), b(), X) -> f#(X, X, X), f#(active X1, X2, X3) -> f#(X1, X2, X3))
     (mark# f(X1, X2, X3) -> mark# X1, mark# f(X1, X2, X3) -> mark# X1)
     (mark# f(X1, X2, X3) -> mark# X1, mark# f(X1, X2, X3) -> mark# X3)
     (mark# f(X1, X2, X3) -> mark# X1, mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3))
     (mark# f(X1, X2, X3) -> mark# X1, mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3))
     (mark# f(X1, X2, X3) -> mark# X1, mark# a() -> active# a())
     (mark# f(X1, X2, X3) -> mark# X1, mark# b() -> active# b())
     (mark# f(X1, X2, X3) -> mark# X1, mark# c() -> active# c())
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> mark# X1)
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> mark# X3)
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3))
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3))
     (mark# f(X1, X2, X3) -> mark# X3, mark# a() -> active# a())
     (mark# f(X1, X2, X3) -> mark# X3, mark# b() -> active# b())
     (mark# f(X1, X2, X3) -> mark# X3, mark# c() -> active# c())
     (active# c() -> mark# a(), mark# f(X1, X2, X3) -> mark# X1)
     (active# c() -> mark# a(), mark# f(X1, X2, X3) -> mark# X3)
     (active# c() -> mark# a(), mark# f(X1, X2, X3) -> f#(mark X1, X2, mark X3))
     (active# c() -> mark# a(), mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3))
     (active# c() -> mark# a(), mark# a() -> active# a())
     (active# c() -> mark# a(), mark# b() -> active# b())
     (active# c() -> mark# a(), mark# c() -> active# c())
     (mark# b() -> active# b(), active# f(a(), b(), X) -> mark# f(X, X, X))
     (mark# b() -> active# b(), active# f(a(), b(), X) -> f#(X, X, X))
     (mark# b() -> active# b(), active# c() -> mark# a())
     (mark# b() -> active# b(), active# c() -> mark# b())
     (mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3), active# f(a(), b(), X) -> mark# f(X, X, X))
     (mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3), active# f(a(), b(), X) -> f#(X, X, X))
     (mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3), active# c() -> mark# a())
     (mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3), active# c() -> mark# b())}
    STATUS:
     arrows: 0.657439
     SCCS (2):
      Scc:
       {   mark# f(X1, X2, X3) -> mark# X1,
           mark# f(X1, X2, X3) -> mark# X3,
           mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3),
                     mark# a() -> active# a(),
                     mark# b() -> active# b(),
                     mark# c() -> active# c(),
        active# f(a(), b(), X) -> mark# f(X, X, X),
                   active# c() -> mark# a(),
                   active# c() -> mark# b()}
      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 (9):
       Strict:
        {   mark# f(X1, X2, X3) -> mark# X1,
            mark# f(X1, X2, X3) -> mark# X3,
            mark# f(X1, X2, X3) -> active# f(mark X1, X2, mark X3),
                      mark# a() -> active# a(),
                      mark# b() -> active# b(),
                      mark# c() -> active# c(),
         active# f(a(), b(), X) -> mark# f(X, X, X),
                    active# c() -> mark# a(),
                    active# c() -> mark# b()}
       Weak:
       {   mark f(X1, X2, X3) -> active f(mark 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(mark 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