(VAR X Y X1 X2 X3)
(RULES 
active(fact(X)) -> mark(if(zero(X),s(0),prod(X,fact(p(X)))))
active(add(0,X)) -> mark(X)
active(add(s(X),Y)) -> mark(s(add(X,Y)))
active(prod(0,X)) -> mark(0)
active(prod(s(X),Y)) -> mark(add(Y,prod(X,Y)))
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
active(zero(0)) -> mark(true)
active(zero(s(X))) -> mark(false)
active(p(s(X))) -> mark(X)
mark(fact(X)) -> active(fact(mark(X)))
mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
mark(zero(X)) -> active(zero(mark(X)))
mark(s(X)) -> active(s(mark(X)))
mark(0) -> active(0)
mark(prod(X1,X2)) -> active(prod(mark(X1),mark(X2)))
mark(p(X)) -> active(p(mark(X)))
mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
mark(true) -> active(true)
mark(false) -> active(false)
fact(mark(X)) -> fact(X)
fact(active(X)) -> fact(X)
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)
zero(mark(X)) -> zero(X)
zero(active(X)) -> zero(X)
s(mark(X)) -> s(X)
s(active(X)) -> s(X)
prod(mark(X1),X2) -> prod(X1,X2)
prod(X1,mark(X2)) -> prod(X1,X2)
prod(active(X1),X2) -> prod(X1,X2)
prod(X1,active(X2)) -> prod(X1,X2)
p(mark(X)) -> p(X)
p(active(X)) -> p(X)
add(mark(X1),X2) -> add(X1,X2)
add(X1,mark(X2)) -> add(X1,X2)
add(active(X1),X2) -> add(X1,X2)
add(X1,active(X2)) -> add(X1,X2)
)