TPTP-Examples/fof_conjecture.p
2023-03-27 11:01:47 -04:00

12 lines
232 B
OpenEdge ABL

include('Axioms/NUM-ROZEK.ax').
%-- Define Even
fof(h1, hypothesis, even("zero")).
fof(h2, hypothesis,
![X] : (even(X) => even(add(X, "two")))
).
%-- Problem
fof(c1, conjecture,
![X] : (even(X) => even(add(X, "four")))
).