MAYBE
Time: 8.539211
TRS:
 {      minus_active(x, y) -> minus(x, y),
      minus_active(0(), y) -> 0(),
    minus_active(s x, s y) -> minus_active(x, y),
                  mark 0() -> 0(),
                  mark s x -> s mark x,
          mark minus(x, y) -> minus_active(x, y),
             mark ge(x, y) -> ge_active(x, y),
            mark div(x, y) -> div_active(mark x, y),
          mark if(x, y, z) -> if_active(mark x, y, z),
           ge_active(x, y) -> ge(x, y),
         ge_active(x, 0()) -> true(),
       ge_active(0(), s y) -> false(),
       ge_active(s x, s y) -> ge_active(x, y),
          div_active(x, y) -> div(x, y),
      div_active(0(), s y) -> 0(),
      div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
        if_active(x, y, z) -> if(x, y, z),
   if_active(true(), x, y) -> mark x,
  if_active(false(), x, y) -> mark y}
 DP:
  DP:
   {  minus_active#(s x, s y) -> minus_active#(x, y),
                    mark# s x -> mark# x,
            mark# minus(x, y) -> minus_active#(x, y),
               mark# ge(x, y) -> ge_active#(x, y),
              mark# div(x, y) -> mark# x,
              mark# div(x, y) -> div_active#(mark x, y),
            mark# if(x, y, z) -> mark# x,
            mark# if(x, y, z) -> if_active#(mark x, y, z),
         ge_active#(s x, s y) -> ge_active#(x, y),
        div_active#(s x, s y) -> ge_active#(x, y),
        div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()),
     if_active#(true(), x, y) -> mark# x,
    if_active#(false(), x, y) -> mark# y}
  TRS:
  {      minus_active(x, y) -> minus(x, y),
       minus_active(0(), y) -> 0(),
     minus_active(s x, s y) -> minus_active(x, y),
                   mark 0() -> 0(),
                   mark s x -> s mark x,
           mark minus(x, y) -> minus_active(x, y),
              mark ge(x, y) -> ge_active(x, y),
             mark div(x, y) -> div_active(mark x, y),
           mark if(x, y, z) -> if_active(mark x, y, z),
            ge_active(x, y) -> ge(x, y),
          ge_active(x, 0()) -> true(),
        ge_active(0(), s y) -> false(),
        ge_active(s x, s y) -> ge_active(x, y),
           div_active(x, y) -> div(x, y),
       div_active(0(), s y) -> 0(),
       div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
         if_active(x, y, z) -> if(x, y, z),
    if_active(true(), x, y) -> mark x,
   if_active(false(), x, y) -> mark y}
  UR:
   {      minus_active(x, y) -> minus(x, y),
        minus_active(0(), y) -> 0(),
      minus_active(s x, s y) -> minus_active(x, y),
                    mark 0() -> 0(),
                    mark s x -> s mark x,
            mark minus(x, y) -> minus_active(x, y),
               mark ge(x, y) -> ge_active(x, y),
              mark div(x, y) -> div_active(mark x, y),
            mark if(x, y, z) -> if_active(mark x, y, z),
             ge_active(x, y) -> ge(x, y),
           ge_active(x, 0()) -> true(),
         ge_active(0(), s y) -> false(),
         ge_active(s x, s y) -> ge_active(x, y),
            div_active(x, y) -> div(x, y),
        div_active(0(), s y) -> 0(),
        div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
          if_active(x, y, z) -> if(x, y, z),
     if_active(true(), x, y) -> mark x,
    if_active(false(), x, y) -> mark y,
                     a(w, v) -> w,
                     a(w, v) -> v}
   EDG:
    {(div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()), if_active#(false(), x, y) -> mark# y)
     (div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()), if_active#(true(), x, y) -> mark# x)
     (mark# s x -> mark# x, mark# if(x, y, z) -> if_active#(mark x, y, z))
     (mark# s x -> mark# x, mark# if(x, y, z) -> mark# x)
     (mark# s x -> mark# x, mark# div(x, y) -> div_active#(mark x, y))
     (mark# s x -> mark# x, mark# div(x, y) -> mark# x)
     (mark# s x -> mark# x, mark# ge(x, y) -> ge_active#(x, y))
     (mark# s x -> mark# x, mark# minus(x, y) -> minus_active#(x, y))
     (mark# s x -> mark# x, mark# s x -> mark# x)
     (mark# if(x, y, z) -> mark# x, mark# if(x, y, z) -> if_active#(mark x, y, z))
     (mark# if(x, y, z) -> mark# x, mark# if(x, y, z) -> mark# x)
     (mark# if(x, y, z) -> mark# x, mark# div(x, y) -> div_active#(mark x, y))
     (mark# if(x, y, z) -> mark# x, mark# div(x, y) -> mark# x)
     (mark# if(x, y, z) -> mark# x, mark# ge(x, y) -> ge_active#(x, y))
     (mark# if(x, y, z) -> mark# x, mark# minus(x, y) -> minus_active#(x, y))
     (mark# if(x, y, z) -> mark# x, mark# s x -> mark# x)
     (mark# if(x, y, z) -> if_active#(mark x, y, z), if_active#(false(), x, y) -> mark# y)
     (mark# if(x, y, z) -> if_active#(mark x, y, z), if_active#(true(), x, y) -> mark# x)
     (mark# minus(x, y) -> minus_active#(x, y), minus_active#(s x, s y) -> minus_active#(x, y))
     (ge_active#(s x, s y) -> ge_active#(x, y), ge_active#(s x, s y) -> ge_active#(x, y))
     (div_active#(s x, s y) -> ge_active#(x, y), ge_active#(s x, s y) -> ge_active#(x, y))
     (mark# ge(x, y) -> ge_active#(x, y), ge_active#(s x, s y) -> ge_active#(x, y))
     (minus_active#(s x, s y) -> minus_active#(x, y), minus_active#(s x, s y) -> minus_active#(x, y))
     (if_active#(true(), x, y) -> mark# x, mark# s x -> mark# x)
     (if_active#(true(), x, y) -> mark# x, mark# minus(x, y) -> minus_active#(x, y))
     (if_active#(true(), x, y) -> mark# x, mark# ge(x, y) -> ge_active#(x, y))
     (if_active#(true(), x, y) -> mark# x, mark# div(x, y) -> mark# x)
     (if_active#(true(), x, y) -> mark# x, mark# div(x, y) -> div_active#(mark x, y))
     (if_active#(true(), x, y) -> mark# x, mark# if(x, y, z) -> mark# x)
     (if_active#(true(), x, y) -> mark# x, mark# if(x, y, z) -> if_active#(mark x, y, z))
     (mark# div(x, y) -> mark# x, mark# s x -> mark# x)
     (mark# div(x, y) -> mark# x, mark# minus(x, y) -> minus_active#(x, y))
     (mark# div(x, y) -> mark# x, mark# ge(x, y) -> ge_active#(x, y))
     (mark# div(x, y) -> mark# x, mark# div(x, y) -> mark# x)
     (mark# div(x, y) -> mark# x, mark# div(x, y) -> div_active#(mark x, y))
     (mark# div(x, y) -> mark# x, mark# if(x, y, z) -> mark# x)
     (mark# div(x, y) -> mark# x, mark# if(x, y, z) -> if_active#(mark x, y, z))
     (if_active#(false(), x, y) -> mark# y, mark# s x -> mark# x)
     (if_active#(false(), x, y) -> mark# y, mark# minus(x, y) -> minus_active#(x, y))
     (if_active#(false(), x, y) -> mark# y, mark# ge(x, y) -> ge_active#(x, y))
     (if_active#(false(), x, y) -> mark# y, mark# div(x, y) -> mark# x)
     (if_active#(false(), x, y) -> mark# y, mark# div(x, y) -> div_active#(mark x, y))
     (if_active#(false(), x, y) -> mark# y, mark# if(x, y, z) -> mark# x)
     (if_active#(false(), x, y) -> mark# y, mark# if(x, y, z) -> if_active#(mark x, y, z))
     (mark# div(x, y) -> div_active#(mark x, y), div_active#(s x, s y) -> ge_active#(x, y))
     (mark# div(x, y) -> div_active#(mark x, y), div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()))}
    STATUS:
     arrows: 0.727811
     SCCS (3):
      Scc:
       {                mark# s x -> mark# x,
                  mark# div(x, y) -> mark# x,
                  mark# div(x, y) -> div_active#(mark x, y),
                mark# if(x, y, z) -> mark# x,
                mark# if(x, y, z) -> if_active#(mark x, y, z),
            div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()),
         if_active#(true(), x, y) -> mark# x,
        if_active#(false(), x, y) -> mark# y}
      Scc:
       {minus_active#(s x, s y) -> minus_active#(x, y)}
      Scc:
       {ge_active#(s x, s y) -> ge_active#(x, y)}
      
      SCC (8):
       Strict:
        {                mark# s x -> mark# x,
                   mark# div(x, y) -> mark# x,
                   mark# div(x, y) -> div_active#(mark x, y),
                 mark# if(x, y, z) -> mark# x,
                 mark# if(x, y, z) -> if_active#(mark x, y, z),
             div_active#(s x, s y) -> if_active#(ge_active(x, y), s div(minus(x, y), s y), 0()),
          if_active#(true(), x, y) -> mark# x,
         if_active#(false(), x, y) -> mark# y}
       Weak:
       {      minus_active(x, y) -> minus(x, y),
            minus_active(0(), y) -> 0(),
          minus_active(s x, s y) -> minus_active(x, y),
                        mark 0() -> 0(),
                        mark s x -> s mark x,
                mark minus(x, y) -> minus_active(x, y),
                   mark ge(x, y) -> ge_active(x, y),
                  mark div(x, y) -> div_active(mark x, y),
                mark if(x, y, z) -> if_active(mark x, y, z),
                 ge_active(x, y) -> ge(x, y),
               ge_active(x, 0()) -> true(),
             ge_active(0(), s y) -> false(),
             ge_active(s x, s y) -> ge_active(x, y),
                div_active(x, y) -> div(x, y),
            div_active(0(), s y) -> 0(),
            div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
              if_active(x, y, z) -> if(x, y, z),
         if_active(true(), x, y) -> mark x,
        if_active(false(), x, y) -> mark y}
       Open
      
      
      SCC (1):
       Strict:
        {minus_active#(s x, s y) -> minus_active#(x, y)}
       Weak:
       {      minus_active(x, y) -> minus(x, y),
            minus_active(0(), y) -> 0(),
          minus_active(s x, s y) -> minus_active(x, y),
                        mark 0() -> 0(),
                        mark s x -> s mark x,
                mark minus(x, y) -> minus_active(x, y),
                   mark ge(x, y) -> ge_active(x, y),
                  mark div(x, y) -> div_active(mark x, y),
                mark if(x, y, z) -> if_active(mark x, y, z),
                 ge_active(x, y) -> ge(x, y),
               ge_active(x, 0()) -> true(),
             ge_active(0(), s y) -> false(),
             ge_active(s x, s y) -> ge_active(x, y),
                div_active(x, y) -> div(x, y),
            div_active(0(), s y) -> 0(),
            div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
              if_active(x, y, z) -> if(x, y, z),
         if_active(true(), x, y) -> mark x,
        if_active(false(), x, y) -> mark y}
       Open
      
      SCC (1):
       Strict:
        {ge_active#(s x, s y) -> ge_active#(x, y)}
       Weak:
       {      minus_active(x, y) -> minus(x, y),
            minus_active(0(), y) -> 0(),
          minus_active(s x, s y) -> minus_active(x, y),
                        mark 0() -> 0(),
                        mark s x -> s mark x,
                mark minus(x, y) -> minus_active(x, y),
                   mark ge(x, y) -> ge_active(x, y),
                  mark div(x, y) -> div_active(mark x, y),
                mark if(x, y, z) -> if_active(mark x, y, z),
                 ge_active(x, y) -> ge(x, y),
               ge_active(x, 0()) -> true(),
             ge_active(0(), s y) -> false(),
             ge_active(s x, s y) -> ge_active(x, y),
                div_active(x, y) -> div(x, y),
            div_active(0(), s y) -> 0(),
            div_active(s x, s y) -> if_active(ge_active(x, y), s div(minus(x, y), s y), 0()),
              if_active(x, y, z) -> if(x, y, z),
         if_active(true(), x, y) -> mark x,
        if_active(false(), x, y) -> mark y}
       Open