MAYBE
Time: 0.913620
TRS:
 {  a__f(X1, X2, X3) -> f(X1, X2, X3),
   a__f(b(), X, c()) -> a__f(X, a__c(), X),
              a__c() -> b(),
              a__c() -> c(),
            mark b() -> b(),
            mark c() -> a__c(),
  mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
 DP:
  DP:
   { a__f#(b(), X, c()) -> a__f#(X, a__c(), X),
     a__f#(b(), X, c()) -> a__c#(),
              mark# c() -> a__c#(),
    mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3),
    mark# f(X1, X2, X3) -> mark# X2}
  TRS:
  {  a__f(X1, X2, X3) -> f(X1, X2, X3),
    a__f(b(), X, c()) -> a__f(X, a__c(), X),
               a__c() -> b(),
               a__c() -> c(),
             mark b() -> b(),
             mark c() -> a__c(),
   mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
  UR:
   {  a__f(X1, X2, X3) -> f(X1, X2, X3),
     a__f(b(), X, c()) -> a__f(X, a__c(), X),
                a__c() -> b(),
                a__c() -> c(),
              mark b() -> b(),
              mark c() -> a__c(),
    mark f(X1, X2, X3) -> a__f(X1, mark X2, X3),
               a(x, y) -> x,
               a(x, y) -> y}
   EDG:
    {(a__f#(b(), X, c()) -> a__f#(X, a__c(), X), a__f#(b(), X, c()) -> a__c#())
     (a__f#(b(), X, c()) -> a__f#(X, a__c(), X), a__f#(b(), X, c()) -> a__f#(X, a__c(), X))
     (mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3), a__f#(b(), X, c()) -> a__f#(X, a__c(), X))
     (mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3), a__f#(b(), X, c()) -> a__c#())
     (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> a__c#())
     (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3))
     (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2)}
    STATUS:
     arrows: 0.720000
     SCCS (2):
      Scc:
       {mark# f(X1, X2, X3) -> mark# X2}
      Scc:
       {a__f#(b(), X, c()) -> a__f#(X, a__c(), X)}
      
      SCC (1):
       Strict:
        {mark# f(X1, X2, X3) -> mark# X2}
       Weak:
       {  a__f(X1, X2, X3) -> f(X1, X2, X3),
         a__f(b(), X, c()) -> a__f(X, a__c(), X),
                    a__c() -> b(),
                    a__c() -> c(),
                  mark b() -> b(),
                  mark c() -> a__c(),
        mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [a__f](x0, x1, x2) = x0 + x1 + 1,
         
         [f](x0, x1, x2) = x0 + 1,
         
         [mark](x0) = 0,
         
         [a__c] = 0,
         
         [b] = 0,
         
         [c] = 1,
         
         [mark#](x0) = x0 + 1
        Strict:
         mark# f(X1, X2, X3) -> mark# X2
         2 + 0X1 + 1X2 + 0X3 >= 1 + 1X2
        Weak:
         mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)
         0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 1X3
         mark c() -> a__c()
         0 >= 0
         mark b() -> b()
         0 >= 0
         a__c() -> c()
         0 >= 1
         a__c() -> b()
         0 >= 0
         a__f(b(), X, c()) -> a__f(X, a__c(), X)
         2 + 0X >= 1 + 2X
         a__f(X1, X2, X3) -> f(X1, X2, X3)
         1 + 1X1 + 0X2 + 1X3 >= 1 + 0X1 + 1X2 + 0X3
       Qed
     
     SCC (1):
      Strict:
       {a__f#(b(), X, c()) -> a__f#(X, a__c(), X)}
      Weak:
      {  a__f(X1, X2, X3) -> f(X1, X2, X3),
        a__f(b(), X, c()) -> a__f(X, a__c(), X),
                   a__c() -> b(),
                   a__c() -> c(),
                 mark b() -> b(),
                 mark c() -> a__c(),
       mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
      Fail