StepUsing
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and (factor(X,Y)) and (factor(Y,Z))=> factor(X,Z) ;
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true=> not ((factor(X,Y)) and (factor(Y,Z)) and not (factor(X,Z))) ; Inversion
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and true=> not ((factor(X,Y)) and not (factor(X,Z)) and Y * V0 = Z) ; Induction factor
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and true=> not ((factor(X,Y)) and not (factor(X,Z)) and Y * V0 = Z and not (factor(X,Y * V0))) ; Inference
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and true=> not ((factor(X,Y)) and not (factor(X,Z)) and Y * V0 = Z and not (factor(X,Y * V0)) and (factor(Y,Z))) ; Induction factor
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and true=> not ((factor(X,Y)) and not (factor(X,Z)) and Y * V0 = Z and not (factor(X,Y * V0)) and (factor(Y,Z)) and (factor(Y,Y * V0))) ; Inference
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and integer(V1) and exists(V1) and true=> not ( not (factor(X,Z)) and Y * V0 = Z and not (factor(X,Y * V0)) and (factor( Y,Z)) and (factor(Y,Y * V0)) and X * V1 = Y) ; Induction factor
integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and integer(V0) and exists(V0) and integer(V1) and exists(V1) and true=> not ( not (factor(X,Z)) and Y * V0 = Z and not (factor(X,Y * V0)) and (factor( Y,Z)) and (factor(Y,Y * V0)) and X * V1 = Y and X * V1 * V0 = Z) ; Inference
true; Induction factor