MAYBE
Time: 0.167614
TRS:
 {              minus(x, 0()) -> x,
              minus(s x, s y) -> minus(x, y),
               quot(0(), s y) -> 0(),
               quot(s x, s y) -> s quot(minus(x, y), s y),
                   le(0(), y) -> true(),
                 le(s x, 0()) -> false(),
                 le(s x, s y) -> le(x, y),
                      inc 0() -> s 0(),
                      inc s x -> s inc x,
                logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                        log x -> logIter(x, 0()),
     if(true(), true(), x, y) -> logIter(x, y),
  if(true(), false(), x, s y) -> y,
         if(false(), b, x, y) -> logZeroError()}
 DP:
  DP:
   {         minus#(s x, s y) -> minus#(x, y),
              quot#(s x, s y) -> minus#(x, y),
              quot#(s x, s y) -> quot#(minus(x, y), s y),
                le#(s x, s y) -> le#(x, y),
                     inc# s x -> inc# x,
               logIter#(x, y) -> quot#(x, s s 0()),
               logIter#(x, y) -> le#(s 0(), x),
               logIter#(x, y) -> le#(s s 0(), x),
               logIter#(x, y) -> inc# y,
               logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                       log# x -> logIter#(x, 0()),
    if#(true(), true(), x, y) -> logIter#(x, y)}
  TRS:
  {              minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y),
                quot(0(), s y) -> 0(),
                quot(s x, s y) -> s quot(minus(x, y), s y),
                    le(0(), y) -> true(),
                  le(s x, 0()) -> false(),
                  le(s x, s y) -> le(x, y),
                       inc 0() -> s 0(),
                       inc s x -> s inc x,
                 logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                         log x -> logIter(x, 0()),
      if(true(), true(), x, y) -> logIter(x, y),
   if(true(), false(), x, s y) -> y,
          if(false(), b, x, y) -> logZeroError()}
  UR:
   {  minus(x, 0()) -> x,
    minus(s x, s y) -> minus(x, y),
     quot(0(), s y) -> 0(),
     quot(s x, s y) -> s quot(minus(x, y), s y),
         le(0(), y) -> true(),
       le(s x, 0()) -> false(),
       le(s x, s y) -> le(x, y),
            inc 0() -> s 0(),
            inc s x -> s inc x,
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y), if#(true(), true(), x, y) -> logIter#(x, y))
     (logIter#(x, y) -> inc# y, inc# s x -> inc# x)
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> inc# y)
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> le#(s s 0(), x))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> le#(s 0(), x))
     (if#(true(), true(), x, y) -> logIter#(x, y), logIter#(x, y) -> quot#(x, s s 0()))
     (inc# s x -> inc# x, inc# s x -> inc# x)
     (logIter#(x, y) -> le#(s s 0(), x), le#(s x, s y) -> le#(x, y))
     (logIter#(x, y) -> le#(s 0(), x), le#(s x, s y) -> le#(x, y))
     (logIter#(x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> minus#(x, y))
     (logIter#(x, y) -> quot#(x, s s 0()), quot#(s x, s y) -> quot#(minus(x, y), s y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (log# x -> logIter#(x, 0()), logIter#(x, y) -> quot#(x, s s 0()))
     (log# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s 0(), x))
     (log# x -> logIter#(x, 0()), logIter#(x, y) -> le#(s s 0(), x))
     (log# x -> logIter#(x, 0()), logIter#(x, y) -> inc# y)
     (log# x -> logIter#(x, 0()), logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
    STATUS:
     arrows: 0.847222
     SCCS (5):
      Scc:
       {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
        if#(true(), true(), x, y) -> logIter#(x, y)}
      Scc:
       {inc# s x -> inc# x}
      Scc:
       {le#(s x, s y) -> le#(x, y)}
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      
      
      SCC (2):
       Strict:
        {           logIter#(x, y) -> if#(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
         if#(true(), true(), x, y) -> logIter#(x, y)}
       Weak:
       {              minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                     quot(0(), s y) -> 0(),
                     quot(s x, s y) -> s quot(minus(x, y), s y),
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                              log x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError()}
       Fail
      
      SCC (1):
       Strict:
        {inc# s x -> inc# x}
       Weak:
       {              minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                     quot(0(), s y) -> 0(),
                     quot(s x, s y) -> s quot(minus(x, y), s y),
                         le(0(), y) -> true(),
                       le(s x, 0()) -> false(),
                       le(s x, s y) -> le(x, y),
                            inc 0() -> s 0(),
                            inc s x -> s inc x,
                      logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                              log x -> logIter(x, 0()),
           if(true(), true(), x, y) -> logIter(x, y),
        if(true(), false(), x, s y) -> y,
               if(false(), b, x, y) -> logZeroError()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2, x3) = 0,
         
         [minus](x0, x1) = x0 + 1,
         
         [quot](x0, x1) = x0 + 1,
         
         [le](x0, x1) = x0 + 1,
         
         [logIter](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [inc](x0) = x0 + 1,
         
         [log](x0) = 0,
         
         [0] = 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [logZeroError] = 0,
         
         [inc#](x0) = x0
        Strict:
         inc# s x -> inc# x
         1 + 1x >= 0 + 1x
        Weak:
         if(false(), b, x, y) -> logZeroError()
         0 + 0x + 0y + 0b >= 0
         if(true(), false(), x, s y) -> y
         0 + 0x + 0y >= 1y
         if(true(), true(), x, y) -> logIter(x, y)
         0 + 0x + 0y >= 1 + 0x + 1y
         log x -> logIter(x, 0())
         0 + 0x >= 2 + 0x
         logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y)
         1 + 0x + 1y >= 0 + 0x + 0y
         inc s x -> s inc x
         2 + 1x >= 2 + 1x
         inc 0() -> s 0()
         2 >= 2
         le(s x, s y) -> le(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
         le(s x, 0()) -> false()
         2 + 1x >= 0
         le(0(), y) -> true()
         2 + 0y >= 0
         quot(s x, s y) -> s quot(minus(x, y), s y)
         2 + 0x + 1y >= 3 + 0x + 1y
         quot(0(), s y) -> 0()
         2 + 1y >= 1
         minus(s x, s y) -> minus(x, y)
         2 + 0x + 1y >= 1 + 0x + 1y
         minus(x, 0()) -> x
         2 + 0x >= 1x
       Qed
     
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {              minus(x, 0()) -> x,
                   minus(s x, s y) -> minus(x, y),
                    quot(0(), s y) -> 0(),
                    quot(s x, s y) -> s quot(minus(x, y), s y),
                        le(0(), y) -> true(),
                      le(s x, 0()) -> false(),
                      le(s x, s y) -> le(x, y),
                           inc 0() -> s 0(),
                           inc s x -> s inc x,
                     logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                             log x -> logIter(x, 0()),
          if(true(), true(), x, y) -> logIter(x, y),
       if(true(), false(), x, s y) -> y,
              if(false(), b, x, y) -> logZeroError()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2, x3) = 0,
        
        [minus](x0, x1) = x0 + 1,
        
        [quot](x0, x1) = x0 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [logIter](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [inc](x0) = x0 + 1,
        
        [log](x0) = 0,
        
        [0] = 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [logZeroError] = 0,
        
        [le#](x0, x1) = x0
       Strict:
        le#(s x, s y) -> le#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        if(false(), b, x, y) -> logZeroError()
        0 + 0x + 0y + 0b >= 0
        if(true(), false(), x, s y) -> y
        0 + 0x + 0y >= 1y
        if(true(), true(), x, y) -> logIter(x, y)
        0 + 0x + 0y >= 1 + 0x + 1y
        log x -> logIter(x, 0())
        0 + 0x >= 2 + 0x
        logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y)
        1 + 0x + 1y >= 0 + 0x + 0y
        inc s x -> s inc x
        2 + 1x >= 2 + 1x
        inc 0() -> s 0()
        2 >= 2
        le(s x, s y) -> le(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
        le(s x, 0()) -> false()
        2 + 1x >= 0
        le(0(), y) -> true()
        2 + 0y >= 0
        quot(s x, s y) -> s quot(minus(x, y), s y)
        2 + 0x + 1y >= 3 + 0x + 1y
        quot(0(), s y) -> 0()
        2 + 1y >= 1
        minus(s x, s y) -> minus(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
      Qed
     
     SCC (1):
      Strict:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Weak:
      {              minus(x, 0()) -> x,
                   minus(s x, s y) -> minus(x, y),
                    quot(0(), s y) -> 0(),
                    quot(s x, s y) -> s quot(minus(x, y), s y),
                        le(0(), y) -> true(),
                      le(s x, 0()) -> false(),
                      le(s x, s y) -> le(x, y),
                           inc 0() -> s 0(),
                           inc s x -> s inc x,
                     logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                             log x -> logIter(x, 0()),
          if(true(), true(), x, y) -> logIter(x, y),
       if(true(), false(), x, s y) -> y,
              if(false(), b, x, y) -> logZeroError()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2, x3) = x0 + x1 + 1,
        
        [minus](x0, x1) = x0,
        
        [quot](x0, x1) = x0 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [logIter](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [inc](x0) = x0 + 1,
        
        [log](x0) = 0,
        
        [0] = 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [logZeroError] = 0,
        
        [quot#](x0, x1) = x0 + 1
       Strict:
        quot#(s x, s y) -> quot#(minus(x, y), s y)
        2 + 1x + 0y >= 1 + 1x + 0y
       Weak:
        if(false(), b, x, y) -> logZeroError()
        1 + 1x + 1y + 0b >= 0
        if(true(), false(), x, s y) -> y
        2 + 1x + 1y >= 1y
        if(true(), true(), x, y) -> logIter(x, y)
        1 + 1x + 1y >= 1 + 0x + 1y
        log x -> logIter(x, 0())
        0 + 0x >= 2 + 0x
        logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y)
        1 + 0x + 1y >= 6 + 0x + 1y
        inc s x -> s inc x
        2 + 1x >= 2 + 1x
        inc 0() -> s 0()
        2 >= 2
        le(s x, s y) -> le(x, y)
        2 + 1x + 0y >= 1 + 1x + 0y
        le(s x, 0()) -> false()
        2 + 1x >= 0
        le(0(), y) -> true()
        2 + 0y >= 0
        quot(s x, s y) -> s quot(minus(x, y), s y)
        2 + 0x + 1y >= 3 + 0x + 1y
        quot(0(), s y) -> 0()
        2 + 1y >= 1
        minus(s x, s y) -> minus(x, y)
        1 + 1x + 0y >= 0 + 1x + 0y
        minus(x, 0()) -> x
        0 + 1x >= 1x
      Qed
    
    SCC (1):
     Strict:
      {minus#(s x, s y) -> minus#(x, y)}
     Weak:
     {              minus(x, 0()) -> x,
                  minus(s x, s y) -> minus(x, y),
                   quot(0(), s y) -> 0(),
                   quot(s x, s y) -> s quot(minus(x, y), s y),
                       le(0(), y) -> true(),
                     le(s x, 0()) -> false(),
                     le(s x, s y) -> le(x, y),
                          inc 0() -> s 0(),
                          inc s x -> s inc x,
                    logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y),
                            log x -> logIter(x, 0()),
         if(true(), true(), x, y) -> logIter(x, y),
      if(true(), false(), x, s y) -> y,
             if(false(), b, x, y) -> logZeroError()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2, x3) = 0,
       
       [minus](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [le](x0, x1) = x0 + 1,
       
       [logIter](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [inc](x0) = x0 + 1,
       
       [log](x0) = 0,
       
       [0] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [logZeroError] = 0,
       
       [minus#](x0, x1) = x0
      Strict:
       minus#(s x, s y) -> minus#(x, y)
       1 + 0x + 1y >= 0 + 0x + 1y
      Weak:
       if(false(), b, x, y) -> logZeroError()
       0 + 0x + 0y + 0b >= 0
       if(true(), false(), x, s y) -> y
       0 + 0x + 0y >= 1y
       if(true(), true(), x, y) -> logIter(x, y)
       0 + 0x + 0y >= 1 + 0x + 1y
       log x -> logIter(x, 0())
       0 + 0x >= 2 + 0x
       logIter(x, y) -> if(le(s 0(), x), le(s s 0(), x), quot(x, s s 0()), inc y)
       1 + 0x + 1y >= 0 + 0x + 0y
       inc s x -> s inc x
       2 + 1x >= 2 + 1x
       inc 0() -> s 0()
       2 >= 2
       le(s x, s y) -> le(x, y)
       2 + 1x + 0y >= 1 + 1x + 0y
       le(s x, 0()) -> false()
       2 + 1x >= 0
       le(0(), y) -> true()
       2 + 0y >= 0
       quot(s x, s y) -> s quot(minus(x, y), s y)
       2 + 0x + 1y >= 3 + 0x + 1y
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       minus(s x, s y) -> minus(x, y)
       2 + 0x + 1y >= 1 + 0x + 1y
       minus(x, 0()) -> x
       2 + 0x >= 1x
     Qed