MAYBE
Time: 4.441069
TRS:
 {    -(x, 0()) -> x,
    -(s x, s y) -> -(x, y),
    min(x, 0()) -> 0(),
    min(0(), y) -> 0(),
  min(s x, s y) -> s min(x, y),
      twice 0() -> 0(),
      twice s x -> s s twice x,
    f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
    f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
 DP:
  DP:
   {  -#(s x, s y) -> -#(x, y),
    min#(s x, s y) -> min#(x, y),
        twice# s x -> twice# x,
      f#(s x, s y) -> -#(x, min(x, y)),
      f#(s x, s y) -> -#(y, min(x, y)),
      f#(s x, s y) -> min#(x, y),
      f#(s x, s y) -> twice# min(x, y),
      f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)),
      f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y))}
  TRS:
  {    -(x, 0()) -> x,
     -(s x, s y) -> -(x, y),
     min(x, 0()) -> 0(),
     min(0(), y) -> 0(),
   min(s x, s y) -> s min(x, y),
       twice 0() -> 0(),
       twice s x -> s s twice x,
     f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
     f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
  UR:
   {    -(x, 0()) -> x,
      -(s x, s y) -> -(x, y),
      min(x, 0()) -> 0(),
      min(0(), y) -> 0(),
    min(s x, s y) -> s min(x, y),
        twice 0() -> 0(),
        twice s x -> s s twice x,
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (f#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> twice# min(x, y))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> min#(x, y))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> -#(y, min(x, y)))
     (f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)), f#(s x, s y) -> -#(x, min(x, y)))
     (f#(s x, s y) -> -#(y, min(x, y)), -#(s x, s y) -> -#(x, y))
     (f#(s x, s y) -> twice# min(x, y), twice# s x -> twice# x)
     (f#(s x, s y) -> -#(x, min(x, y)), -#(s x, s y) -> -#(x, y))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> -#(x, min(x, y)))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> -#(y, min(x, y)))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> min#(x, y))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> twice# min(x, y))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)))
     (f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)), f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y)))
     (min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y))
     (twice# s x -> twice# x, twice# s x -> twice# x)}
    STATUS:
     arrows: 0.765432
     SCCS (4):
      Scc:
       {f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)),
        f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y))}
      Scc:
       {min#(s x, s y) -> min#(x, y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {twice# s x -> twice# x}
      
      SCC (2):
       Strict:
        {f#(s x, s y) -> f#(-(x, min(x, y)), s twice min(x, y)),
         f#(s x, s y) -> f#(-(y, min(x, y)), s twice min(x, y))}
       Weak:
       {    -(x, 0()) -> x,
          -(s x, s y) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
        min(s x, s y) -> s min(x, y),
            twice 0() -> 0(),
            twice s x -> s s twice x,
          f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
          f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {min#(s x, s y) -> min#(x, y)}
       Weak:
       {    -(x, 0()) -> x,
          -(s x, s y) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
        min(s x, s y) -> s min(x, y),
            twice 0() -> 0(),
            twice s x -> s s twice x,
          f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
          f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
       Open
      SCC (1):
       Strict:
        {-#(s x, s y) -> -#(x, y)}
       Weak:
       {    -(x, 0()) -> x,
          -(s x, s y) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
        min(s x, s y) -> s min(x, y),
            twice 0() -> 0(),
            twice s x -> s s twice x,
          f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
          f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
       Open
      SCC (1):
       Strict:
        {twice# s x -> twice# x}
       Weak:
       {    -(x, 0()) -> x,
          -(s x, s y) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
        min(s x, s y) -> s min(x, y),
            twice 0() -> 0(),
            twice s x -> s s twice x,
          f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y)),
          f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))}
       Open