E 1.8 Proof Output

E use the current version of the new TSTP output format, documented in [SSCG2006]. Initial clauses and formulas are renamed, but sourced to their input file and original name. The following rule names are defined for the main proof search:

er

Equality resolution: x!=a v x=x ==> a=a

pm

Paramodulation. Note that E considers all literals as equational, and thus also performs resolution by a combination of top-level paramodulation and (implicit) clause normalization.

spm

Simultaneous Paramodulation. This is similr to paramodulation, but replaces all instances of the same term in the original clause in one step.

ef

Equality factoring (factor equations on one side only, move the remaining disequation into the precondition): x=a v b=c v x=d ==> a!=c v b=c vb=d

apply_def

Apply a definition, usually replacing a complex formula by a single literal.

introduced(definition)

Introduce a new definition.

rw

Rewriting, each rw-expression corresponds to exacly one rewrite step with the named clause. This is also used for equational unfolding.

sr

Simplify-reflect: An (equational) version of unit-cutting. As as example, see this positive simplify-reflect step: [a=b], [f(a)!=f(b)] => [].

csr

Contextual simplify-reflect (also known as contextual literal cutting or subsumption resolution): Literal cutting with non-unit clauses if one of the literals is implied in the context of the clause to be simplified.

ar

AC-resolution: Delete literals that are trivial modulo the AC-theory induced by the named clauses

cn

Clause normalize, delete trivial and repeated literals. This step is often implicit, but can sometimes occcur explicitely.

condense

Apply condensation (replace the clause by one of its factors that is more general).

Additionally, the clausification will use additional rule names:

assume_negation

Negate a conjecture for a proof by refutation.

fof_nnf

Convert a formula to negation normal form by moving negation signs inward to the literals, and eleminating equivalences and implications.

shift_quantors

Move quantors (inwards for mini-scoping or outwards for the final conjunctive normal form).

variable_rename

Rename bound variables to make sure each quantor binds a different variable.

skolemize

Eliminate existential quantors via Skolemization.

distribute

Apply distributivity law to move and outwards over or.

split_conjunct

Split of one conjunct from a formula in conjunctive normal form to create a clause.

fof_simplification

Perform standard simplification steps on the formula. This may also replaces back implications and exclusive or with equivalent constructs using implications and equivalences.

The first proof uses most inferences, although it uses some in fairly trivial ways. The second is the required CASC proof for SYN075-1, and contains examples for "ef" and "csr". The final proof is for SYN075+1, and also contains the clausification steps.

ALL_RULES

