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 ]
Try persistent and layer-preserving decomposition...
Sort Assignment:
 0 : 19=>19
 p : 19=>19
 s : 19=>19
 sq : 19=>19
 twice : 19=>19
maximal types: {19}
...decomposition failed.
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 ]
unknown Non-Omega-Overlapping
unknown Right-Reducible
Check distinct normal forms in critical pair closure
convertible distinct normal forms: p(?x) = s(s(s(s(s(s(s(s(s(s(s(?x)))))))))))
problems/954.trs: Success(not UNC)
(8 msec.)