MAYBE
Time: 0.001732
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),
  plus(s plus(x, y), z) -> s plus(plus(x, y), z)}
 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),
    plus#(s plus(x, y), z) -> plus#(plus(x, y), z)}
  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),
   plus(s plus(x, y), z) -> s plus(plus(x, y), z)}
  UR:
   {        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),
    plus(s plus(x, y), z) -> s plus(plus(x, y), z),
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(minus(x, y), double 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#(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) -> minus#(x, y))
     (plus#(s x, y) -> double# y, double# s x -> double# x)
     (plus#(s x, y) -> plus#(minus(x, y), double y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z))
     (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))
     (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))
     (plus#(s x, y) -> plus#(x, s y), plus#(s plus(x, y), z) -> plus#(plus(x, y), z))
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> minus#(x, y))
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> double# y)
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(x, y))
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(x, s y))
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s x, y) -> plus#(minus(x, y), double y))
     (plus#(s plus(x, y), z) -> plus#(plus(x, y), z), plus#(s plus(x, y), z) -> plus#(plus(x, y), z))
     (plus#(s x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (double# s x -> double# x, double# s x -> double# x)}
    STATUS:
     arrows: 0.562500
     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),
        plus#(s plus(x, y), z) -> plus#(plus(x, y), z)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {double# s x -> double# x}
      
      SCC (4):
       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),
         plus#(s plus(x, y), z) -> plus#(plus(x, y), z)}
       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),
        plus(s plus(x, y), z) -> s plus(plus(x, y), z)}
       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),
        plus(s plus(x, y), z) -> s plus(plus(x, y), z)}
       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),
        plus(s plus(x, y), z) -> s plus(plus(x, y), z)}
       Open