YES
Time: 0.008724
TRS:
 {  a__f(X1, X2, X3) -> f(X1, X2, X3),
     a__f(a(), X, X) -> a__f(X, a__b(), b()),
              a__b() -> b(),
              a__b() -> a(),
            mark b() -> a__b(),
            mark a() -> a(),
  mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
 DP:
  DP:
   {   a__f#(a(), X, X) -> a__f#(X, a__b(), b()),
       a__f#(a(), X, X) -> a__b#(),
              mark# b() -> a__b#(),
    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(a(), X, X) -> a__f(X, a__b(), b()),
               a__b() -> b(),
               a__b() -> a(),
             mark b() -> a__b(),
             mark a() -> a(),
   mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)}
  EDG:
   {(a__f#(a(), X, X) -> a__f#(X, a__b(), b()), a__f#(a(), X, X) -> a__b#())
    (a__f#(a(), X, X) -> a__f#(X, a__b(), b()), a__f#(a(), X, X) -> a__f#(X, a__b(), b()))
    (mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3), a__f#(a(), X, X) -> a__f#(X, a__b(), b()))
    (mark# f(X1, X2, X3) -> a__f#(X1, mark X2, X3), a__f#(a(), X, X) -> a__b#())
    (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> a__b#())
    (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#(a(), X, X) -> a__f#(X, a__b(), b())}
     
     SCC (1):
      Strict:
       {mark# f(X1, X2, X3) -> mark# X2}
      Weak:
      {  a__f(X1, X2, X3) -> f(X1, X2, X3),
          a__f(a(), X, X) -> a__f(X, a__b(), b()),
                   a__b() -> b(),
                   a__b() -> a(),
                 mark b() -> a__b(),
                 mark a() -> a(),
       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 + 1,
        
        [f](x0, x1, x2) = x0 + 1,
        
        [mark](x0) = 0,
        
        [a__b] = 0,
        
        [b] = 0,
        
        [a] = 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 + 0X3
        mark a() -> a()
        0 >= 1
        mark b() -> a__b()
        0 >= 0
        a__b() -> a()
        0 >= 1
        a__b() -> b()
        0 >= 0
        a__f(a(), X, X) -> a__f(X, a__b(), b())
        2 + 0X >= 1 + 1X
        a__f(X1, X2, X3) -> f(X1, X2, X3)
        1 + 1X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3
      Qed
    
    SCC (1):
     Strict:
      {a__f#(a(), X, X) -> a__f#(X, a__b(), b())}
     Weak:
     {  a__f(X1, X2, X3) -> f(X1, X2, X3),
         a__f(a(), X, X) -> a__f(X, a__b(), b()),
                  a__b() -> b(),
                  a__b() -> a(),
                mark b() -> a__b(),
                mark a() -> a(),
      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 + 1,
       
       [f](x0, x1, x2) = 0,
       
       [mark](x0) = 0,
       
       [a__b] = 0,
       
       [b] = 0,
       
       [a] = 1,
       
       [a__f#](x0, x1, x2) = x0 + x1
      Strict:
       a__f#(a(), X, X) -> a__f#(X, a__b(), b())
       1 + 1X >= 0 + 1X
      Weak:
       mark f(X1, X2, X3) -> a__f(X1, mark X2, X3)
       0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3
       mark a() -> a()
       0 >= 1
       mark b() -> a__b()
       0 >= 0
       a__b() -> a()
       0 >= 1
       a__b() -> b()
       0 >= 0
       a__f(a(), X, X) -> a__f(X, a__b(), b())
       2 + 0X >= 1 + 1X
       a__f(X1, X2, X3) -> f(X1, X2, X3)
       1 + 1X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     Qed