MAYBE
Time: 1.527718
TRS:
 {  a__f(X1, X2, X3) -> f(X1, X2, X3),
   a__f(a(), b(), X) -> a__f(X, X, mark X),
            mark a() -> a(),
            mark b() -> b(),
  mark f(X1, X2, X3) -> a__f(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#(X, X, mark X),
     a__f#(a(), b(), X) -> mark# X,
    mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3),
    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(X, X, mark X),
             mark a() -> a(),
             mark b() -> b(),
   mark f(X1, X2, X3) -> a__f(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(X, X, mark X),
              mark a() -> a(),
              mark b() -> b(),
    mark f(X1, X2, X3) -> a__f(X1, X2, mark X3),
              mark c() -> a__c(),
                a__c() -> a(),
                a__c() -> b(),
                a__c() -> c(),
               d(x, y) -> x,
               d(x, y) -> y}
   EDG:
    {(mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3), a__f#(a(), b(), X) -> mark# X)
     (mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3), a__f#(a(), b(), X) -> a__f#(X, X, mark X))
     (a__f#(a(), b(), X) -> mark# X, mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3))
     (a__f#(a(), b(), X) -> mark# X, mark# f(X1, X2, X3) -> mark# X3)
     (a__f#(a(), b(), X) -> mark# X, mark# c() -> a__c#())
     (mark# f(X1, X2, X3) -> mark# X3, mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3))
     (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#())
     (a__f#(a(), b(), X) -> a__f#(X, X, mark X), a__f#(a(), b(), X) -> a__f#(X, X, mark X))
     (a__f#(a(), b(), X) -> a__f#(X, X, mark X), a__f#(a(), b(), X) -> mark# X)}
    STATUS:
     arrows: 0.600000
     SCCS (1):
      Scc:
       { a__f#(a(), b(), X) -> a__f#(X, X, mark X),
         a__f#(a(), b(), X) -> mark# X,
        mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3),
        mark# f(X1, X2, X3) -> mark# X3}
      
      SCC (4):
       Strict:
        { a__f#(a(), b(), X) -> a__f#(X, X, mark X),
          a__f#(a(), b(), X) -> mark# X,
         mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3),
         mark# f(X1, X2, X3) -> mark# X3}
       Weak:
       {  a__f(X1, X2, X3) -> f(X1, X2, X3),
         a__f(a(), b(), X) -> a__f(X, X, mark X),
                  mark a() -> a(),
                  mark b() -> b(),
        mark f(X1, X2, X3) -> a__f(X1, X2, mark X3),
                  mark c() -> a__c(),
                    a__c() -> a(),
                    a__c() -> b(),
                    a__c() -> c()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a__f](x0, x1, x2) = x0 + 1,
         
         [f](x0, x1, x2) = x0 + 1,
         
         [mark](x0) = x0,
         
         [a] = 0,
         
         [b] = 0,
         
         [a__c] = 0,
         
         [c] = 0,
         
         [a__f#](x0, x1, x2) = x0 + 1,
         
         [mark#](x0) = x0 + 1
        Strict:
         mark# f(X1, X2, X3) -> mark# X3
         2 + 0X1 + 0X2 + 1X3 >= 1 + 1X3
         mark# f(X1, X2, X3) -> a__f#(X1, X2, mark X3)
         2 + 0X1 + 0X2 + 1X3 >= 1 + 0X1 + 0X2 + 1X3
         a__f#(a(), b(), X) -> mark# X
         1 + 1X >= 1 + 1X
         a__f#(a(), b(), X) -> a__f#(X, X, mark X)
         1 + 1X >= 1 + 1X
        Weak:
         a__c() -> c()
         0 >= 0
         a__c() -> b()
         0 >= 0
         a__c() -> a()
         0 >= 0
         mark c() -> a__c()
         0 >= 0
         mark f(X1, X2, X3) -> a__f(X1, X2, mark X3)
         1 + 0X1 + 0X2 + 1X3 >= 1 + 0X1 + 0X2 + 1X3
         mark b() -> b()
         0 >= 0
         mark a() -> a()
         0 >= 0
         a__f(a(), b(), X) -> a__f(X, X, mark X)
         1 + 1X >= 1 + 1X
         a__f(X1, X2, X3) -> f(X1, X2, X3)
         1 + 0X1 + 0X2 + 1X3 >= 1 + 0X1 + 0X2 + 1X3
       SCCS (1):
        Scc:
         {a__f#(a(), b(), X) -> a__f#(X, X, mark X)}
        
        SCC (1):
         Strict:
          {a__f#(a(), b(), X) -> a__f#(X, X, mark X)}
         Weak:
         {  a__f(X1, X2, X3) -> f(X1, X2, X3),
           a__f(a(), b(), X) -> a__f(X, X, mark X),
                    mark a() -> a(),
                    mark b() -> b(),
          mark f(X1, X2, X3) -> a__f(X1, X2, mark X3),
                    mark c() -> a__c(),
                      a__c() -> a(),
                      a__c() -> b(),
                      a__c() -> c()}
         Fail