MAYBE
Time: 0.076002
TRS:
 {  minus(x, 0()) -> x,
  minus(s x, s y) -> minus(x, y),
       double 0() -> 0(),
       double s x -> s s double x,
     plus(0(), y) -> y,
     plus(s x, y) -> s plus(x, y),
     plus(s x, y) -> s plus(minus(x, y), double y),
     plus(s x, y) -> plus(x, s y)}
 DP:
  DP:
   {minus#(s x, s y) -> minus#(x, y),
         double# s x -> double# x,
       plus#(s x, y) -> minus#(x, y),
       plus#(s x, y) -> double# y,
       plus#(s x, y) -> plus#(x, y),
       plus#(s x, y) -> plus#(x, s y),
       plus#(s x, y) -> plus#(minus(x, y), double y)}
  TRS:
  {  minus(x, 0()) -> x,
   minus(s x, s y) -> minus(x, y),
        double 0() -> 0(),
        double s x -> s s double x,
      plus(0(), y) -> y,
      plus(s x, y) -> s plus(x, y),
      plus(s x, y) -> s plus(minus(x, y), double y),
      plus(s x, y) -> plus(x, s y)}
  UR:
   {  minus(x, 0()) -> x,
    minus(s x, s y) -> minus(x, y),
         double 0() -> 0(),
         double s x -> s s double x,
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(minus(x, y), double y))
     (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, s y))
     (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> double# y)
     (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s x, y) -> minus#(x, y))
     (double# s x -> double# x, double# s x -> double# x)
     (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> double# y)
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, s y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(minus(x, y), double y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (plus#(s x, y) -> double# y, double# s x -> double# x)
     (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> double# y)
     (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y))
     (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(minus(x, y), double y))}
    STATUS:
     arrows: 0.612245
     SCCS (3):
      Scc:
       {plus#(s x, y) -> plus#(x, y),
        plus#(s x, y) -> plus#(x, s y),
        plus#(s x, y) -> plus#(minus(x, y), double y)}
      Scc:
       {double# s x -> double# x}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      
      SCC (3):
       Strict:
        {plus#(s x, y) -> plus#(x, y),
         plus#(s x, y) -> plus#(x, s y),
         plus#(s x, y) -> plus#(minus(x, y), double y)}
       Weak:
       {  minus(x, 0()) -> x,
        minus(s x, s y) -> minus(x, y),
             double 0() -> 0(),
             double s x -> s s double x,
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(x, y),
           plus(s x, y) -> s plus(minus(x, y), double y),
           plus(s x, y) -> plus(x, s y)}
       Open
      
      SCC (1):
       Strict:
        {double# s x -> double# x}
       Weak:
       {  minus(x, 0()) -> x,
        minus(s x, s y) -> minus(x, y),
             double 0() -> 0(),
             double s x -> s s double x,
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(x, y),
           plus(s x, y) -> s plus(minus(x, y), double y),
           plus(s x, y) -> plus(x, s y)}
       Open
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {  minus(x, 0()) -> x,
        minus(s x, s y) -> minus(x, y),
             double 0() -> 0(),
             double s x -> s s double x,
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(x, y),
           plus(s x, y) -> s plus(minus(x, y), double y),
           plus(s x, y) -> plus(x, s y)}
       Open