MAYBE
Time: 0.007696
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:
  DP:
   { 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}
  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}
  UR:
   {   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# f X -> mark# X, mark# if(X1, X2, X3) -> mark# X2)
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (mark# f X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, mark X2, X3))
     (mark# f X -> mark# X, mark# f X -> a__f# mark X)
     (mark# f X -> mark# X, mark# f X -> 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) -> a__if#(mark X1, mark X2, X3), a__if#(true(), X, Y) -> mark# X)
     (mark# f X -> a__f# mark X, a__f# X -> mark# X)
     (mark# f X -> a__f# mark X, a__f# X -> a__if#(mark X, c(), f true()))
     (a__f# X -> a__if#(mark X, c(), f true()), a__if#(false(), X, Y) -> mark# Y)
     (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# 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)
     (mark# if(X1, X2, X3) -> mark# X1, mark# f X -> mark# X)
     (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 -> mark# X, mark# f X -> mark# X)
     (a__f# X -> mark# X, mark# f X -> a__f# mark X)
     (a__f# X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, mark X2, X3))
     (a__f# X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
     (a__f# X -> mark# X, mark# if(X1, X2, X3) -> mark# X2)
     (a__if#(true(), X, Y) -> mark# X, mark# f X -> mark# X)
     (a__if#(true(), X, Y) -> mark# X, mark# f X -> a__f# mark X)
     (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)}
    STATUS:
     arrows: 0.555556
     SCCS (1):
      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 (9):
       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}
       Open