MAYBE
Time: 2.374670
TRS:
 {    a__minus(X1, X2) -> minus(X1, X2),
      a__minus(0(), Y) -> 0(),
    a__minus(s X, s Y) -> a__minus(X, Y),
        a__geq(X, 0()) -> true(),
        a__geq(X1, X2) -> geq(X1, X2),
      a__geq(0(), s Y) -> false(),
      a__geq(s X, s Y) -> a__geq(X, Y),
        a__div(X1, X2) -> div(X1, X2),
      a__div(0(), s Y) -> 0(),
      a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
     a__if(X1, X2, X3) -> if(X1, X2, X3),
   a__if(true(), X, Y) -> mark X,
  a__if(false(), X, Y) -> mark Y,
              mark 0() -> 0(),
              mark s X -> s mark X,
           mark true() -> true(),
          mark false() -> false(),
      mark div(X1, X2) -> a__div(mark X1, X2),
    mark minus(X1, X2) -> a__minus(X1, X2),
      mark geq(X1, X2) -> a__geq(X1, X2),
   mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)}
 DP:
  DP:
   {  a__minus#(s X, s Y) -> a__minus#(X, Y),
        a__geq#(s X, s Y) -> a__geq#(X, Y),
        a__div#(s X, s Y) -> a__geq#(X, Y),
        a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
     a__if#(true(), X, Y) -> mark# X,
    a__if#(false(), X, Y) -> mark# Y,
                mark# s X -> mark# X,
        mark# div(X1, X2) -> a__div#(mark X1, X2),
        mark# div(X1, X2) -> mark# X1,
      mark# minus(X1, X2) -> a__minus#(X1, X2),
        mark# geq(X1, X2) -> a__geq#(X1, X2),
     mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
     mark# if(X1, X2, X3) -> mark# X1}
  TRS:
  {    a__minus(X1, X2) -> minus(X1, X2),
       a__minus(0(), Y) -> 0(),
     a__minus(s X, s Y) -> a__minus(X, Y),
         a__geq(X, 0()) -> true(),
         a__geq(X1, X2) -> geq(X1, X2),
       a__geq(0(), s Y) -> false(),
       a__geq(s X, s Y) -> a__geq(X, Y),
         a__div(X1, X2) -> div(X1, X2),
       a__div(0(), s Y) -> 0(),
       a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
      a__if(X1, X2, X3) -> if(X1, X2, X3),
    a__if(true(), X, Y) -> mark X,
   a__if(false(), X, Y) -> mark Y,
               mark 0() -> 0(),
               mark s X -> s mark X,
            mark true() -> true(),
           mark false() -> false(),
       mark div(X1, X2) -> a__div(mark X1, X2),
     mark minus(X1, X2) -> a__minus(X1, X2),
       mark geq(X1, X2) -> a__geq(X1, X2),
    mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)}
  EDG:
   {(a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(false(), X, Y) -> mark# Y)
    (a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X)
    (mark# geq(X1, X2) -> a__geq#(X1, X2), a__geq#(s X, s Y) -> a__geq#(X, Y))
    (mark# div(X1, X2) -> a__div#(mark X1, X2), a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()))
    (mark# div(X1, X2) -> a__div#(mark X1, X2), a__div#(s X, s Y) -> a__geq#(X, Y))
    (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# s X -> mark# X, mark# geq(X1, X2) -> a__geq#(X1, X2))
    (mark# s X -> mark# X, mark# minus(X1, X2) -> a__minus#(X1, X2))
    (mark# s X -> mark# X, mark# div(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2))
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (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, X2, X3))
    (mark# if(X1, X2, X3) -> mark# X1, mark# geq(X1, X2) -> a__geq#(X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# minus(X1, X2) -> a__minus#(X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# div(X1, X2) -> mark# X1)
    (mark# if(X1, X2, X3) -> mark# X1, mark# div(X1, X2) -> a__div#(mark X1, X2))
    (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
    (a__geq#(s X, s Y) -> a__geq#(X, Y), a__geq#(s X, s Y) -> a__geq#(X, Y))
    (a__div#(s X, s Y) -> a__geq#(X, Y), a__geq#(s X, s Y) -> a__geq#(X, Y))
    (a__minus#(s X, s Y) -> a__minus#(X, Y), a__minus#(s X, s Y) -> a__minus#(X, Y))
    (mark# div(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# div(X1, X2) -> mark# X1, mark# div(X1, X2) -> a__div#(mark X1, X2))
    (mark# div(X1, X2) -> mark# X1, mark# div(X1, X2) -> mark# X1)
    (mark# div(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(X1, X2))
    (mark# div(X1, X2) -> mark# X1, mark# geq(X1, X2) -> a__geq#(X1, X2))
    (mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X)
    (a__if#(true(), X, Y) -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2))
    (a__if#(true(), X, Y) -> mark# X, mark# div(X1, X2) -> mark# X1)
    (a__if#(true(), X, Y) -> mark# X, mark# minus(X1, X2) -> a__minus#(X1, X2))
    (a__if#(true(), X, Y) -> mark# X, mark# geq(X1, X2) -> a__geq#(X1, X2))
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X)
    (a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> a__div#(mark X1, X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> mark# X1)
    (a__if#(false(), X, Y) -> mark# Y, mark# minus(X1, X2) -> a__minus#(X1, X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# geq(X1, X2) -> a__geq#(X1, X2))
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3))
    (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1)
    (mark# minus(X1, X2) -> a__minus#(X1, X2), a__minus#(s X, s Y) -> a__minus#(X, Y))
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X)
    (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)}
   STATUS:
    arrows: 0.727811
    SCCS (3):
     Scc:
      {    a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
        a__if#(true(), X, Y) -> mark# X,
       a__if#(false(), X, Y) -> mark# Y,
                   mark# s X -> mark# X,
           mark# div(X1, X2) -> a__div#(mark X1, X2),
           mark# div(X1, X2) -> mark# X1,
        mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
        mark# if(X1, X2, X3) -> mark# X1}
     Scc:
      {a__minus#(s X, s Y) -> a__minus#(X, Y)}
     Scc:
      {a__geq#(s X, s Y) -> a__geq#(X, Y)}
     
     SCC (8):
      Strict:
       {    a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
         a__if#(true(), X, Y) -> mark# X,
        a__if#(false(), X, Y) -> mark# Y,
                    mark# s X -> mark# X,
            mark# div(X1, X2) -> a__div#(mark X1, X2),
            mark# div(X1, X2) -> mark# X1,
         mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3),
         mark# if(X1, X2, X3) -> mark# X1}
      Weak:
      {    a__minus(X1, X2) -> minus(X1, X2),
           a__minus(0(), Y) -> 0(),
         a__minus(s X, s Y) -> a__minus(X, Y),
             a__geq(X, 0()) -> true(),
             a__geq(X1, X2) -> geq(X1, X2),
           a__geq(0(), s Y) -> false(),
           a__geq(s X, s Y) -> a__geq(X, Y),
             a__div(X1, X2) -> div(X1, X2),
           a__div(0(), s Y) -> 0(),
           a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
          a__if(X1, X2, X3) -> if(X1, X2, X3),
        a__if(true(), X, Y) -> mark X,
       a__if(false(), X, Y) -> mark Y,
                   mark 0() -> 0(),
                   mark s X -> s mark X,
                mark true() -> true(),
               mark false() -> false(),
           mark div(X1, X2) -> a__div(mark X1, X2),
         mark minus(X1, X2) -> a__minus(X1, X2),
           mark geq(X1, X2) -> a__geq(X1, X2),
        mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)}
      Open
     
     
     SCC (1):
      Strict:
       {a__minus#(s X, s Y) -> a__minus#(X, Y)}
      Weak:
      {    a__minus(X1, X2) -> minus(X1, X2),
           a__minus(0(), Y) -> 0(),
         a__minus(s X, s Y) -> a__minus(X, Y),
             a__geq(X, 0()) -> true(),
             a__geq(X1, X2) -> geq(X1, X2),
           a__geq(0(), s Y) -> false(),
           a__geq(s X, s Y) -> a__geq(X, Y),
             a__div(X1, X2) -> div(X1, X2),
           a__div(0(), s Y) -> 0(),
           a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
          a__if(X1, X2, X3) -> if(X1, X2, X3),
        a__if(true(), X, Y) -> mark X,
       a__if(false(), X, Y) -> mark Y,
                   mark 0() -> 0(),
                   mark s X -> s mark X,
                mark true() -> true(),
               mark false() -> false(),
           mark div(X1, X2) -> a__div(mark X1, X2),
         mark minus(X1, X2) -> a__minus(X1, X2),
           mark geq(X1, X2) -> a__geq(X1, X2),
        mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)}
      Open
     
     SCC (1):
      Strict:
       {a__geq#(s X, s Y) -> a__geq#(X, Y)}
      Weak:
      {    a__minus(X1, X2) -> minus(X1, X2),
           a__minus(0(), Y) -> 0(),
         a__minus(s X, s Y) -> a__minus(X, Y),
             a__geq(X, 0()) -> true(),
             a__geq(X1, X2) -> geq(X1, X2),
           a__geq(0(), s Y) -> false(),
           a__geq(s X, s Y) -> a__geq(X, Y),
             a__div(X1, X2) -> div(X1, X2),
           a__div(0(), s Y) -> 0(),
           a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()),
          a__if(X1, X2, X3) -> if(X1, X2, X3),
        a__if(true(), X, Y) -> mark X,
       a__if(false(), X, Y) -> mark Y,
                   mark 0() -> 0(),
                   mark s X -> s mark X,
                mark true() -> true(),
               mark false() -> false(),
           mark div(X1, X2) -> a__div(mark X1, X2),
         mark minus(X1, X2) -> a__minus(X1, X2),
           mark geq(X1, X2) -> a__geq(X1, X2),
        mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)}
      Open