The source and useful information are optional. The languages currently supported are

A problem is a list of annotated formulae, typically without the source or useful information. (This is a description of an ordinary problem - the TPTP language can do more than this.)

- Name:
The name is a word starting lower case, e.g.,
`original_f1`, or a single quoted word, e.g.,`'A crazy $ name'`. - Role:
The role is typically one of
`axiom`for axioms,`conjecture`for conjectures, or`negated_conjecture`for negated conjectures. A full list of the posssible roles is in the TPTP syntax. - Logical formula: The logical formula uses a consistent and easily understood notation that can be seen in the BNF for THF, BNF for TFF. BNF for FOF, and BNF for CNF.

%------------------------------------------------------------------------ %----All (hu)men are created equal. John is a human. John got an F grade. %----There is someone (a human) who got an A grade. An A grade is not %----equal to an F grade. Grades are not human. Therefore there is %----another human created equal to John. fof(all_created_equal,axiom,( ! [H1,H2] : ( ( human(H1) & human(H2) ) => created_equal(H1,H2) ) )). fof(john,axiom,( human(john) )). fof(john_failed,axiom,( grade(john) = f )). fof(someone_got_an_a,axiom,( ? [H] : ( human(H) & grade(H) = a ) )). fof(distinct_grades,axiom,( a != f )). fof(grades_not_human,axiom,( ! [G] : ~ human(grade(G)) )). fof(someone_not_john,conjecture,( ? [H] : ( human(H) & created_equal(H,john) & H != john ) )). %--------------------------------------------------------------------

Once the syntax is OK, go to SystemOnTPTP and choose an ATP System (E is a safe bet). RunSelectedSystems and see if it solves the problem.