MAYBE
Time: 0.002334
TRS:
 {cond(true(), x, y) -> s minus(x, s y),
     equal(s x, s y) -> equal(x, y),
     equal(s x, 0()) -> false(),
     equal(0(), s y) -> false(),
     equal(0(), 0()) -> true(),
         min(u, 0()) -> 0(),
       min(s u, s v) -> s min(u, v),
         min(0(), v) -> 0(),
         minus(x, y) -> cond(equal(min(x, y), y), x, y)}
 DP:
  DP:
   {cond#(true(), x, y) -> minus#(x, s y),
       equal#(s x, s y) -> equal#(x, y),
         min#(s u, s v) -> min#(u, v),
           minus#(x, y) -> cond#(equal(min(x, y), y), x, y),
           minus#(x, y) -> equal#(min(x, y), y),
           minus#(x, y) -> min#(x, y)}
  TRS:
  {cond(true(), x, y) -> s minus(x, s y),
      equal(s x, s y) -> equal(x, y),
      equal(s x, 0()) -> false(),
      equal(0(), s y) -> false(),
      equal(0(), 0()) -> true(),
          min(u, 0()) -> 0(),
        min(s u, s v) -> s min(u, v),
          min(0(), v) -> 0(),
          minus(x, y) -> cond(equal(min(x, y), y), x, y)}
  UR:
   {equal(s x, s y) -> equal(x, y),
    equal(s x, 0()) -> false(),
    equal(0(), s y) -> false(),
    equal(0(), 0()) -> true(),
        min(u, 0()) -> 0(),
      min(s u, s v) -> s min(u, v),
        min(0(), v) -> 0(),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
     (minus#(x, y) -> min#(x, y), min#(s u, s v) -> min#(u, v))
     (minus#(x, y) -> equal#(min(x, y), y), equal#(s x, s y) -> equal#(x, y))
     (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> cond#(equal(min(x, y), y), x, y))
     (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> equal#(min(x, y), y))
     (cond#(true(), x, y) -> minus#(x, s y), minus#(x, y) -> min#(x, y))
     (minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s y))
     (min#(s u, s v) -> min#(u, v), min#(s u, s v) -> min#(u, v))}
    STATUS:
     arrows: 0.777778
     SCCS (3):
      Scc:
       {cond#(true(), x, y) -> minus#(x, s y),
               minus#(x, y) -> cond#(equal(min(x, y), y), x, y)}
      Scc:
       {equal#(s x, s y) -> equal#(x, y)}
      Scc:
       {min#(s u, s v) -> min#(u, v)}
      
      SCC (2):
       Strict:
        {cond#(true(), x, y) -> minus#(x, s y),
                minus#(x, y) -> cond#(equal(min(x, y), y), x, y)}
       Weak:
       {cond(true(), x, y) -> s minus(x, s y),
           equal(s x, s y) -> equal(x, y),
           equal(s x, 0()) -> false(),
           equal(0(), s y) -> false(),
           equal(0(), 0()) -> true(),
               min(u, 0()) -> 0(),
             min(s u, s v) -> s min(u, v),
               min(0(), v) -> 0(),
               minus(x, y) -> cond(equal(min(x, y), y), x, y)}
       Open
      
      
      SCC (1):
       Strict:
        {equal#(s x, s y) -> equal#(x, y)}
       Weak:
       {cond(true(), x, y) -> s minus(x, s y),
           equal(s x, s y) -> equal(x, y),
           equal(s x, 0()) -> false(),
           equal(0(), s y) -> false(),
           equal(0(), 0()) -> true(),
               min(u, 0()) -> 0(),
             min(s u, s v) -> s min(u, v),
               min(0(), v) -> 0(),
               minus(x, y) -> cond(equal(min(x, y), y), x, y)}
       Open
      SCC (1):
       Strict:
        {min#(s u, s v) -> min#(u, v)}
       Weak:
       {cond(true(), x, y) -> s minus(x, s y),
           equal(s x, s y) -> equal(x, y),
           equal(s x, 0()) -> false(),
           equal(0(), s y) -> false(),
           equal(0(), 0()) -> true(),
               min(u, 0()) -> 0(),
             min(s u, s v) -> s min(u, v),
               min(0(), v) -> 0(),
               minus(x, y) -> cond(equal(min(x, y), y), x, y)}
       Open