MAYBE
MAYBE
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())
 }
 DUP: We consider a non-duplicating system.
  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())
   }
  Fail