YES
Time: 0.303173
TRS:
 {    p s x -> x,
      s p x -> x,
  +(p x, y) -> p +(x, y),
  +(s x, y) -> s +(x, y),
  +(0(), y) -> y,
  minus p x -> s minus x,
  minus s x -> p minus x,
  minus 0() -> 0(),
  *(p x, y) -> +(*(x, y), minus y),
  *(s x, y) -> +(*(x, y), y),
  *(0(), y) -> 0()}
 DP:
  DP:
   {+#(p x, y) -> p# +(x, y),
    +#(p x, y) -> +#(x, y),
    +#(s x, y) -> s# +(x, y),
    +#(s x, y) -> +#(x, y),
    minus# p x -> s# minus x,
    minus# p x -> minus# x,
    minus# s x -> p# minus x,
    minus# s x -> minus# x,
    *#(p x, y) -> +#(*(x, y), minus y),
    *#(p x, y) -> minus# y,
    *#(p x, y) -> *#(x, y),
    *#(s x, y) -> +#(*(x, y), y),
    *#(s x, y) -> *#(x, y)}
  TRS:
  {    p s x -> x,
       s p x -> x,
   +(p x, y) -> p +(x, y),
   +(s x, y) -> s +(x, y),
   +(0(), y) -> y,
   minus p x -> s minus x,
   minus s x -> p minus x,
   minus 0() -> 0(),
   *(p x, y) -> +(*(x, y), minus y),
   *(s x, y) -> +(*(x, y), y),
   *(0(), y) -> 0()}
  EDG:
   {(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
    (+#(s x, y) -> +#(x, y), +#(s x, y) -> s# +(x, y))
    (+#(s x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
    (+#(s x, y) -> +#(x, y), +#(p x, y) -> p# +(x, y))
    (*#(s x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
    (*#(s x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
    (*#(s x, y) -> *#(x, y), *#(p x, y) -> *#(x, y))
    (*#(s x, y) -> *#(x, y), *#(p x, y) -> minus# y)
    (*#(s x, y) -> *#(x, y), *#(p x, y) -> +#(*(x, y), minus y))
    (minus# p x -> minus# x, minus# s x -> minus# x)
    (minus# p x -> minus# x, minus# s x -> p# minus x)
    (minus# p x -> minus# x, minus# p x -> minus# x)
    (minus# p x -> minus# x, minus# p x -> s# minus x)
    (*#(p x, y) -> minus# y, minus# s x -> minus# x)
    (*#(p x, y) -> minus# y, minus# s x -> p# minus x)
    (*#(p x, y) -> minus# y, minus# p x -> minus# x)
    (*#(p x, y) -> minus# y, minus# p x -> s# minus x)
    (*#(p x, y) -> +#(*(x, y), minus y), +#(p x, y) -> p# +(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(p x, y) -> +#(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(s x, y) -> s# +(x, y))
    (*#(p x, y) -> +#(*(x, y), minus y), +#(s x, y) -> +#(x, y))
    (minus# s x -> minus# x, minus# p x -> s# minus x)
    (minus# s x -> minus# x, minus# p x -> minus# x)
    (minus# s x -> minus# x, minus# s x -> p# minus x)
    (minus# s x -> minus# x, minus# s x -> minus# x)
    (*#(s x, y) -> +#(*(x, y), y), +#(p x, y) -> p# +(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(p x, y) -> +#(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(s x, y) -> s# +(x, y))
    (*#(s x, y) -> +#(*(x, y), y), +#(s x, y) -> +#(x, y))
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> +#(*(x, y), minus y))
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> minus# y)
    (*#(p x, y) -> *#(x, y), *#(p x, y) -> *#(x, y))
    (*#(p x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
    (*#(p x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
    (+#(p x, y) -> +#(x, y), +#(p x, y) -> p# +(x, y))
    (+#(p x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
    (+#(p x, y) -> +#(x, y), +#(s x, y) -> s# +(x, y))
    (+#(p x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))}
   STATUS:
    arrows: 0.775148
    SCCS (3):
     Scc:
      {*#(p x, y) -> *#(x, y),
       *#(s x, y) -> *#(x, y)}
     Scc:
      {minus# p x -> minus# x,
       minus# s x -> minus# x}
     Scc:
      {+#(p x, y) -> +#(x, y),
       +#(s x, y) -> +#(x, y)}
     
     SCC (2):
      Strict:
       {*#(p x, y) -> *#(x, y),
        *#(s x, y) -> *#(x, y)}
      Weak:
      {    p s x -> x,
           s p x -> x,
       +(p x, y) -> p +(x, y),
       +(s x, y) -> s +(x, y),
       +(0(), y) -> y,
       minus p x -> s minus x,
       minus s x -> p minus x,
       minus 0() -> 0(),
       *(p x, y) -> +(*(x, y), minus y),
       *(s x, y) -> +(*(x, y), y),
       *(0(), y) -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0,
        
        [*](x0, x1) = 0,
        
        [p](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [minus](x0) = x0 + 1,
        
        [0] = 1,
        
        [*#](x0, x1) = x0
       Strict:
        *#(s x, y) -> *#(x, y)
        1 + 1x + 0y >= 0 + 1x + 0y
        *#(p x, y) -> *#(x, y)
        0 + 1x + 0y >= 0 + 1x + 0y
       Weak:
        *(0(), y) -> 0()
        0 + 0y >= 1
        *(s x, y) -> +(*(x, y), y)
        0 + 0x + 0y >= 0 + 0x + 1y
        *(p x, y) -> +(*(x, y), minus y)
        0 + 0x + 0y >= 1 + 0x + 1y
        minus 0() -> 0()
        2 >= 1
        minus s x -> p minus x
        2 + 1x >= 1 + 1x
        minus p x -> s minus x
        1 + 1x >= 2 + 1x
        +(0(), y) -> y
        0 + 1y >= 1y
        +(s x, y) -> s +(x, y)
        0 + 0x + 1y >= 1 + 0x + 1y
        +(p x, y) -> p +(x, y)
        0 + 0x + 1y >= 0 + 0x + 1y
        s p x -> x
        1 + 1x >= 1x
        p s x -> x
        1 + 1x >= 1x
      SCCS (1):
       Scc:
        {*#(p x, y) -> *#(x, y)}
       
       SCC (1):
        Strict:
         {*#(p x, y) -> *#(x, y)}
        Weak:
        {    p s x -> x,
             s p x -> x,
         +(p x, y) -> p +(x, y),
         +(s x, y) -> s +(x, y),
         +(0(), y) -> y,
         minus p x -> s minus x,
         minus s x -> p minus x,
         minus 0() -> 0(),
         *(p x, y) -> +(*(x, y), minus y),
         *(s x, y) -> +(*(x, y), y),
         *(0(), y) -> 0()}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [+](x0, x1) = x0 + 1,
          
          [*](x0, x1) = 0,
          
          [p](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [minus](x0) = x0 + 1,
          
          [0] = 1,
          
          [*#](x0, x1) = x0
         Strict:
          *#(p x, y) -> *#(x, y)
          1 + 1x + 0y >= 0 + 1x + 0y
         Weak:
          *(0(), y) -> 0()
          0 + 0y >= 1
          *(s x, y) -> +(*(x, y), y)
          0 + 0x + 0y >= 1 + 0x + 0y
          *(p x, y) -> +(*(x, y), minus y)
          0 + 0x + 0y >= 1 + 0x + 0y
          minus 0() -> 0()
          2 >= 1
          minus s x -> p minus x
          2 + 1x >= 2 + 1x
          minus p x -> s minus x
          2 + 1x >= 2 + 1x
          +(0(), y) -> y
          2 + 0y >= 1y
          +(s x, y) -> s +(x, y)
          2 + 1x + 0y >= 2 + 1x + 0y
          +(p x, y) -> p +(x, y)
          2 + 1x + 0y >= 2 + 1x + 0y
          s p x -> x
          2 + 1x >= 1x
          p s x -> x
          2 + 1x >= 1x
        Qed
    
    
    SCC (2):
     Strict:
      {minus# p x -> minus# x,
       minus# s x -> minus# x}
     Weak:
     {    p s x -> x,
          s p x -> x,
      +(p x, y) -> p +(x, y),
      +(s x, y) -> s +(x, y),
      +(0(), y) -> y,
      minus p x -> s minus x,
      minus s x -> p minus x,
      minus 0() -> 0(),
      *(p x, y) -> +(*(x, y), minus y),
      *(s x, y) -> +(*(x, y), y),
      *(0(), y) -> 0()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [+](x0, x1) = x0,
       
       [*](x0, x1) = 0,
       
       [p](x0) = x0,
       
       [s](x0) = x0 + 1,
       
       [minus](x0) = x0 + 1,
       
       [0] = 1,
       
       [minus#](x0) = x0
      Strict:
       minus# s x -> minus# x
       1 + 1x >= 0 + 1x
       minus# p x -> minus# x
       0 + 1x >= 0 + 1x
      Weak:
       *(0(), y) -> 0()
       0 + 0y >= 1
       *(s x, y) -> +(*(x, y), y)
       0 + 0x + 0y >= 0 + 0x + 1y
       *(p x, y) -> +(*(x, y), minus y)
       0 + 0x + 0y >= 1 + 0x + 1y
       minus 0() -> 0()
       2 >= 1
       minus s x -> p minus x
       2 + 1x >= 1 + 1x
       minus p x -> s minus x
       1 + 1x >= 2 + 1x
       +(0(), y) -> y
       0 + 1y >= 1y
       +(s x, y) -> s +(x, y)
       0 + 0x + 1y >= 1 + 0x + 1y
       +(p x, y) -> p +(x, y)
       0 + 0x + 1y >= 0 + 0x + 1y
       s p x -> x
       1 + 1x >= 1x
       p s x -> x
       1 + 1x >= 1x
     SCCS (1):
      Scc:
       {minus# p x -> minus# x}
      
      SCC (1):
       Strict:
        {minus# p x -> minus# x}
       Weak:
       {    p s x -> x,
            s p x -> x,
        +(p x, y) -> p +(x, y),
        +(s x, y) -> s +(x, y),
        +(0(), y) -> y,
        minus p x -> s minus x,
        minus s x -> p minus x,
        minus 0() -> 0(),
        *(p x, y) -> +(*(x, y), minus y),
        *(s x, y) -> +(*(x, y), y),
        *(0(), y) -> 0()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + 1,
         
         [*](x0, x1) = 0,
         
         [p](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [minus](x0) = x0 + 1,
         
         [0] = 1,
         
         [minus#](x0) = x0
        Strict:
         minus# p x -> minus# x
         1 + 1x >= 0 + 1x
        Weak:
         *(0(), y) -> 0()
         0 + 0y >= 1
         *(s x, y) -> +(*(x, y), y)
         0 + 0x + 0y >= 1 + 0x + 0y
         *(p x, y) -> +(*(x, y), minus y)
         0 + 0x + 0y >= 1 + 0x + 0y
         minus 0() -> 0()
         2 >= 1
         minus s x -> p minus x
         2 + 1x >= 2 + 1x
         minus p x -> s minus x
         2 + 1x >= 2 + 1x
         +(0(), y) -> y
         2 + 0y >= 1y
         +(s x, y) -> s +(x, y)
         2 + 1x + 0y >= 2 + 1x + 0y
         +(p x, y) -> p +(x, y)
         2 + 1x + 0y >= 2 + 1x + 0y
         s p x -> x
         2 + 1x >= 1x
         p s x -> x
         2 + 1x >= 1x
       Qed
   
   
   
   SCC (2):
    Strict:
     {+#(p x, y) -> +#(x, y),
      +#(s x, y) -> +#(x, y)}
    Weak:
    {    p s x -> x,
         s p x -> x,
     +(p x, y) -> p +(x, y),
     +(s x, y) -> s +(x, y),
     +(0(), y) -> y,
     minus p x -> s minus x,
     minus s x -> p minus x,
     minus 0() -> 0(),
     *(p x, y) -> +(*(x, y), minus y),
     *(s x, y) -> +(*(x, y), y),
     *(0(), y) -> 0()}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [+](x0, x1) = x0,
      
      [*](x0, x1) = 0,
      
      [p](x0) = x0,
      
      [s](x0) = x0 + 1,
      
      [minus](x0) = x0 + 1,
      
      [0] = 1,
      
      [+#](x0, x1) = x0
     Strict:
      +#(s x, y) -> +#(x, y)
      1 + 1x + 0y >= 0 + 1x + 0y
      +#(p x, y) -> +#(x, y)
      0 + 1x + 0y >= 0 + 1x + 0y
     Weak:
      *(0(), y) -> 0()
      0 + 0y >= 1
      *(s x, y) -> +(*(x, y), y)
      0 + 0x + 0y >= 0 + 0x + 1y
      *(p x, y) -> +(*(x, y), minus y)
      0 + 0x + 0y >= 1 + 0x + 1y
      minus 0() -> 0()
      2 >= 1
      minus s x -> p minus x
      2 + 1x >= 1 + 1x
      minus p x -> s minus x
      1 + 1x >= 2 + 1x
      +(0(), y) -> y
      0 + 1y >= 1y
      +(s x, y) -> s +(x, y)
      0 + 0x + 1y >= 1 + 0x + 1y
      +(p x, y) -> p +(x, y)
      0 + 0x + 1y >= 0 + 0x + 1y
      s p x -> x
      1 + 1x >= 1x
      p s x -> x
      1 + 1x >= 1x
    SCCS (1):
     Scc:
      {+#(p x, y) -> +#(x, y)}
     
     SCC (1):
      Strict:
       {+#(p x, y) -> +#(x, y)}
      Weak:
      {    p s x -> x,
           s p x -> x,
       +(p x, y) -> p +(x, y),
       +(s x, y) -> s +(x, y),
       +(0(), y) -> y,
       minus p x -> s minus x,
       minus s x -> p minus x,
       minus 0() -> 0(),
       *(p x, y) -> +(*(x, y), minus y),
       *(s x, y) -> +(*(x, y), y),
       *(0(), y) -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [+](x0, x1) = x0 + 1,
        
        [*](x0, x1) = 0,
        
        [p](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [minus](x0) = x0 + 1,
        
        [0] = 1,
        
        [+#](x0, x1) = x0
       Strict:
        +#(p x, y) -> +#(x, y)
        1 + 1x + 0y >= 0 + 1x + 0y
       Weak:
        *(0(), y) -> 0()
        0 + 0y >= 1
        *(s x, y) -> +(*(x, y), y)
        0 + 0x + 0y >= 1 + 0x + 0y
        *(p x, y) -> +(*(x, y), minus y)
        0 + 0x + 0y >= 1 + 0x + 0y
        minus 0() -> 0()
        2 >= 1
        minus s x -> p minus x
        2 + 1x >= 2 + 1x
        minus p x -> s minus x
        2 + 1x >= 2 + 1x
        +(0(), y) -> y
        2 + 0y >= 1y
        +(s x, y) -> s +(x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        +(p x, y) -> p +(x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        s p x -> x
        2 + 1x >= 1x
        p s x -> x
        2 + 1x >= 1x
      Qed