Prove:

factor(X, Y) and factor(Y, Z) =>

Given:

integer(X) and integer(Y) and integer(Z) =>
X * (Y * Z) = (X * Y) * Z

and:

integer(X) and integer(Y) => X * Y = Y * X

and:

integer(X) and integer(Y) and factor(X, Y) <=>
exists(Z) and integer(Z) and X * Z = Y

Test as a text file.