YES
TRS:
 {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
  +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
           +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                 +(p2(), p1()) -> +(p1(), p2()),
                 +(+(x, y), z) -> +(x, +(y, z)),
        +(p1(), +(p2(), p2())) -> p5(),
  +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
           +(p1(), +(p1(), x)) -> +(p2(), x),
                 +(p1(), p1()) -> p2(),
                 +(p5(), p2()) -> +(p2(), p5()),
           +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
           +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
           +(p5(), +(p5(), x)) -> +(p10(), x),
                 +(p5(), p1()) -> +(p1(), p5()),
                 +(p5(), p5()) -> p10(),
                +(p10(), p2()) -> +(p2(), p10()),
          +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
          +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
          +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                +(p10(), p1()) -> +(p1(), p10()),
                +(p10(), p5()) -> +(p5(), p10())}
 DP:
  Strict:
   {      +#(p2(), +(p2(), p2())) -> +#(p1(), p5()),
    +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)),
    +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x),
             +#(p2(), +(p1(), x)) -> +#(p2(), x),
             +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)),
                   +#(p2(), p1()) -> +#(p1(), p2()),
                   +#(+(x, y), z) -> +#(x, +(y, z)),
                   +#(+(x, y), z) -> +#(y, z),
    +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x),
             +#(p1(), +(p1(), x)) -> +#(p2(), x),
                   +#(p5(), p2()) -> +#(p2(), p5()),
             +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)),
             +#(p5(), +(p2(), x)) -> +#(p5(), x),
             +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)),
             +#(p5(), +(p1(), x)) -> +#(p5(), x),
             +#(p5(), +(p5(), x)) -> +#(p10(), x),
                   +#(p5(), p1()) -> +#(p1(), p5()),
                  +#(p10(), p2()) -> +#(p2(), p10()),
            +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)),
            +#(p10(), +(p2(), x)) -> +#(p10(), x),
            +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)),
            +#(p10(), +(p1(), x)) -> +#(p10(), x),
            +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)),
            +#(p10(), +(p5(), x)) -> +#(p10(), x),
                  +#(p10(), p1()) -> +#(p1(), p10()),
                  +#(p10(), p5()) -> +#(p5(), p10())}
  Weak:
  {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
   +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
            +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                  +(p2(), p1()) -> +(p1(), p2()),
                  +(+(x, y), z) -> +(x, +(y, z)),
         +(p1(), +(p2(), p2())) -> p5(),
   +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
            +(p1(), +(p1(), x)) -> +(p2(), x),
                  +(p1(), p1()) -> p2(),
                  +(p5(), p2()) -> +(p2(), p5()),
            +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
            +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
            +(p5(), +(p5(), x)) -> +(p10(), x),
                  +(p5(), p1()) -> +(p1(), p5()),
                  +(p5(), p5()) -> p10(),
                 +(p10(), p2()) -> +(p2(), p10()),
           +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
           +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
           +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                 +(p10(), p1()) -> +(p1(), p10()),
                 +(p10(), p5()) -> +(p5(), p10())}
  EDG:
   {
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2()))
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(p2(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), p1()) -> +#(p1(), p2()))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(p1(), +(p1(), x)) -> +#(p2(), x), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5()))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(p5(), +(p1(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(p10(), +(p2(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(p10(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), p1()) -> +#(p1(), p10()))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), p1()) -> +#(p1(), p5()))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), p1()) -> +#(p1(), p2()))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(y, z), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), p2())) -> +#(p1(), p5()))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p2(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)), +#(p1(), +(p1(), x)) -> +#(p2(), x))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()))
    (+#(p10(), +(p1(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p2()) -> +#(p2(), p10()))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p2(), x)) -> +#(p10(), x))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p1(), x)) -> +#(p10(), x))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), +(p5(), x)) -> +#(p10(), x))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p1()) -> +#(p1(), p10()))
    (+#(p5(), +(p5(), x)) -> +#(p10(), x), +#(p10(), p5()) -> +#(p5(), p10()))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(p5(), +(p2(), x)) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5()))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5()))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p2()) -> +#(p2(), p5()))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p2(), x)) -> +#(p5(), x))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p1(), x)) -> +#(p5(), x))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), +(p5(), x)) -> +#(p10(), x))
    (+#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x), +#(p5(), p1()) -> +#(p1(), p5()))
   }
   SCCS:
    Scc:
     {+#(+(x, y), z) -> +#(x, +(y, z)),
      +#(+(x, y), z) -> +#(y, z)}
    Scc:
     {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)),
      +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x),
               +#(p2(), +(p1(), x)) -> +#(p2(), x),
               +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)),
      +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x),
               +#(p1(), +(p1(), x)) -> +#(p2(), x),
               +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)),
               +#(p5(), +(p2(), x)) -> +#(p5(), x),
               +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)),
               +#(p5(), +(p1(), x)) -> +#(p5(), x),
               +#(p5(), +(p5(), x)) -> +#(p10(), x),
              +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)),
              +#(p10(), +(p2(), x)) -> +#(p10(), x),
              +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)),
              +#(p10(), +(p1(), x)) -> +#(p10(), x),
              +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)),
              +#(p10(), +(p5(), x)) -> +#(p10(), x)}
    SCC:
     Strict:
      {+#(+(x, y), z) -> +#(x, +(y, z)),
       +#(+(x, y), z) -> +#(y, z)}
     Weak:
     {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
      +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
               +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                     +(p2(), p1()) -> +(p1(), p2()),
                     +(+(x, y), z) -> +(x, +(y, z)),
            +(p1(), +(p2(), p2())) -> p5(),
      +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
               +(p1(), +(p1(), x)) -> +(p2(), x),
                     +(p1(), p1()) -> p2(),
                     +(p5(), p2()) -> +(p2(), p5()),
               +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
               +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
               +(p5(), +(p5(), x)) -> +(p10(), x),
                     +(p5(), p1()) -> +(p1(), p5()),
                     +(p5(), p5()) -> p10(),
                    +(p10(), p2()) -> +(p2(), p10()),
              +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
              +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
              +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                    +(p10(), p1()) -> +(p1(), p10()),
                    +(p10(), p5()) -> +(p5(), p10())}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {+#(+(x, y), z) -> +#(y, z)}
      EDG:
       {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))}
       SCCS:
        Scc:
         {+#(+(x, y), z) -> +#(y, z)}
        SCC:
         Strict:
          {+#(+(x, y), z) -> +#(y, z)}
         Weak:
         {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
          +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
                   +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                         +(p2(), p1()) -> +(p1(), p2()),
                         +(+(x, y), z) -> +(x, +(y, z)),
                +(p1(), +(p2(), p2())) -> p5(),
          +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
                   +(p1(), +(p1(), x)) -> +(p2(), x),
                         +(p1(), p1()) -> p2(),
                         +(p5(), p2()) -> +(p2(), p5()),
                   +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
                   +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
                   +(p5(), +(p5(), x)) -> +(p10(), x),
                         +(p5(), p1()) -> +(p1(), p5()),
                         +(p5(), p5()) -> p10(),
                        +(p10(), p2()) -> +(p2(), p10()),
                  +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
                  +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
                  +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                        +(p10(), p1()) -> +(p1(), p10()),
                        +(p10(), p5()) -> +(p5(), p10())}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)),
       +#(p2(), +(p2(), +(p2(), x))) -> +#(p5(), x),
                +#(p2(), +(p1(), x)) -> +#(p2(), x),
                +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)),
       +#(p1(), +(p2(), +(p2(), x))) -> +#(p5(), x),
                +#(p1(), +(p1(), x)) -> +#(p2(), x),
                +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)),
                +#(p5(), +(p2(), x)) -> +#(p5(), x),
                +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)),
                +#(p5(), +(p1(), x)) -> +#(p5(), x),
                +#(p5(), +(p5(), x)) -> +#(p10(), x),
               +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)),
               +#(p10(), +(p2(), x)) -> +#(p10(), x),
               +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)),
               +#(p10(), +(p1(), x)) -> +#(p10(), x),
               +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)),
               +#(p10(), +(p5(), x)) -> +#(p10(), x)}
     Weak:
     {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
      +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
               +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                     +(p2(), p1()) -> +(p1(), p2()),
                     +(+(x, y), z) -> +(x, +(y, z)),
            +(p1(), +(p2(), p2())) -> p5(),
      +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
               +(p1(), +(p1(), x)) -> +(p2(), x),
                     +(p1(), p1()) -> p2(),
                     +(p5(), p2()) -> +(p2(), p5()),
               +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
               +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
               +(p5(), +(p5(), x)) -> +(p10(), x),
                     +(p5(), p1()) -> +(p1(), p5()),
                     +(p5(), p5()) -> p10(),
                    +(p10(), p2()) -> +(p2(), p10()),
              +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
              +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
              +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                    +(p10(), p1()) -> +(p1(), p10()),
                    +(p10(), p5()) -> +(p5(), p10())}
     POLY:
      Argument Filtering:
       pi(p10) = [], pi(p5) = [], pi(p1) = [], pi(+#) = [0,1], pi(+) = [0,1], pi(p2) = []
      Usable Rules:
       {}
      Interpretation:
       [+#](x0, x1) = x0 + x1,
       [+](x0, x1) = x0 + x1 + 1,
       [p10] = 0,
       [p5] = 1,
       [p1] = 0,
       [p2] = 0
      Strict:
       {+#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)),
                 +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)),
                 +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)),
                 +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)),
                +#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)),
                +#(p10(), +(p1(), x)) -> +#(p1(), +(p10(), x)),
                +#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x))}
      Weak:
       {      +(p2(), +(p2(), p2())) -> +(p1(), p5()),
        +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x)),
                 +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x)),
                       +(p2(), p1()) -> +(p1(), p2()),
                       +(+(x, y), z) -> +(x, +(y, z)),
              +(p1(), +(p2(), p2())) -> p5(),
        +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x),
                 +(p1(), +(p1(), x)) -> +(p2(), x),
                       +(p1(), p1()) -> p2(),
                       +(p5(), p2()) -> +(p2(), p5()),
                 +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x)),
                 +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x)),
                 +(p5(), +(p5(), x)) -> +(p10(), x),
                       +(p5(), p1()) -> +(p1(), p5()),
                       +(p5(), p5()) -> p10(),
                      +(p10(), p2()) -> +(p2(), p10()),
                +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x)),
                +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x)),
                +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x)),
                      +(p10(), p1()) -> +(p1(), p10()),
                      +(p10(), p5()) -> +(p5(), p10())}
      EDG:
       {(+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)))
        (+#(p10(), +(p5(), x)) -> +#(p5(), +(p10(), x)), +#(p5(), +(p1(), x)) -> +#(p1(), +(p5(), x)))
        (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
        (+#(p10(), +(p2(), x)) -> +#(p2(), +(p10(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))
        (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p2(), +(p2(), x))) -> +#(p1(), +(p5(), x)))
        (+#(p5(), +(p2(), x)) -> +#(p2(), +(p5(), x)), +#(p2(), +(p1(), x)) -> +#(p1(), +(p2(), x)))}
       SCCS:
        
        Qed