# No SinE strategy applied
fof(c_0_1, axiom, (![X1]:?[X2]:r(X1,X2)) , file('example.p', axTotal)).
fof(c_0_2, axiom, (![X1]:![X2]:(r(X1,X2)=>![X3]:r(X1,f(X2,X3)))) , file('example.p', axExtends)).
fof(c_0_3, axiom, (![X1]:(p(X1)|p(f(X1,a)))) , file('example.p', axAlt)).
fof(c_0_4, conjecture, (![X1]:?[X2]:(r(X1,X2)&p(X2))) , file('example.p', c)).
fof(c_0_5, negated_conjecture, (~(![X1]:?[X2]:(r(X1,X2)&p(X2)))) ,inference(assume_negation, [status(cth)],[c_0_4])).
fof(c_0_6, plain, (![X3]:?[X4]:r(X3,X4)) ,inference(variable_rename, [status(thm)],[c_0_1])).
fof(c_0_7, plain, (![X3]:r(X3,esk1_1(X3))) ,inference(skolemize, [status(esa)], [c_0_6])).
cnf(c_0_8,plain,(r(X1,esk1_1(X1))),inference(split_conjunct, [status(thm)],[c_0_7])).
fof(c_0_9, plain, (![X1]:![X2]:(~r(X1,X2)|![X3]:r(X1,f(X2,X3)))) ,inference(fof_nnf, [status(thm)],[c_0_2])).
fof(c_0_10, plain, (![X4]:![X5]:(~r(X4,X5)|![X6]:r(X4,f(X5,X6)))) ,inference(variable_rename, [status(thm)],[c_0_9])).
fof(c_0_11, plain, (![X4]:![X5]:![X6]:(~r(X4,X5)|r(X4,f(X5,X6)))) ,inference(shift_quantors, [status(thm)],[c_0_10])).
cnf(c_0_12,plain,(r(X1,f(X2,X3))|~r(X1,X2)),inference(split_conjunct, [status(thm)],[c_0_11])).
fof(c_0_13, plain, (![X2]:(p(X2)|p(f(X2,a)))) ,inference(variable_rename, [status(thm)],[c_0_3])).
cnf(c_0_14,plain,(p(f(X1,a))|p(X1)),inference(split_conjunct, [status(thm)],[c_0_13])).
fof(c_0_15, negated_conjecture, (?[X1]:![X2]:(~r(X1,X2)|~p(X2))) ,inference(fof_nnf, [status(thm)],[c_0_5])).
fof(c_0_16, negated_conjecture, (?[X3]:![X4]:(~r(X3,X4)|~p(X4))) ,inference(variable_rename, [status(thm)],[c_0_15])).
fof(c_0_17, negated_conjecture, (![X4]:(~r(esk2_0,X4)|~p(X4))) ,inference(skolemize, [status(esa)], [c_0_16])).
cnf(c_0_18,negated_conjecture,(~p(X1)|~r(esk2_0,X1)),inference(split_conjunct, [status(thm)],[c_0_17])).
# Auto-Ordering is analysing problem.
# Problem is type GHNFNFFSF21SS
# Auto-mode selected ordering type KBO6
# Auto-mode selected ordering precedence scheme <invfreqconjmax>
# Auto-mode selected weight ordering scheme <invfreqrank>
#
# Auto-Heuristic is analysing problem.
# Problem is type GHNFNFFSF21SS
# Auto-Mode selected heuristic G_E___107_C45_F1_PI_AE_Q7_CS_SP_PS_S0Y
# and selection function SelectMaxLComplexAvoidPosPred.
#
# No equality, disabling AC handling.
#
# Initializing proof state
cnf(c_0_19,plain,(r(X1,esk1_1(X1))), c_0_8,['eval']).
cnf(c_0_20,negated_conjecture,(~p(X1)|~r(esk2_0,X1)), c_0_18,['eval']).
cnf(c_0_21,plain,(p(X1)|p(f(X1,a))), c_0_14,['eval']).
cnf(c_0_22,plain,(r(X1,f(X2,X3))|~r(X1,X2)), c_0_12,['eval']).
cnf(c_0_23,negated_conjecture,(~p(X1)|~r(esk2_0,X1)), c_0_20,['new_given']).
cnf(c_0_24,plain,(r(X1,esk1_1(X1))), c_0_19,['new_given']).
cnf(c_0_25,plain,(p(f(X1,a))|p(X1)), c_0_21,['new_given']).
cnf(c_0_26,plain,(r(X1,f(X2,X3))|~r(X1,X2)), c_0_22,['new_given']).
# Presaturation interreduction done
cnf(c_0_27,plain,(r(X1,esk1_1(X1))), c_0_24,['move_eval']).
cnf(c_0_28,negated_conjecture,(~p(X1)|~r(esk2_0,X1)), c_0_23,['move_eval']).
cnf(c_0_29,plain,(p(f(X1,a))|p(X1)), c_0_25,['move_eval']).
cnf(c_0_30,plain,(r(X1,f(X2,X3))|~r(X1,X2)), c_0_26,['move_eval']).
cnf(c_0_31,plain,(r(X1,esk1_1(X1))), c_0_27,['new_given']).
cnf(c_0_32,plain,(p(f(X1,a))|p(X1)), c_0_29,['new_given']).
cnf(c_0_33,plain,(r(X1,f(X2,X3))|~r(X1,X2)), c_0_30,['new_given']).
cnf(c_0_34,negated_conjecture,(~p(X1)|~r(esk2_0,X1)), c_0_28,['new_given']).
cnf(c_0_35,negated_conjecture,(p(X1)|~r(esk2_0,f(X1,a))),inference(spm,[status(thm)],[c_0_34,c_0_32,theory(equality)])).
cnf(c_0_36,negated_conjecture,(p(X1)|~r(esk2_0,f(X1,a))), c_0_35,['eval']).
cnf(c_0_37,negated_conjecture,(p(X1)|~r(esk2_0,f(X1,a))), c_0_36,['new_given']).
cnf(c_0_38,negated_conjecture,(p(X1)|~r(esk2_0,X1)),inference(spm,[status(thm)],[c_0_37,c_0_33,theory(equality)])).
cnf(c_0_39,negated_conjecture,(p(X1)|~r(esk2_0,X1)), c_0_38,['eval']).
cnf(c_0_40,negated_conjecture,(~r(esk2_0,X1)),inference(csr,[status(thm)],[c_0_39,c_0_34,theory(equality,[symmetry])])).
cnf(c_0_41,negated_conjecture,(~r(esk2_0,X1)), c_0_40,['new_given']).
cnf(c_0_42,negated_conjecture,($false),inference(spm,[status(thm)],[c_0_41,c_0_31,theory(equality)])).
cnf(c_0_43,negated_conjecture,(~r(esk2_0,X1)),inference(spm,[status(thm)],[c_0_41,c_0_33,theory(equality)])).
cnf(c_0_44,negated_conjecture,($false), c_0_42,['proof']).
# Proof found!
# SZS status Theorem
# Parsed axioms : 4
# Removed by relevancy pruning/SinE : 0
# Initial clauses : 4
# Removed in clause preprocessing : 0
# Initial clauses in saturation : 4
# Processed clauses : 10
# ...of these trivial : 0
# ...subsumed : 0
# ...remaining for further processing : 10
# Other redundant clauses eliminated : 0
# Clauses deleted for lack of memory : 0
# Backward-subsumed : 0
# Backward-rewritten : 0
# Generated clauses : 4
# ...of the previous two non-trivial : 2
# Contextual simplify-reflections : 1
# Paramodulations : 4
# Factorizations : 0
# Equation resolutions : 0
# Current number of processed clauses : 6
# Positive orientable unit clauses : 1
# Positive unorientable unit clauses: 0
# Negative unit clauses : 1
# Non-unit-clauses : 4
# Current number of unprocessed clauses: 0
# ...number of literals in the above : 0
# Clause-clause subsumption calls (NU) : 2
# Rec. Clause-clause subsumption calls : 2
# Non-unit clause-clause subsumptions : 1
# Unit Clause-clause subsumption calls : 2
# Rewrite failures with RHS unbound : 0
# BW rewrite match attempts : 0
# BW rewrite match successes : 0
# Condensation attempts : 0
# Condensation successes : 0
Menu