MAYBE
Time: 0.028437
TRS:
 {  minus(x, x) -> 0(),
    minus(x, y) -> cond(min(x, y), x, y),
  cond(y, x, y) -> s minus(x, s y),
    min(u, 0()) -> 0(),
    min(0(), v) -> 0(),
  min(s u, s v) -> s min(u, v)}
 DP:
  DP:
   {  minus#(x, y) -> cond#(min(x, y), x, y),
      minus#(x, y) -> min#(x, y),
    cond#(y, x, y) -> minus#(x, s y),
    min#(s u, s v) -> min#(u, v)}
  TRS:
  {  minus(x, x) -> 0(),
     minus(x, y) -> cond(min(x, y), x, y),
   cond(y, x, y) -> s minus(x, s y),
     min(u, 0()) -> 0(),
     min(0(), v) -> 0(),
   min(s u, s v) -> s min(u, v)}
  EDG:
   {(cond#(y, x, y) -> minus#(x, s y), minus#(x, y) -> min#(x, y))
    (cond#(y, x, y) -> minus#(x, s y), minus#(x, y) -> cond#(min(x, y), x, y))
    (minus#(x, y) -> min#(x, y), min#(s u, s v) -> min#(u, v))
    (min#(s u, s v) -> min#(u, v), min#(s u, s v) -> min#(u, v))
    (minus#(x, y) -> cond#(min(x, y), x, y), cond#(y, x, y) -> minus#(x, s y))}
   STATUS:
    arrows: 0.687500
    SCCS (2):
     Scc:
      {  minus#(x, y) -> cond#(min(x, y), x, y),
       cond#(y, x, y) -> minus#(x, s y)}
     Scc:
      {min#(s u, s v) -> min#(u, v)}
     
     SCC (2):
      Strict:
       {  minus#(x, y) -> cond#(min(x, y), x, y),
        cond#(y, x, y) -> minus#(x, s y)}
      Weak:
      {  minus(x, x) -> 0(),
         minus(x, y) -> cond(min(x, y), x, y),
       cond(y, x, y) -> s minus(x, s y),
         min(u, 0()) -> 0(),
         min(0(), v) -> 0(),
       min(s u, s v) -> s min(u, v)}
      Fail
     
     SCC (1):
      Strict:
       {min#(s u, s v) -> min#(u, v)}
      Weak:
      {  minus(x, x) -> 0(),
         minus(x, y) -> cond(min(x, y), x, y),
       cond(y, x, y) -> s minus(x, s y),
         min(u, 0()) -> 0(),
         min(0(), v) -> 0(),
       min(s u, s v) -> s min(u, v)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cond](x0, x1, x2) = x0 + x1 + x2 + 1,
        
        [minus](x0, x1) = 0,
        
        [min](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [min#](x0, x1) = x0
       Strict:
        min#(s u, s v) -> min#(u, v)
        1 + 1v + 0u >= 0 + 1v + 0u
       Weak:
        min(s u, s v) -> s min(u, v)
        3 + 1v + 1u >= 2 + 1v + 1u
        min(0(), v) -> 0()
        2 + 1v >= 1
        min(u, 0()) -> 0()
        2 + 1u >= 1
        cond(y, x, y) -> s minus(x, s y)
        1 + 1x + 2y >= 1 + 0x + 0y
        minus(x, y) -> cond(min(x, y), x, y)
        0 + 0x + 0y >= 2 + 2x + 2y
        minus(x, x) -> 0()
        0 + 0x >= 1
      Qed