MAYBE
(ignored inputs)COMMENT TPDB SRS_Standard/Secret_06_SRS/aprove04
Rewrite Rules:
   [ 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 ]
Apply Direct Methods...
Inner CPs:
   [ sq(?x_7) = p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(?x_7))))))))))))))))),
     twice(?x_7) = 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_7))))))))))))))))))))))))))),
     p(?x_5) = p(?x_5),
     p(?x_7) = 0(s(s(s(s(s(s(s(s(s(s(s(?x_7)))))))))))) ]
Outer CPs:
   [  ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
954.trs: Failure(unknown CR)
(0 msec.)