# SZS status Theorem
# SZS output start CNFRefutation.
fof(c_0_0, axiom, (((d=c|d=c)<=>h(i(e))=h(i(a)))), file('ALL_RULES.p', guarded_eq)).
fof(c_0_1, conjecture, ((?[X3]:?[X4]:?[X1]:?[X2]:?[X5]:(k(a,b)=k(X3,X3)&f(f(g(X2,X5),X1),f(X4,X3))=f(f(X3,X4),f(X1,g(X2,X5))))&![X6]:p(X6))), file('ALL_RULES.p', conj)).
cnf(c_0_2, axiom, (c=b|X1!=X2|X3!=X4|d!=c), file('ALL_RULES.p', split_or_condense)).
cnf(c_0_3, axiom, (i(X1)=i(X2)), file('ALL_RULES.p', identity)).
cnf(c_0_4, axiom, (p(X1)), file('ALL_RULES.p', p_holds)).
cnf(c_0_5, axiom, (f(X1,X2)=f(X2,X1)), file('ALL_RULES.p', comm_f)).
cnf(c_0_6, axiom, (g(X1,X2)=g(X2,X1)), file('ALL_RULES.p', comm_g)).
cnf(c_0_7, axiom, (f(f(X1,X2),X3)=f(X1,f(X2,X3))), file('ALL_RULES.p', ass_f)).
cnf(c_0_8, axiom, (a=b|c=a|e=a), file('ALL_RULES.p', consts1)).
cnf(c_0_9, axiom, (a=b|c=a|e!=a), file('ALL_RULES.p', consts2)).
fof(c_0_10, plain, ((~epred2_0<=>![X2]:![X1]:X1!=X2)), introduced(definition)).
cnf(c_0_11, plain, (epred2_0|X1!=X2), inference(split_equiv,[status(thm)],[c_0_10])).
fof(c_0_12, plain, ((~epred1_0<=>![X4]:![X3]:((c=b|X3!=X4)|d!=c))), introduced(definition)).
cnf(c_0_13, plain, (epred2_0), inference(er,[status(thm)],[c_0_11])).
fof(c_0_14, plain, ((d=c<=>h(i(e))=h(i(a)))), inference(fof_simplification,[status(thm)],[c_0_0])).
fof(c_0_15, negated_conjecture, (~((?[X3]:?[X4]:?[X1]:?[X2]:?[X5]:(k(a,b)=k(X3,X3)&f(f(g(X2,X5),X1),f(X4,X3))=f(f(X3,X4),f(X1,g(X2,X5))))&![X6]:p(X6)))), inference(assume_negation,[status(cth)],[c_0_1])).
cnf(c_0_16, plain, (~epred1_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_2, c_0_12]), c_0_10]), c_0_13])])).
fof(c_0_17, plain, (((d!=c|h(i(e))=h(i(a)))&(h(i(e))!=h(i(a))|d=c))), inference(fof_nnf,[status(thm)],[c_0_14])).
fof(c_0_18, negated_conjecture, (![X7]:![X8]:![X9]:![X10]:![X11]:((k(a,b)!=k(X7,X7)|f(f(g(X10,X11),X9),f(X8,X7))!=f(f(X7,X8),f(X9,g(X10,X11))))|~p(esk1_0))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])])])])])).
cnf(c_0_19, plain, (c=b|d!=c|X1!=X2), inference(sr,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_12]), c_0_16])).
cnf(c_0_20, plain, (d=c|h(i(e))!=h(i(a))), inference(split_conjunct,[status(thm)],[c_0_17])).
cnf(c_0_21, negated_conjecture, (~p(esk1_0)|f(f(g(X1,X2),X3),f(X4,X5))!=f(f(X5,X4),f(X3,g(X1,X2)))|k(a,b)!=k(X5,X5)), inference(split_conjunct,[status(thm)],[c_0_18])).
cnf(c_0_22, plain, (c=b|d!=c), inference(er,[status(thm)],[c_0_19])).
cnf(c_0_23, plain, (d=c), inference(sr,[status(thm)],[c_0_20, c_0_3])).
cnf(c_0_24, negated_conjecture, (k(a,b)!=k(X5,X5)|f(f(g(X1,X2),X3),f(X4,X5))!=f(f(X5,X4),f(X3,g(X1,X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_4])])).
cnf(c_0_25, plain, (f(X1,X2)=f(X2,X1)), c_0_5).
cnf(c_0_26, plain, (g(X1,X2)=g(X2,X1)), c_0_6).
cnf(c_0_27, plain, (f(f(X1,X2),X3)=f(X1,f(X2,X3))), c_0_7).
cnf(c_0_28, plain, (c=a|a=b), inference(csr,[status(thm)],[c_0_8, c_0_9])).
cnf(c_0_29, plain, (c=b), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
cnf(c_0_30, negated_conjecture, (k(a,b)!=k(X1,X1)), inference(ar,[status(thm)],[c_0_24, c_0_25, c_0_26, c_0_27])).
cnf(c_0_31, plain, (a=b), inference(pm,[status(thm)],[c_0_28, c_0_29])).
cnf(c_0_32, negated_conjecture, (k(b,b)!=k(X1,X1)), inference(rw,[status(thm)],[c_0_30, c_0_31])).
cnf(c_0_33, negated_conjecture, ($false), inference(er,[status(thm)],[c_0_32]), ['proof']).
# SZS output end CNFRefutation.

SYN075-1

# SZS status Unsatisfiable
# SZS output start CNFRefutation.
cnf(c_0_0, negated_conjecture, (big_f(X1,f(X2))|f(X2)=X2|X1!=g(X2)), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_6)).
cnf(c_0_1, negated_conjecture, (f(X2)=X2|~big_f(X1,f(X2))|X1!=g(X2)), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_4)).
cnf(c_0_2, negated_conjecture, (big_f(h(X1,X2),f(X1))|h(X1,X2)=X2|f(X1)!=X1), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_9)).
cnf(c_0_3, axiom, (X1=a|~big_f(X1,X2)), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_1)).
cnf(c_0_4, negated_conjecture, (f(X1)!=X1|h(X1,X2)!=X2|~big_f(h(X1,X2),f(X1))), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_10)).
cnf(c_0_5, axiom, (big_f(X1,X2)|X1!=a|X2!=b), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075-1.p', clause_3)).
cnf(c_0_6, negated_conjecture, (f(X1)=X1|g(X1)!=X2), inference(csr,[status(thm)],[c_0_0, c_0_1])).
cnf(c_0_7, negated_conjecture, (f(X1)=X1), inference(er,[status(thm)],[c_0_6])).
cnf(c_0_8, negated_conjecture, (h(X1,X2)=X2|big_f(h(X1,X2),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_2, c_0_7]), c_0_7])])).
cnf(c_0_9, negated_conjecture, (h(X1,X2)=a|h(X1,X2)=X2), inference(pm,[status(thm)],[c_0_3, c_0_8])).
cnf(c_0_10, negated_conjecture, (h(X1,X2)!=X2|~big_f(h(X1,X2),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_4, c_0_7]), c_0_7])])).
cnf(c_0_11, negated_conjecture, (h(X1,X2)=X2|a!=X2), inference(ef,[status(thm)],[c_0_9])).
fof(c_0_12, plain, ((~epred1_0<=>![X2]:a!=X2)), introduced(definition)).
cnf(c_0_13, negated_conjecture, (h(X1,X2)!=X2|~big_f(X2,X1)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_10, c_0_11]), c_0_3])).
cnf(c_0_14, negated_conjecture, (h(X1,X2)=X2|big_f(a,X1)), inference(pm,[status(thm)],[c_0_8, c_0_9])).
cnf(c_0_15, negated_conjecture, (epred1_0|a!=X1), inference(split_equiv,[status(thm)],[c_0_12])).
fof(c_0_16, plain, ((~epred2_0<=>![X1]:b!=X1)), introduced(definition)).
cnf(c_0_17, negated_conjecture, (big_f(a,X1)|~big_f(X2,X1)), inference(pm,[status(thm)],[c_0_13, c_0_14])).
cnf(c_0_18, negated_conjecture, (~big_f(X1,X2)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_13, c_0_11]), c_0_3])).
cnf(c_0_19, negated_conjecture, (epred1_0), inference(er,[status(thm)],[c_0_15])).
cnf(c_0_20, negated_conjecture, (~epred2_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(sr,[status(thm)],[inference(pm,[status(thm)],[c_0_17, c_0_5]), c_0_18]), c_0_12]), c_0_16]), c_0_19])])).
cnf(c_0_21, negated_conjecture, (b!=X1), inference(sr,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_16]), c_0_20])).
cnf(c_0_22, negated_conjecture, ($false), inference(er,[status(thm)],[c_0_21]), ['proof']).
# SZS output end CNFRefutation.

