MAYBE
Time: 0.281959
TRS:
 {        -(x, 0()) -> x,
        -(0(), s y) -> 0(),
        -(s x, s y) -> -(x, y),
         lt(x, 0()) -> false(),
       lt(0(), s y) -> true(),
       lt(s x, s y) -> lt(x, y),
  if(false(), x, y) -> y,
   if(true(), x, y) -> x,
        div(x, 0()) -> 0(),
        div(0(), y) -> 0(),
      div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))}
 DP:
  DP:
   {  -#(s x, s y) -> -#(x, y),
     lt#(s x, s y) -> lt#(x, y),
    div#(s x, s y) -> -#(x, y),
    div#(s x, s y) -> lt#(x, y),
    div#(s x, s y) -> if#(lt(x, y), 0(), s div(-(x, y), s y)),
    div#(s x, s y) -> div#(-(x, y), s y)}
  TRS:
  {        -(x, 0()) -> x,
         -(0(), s y) -> 0(),
         -(s x, s y) -> -(x, y),
          lt(x, 0()) -> false(),
        lt(0(), s y) -> true(),
        lt(s x, s y) -> lt(x, y),
   if(false(), x, y) -> y,
    if(true(), x, y) -> x,
         div(x, 0()) -> 0(),
         div(0(), y) -> 0(),
       div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))}
  UR:
   {        -(x, 0()) -> x,
          -(0(), s y) -> 0(),
          -(s x, s y) -> -(x, y),
           lt(x, 0()) -> false(),
         lt(0(), s y) -> true(),
         lt(s x, s y) -> lt(x, y),
    if(false(), x, y) -> y,
     if(true(), x, y) -> x,
          div(0(), y) -> 0(),
        div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y)),
              a(z, w) -> z,
              a(z, w) -> w}
   EDG:
    {(lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (div#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
     (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> -#(x, y))
     (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> lt#(x, y))
     (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> if#(lt(x, y), 0(), s div(-(x, y), s y)))
     (div#(s x, s y) -> div#(-(x, y), s y), div#(s x, s y) -> div#(-(x, y), s y))
     (div#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))}
    STATUS:
     arrows: 0.777778
     SCCS (3):
      Scc:
       {div#(s x, s y) -> div#(-(x, y), s y)}
      Scc:
       {lt#(s x, s y) -> lt#(x, y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      
      SCC (1):
       Strict:
        {div#(s x, s y) -> div#(-(x, y), s y)}
       Weak:
       {        -(x, 0()) -> x,
              -(0(), s y) -> 0(),
              -(s x, s y) -> -(x, y),
               lt(x, 0()) -> false(),
             lt(0(), s y) -> true(),
             lt(s x, s y) -> lt(x, y),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
              div(x, 0()) -> 0(),
              div(0(), y) -> 0(),
            div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))}
       Open
      
      
      
      SCC (1):
       Strict:
        {lt#(s x, s y) -> lt#(x, y)}
       Weak:
       {        -(x, 0()) -> x,
              -(0(), s y) -> 0(),
              -(s x, s y) -> -(x, y),
               lt(x, 0()) -> false(),
             lt(0(), s y) -> true(),
             lt(s x, s y) -> lt(x, y),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
              div(x, 0()) -> 0(),
              div(0(), y) -> 0(),
            div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))}
       Open
      SCC (1):
       Strict:
        {-#(s x, s y) -> -#(x, y)}
       Weak:
       {        -(x, 0()) -> x,
              -(0(), s y) -> 0(),
              -(s x, s y) -> -(x, y),
               lt(x, 0()) -> false(),
             lt(0(), s y) -> true(),
             lt(s x, s y) -> lt(x, y),
        if(false(), x, y) -> y,
         if(true(), x, y) -> x,
              div(x, 0()) -> 0(),
              div(0(), y) -> 0(),
            div(s x, s y) -> if(lt(x, y), 0(), s div(-(x, y), s y))}
       Open