%------------------------------------------------------------------------
%----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 a
%----human other than 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)
& H != john ) )).
%--------------------------------------------------------------------
|
%--------------------------------------------------------------------
fof(3,axiom,(
grade(john) = f ),
file('CreatedEqual.p',john_failed)).
fof(4,axiom,(
? [X3] :
( human(X3)
& grade(X3) = a ) ),
file('CreatedEqual.p',someone_got_an_a)).
fof(5,axiom,(
a != f ),
file('CreatedEqual.p',distinct_grades)).
fof(7,conjecture,(
? [X3] :
( human(X3)
& X3 != john ) ),
file('CreatedEqual.p',someone_not_john)).
fof(8,negated_conjecture,(
~ ? [X3] :
( human(X3)
& X3 != john ) ),
inference(assume_negation,[status(cth)],[7])).
cnf(14,plain,
( grade(john) = f ),
inference(split_conjunct,[status(thm)],[3])).
fof(16,plain,
( human(esk1_0)
& grade(esk1_0) = a ),
inference(skolemize,[status(sap)],[4])).
cnf(17,plain,
( grade(esk1_0) = a ),
inference(split_conjunct,[status(thm)],[16])).
cnf(18,plain,
( human(esk1_0) ),
inference(split_conjunct,[status(thm)],[16])).
cnf(19,plain,
( a != f ),
inference(split_conjunct,[status(thm)],[5])).
fof(22,negated_conjecture,(
! [X3] :
( ~ human(X3)
| X3 = john ) ),
inference(fof_nnf,[status(thm)],[8])).
cnf(24,negated_conjecture,
( X1 = john
| ~ human(X1) ),
inference(split_conjunct,[status(thm)],[22])).
cnf(25,negated_conjecture,
( john = esk1_0 ),
inference(spm,[status(thm)],[24,18])).
cnf(28,plain,
( f = a ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[17,25]),14])).
cnf(29,plain,
( $false ),
inference(sr,[status(thm)],[28,19])).
%--------------------------------------------------------------------
|