SYN075+1

fof(c_0_0, conjecture, (?[X2]:![X4]:(?[X1]:![X3]:(big_f(X3,X4)<=>X3=X1)<=>X4=X2)), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075+1.p', pel52)).
fof(c_0_1, axiom, (?[X1]:?[X2]:![X3]:![X4]:(big_f(X3,X4)<=>(X3=X1&X4=X2))), file('/Users/schulz/EPROVER/TPTP_6.0.0_FLAT/SYN075+1.p', pel52_1)).
fof(c_0_2, negated_conjecture, (~(?[X2]:![X4]:(?[X1]:![X3]:(big_f(X3,X4)<=>X3=X1)<=>X4=X2))), inference(assume_negation,[status(cth)],[c_0_0])).
fof(c_0_3, plain, (![X7]:![X8]:![X9]:![X10]:(((X7=esk1_0|~big_f(X7,X8))&(X8=esk2_0|~big_f(X7,X8)))&((X9!=esk1_0|X10!=esk2_0)|big_f(X9,X10)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])])])])).
fof(c_0_4, negated_conjecture, (![X5]:![X7]:![X10]:![X11]:((((~big_f(esk4_2(X5,X7),esk3_1(X5))|esk4_2(X5,X7)!=X7)|esk3_1(X5)!=X5)&((big_f(esk4_2(X5,X7),esk3_1(X5))|esk4_2(X5,X7)=X7)|esk3_1(X5)!=X5))&(((~big_f(X10,esk3_1(X5))|X10=esk5_1(X5))|esk3_1(X5)=X5)&((X11!=esk5_1(X5)|big_f(X11,esk3_1(X5)))|esk3_1(X5)=X5)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])])).
cnf(c_0_5, plain, (X2=esk2_0|~big_f(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_6, negated_conjecture, (esk3_1(X1)=X1|big_f(X2,esk3_1(X1))|X2!=esk5_1(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_7, negated_conjecture, (esk3_1(X1)=esk2_0|esk3_1(X1)=X1|esk5_1(X1)!=X2), inference(pm,[status(thm)],[c_0_5, c_0_6])).
cnf(c_0_8, negated_conjecture, (esk3_1(X1)=esk2_0|esk3_1(X1)=X1), inference(er,[status(thm)],[c_0_7])).
cnf(c_0_9, plain, (X1=esk1_0|~big_f(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_10, negated_conjecture, (esk4_2(X1,X2)=X2|big_f(esk4_2(X1,X2),esk3_1(X1))|esk3_1(X1)!=X1), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_11, negated_conjecture, (esk3_1(X1)!=X1|esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),esk3_1(X1))), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_12, negated_conjecture, (esk3_1(X1)=X1|esk2_0!=X1), inference(ef,[status(thm)],[c_0_8])).
cnf(c_0_13, negated_conjecture, (esk4_2(X1,X2)=esk1_0|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1), inference(pm,[status(thm)],[c_0_9, c_0_10])).
cnf(c_0_14, negated_conjecture, (esk4_2(X1,X2)!=X2|esk3_1(X1)!=X1|~big_f(esk4_2(X1,X2),X1)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_11, c_0_12]), c_0_5])).
cnf(c_0_15, negated_conjecture, (esk4_2(X1,X2)=X2|esk3_1(X1)!=X1|esk1_0!=X2), inference(ef,[status(thm)],[c_0_13])).
cnf(c_0_16, negated_conjecture, (esk4_2(X1,X2)!=X2|esk3_1(X1)!=X1|~big_f(X2,X1)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_14, c_0_15]), c_0_9])).
cnf(c_0_17, negated_conjecture, (esk4_2(X1,X2)=X2|esk3_1(X1)=esk2_0), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_5, c_0_10]), c_0_8])).
cnf(c_0_18, negated_conjecture, (esk3_1(X1)=X1|big_f(X2,esk2_0)|esk5_1(X1)!=X2), inference(pm,[status(thm)],[c_0_6, c_0_8])).
cnf(c_0_19, negated_conjecture, (esk3_1(X1)=esk2_0|~big_f(X2,X1)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_16, c_0_17]), c_0_8])).
cnf(c_0_20, negated_conjecture, (esk3_1(X1)=X1|big_f(esk5_1(X1),esk2_0)), inference(er,[status(thm)],[c_0_18])).
cnf(c_0_21, negated_conjecture, (esk4_2(X1,X2)=esk1_0|esk3_1(X1)!=X1|X2!=esk1_0), inference(ef,[status(thm)],[c_0_13])).
cnf(c_0_22, negated_conjecture, (esk3_1(esk2_0)=esk2_0|esk3_1(X1)=X1), inference(pm,[status(thm)],[c_0_19, c_0_20])).
cnf(c_0_23, negated_conjecture, (esk3_1(X1)!=X1|~big_f(X2,X1)), inference(csr,[status(thm)],[inference(pm,[status(thm)],[c_0_16, c_0_21]), c_0_9])).
cnf(c_0_24, negated_conjecture, (esk3_1(esk2_0)=esk2_0), inference(ef,[status(thm)],[c_0_22])).
fof(c_0_25, plain, ((~epred11_0<=>![X1]:esk1_0!=X1)), introduced(definition)).
cnf(c_0_26, negated_conjecture, (esk3_1(X1)=X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(pm,[status(thm)],[c_0_23, c_0_20]), c_0_24])])).
cnf(c_0_27, negated_conjecture, (epred11_0|esk1_0!=X1), inference(split_equiv,[status(thm)],[c_0_25])).
fof(c_0_28, plain, ((~epred12_0<=>![X2]:esk2_0!=X2)), introduced(definition)).
cnf(c_0_29, negated_conjecture, (~big_f(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_26])])).
cnf(c_0_30, plain, (big_f(X1,X2)|X2!=esk2_0|X1!=esk1_0), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_31, negated_conjecture, (epred11_0), inference(er,[status(thm)],[c_0_27])).
cnf(c_0_32, negated_conjecture, (epred12_0|esk2_0!=X1), inference(split_equiv,[status(thm)],[c_0_28])).
cnf(c_0_33, negated_conjecture, (~epred12_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(pm,[status(thm)],[c_0_29, c_0_30]), c_0_25]), c_0_28]), c_0_31])])).
cnf(c_0_34, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_32]), c_0_33]), ['proof']).
# SZS output end CNFRefutation.