(VAR x y z )
(RULES 
        p(0) -> 0
        p(s(x)) -> x
        plus(x, 0) -> x
        plus(0, y) -> y
        plus(s(x), y) -> s(plus(x, y))
        plus(s(x), y) -> s(plus(p(s(x)), y))
        plus(x, s(y)) -> s(plus(x, p(s(y))))
        times(0, y) -> 0
        times(s(0), y) -> y
        times(s(x), y) -> plus(y, times(x, y))
        div(0, y) -> 0
        div(x, y) -> quot(x, y, y)
        quot(zero(y), s(y), z) -> 0
        quot(s(x), s(y), z) -> quot(x, y, z)
        quot(x, 0, s(z)) -> s(div(x, s(z)))
        div(div(x, y), z) -> div(x, times(zero(y), z))
        eq(0, 0) -> true
        eq(s(x), 0) -> false
        eq(0, s(y)) -> false
        eq(s(x), s(y)) -> eq(x, y)
        divides(y, x) -> eq(x, times(div(x, y), y))
        prime(s(s(x))) -> pr(s(s(x)), s(x))
        pr(x, s(0)) -> true
        pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
        if(true, x, y) -> false
        if(false, x, y) -> pr(x, y)
        zero(div(x, x)) -> x
        zero(divides(x, x)) -> x
        zero(times(x, x)) -> x
        zero(quot(x, x, x)) -> x
        zero(s(x)) -> if(eq(x, s(0)), plus(zero(0), 0), s(plus(0, zero(0))))
        
)