MAYBE
Time: 5.415576
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))}
  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))}
      Fail
     
     
     
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [-](x0, x1) = x0 + 1,
        
        [min](x0, x1) = x0 + x1 + 1,
        
        [f](x0, x1) = x0 + x1,
        
        [s](x0) = x0 + 1,
        
        [twice](x0) = x0 + 1,
        
        [0] = 1,
        
        [min#](x0, x1) = x0
       Strict:
        min#(s x, s y) -> min#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))
        2 + 1x + 1y >= 5 + 2x + 2y
        f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y))
        2 + 1x + 1y >= 5 + 2x + 2y
        twice s x -> s s twice x
        2 + 1x >= 3 + 1x
        twice 0() -> 0()
        2 >= 1
        min(s x, s y) -> s min(x, y)
        3 + 1x + 1y >= 2 + 1x + 1y
        min(0(), y) -> 0()
        2 + 1y >= 1
        min(x, 0()) -> 0()
        2 + 1x >= 1
        -(s x, s y) -> -(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        -(x, 0()) -> x
        2 + 0x >= 1x
      Qed
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [-](x0, x1) = x0 + 1,
       
       [min](x0, x1) = x0 + x1 + 1,
       
       [f](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 1,
       
       [twice](x0) = x0 + 1,
       
       [0] = 1,
       
       [-#](x0, x1) = x0
      Strict:
       -#(s x, s y) -> -#(x, y)
       1 + 0x + 1y >= 0 + 0x + 1y
      Weak:
       f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))
       2 + 1x + 1y >= 5 + 2x + 2y
       f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y))
       2 + 1x + 1y >= 5 + 2x + 2y
       twice s x -> s s twice x
       2 + 1x >= 3 + 1x
       twice 0() -> 0()
       2 >= 1
       min(s x, s y) -> s min(x, y)
       3 + 1x + 1y >= 2 + 1x + 1y
       min(0(), y) -> 0()
       2 + 1y >= 1
       min(x, 0()) -> 0()
       2 + 1x >= 1
       -(s x, s y) -> -(x, y)
       2 + 0x + 1y >= 1 + 0x + 1y
       -(x, 0()) -> x
       2 + 0x >= 1x
     Qed
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [-](x0, x1) = x0 + 1,
       
       [min](x0, x1) = x0 + x1 + 1,
       
       [f](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [twice](x0) = x0 + 1,
       
       [0] = 1,
       
       [twice#](x0) = x0
      Strict:
       twice# s x -> twice# x
       1 + 1x >= 0 + 1x
      Weak:
       f(s x, s y) -> f(-(y, min(x, y)), s twice min(x, y))
       2 + 1x + 0y >= 3 + 1x + 1y
       f(s x, s y) -> f(-(x, min(x, y)), s twice min(x, y))
       2 + 1x + 0y >= 3 + 1x + 1y
       twice s x -> s s twice x
       2 + 1x >= 3 + 1x
       twice 0() -> 0()
       2 >= 1
       min(s x, s y) -> s min(x, y)
       3 + 1x + 1y >= 2 + 1x + 1y
       min(0(), y) -> 0()
       2 + 1y >= 1
       min(x, 0()) -> 0()
       2 + 1x >= 1
       -(s x, s y) -> -(x, y)
       2 + 0x + 1y >= 1 + 0x + 1y
       -(x, 0()) -> x
       2 + 0x >= 1x
     Qed