(VAR x1 )
(RULES 
        twoto(0(x1)) -> p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1))))))))))))))))
        twoto(s(x1)) -> p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))
        twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1)))))))))))))
        twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1)))))))))))))))))))
        p(p(s(x1))) -> p(x1)
        p(s(x1)) -> x1
        p(0(x1)) -> 0(s(s(s(s(p(s(x1)))))))
        0(x1) -> x1
        
)