NO
(ignored inputs)COMMENT TPDB SRS_Standard/Secret_06_SRS/aprove04
input TRS:
   [ sq(0(?x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(?x))))))))))))))))),
     sq(s(?x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(?x))))))))))))))))))))))))))))))))),
     twice(0(?x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(?x))))))))))))))))))))))))))),
     twice(s(?x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(?x))))))))))))))),
     p(p(s(?x))) -> p(?x),
     p(s(?x)) -> ?x,
     p(0(?x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(?x)))))))))))),
     0(?x) -> ?x ]
TRS:
   [ sq(0(?x)) -> p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(?x))))))))))))))))),
     sq(s(?x)) -> s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(?x))))))))))))))))))))))))))))))))),
     twice(0(?x)) -> p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(?x))))))))))))))))))))))))))),
     twice(s(?x)) -> p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(?x))))))))))))))),
     p(p(s(?x))) -> p(?x),
     p(s(?x)) -> ?x,
     p(0(?x)) -> 0(s(s(s(s(s(s(s(s(s(s(s(?x)))))))))))),
     0(?x) -> ?x ]
New rules by rule reversing:
   [ p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(?x))))))))))))))))) -> sq(0(?x)),
     sq(s(?x)) -> sq(s(?x)),
     s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(?x))))))))))))))))))))))))))))))))) -> sq(s(?x)),
     p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(?x))))))))))))))))))))))))))) -> twice(0(?x)),
     twice(s(?x)) -> twice(s(?x)),
     p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(?x))))))))))))))) -> twice(s(?x)),
     p(p(s(?x))) -> p(?x),
     p(s(?x)) -> ?x,
     0(s(s(s(s(s(s(s(s(s(s(s(?x)))))))))))) -> p(0(?x)),
     0(?x) -> ?x ]
Check distinct normal forms in critical pair closure
convertible distinct normal forms: s(s(s(s(s(s(s(s(s(s(s(?x_1))))))))))) = p(?x_1)
problems/954.trs: Success(not UNC)
(4 msec.)