MAYBE
Time: 0.202467
TRS:
 {       minus(x, x) -> 0(),
         minus(x, y) -> cond(equal(min(x, y), y), x, y),
  cond(true(), x, y) -> s minus(x, s y),
     equal(0(), 0()) -> true(),
     equal(0(), s y) -> false(),
     equal(s x, 0()) -> false(),
     equal(s x, s y) -> equal(x, y),
         min(u, 0()) -> 0(),
         min(0(), v) -> 0(),
       min(s u, s v) -> s min(u, v)}
 DP:
  DP:
   {       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),
    cond#(true(), x, y) -> minus#(x, s y),
       equal#(s x, s y) -> equal#(x, y),
         min#(s u, s v) -> min#(u, v)}
  TRS:
  {       minus(x, x) -> 0(),
          minus(x, y) -> cond(equal(min(x, y), y), x, y),
   cond(true(), x, y) -> s minus(x, s y),
      equal(0(), 0()) -> true(),
      equal(0(), s y) -> false(),
      equal(s x, 0()) -> false(),
      equal(s x, s y) -> equal(x, y),
          min(u, 0()) -> 0(),
          min(0(), v) -> 0(),
        min(s u, s v) -> s min(u, v)}
  UR:
   {equal(0(), 0()) -> true(),
    equal(0(), s y) -> false(),
    equal(s x, 0()) -> false(),
    equal(s x, s y) -> equal(x, y),
        min(u, 0()) -> 0(),
        min(0(), v) -> 0(),
      min(s u, s v) -> s min(u, v)}
   EDG:
    {(minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s y))
     (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
     (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) -> 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))}
    EDG:
     {(minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s y))
      (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
      (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) -> 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))}
     EDG:
      {(minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s y))
       (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
       (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) -> 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))}
      EDG:
       {(minus#(x, y) -> cond#(equal(min(x, y), y), x, y), cond#(true(), x, y) -> minus#(x, s y))
        (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
        (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) -> 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))}
       STATUS:
        arrows: 0.777778
        SCCS (3):
         Scc:
          {       minus#(x, y) -> cond#(equal(min(x, y), y), x, y),
           cond#(true(), x, y) -> minus#(x, s y)}
         Scc:
          {equal#(s x, s y) -> equal#(x, y)}
         Scc:
          {min#(s u, s v) -> min#(u, v)}
         
         SCC (2):
          Strict:
           {       minus#(x, y) -> cond#(equal(min(x, y), y), x, y),
            cond#(true(), x, y) -> minus#(x, s y)}
          Weak:
          {       minus(x, x) -> 0(),
                  minus(x, y) -> cond(equal(min(x, y), y), x, y),
           cond(true(), x, y) -> s minus(x, s y),
              equal(0(), 0()) -> true(),
              equal(0(), s y) -> false(),
              equal(s x, 0()) -> false(),
              equal(s x, s y) -> equal(x, y),
                  min(u, 0()) -> 0(),
                  min(0(), v) -> 0(),
                min(s u, s v) -> s min(u, v)}
          Open
         
         
         SCC (1):
          Strict:
           {equal#(s x, s y) -> equal#(x, y)}
          Weak:
          {       minus(x, x) -> 0(),
                  minus(x, y) -> cond(equal(min(x, y), y), x, y),
           cond(true(), x, y) -> s minus(x, s y),
              equal(0(), 0()) -> true(),
              equal(0(), s y) -> false(),
              equal(s x, 0()) -> false(),
              equal(s x, s y) -> equal(x, y),
                  min(u, 0()) -> 0(),
                  min(0(), v) -> 0(),
                min(s u, s v) -> s min(u, v)}
          Open
         SCC (1):
          Strict:
           {min#(s u, s v) -> min#(u, v)}
          Weak:
          {       minus(x, x) -> 0(),
                  minus(x, y) -> cond(equal(min(x, y), y), x, y),
           cond(true(), x, y) -> s minus(x, s y),
              equal(0(), 0()) -> true(),
              equal(0(), s y) -> false(),
              equal(s x, 0()) -> false(),
              equal(s x, s y) -> equal(x, y),
                  min(u, 0()) -> 0(),
                  min(0(), v) -> 0(),
                min(s u, s v) -> s min(u, v)}
          Open