% START OF SYSTEM OUTPUT
Running first-order theorem proving
Running: /exp/home/tptp/Systems/E---3.1/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=30 /tmp/tmp.TJJNrrhI5i/E---3.1_5376.p
# Version: 3.1.0
# Preprocessing class: FSMSSMSSSSSNFFN.
# Scheduled 4 strats onto 8 cores with 30 seconds (240 total)
# Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 150s (5) cores
# Starting new_bool_3 with 30s (1) cores
# Starting new_bool_1 with 30s (1) cores
# Starting sh5l with 30s (1) cores
# sh5l with pid 5397 completed with status 0
# Result found by sh5l
# Preprocessing class: FSMSSMSSSSSNFFN.
# Scheduled 4 strats onto 8 cores with 30 seconds (240 total)
# Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 150s (5) cores
# Starting new_bool_3 with 30s (1) cores
# Starting new_bool_1 with 30s (1) cores
# Starting sh5l with 30s (1) cores
# SinE strategy is gf500_gu_R04_F100_L20000
# Search class: FGHSF-FFMM11-SFFFFFNN
# Scheduled 4 strats onto 1 cores with 30 seconds (30 total)
# Starting SAT001_MinMin_p005000_rr_RG with 19s (1) cores
# SAT001_MinMin_p005000_rr_RG with pid 5399 completed with status 0
# Result found by SAT001_MinMin_p005000_rr_RG
# Preprocessing class: FSMSSMSSSSSNFFN.
# Scheduled 4 strats onto 8 cores with 30 seconds (240 total)
# Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 150s (5) cores
# Starting new_bool_3 with 30s (1) cores
# Starting new_bool_1 with 30s (1) cores
# Starting sh5l with 30s (1) cores
# SinE strategy is gf500_gu_R04_F100_L20000
# Search class: FGHSF-FFMM11-SFFFFFNN
# Scheduled 4 strats onto 1 cores with 30 seconds (30 total)
# Starting SAT001_MinMin_p005000_rr_RG with 19s (1) cores
# Preprocessing time       : 0.001 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(prove_formulae, conjecture, ((((((![X1, X2]:(((human(X1)&human(X2))=>created_equal(X1,X2)))&human(john))&grade_of(john)=f)&?[X3]:((human(X3)&grade_of(X3)=a)))&a!=f)&![X4]:(~(human(grade_of(X4)))))&~(![X1, X2]:((((human(X1)&human(X2))&created_equal(X1,X2))<=>X1=X2)))), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', prove_formulae)).
cnf(c_0_26, axiom, (a!=f), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_26)).
cnf(c_0_16, axiom, (~human(grade_of(X1))), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_16)).
cnf(c_0_18, axiom, (grade_of(john)=f), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_18)).
cnf(c_0_28, axiom, (human(john)), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_28)).
cnf(c_0_17, axiom, (grade_of(esk3_0)=a), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_17)).
cnf(c_0_27, axiom, (human(esk3_0)), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_27)).
cnf(c_0_15, axiom, (created_equal(X1,X2)|~human(X1)|~human(X2)), file('/tmp/tmp.TJJNrrhI5i/E---3.1_5376.p', c_0_15)).
fof(c_0_37, negated_conjecture, ~(((((((![X1, X2]:(((human(X1)&human(X2))=>created_equal(X1,X2)))&human(john))&grade_of(john)=f)&?[X3]:((human(X3)&grade_of(X3)=a)))&a!=f)&![X4]:(~human(grade_of(X4))))&~(![X1, X2]:((((human(X1)&human(X2))&created_equal(X1,X2))<=>X1=X2))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[prove_formulae])])).
fof(c_0_38, negated_conjecture, ![X7, X9, X10]:(((((~human(X9)|~human(X10)|~created_equal(X9,X10)|X9=X10|(human(esk4_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(((human(X9)|X9!=X10|(human(esk4_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(human(X10)|X9!=X10|(human(esk4_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0)))))&(created_equal(X9,X10)|X9!=X10|(human(esk4_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))))&((~human(X9)|~human(X10)|~created_equal(X9,X10)|X9=X10|(human(esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(((human(X9)|X9!=X10|(human(esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(human(X10)|X9!=X10|(human(esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0)))))&(created_equal(X9,X10)|X9!=X10|(human(esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0)))))))&((~human(X9)|~human(X10)|~created_equal(X9,X10)|X9=X10|(~created_equal(esk4_0,esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(((human(X9)|X9!=X10|(~created_equal(esk4_0,esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0))))&(human(X10)|X9!=X10|(~created_equal(esk4_0,esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0)))))&(created_equal(X9,X10)|X9!=X10|(~created_equal(esk4_0,esk5_0)|~human(john)|grade_of(john)!=f|(~human(X7)|grade_of(X7)!=a)|a=f|human(grade_of(esk6_0)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])])])])).
cnf(c_0_39, plain, (a!=f), inference(fof_simplification,[status(thm)],[c_0_26])).
cnf(c_0_40, plain, (~human(grade_of(X1))), inference(fof_simplification,[status(thm)],[c_0_16])).
cnf(c_0_41, negated_conjecture, (human(X1)|human(esk5_0)|a=f|human(grade_of(esk6_0))|X2!=X1|~human(john)|grade_of(john)!=f|~human(X3)|grade_of(X3)!=a), inference(split_conjunct,[status(thm)],[c_0_38])).
cnf(c_0_42, axiom, (grade_of(john)=f), c_0_18).
cnf(c_0_43, axiom, (human(john)), c_0_28).
cnf(c_0_44, plain, (a!=f), c_0_39).
cnf(c_0_45, plain, (~human(grade_of(X1))), c_0_40).
cnf(c_0_46, negated_conjecture, (human(X1)|human(esk4_0)|a=f|human(grade_of(esk6_0))|X2!=X1|~human(john)|grade_of(john)!=f|~human(X3)|grade_of(X3)!=a), inference(split_conjunct,[status(thm)],[c_0_38])).
cnf(c_0_47, negated_conjecture, (human(esk5_0)|human(X1)|grade_of(X2)!=a|~human(X2)), inference(er,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42]), c_0_43])]), c_0_44]), c_0_45])])).
cnf(c_0_48, axiom, (grade_of(esk3_0)=a), c_0_17).
cnf(c_0_49, axiom, (human(esk3_0)), c_0_27).
cnf(c_0_50, negated_conjecture, (human(esk4_0)|human(X1)|grade_of(X2)!=a|~human(X2)), inference(er,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_42]), c_0_43])]), c_0_44]), c_0_45])])).
cnf(c_0_51, negated_conjecture, (human(X1)|a=f|human(grade_of(esk6_0))|X2!=X1|~created_equal(esk4_0,esk5_0)|~human(john)|grade_of(john)!=f|~human(X3)|grade_of(X3)!=a), inference(split_conjunct,[status(thm)],[c_0_38])).
cnf(c_0_52, plain, (created_equal(X1,X2)|~human(X1)|~human(X2)), inference(fof_simplification,[status(thm)],[c_0_15])).
cnf(c_0_53, negated_conjecture, (human(esk5_0)|human(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_49])])).
cnf(c_0_54, negated_conjecture, (human(esk4_0)|human(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_48]), c_0_49])])).
cnf(c_0_55, negated_conjecture, (human(X1)|grade_of(X2)!=a|~human(X2)|~created_equal(esk4_0,esk5_0)), inference(er,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_42]), c_0_43])]), c_0_44]), c_0_45])])).
cnf(c_0_56, plain, (created_equal(X1,X2)|~human(X1)|~human(X2)), c_0_52).
cnf(c_0_57, negated_conjecture, (human(esk5_0)), inference(ef,[status(thm)],[c_0_53])).
cnf(c_0_58, negated_conjecture, (human(esk4_0)), inference(ef,[status(thm)],[c_0_54])).
cnf(c_0_59, negated_conjecture, (human(X1)|grade_of(X2)!=a|~human(X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_57]), c_0_58])])).
cnf(c_0_60, negated_conjecture, (human(X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_48]), c_0_49])])).
cnf(c_0_61, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_60])]), ['proof']).
# SZS output end CNFRefutation
# Parsed axioms                        : 14
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 25
# Removed in clause preprocessing      : 0
# Initial clauses in saturation        : 25
# Processed clauses                    : 57
# ...of these trivial                  : 0
# ...subsumed                          : 7
# ...remaining for further processing  : 50
# Other redundant clauses eliminated   : 6
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 5
# Backward-rewritten                   : 12
# Generated clauses                    : 24
# ...of the previous two non-redundant : 24
# ...aggressively subsumed             : 0
# Contextual simplify-reflections      : 9
# Paramodulations                      : 14
# Factorizations                       : 4
# NegExts                              : 0
# Equation resolutions                 : 6
# Disequality decompositions           : 0
# Total rewrite steps                  : 37
# ...of those cached                   : 21
# Propositional unsat checks           : 0
#    Propositional check models        : 0
#    Propositional check unsatisfiable : 0
#    Propositional clauses             : 0
#    Propositional clauses after purity: 0
#    Propositional unsat core size     : 0
#    Propositional preprocessing time  : 0.000
#    Propositional encoding time       : 0.000
#    Propositional solver time         : 0.000
#    Success case prop preproc time    : 0.000
#    Success case prop encoding time   : 0.000
#    Success case prop solver time     : 0.000
# Current number of processed clauses  : 5
#    Positive orientable unit clauses  : 3
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 1
#    Non-unit-clauses                  : 1
# Current number of unprocessed clauses: 7
# ...number of literals in the above   : 26
# Current number of archived formulas  : 0
# Current number of archived clauses   : 39
# Clause-clause subsumption calls (NU) : 94
# Rec. Clause-clause subsumption calls : 33
# Non-unit clause-clause subsumptions  : 15
# Unit Clause-clause subsumption calls : 6
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 13
# BW rewrite match successes           : 13
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 1482
# Search garbage collected termcells   : 211

# -------------------------------------------------
# User time                : 0.004 s
# System time              : 0.002 s
# Total time               : 0.006 s
# Maximum resident set size: 1748 pages

# -------------------------------------------------
# User time                : 0.006 s
# System time              : 0.004 s
# Total time               : 0.010 s
# Maximum resident set size: 1716 pages
% E---3.1 exiting

% END OF SYSTEM OUTPUT
% RESULT: FOF_Saturation.s - E---3.1 says Theorem - CPU = 0.11 WC = 0.10 
% OUTPUT: FOF_Saturation.s - E---3.1 says CNFRefutation - CPU = 0.11 WC = 0.10