(VAR x1 )
(RULES 
        v(s(x1)) -> s(p(p(s(s(s(s(s(s(s(s(w(p(p(s(s(p(s(p(s(x1))))))))))))))))))))
        v(0(x1)) -> p(p(s(s(0(p(p(s(s(s(s(s(x1))))))))))))
        w(s(x1)) -> s(s(s(s(s(s(p(p(s(s(v(p(p(s(s(s(p(p(s(s(x1))))))))))))))))))))
        w(0(x1)) -> p(s(p(p(p(p(p(p(p(p(s(s(0(s(s(s(s(s(s(x1)))))))))))))))))))
        p(p(s(x1))) -> p(x1)
        p(s(x1)) -> x1
        p(0(x1)) -> 0(s(s(s(s(s(s(s(p(s(x1))))))))))
        
)