MAYBE
Time: 0.015543
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)}
  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