YES

Problem:
 s(p(x)) -> x
 p(s(x)) -> x

Proof:
 Church Rosser Transformation Processor:
  
  critical peaks: joinable
  Qed