MAYBE
Time: 0.002353
TRS:
 {  a__f(X1, X2, X3) -> f(X1, X2, X3),
   a__f(a(), b(), X) -> a__f(mark X, X, mark X),
            mark a() -> a(),
            mark b() -> b(),
  mark f(X1, X2, X3) -> a__f(mark X1, X2, mark X3),
            mark c() -> a__c(),
              a__c() -> a(),
              a__c() -> b(),
              a__c() -> c()}
 DP:
  DP:
   { a__f#(a(), b(), X) -> a__f#(mark X, X, mark X),
     a__f#(a(), b(), X) -> mark# X,
    mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3),
    mark# f(X1, X2, X3) -> mark# X1,
    mark# f(X1, X2, X3) -> mark# X3,
              mark# c() -> a__c#()}
  TRS:
  {  a__f(X1, X2, X3) -> f(X1, X2, X3),
    a__f(a(), b(), X) -> a__f(mark X, X, mark X),
             mark a() -> a(),
             mark b() -> b(),
   mark f(X1, X2, X3) -> a__f(mark X1, X2, mark X3),
             mark c() -> a__c(),
               a__c() -> a(),
               a__c() -> b(),
               a__c() -> c()}
  UR:
   {  a__f(X1, X2, X3) -> f(X1, X2, X3),
     a__f(a(), b(), X) -> a__f(mark X, X, mark X),
              mark a() -> a(),
              mark b() -> b(),
    mark f(X1, X2, X3) -> a__f(mark X1, X2, mark X3),
              mark c() -> a__c(),
                a__c() -> a(),
                a__c() -> b(),
                a__c() -> c()}
   EDG:
    {(a__f#(a(), b(), X) -> a__f#(mark X, X, mark X), a__f#(a(), b(), X) -> mark# X)
     (a__f#(a(), b(), X) -> a__f#(mark X, X, mark X), a__f#(a(), b(), X) -> a__f#(mark X, X, mark X))
     (a__f#(a(), b(), X) -> mark# X, mark# c() -> a__c#())
     (a__f#(a(), b(), X) -> mark# X, mark# f(X1, X2, X3) -> mark# X3)
     (a__f#(a(), b(), X) -> mark# X, mark# f(X1, X2, X3) -> mark# X1)
     (a__f#(a(), b(), X) -> mark# X, mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3))
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3))
     (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# c() -> a__c#())
     (mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3), a__f#(a(), b(), X) -> a__f#(mark X, X, mark X))
     (mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3), a__f#(a(), b(), X) -> mark# X)
     (mark# f(X1, X2, X3) -> mark# X1, mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark 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# c() -> a__c#())}
    STATUS:
     arrows: 0.555556
     SCCS (1):
      Scc:
       { a__f#(a(), b(), X) -> a__f#(mark X, X, mark X),
         a__f#(a(), b(), X) -> mark# X,
        mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3),
        mark# f(X1, X2, X3) -> mark# X1,
        mark# f(X1, X2, X3) -> mark# X3}
      
      SCC (5):
       Strict:
        { a__f#(a(), b(), X) -> a__f#(mark X, X, mark X),
          a__f#(a(), b(), X) -> mark# X,
         mark# f(X1, X2, X3) -> a__f#(mark X1, X2, mark X3),
         mark# f(X1, X2, X3) -> mark# X1,
         mark# f(X1, X2, X3) -> mark# X3}
       Weak:
       {  a__f(X1, X2, X3) -> f(X1, X2, X3),
         a__f(a(), b(), X) -> a__f(mark X, X, mark X),
                  mark a() -> a(),
                  mark b() -> b(),
        mark f(X1, X2, X3) -> a__f(mark X1, X2, mark X3),
                  mark c() -> a__c(),
                    a__c() -> a(),
                    a__c() -> b(),
                    a__c() -> c()}
       Open