MAYBE
TRS:
 {      leq(0(), y) -> true(),
     leq(s(x), 0()) -> false(),
    leq(s(x), s(y)) -> leq(x, y),
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
          -(x, 0()) -> x,
      -(s(x), s(y)) -> -(x, y),
        mod(0(), y) -> 0(),
     mod(s(x), 0()) -> 0(),
    mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))}
 DP:
  Strict:
   {leq#(s(x), s(y)) -> leq#(x, y),
      -#(s(x), s(y)) -> -#(x, y),
    mod#(s(x), s(y)) -> leq#(y, x),
    mod#(s(x), s(y)) -> if#(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x)),
    mod#(s(x), s(y)) -> -#(s(x), s(y)),
    mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y))}
  Weak:
  {      leq(0(), y) -> true(),
      leq(s(x), 0()) -> false(),
     leq(s(x), s(y)) -> leq(x, y),
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
           -(x, 0()) -> x,
       -(s(x), s(y)) -> -(x, y),
         mod(0(), y) -> 0(),
      mod(s(x), 0()) -> 0(),
     mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))}
  EDG:
   {(-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y)), mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y)))
    (mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y)), mod#(s(x), s(y)) -> -#(s(x), s(y)))
    (mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y)), mod#(s(x), s(y)) -> if#(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x)))
    (mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y)), mod#(s(x), s(y)) -> leq#(y, x))
    (mod#(s(x), s(y)) -> -#(s(x), s(y)), -#(s(x), s(y)) -> -#(x, y))
    (leq#(s(x), s(y)) -> leq#(x, y), leq#(s(x), s(y)) -> leq#(x, y))
    (mod#(s(x), s(y)) -> leq#(y, x), leq#(s(x), s(y)) -> leq#(x, y))}
   SCCS:
    Scc:
     {mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y))}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    Scc:
     {leq#(s(x), s(y)) -> leq#(x, y)}
    SCC:
     Strict:
      {mod#(s(x), s(y)) -> mod#(-(s(x), s(y)), s(y))}
     Weak:
     {      leq(0(), y) -> true(),
         leq(s(x), 0()) -> false(),
        leq(s(x), s(y)) -> leq(x, y),
       if(true(), x, y) -> x,
      if(false(), x, y) -> y,
              -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
            mod(0(), y) -> 0(),
         mod(s(x), 0()) -> 0(),
        mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))}
     Fail
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {      leq(0(), y) -> true(),
         leq(s(x), 0()) -> false(),
        leq(s(x), s(y)) -> leq(x, y),
       if(true(), x, y) -> x,
      if(false(), x, y) -> y,
              -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
            mod(0(), y) -> 0(),
         mod(s(x), 0()) -> 0(),
        mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {leq#(s(x), s(y)) -> leq#(x, y)}
     Weak:
     {      leq(0(), y) -> true(),
         leq(s(x), 0()) -> false(),
        leq(s(x), s(y)) -> leq(x, y),
       if(true(), x, y) -> x,
      if(false(), x, y) -> y,
              -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
            mod(0(), y) -> 0(),
         mod(s(x), 0()) -> 0(),
        mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))}
     SPSC:
      Simple Projection:
       pi(leq#) = 0
      Strict:
       {}
      Qed