(VAR X X1 X2 X3 Y )
(RULES 
        active(p(0)) -> mark(0)
        active(p(s(X))) -> mark(X)
        active(leq(0, Y)) -> mark(true)
        active(leq(s(X), 0)) -> mark(false)
        active(leq(s(X), s(Y))) -> mark(leq(X, Y))
        active(if(true, X, Y)) -> mark(X)
        active(if(false, X, Y)) -> mark(Y)
        active(diff(X, Y)) -> mark(if(leq(X, Y), 0, s(diff(p(X), Y))))
        mark(p(X)) -> active(p(mark(X)))
        mark(0) -> active(0)
        mark(s(X)) -> active(s(mark(X)))
        mark(leq(X1, X2)) -> active(leq(mark(X1), mark(X2)))
        mark(true) -> active(true)
        mark(false) -> active(false)
        mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3))
        mark(diff(X1, X2)) -> active(diff(mark(X1), mark(X2)))
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        leq(mark(X1), X2) -> leq(X1, X2)
        leq(X1, mark(X2)) -> leq(X1, X2)
        leq(active(X1), X2) -> leq(X1, X2)
        leq(X1, active(X2)) -> leq(X1, X2)
        if(mark(X1), X2, X3) -> if(X1, X2, X3)
        if(X1, mark(X2), X3) -> if(X1, X2, X3)
        if(X1, X2, mark(X3)) -> if(X1, X2, X3)
        if(active(X1), X2, X3) -> if(X1, X2, X3)
        if(X1, active(X2), X3) -> if(X1, X2, X3)
        if(X1, X2, active(X3)) -> if(X1, X2, X3)
        diff(mark(X1), X2) -> diff(X1, X2)
        diff(X1, mark(X2)) -> diff(X1, X2)
        diff(active(X1), X2) -> diff(X1, X2)
        diff(X1, active(X2)) -> diff(X1, X2)
        
)