MAYBE
TRS:
 {   a__if(X1, X2, X3) -> if(X1, X2, X3),
   a__if(true(), X, Y) -> mark(X),
  a__if(false(), X, Y) -> mark(Y),
             mark(c()) -> c(),
            mark(f(X)) -> a__f(mark(X)),
          mark(true()) -> true(),
         mark(false()) -> false(),
  mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
               a__f(X) -> a__if(mark(X), c(), f(true())),
               a__f(X) -> f(X)}
 DP:
  Strict:
   { a__if#(true(), X, Y) -> mark#(X),
    a__if#(false(), X, Y) -> mark#(Y),
              mark#(f(X)) -> mark#(X),
              mark#(f(X)) -> a__f#(mark(X)),
    mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
    mark#(if(X1, X2, X3)) -> mark#(X1),
    mark#(if(X1, X2, X3)) -> mark#(X2),
                 a__f#(X) -> a__if#(mark(X), c(), f(true())),
                 a__f#(X) -> mark#(X)}
  Weak:
  {   a__if(X1, X2, X3) -> if(X1, X2, X3),
    a__if(true(), X, Y) -> mark(X),
   a__if(false(), X, Y) -> mark(Y),
              mark(c()) -> c(),
             mark(f(X)) -> a__f(mark(X)),
           mark(true()) -> true(),
          mark(false()) -> false(),
   mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                a__f(X) -> a__if(mark(X), c(), f(true())),
                a__f(X) -> f(X)}
  EDG:
   {(mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(false(), X, Y) -> mark#(Y))
    (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(true(), X, Y) -> mark#(X))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (a__if#(true(), X, Y) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (a__if#(true(), X, Y) -> mark#(X), mark#(f(X)) -> mark#(X))
    (a__f#(X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))
    (a__f#(X) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__f#(X) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (a__f#(X) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (a__f#(X) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> mark#(X))
    (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(true(), X, Y) -> mark#(X))
    (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(false(), X, Y) -> mark#(Y))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(X) -> a__if#(mark(X), c(), f(true())))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(X) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (mark#(f(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(f(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> mark#(X))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
    (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X2))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(f(X)) -> mark#(X))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(f(X)) -> a__f#(mark(X)))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
    (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X2))}
   SCCS:
    Scc:
     { a__if#(true(), X, Y) -> mark#(X),
      a__if#(false(), X, Y) -> mark#(Y),
                mark#(f(X)) -> mark#(X),
                mark#(f(X)) -> a__f#(mark(X)),
      mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
      mark#(if(X1, X2, X3)) -> mark#(X1),
      mark#(if(X1, X2, X3)) -> mark#(X2),
                   a__f#(X) -> a__if#(mark(X), c(), f(true())),
                   a__f#(X) -> mark#(X)}
    SCC:
     Strict:
      { a__if#(true(), X, Y) -> mark#(X),
       a__if#(false(), X, Y) -> mark#(Y),
                 mark#(f(X)) -> mark#(X),
                 mark#(f(X)) -> a__f#(mark(X)),
       mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
       mark#(if(X1, X2, X3)) -> mark#(X1),
       mark#(if(X1, X2, X3)) -> mark#(X2),
                    a__f#(X) -> a__if#(mark(X), c(), f(true())),
                    a__f#(X) -> mark#(X)}
     Weak:
     {   a__if(X1, X2, X3) -> if(X1, X2, X3),
       a__if(true(), X, Y) -> mark(X),
      a__if(false(), X, Y) -> mark(Y),
                 mark(c()) -> c(),
                mark(f(X)) -> a__f(mark(X)),
              mark(true()) -> true(),
             mark(false()) -> false(),
      mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                   a__f(X) -> a__if(mark(X), c(), f(true())),
                   a__f(X) -> f(X)}
     POLY:
      Argument Filtering:
       pi(if) = [0,1,2], pi(false) = [], pi(a__f#) = [0], pi(a__f) = [0], pi(true) = [], pi(f) = [0], pi(c) = [], pi(mark#) = 0, pi(mark) = 0, pi(a__if#) = [1,2], pi(a__if) = [0,1,2]
      Usable Rules:
       {}
      Interpretation:
       [a__if#](x0, x1) = x0 + x1,
       [a__f#](x0) = x0 + 1,
       [if](x0, x1, x2) = x0 + x1 + x2,
       [f](x0) = x0 + 1,
       [true] = 0,
       [c] = 0
      Strict:
       { a__if#(true(), X, Y) -> mark#(X),
        a__if#(false(), X, Y) -> mark#(Y),
                  mark#(f(X)) -> a__f#(mark(X)),
        mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
        mark#(if(X1, X2, X3)) -> mark#(X1),
        mark#(if(X1, X2, X3)) -> mark#(X2),
                     a__f#(X) -> a__if#(mark(X), c(), f(true()))}
      Weak:
       {   a__if(X1, X2, X3) -> if(X1, X2, X3),
         a__if(true(), X, Y) -> mark(X),
        a__if(false(), X, Y) -> mark(Y),
                   mark(c()) -> c(),
                  mark(f(X)) -> a__f(mark(X)),
                mark(true()) -> true(),
               mark(false()) -> false(),
        mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                     a__f(X) -> a__if(mark(X), c(), f(true())),
                     a__f(X) -> f(X)}
      EDG:
       {(mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X2))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
        (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> a__f#(mark(X)))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X2))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
        (a__if#(false(), X, Y) -> mark#(Y), mark#(f(X)) -> a__f#(mark(X)))
        (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))
        (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
        (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
        (a__if#(true(), X, Y) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
        (mark#(f(X)) -> a__f#(mark(X)), a__f#(X) -> a__if#(mark(X), c(), f(true())))
        (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(true(), X, Y) -> mark#(X))
        (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(false(), X, Y) -> mark#(Y))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> a__f#(mark(X)))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
        (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X2))
        (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(true(), X, Y) -> mark#(X))
        (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(false(), X, Y) -> mark#(Y))}
       SCCS:
        Scc:
         { a__if#(true(), X, Y) -> mark#(X),
          a__if#(false(), X, Y) -> mark#(Y),
                    mark#(f(X)) -> a__f#(mark(X)),
          mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
          mark#(if(X1, X2, X3)) -> mark#(X1),
          mark#(if(X1, X2, X3)) -> mark#(X2),
                       a__f#(X) -> a__if#(mark(X), c(), f(true()))}
        SCC:
         Strict:
          { a__if#(true(), X, Y) -> mark#(X),
           a__if#(false(), X, Y) -> mark#(Y),
                     mark#(f(X)) -> a__f#(mark(X)),
           mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
           mark#(if(X1, X2, X3)) -> mark#(X1),
           mark#(if(X1, X2, X3)) -> mark#(X2),
                        a__f#(X) -> a__if#(mark(X), c(), f(true()))}
         Weak:
         {   a__if(X1, X2, X3) -> if(X1, X2, X3),
           a__if(true(), X, Y) -> mark(X),
          a__if(false(), X, Y) -> mark(Y),
                     mark(c()) -> c(),
                    mark(f(X)) -> a__f(mark(X)),
                  mark(true()) -> true(),
                 mark(false()) -> false(),
          mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                       a__f(X) -> a__if(mark(X), c(), f(true())),
                       a__f(X) -> f(X)}
         POLY:
          Argument Filtering:
           pi(if) = [0,1,2], pi(false) = [], pi(a__f#) = 0, pi(a__f) = 0, pi(true) = [], pi(f) = 0, pi(c) = [], pi(mark#) = 0, pi(mark) = 0, pi(a__if#) = [0,1,2], pi(a__if) = [0,1,2]
          Usable Rules:
           {}
          Interpretation:
           [a__if#](x0, x1, x2) = x0 + x1 + x2,
           [if](x0, x1, x2) = x0 + x1 + x2,
           [false] = 1,
           [true] = 0,
           [c] = 0
          Strict:
           { a__if#(true(), X, Y) -> mark#(X),
                      mark#(f(X)) -> a__f#(mark(X)),
            mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
            mark#(if(X1, X2, X3)) -> mark#(X1),
            mark#(if(X1, X2, X3)) -> mark#(X2),
                         a__f#(X) -> a__if#(mark(X), c(), f(true()))}
          Weak:
           {   a__if(X1, X2, X3) -> if(X1, X2, X3),
             a__if(true(), X, Y) -> mark(X),
            a__if(false(), X, Y) -> mark(Y),
                       mark(c()) -> c(),
                      mark(f(X)) -> a__f(mark(X)),
                    mark(true()) -> true(),
                   mark(false()) -> false(),
            mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                         a__f(X) -> a__if(mark(X), c(), f(true())),
                         a__f(X) -> f(X)}
          EDG:
           {(a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))
            (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
            (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
            (a__if#(true(), X, Y) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
            (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(true(), X, Y) -> mark#(X))
            (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(true(), X, Y) -> mark#(X))
            (mark#(f(X)) -> a__f#(mark(X)), a__f#(X) -> a__if#(mark(X), c(), f(true())))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(f(X)) -> a__f#(mark(X)))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
            (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X2))
            (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(f(X)) -> a__f#(mark(X)))
            (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
            (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
            (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X2))}
           SCCS:
            Scc:
             { a__if#(true(), X, Y) -> mark#(X),
                        mark#(f(X)) -> a__f#(mark(X)),
              mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
              mark#(if(X1, X2, X3)) -> mark#(X1),
              mark#(if(X1, X2, X3)) -> mark#(X2),
                           a__f#(X) -> a__if#(mark(X), c(), f(true()))}
            SCC:
             Strict:
              { a__if#(true(), X, Y) -> mark#(X),
                         mark#(f(X)) -> a__f#(mark(X)),
               mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
               mark#(if(X1, X2, X3)) -> mark#(X1),
               mark#(if(X1, X2, X3)) -> mark#(X2),
                            a__f#(X) -> a__if#(mark(X), c(), f(true()))}
             Weak:
             {   a__if(X1, X2, X3) -> if(X1, X2, X3),
               a__if(true(), X, Y) -> mark(X),
              a__if(false(), X, Y) -> mark(Y),
                         mark(c()) -> c(),
                        mark(f(X)) -> a__f(mark(X)),
                      mark(true()) -> true(),
                     mark(false()) -> false(),
              mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                           a__f(X) -> a__if(mark(X), c(), f(true())),
                           a__f(X) -> f(X)}
             POLY:
              Argument Filtering:
               pi(if) = [0,1,2], pi(false) = [], pi(a__f#) = [], pi(a__f) = [0], pi(true) = [], pi(f) = [0], pi(c) = [], pi(mark#) = 0, pi(mark) = 0, pi(a__if#) = 1, pi(a__if) = [0,1,2]
              Usable Rules:
               {}
              Interpretation:
               [a__f#] = 0,
               [if](x0, x1, x2) = x0 + x1 + x2,
               [f](x0) = x0 + 1,
               [c] = 0
              Strict:
               { a__if#(true(), X, Y) -> mark#(X),
                mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
                mark#(if(X1, X2, X3)) -> mark#(X1),
                mark#(if(X1, X2, X3)) -> mark#(X2),
                             a__f#(X) -> a__if#(mark(X), c(), f(true()))}
              Weak:
               {   a__if(X1, X2, X3) -> if(X1, X2, X3),
                 a__if(true(), X, Y) -> mark(X),
                a__if(false(), X, Y) -> mark(Y),
                           mark(c()) -> c(),
                          mark(f(X)) -> a__f(mark(X)),
                        mark(true()) -> true(),
                       mark(false()) -> false(),
                mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                             a__f(X) -> a__if(mark(X), c(), f(true())),
                             a__f(X) -> f(X)}
              EDG:
               {(mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X2))
                (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1))
                (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
                (mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3), a__if#(true(), X, Y) -> mark#(X))
                (a__f#(X) -> a__if#(mark(X), c(), f(true())), a__if#(true(), X, Y) -> mark#(X))
                (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
                (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1))
                (mark#(if(X1, X2, X3)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X2))
                (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3))
                (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1))
                (a__if#(true(), X, Y) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X2))}
               SCCS:
                Scc:
                 { a__if#(true(), X, Y) -> mark#(X),
                  mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
                  mark#(if(X1, X2, X3)) -> mark#(X1),
                  mark#(if(X1, X2, X3)) -> mark#(X2)}
                SCC:
                 Strict:
                  { a__if#(true(), X, Y) -> mark#(X),
                   mark#(if(X1, X2, X3)) -> a__if#(mark(X1), mark(X2), X3),
                   mark#(if(X1, X2, X3)) -> mark#(X1),
                   mark#(if(X1, X2, X3)) -> mark#(X2)}
                 Weak:
                 {   a__if(X1, X2, X3) -> if(X1, X2, X3),
                   a__if(true(), X, Y) -> mark(X),
                  a__if(false(), X, Y) -> mark(Y),
                             mark(c()) -> c(),
                            mark(f(X)) -> a__f(mark(X)),
                          mark(true()) -> true(),
                         mark(false()) -> false(),
                  mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3),
                               a__f(X) -> a__if(mark(X), c(), f(true())),
                               a__f(X) -> f(X)}
                 Fail