# Entrants' Sample Solutions

## Darwin 1.2

Peter Baumgartner1, Alexander Fuchs2, Cesare Tinelli2
1Max-Planck-Institut für Informatik Saarbrücken, Germany,
baumgart@mpi-sb.mpg.de
2The University of Iowa, USA
{fuchs,tinelli}@cs.uiowa.edu

### Legend

When Darwin detects that a clause set is satisfiable, it outputs the current context, which encodes the model as formally defined in the Model Evolution paper by Baumgartner and Tinelli. In Darwin's output:
• __-v__(=0) stands for -v
• Variables are represented by numbers, universal variables start with a _, parametric variables with a =, e.g., _0, =0
• Skolem constants are represented by a number enclosed in __, e.g., __10__.
• - is used for negation, e.g., -p(a).
For a short explanation, the context is a set of literals, where each literal provides a default interpretation for all its instances. However, this default interpretation might be blocked by another literal. For example, the context { __-v__(=0), p(f(=0)), -p(f(a)) } specifies the model where exactly all instances of p(f(x)) except for p(f(a)) are true. __-v__(=0) makes all atoms false, the more specific literal p(f(=0)) overrides this partially by making all its instances true, and likewise the more specific literal -p(f(a)) make all its instances (i.e. exactly itself) false again. Thus, if the signature consists only of p, f, a, the specified model is the atom set { p(f(f(a))), p(f(f(f(a)))), p(f(f(f(f(a))))), ... }.

The above example used only proper instantiation. If the instance of two literals overlap, then the positive one is given preference. For example, { __-v__(=0), p(f(a, =0)), -p(f(=0, a)) } makes the positive version of the common instance p(f(a, a)) true.

Finally, the examples up to now used only parametric variables. Universal variables make all there instances true without exception. Thus, { __-v__(=0), p(f(a, =0)), -p(f(_0, a)) } makes p(f(a, a)) false, and { __-v__(=0), p(f(a, _0)), -p(f(_0, a)) } is inconsistent and not a valid model description.

### Sample SAT model for MGT031-1

```-__-v__(=0)
-greater(cardinality_at_time(first_movers, appear(an_organisation, sk2)), number
_of_organizations(e, appear(an_organisation, sk2)))
+greater_or_equal(appear(efficient_producers, e), appear(an_organisation, sk2))
+greater(appear(efficient_producers, e), appear(an_organisation, sk2))
-greater(cardinality_at_time(first_movers, appear(an_organisation, sk2)), zero)
+greater(appear(first_movers, sk2), appear(an_organisation, sk2))
+greater_or_equal(appear(efficient_producers, e), appear(first_movers, sk2))
+greater_or_equal(number_of_organizations(e, appear(an_organisation, sk2)), zero
)
+greater(appear(efficient_producers, e), appear(first_movers, sk2))
+greater_or_equal(appear(first_movers, sk2), appear(an_organisation, sk2))
+greater(number_of_organizations(e, appear(an_organisation, sk2)), zero)
-=(appear(an_organisation, sk2), appear(first_movers, sk2))
+in_environment(sk2, appear(an_organisation, sk2))
+environment(sk2)
```

## EP 0.9

Stephan Schulz
Technische Universität München, Germany, and ITC/irst, Italy
schulz@eprover.de

EP will use the current version of the new TPTP output format. 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. See note on paramodulation above.
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
split
Clause splitting a la Vampire (non-deductive, but maintains unsatisfiability)
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.

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
Eleminate 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.
def_intro
Introduce a (polarity-dependend) definition for a formula.
def_fold
Apply a definition to replace a subformula with a properly defined literal. These last two rules are not yet implemented, and thus not demonstrated below.

The first proof uses all proof search inferences except for "ef", "spm", and "csr", although it uses some in fairly trivial ways. The second is the required 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

```# Problem is unsatisfiable (or provable), constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
cnf(1,axiom,(f(X1,X2)=f(X2,X1)),file('ALL_RULES.lop', at_line_19_column_1)).
cnf(2,axiom,(f(X1,f(X2,X3))=f(f(X1,X2),X3)),file('ALL_RULES.lop', at_line_20_column_1)).
cnf(3,axiom,(g(X1,X2)=g(X2,X1)),file('ALL_RULES.lop', at_line_21_column_1)).
cnf(4,axiom,(f(f(X1,X2),f(X3,g(X4,X5)))!=f(f(g(X4,X5),X3),f(X2,X1))|k(X1,X1)!=k(
a,b)),file('ALL_RULES.lop', at_line_22_column_1)).
cnf(5,axiom,(b=c|X1!=X2|X3!=X4|c!=d),file('ALL_RULES.lop', at_line_24_column_1)).
cnf(6,axiom,(a=b|a=c),file('ALL_RULES.lop', at_line_26_column_1)).
cnf(7,axiom,(i(X1)=i(X2)),file('ALL_RULES.lop', at_line_28_column_1)).
cnf(8,axiom,(c=d|h(i(a))!=h(i(e))),file('ALL_RULES.lop', at_line_29_column_1)).
cnf(13,derived,(k(a,b)!=k(X1,X1)),inference(ar,[status(thm)],[4,1,3,2,theory(equality)])).
cnf(23,derived,(c=b|epred1_0|X3!=X4|d!=c),inference(split,[split(esplit,[])],[5])).
cnf(24,derived,(epred2_0|X1!=X2),inference(split,[split(esplit,[])],[5])).
cnf(25,derived,(~epred2_0|~epred1_0),inference(split,[split(esplit,[])],[5])).
cnf(26,derived,(epred2_0),inference(er,[status(thm)],[24,theory(equality)])).
cnf(27,derived,(\$false|~epred1_0),inference(rw,[status(thm)],[25,26,theory(equality)])).
cnf(28,derived,(~epred1_0),inference(cn,[status(thm)],[27,theory(equality)])).
cnf(29,derived,(c=b|epred1_0|d!=c),inference(er,[status(thm)],[23,theory(equality)])).
cnf(30,derived,(c=b|d!=c),inference(sr,[status(thm)],[29,28,theory(equality)])).
cnf(31,derived,(d=c),inference(sr,[status(thm)],[8,7,theory(equality)])).
cnf(32,derived,(c=b|\$false),inference(rw,[status(thm)],[30,31,theory(equality)])).
cnf(33,derived,(c=b),inference(cn,[status(thm)],[32,theory(equality)])).
cnf(34,derived,(b=a),inference(pm,[status(thm)],[6,33,theory(equality)])).
cnf(36,derived,(k(b,b)!=k(X1,X1)),inference(rw,[status(thm)],[13,34,theory(equality)])).
cnf(75,derived,(\$false),inference(er,[status(thm)],[36,theory(equality)])).
cnf(76,derived,(\$false),75,['proof']).
# Proof object ends here.
```

SYN075-1

```# Problem is unsatisfiable (or provable), constructing proof object
# TSTP exit status: Unsatisfiable
# Proof object starts here.
cnf(1,axiom,(X1=a|~big_f(X1,X2)),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_1)).
cnf(3,axiom,(big_f(X1,X2)|X1!=a|X2!=b),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_3)).
cnf(4,negated_conjecture,(f(X2)=X2|~big_f(X1,f(X2))|X1!=g(X2)),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_4)).
cnf(6,negated_conjecture,(big_f(X1,f(X2))|f(X2)=X2|X1!=g(X2)),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_6)).
cnf(9,negated_conjecture,(big_f(h(X1,X2),f(X1))|h(X1,X2)=X2|f(X1)!=X1),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_9)).
cnf(10,negated_conjecture,(f(X1)!=X1|h(X1,X2)!=X2|~big_f(h(X1,X2),f(X1))),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075-1.p', clause_10)).
cnf(14,negated_conjecture-derived,(f(X2)=X2|g(X2)!=X1),inference(csr,[status(thm)],[4,6])).
cnf(15,negated_conjecture-derived,(f(X1)=X1),inference(er,[status(thm)],[14,theory(equality)])).
cnf(19,negated_conjecture-derived,(h(X1,X2)!=X2|f(X1)!=X1|a!=h(X1,X2)|b!=f(X1)),inference(spm,[status(thm)],[10,3,theory(equality)])).
cnf(23,negated_conjecture-derived,(h(X1,X2)!=a|h(X1,X2)!=X2|X1!=b|f(X1)!=X1),inference(rw,[status(thm)],[19,15,theory(equality)])).
cnf(24,negated_conjecture-derived,(h(X1,X2)!=a|h(X1,X2)!=X2|X1!=b|\$false),inference(rw,[status(thm)],[23,15,theory(equality)])).
cnf(25,negated_conjecture-derived,(h(X1,X2)!=a|h(X1,X2)!=X2|X1!=b),inference(cn,[status(thm)],[24,theory(equality)])).
cnf(28,negated_conjecture-derived,(h(X1,X2)!=X2|\$false|~big_f(h(X1,X2),f(X1))),inference(rw,[status(thm)],[10,15,theory(equality)])).
cnf(29,negated_conjecture-derived,(h(X1,X2)!=X2|\$false|~big_f(h(X1,X2),X1)),inference(rw,[status(thm)],[28,15,theory(equality)])).
cnf(30,negated_conjecture-derived,(h(X1,X2)!=X2|~big_f(h(X1,X2),X1)),inference(cn,[status(thm)],[29,theory(equality)])).
cnf(33,negated_conjecture-derived,(h(X1,X2)=X2|big_f(h(X1,X2),X1)|f(X1)!=X1),inference(rw,[status(thm)],[9,15,theory(equality)])).
cnf(34,negated_conjecture-derived,(h(X1,X2)=X2|big_f(h(X1,X2),X1)|\$false),inference(rw,[status(thm)],[33,15,theory(equality)])).
cnf(35,negated_conjecture-derived,(h(X1,X2)=X2|big_f(h(X1,X2),X1)),inference(cn,[status(thm)],[34,theory(equality)])).
cnf(38,negated_conjecture-derived,(a=h(X1,X2)|h(X1,X2)=X2),inference(spm,[status(thm)],[1,35,theory(equality)])).
cnf(50,negated_conjecture-derived,(h(X1,X2)=a|~big_f(X2,X1)),inference(spm,[status(thm)],[30,38,theory(equality)])).
cnf(56,negated_conjecture-derived,(a!=X2|X1!=b|~big_f(X2,X1)),inference(spm,[status(thm)],[25,50,theory(equality)])).
cnf(59,negated_conjecture-derived,(a!=X2|X1!=b),inference(csr,[status(thm)],[56,3])).
cnf(60,negated_conjecture-derived,(epred1_0|a!=X2),inference(split,[split(esplit,[])],[59])).
cnf(61,negated_conjecture-derived,(epred2_0|X1!=b),inference(split,[split(esplit,[])],[59])).
cnf(62,negated_conjecture-derived,(~epred2_0|~epred1_0),inference(split,[split(esplit,[])],[59])).
cnf(63,negated_conjecture-derived,(epred1_0),inference(er,[status(thm)],[60,theory(equality)])).
cnf(65,negated_conjecture-derived,(epred2_0),inference(er,[status(thm)],[61,theory(equality)])).
cnf(73,negated_conjecture-derived,(\$false|~epred1_0),inference(rw,[status(thm)],[62,65,theory(equality)])).
cnf(74,negated_conjecture-derived,(\$false|\$false),inference(rw,[status(thm)],[73,63,theory(equality)])).
cnf(75,negated_conjecture-derived,(\$false),inference(cn,[status(thm)],[74,theory(equality)])).
cnf(76,negated_conjecture-derived,(\$false),75,['proof']).
# Proof object ends here.
```

SYN075+1

```# Problem is unsatisfiable (or provable), constructing proof object
# TSTP exit status: Theorem
# Proof object starts here.
fof(1, axiom,?[X1]:?[X2]:![X3]:![X4]:(big_f(X3,X4)<=>(X3=X1&X4=X2)),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075+1.p', pel52_1)).
fof(2, conjecture,?[X2]:![X4]:(?[X1]:![X3]:(big_f(X3,X4)<=>X3=X1)<=>X4=X2),file('/Users/schulz/EPROVER/TPTP_3.0.1_FLAT/SYN075+1.p', pel52)).
fof(3, negated_conjecture-derived,~(?[X2]:![X4]:(?[X1]:![X3]:(big_f(X3,X4)<=>X3=X1)<=>X4=X2)),inference(assume_negation,[status(cth)],[2])).
fof(4, derived,?[X1]:?[X2]:![X3]:![X4]:((~(big_f(X3,X4))|(X3=X1&X4=X2))&((~(X3=X1)|~(X4=X2))|big_f(X3,X4))),inference(fof_nnf,[status(thm)],[1])).
fof(5, derived,?[X1]:?[X2]:(![X3]:![X4]:(~(big_f(X3,X4))|(X3=X1&X4=X2))&![X3]:![X4]:((~(X3=X1)|~(X4=X2))|big_f(X3,X4))),inference(shift_quantors,[status(thm)],[4])).
fof(6, derived,?[X5]:?[X6]:(![X7]:![X8]:(~(big_f(X7,X8))|(X7=X5&X8=X6))&![X9]:![X10]:((~(X9=X5)|~(X10=X6))|big_f(X9,X10))),inference(variable_rename,[status(thm)],[5])).
fof(7, derived,(![X7]:![X8]:(~(big_f(X7,X8))|(X7=esk1_0&X8=esk2_0))&![X9]:![X10]:((~(X9=esk1_0)|~(X10=esk2_0))|big_f(X9,X10))),inference(skolemize,[status(sab)],[6])).
fof(8, derived,![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)],[7])).
cnf(9,derived,(big_f(X1,X2)|X2!=esk2_0|X1!=esk1_0),inference(split_conjunct,[status(thm)],[8])).
cnf(10,derived,(X2=esk2_0|~big_f(X1,X2)),inference(split_conjunct,[status(thm)],[8])).
cnf(11,derived,(X1=esk1_0|~big_f(X1,X2)),inference(split_conjunct,[status(thm)],[8])).
fof(12, negated_conjecture-derived,![X2]:?[X4]:((![X1]:?[X3]:((~(big_f(X3,X4))|~(X3=X1))&(big_f(X3,X4)|X3=X1))|~(X4=X2))&(?[X1]:![X3]:((big_f(X3,X4)&X3=X1)|(~(big_f(X3,X4))&~(X3=X1)))|X4=X2)),inference(fof_nnf,[status(thm)],[3])).
fof(13, negated_conjecture-derived,![X5]:?[X6]:((![X7]:?[X8]:((~(big_f(X8,X6))|~(X8=X7))&(big_f(X8,X6)|X8=X7))|~(X6=X5))&(?[X9]:![X10]:((big_f(X10,X6)&X10=X9)|(~(big_f(X10,X6))&~(X10=X9)))|X6=X5)),inference(variable_rename,[status(thm)],[12])).
fof(14, negated_conjecture-derived,![X5]:((![X7]:((~(big_f(esk4_2(X5,X7),esk3_1(X5)))|~(esk4_2(X5,X7)=X7))&(big_f(esk4_2(X5,X7),esk3_1(X5))|esk4_2(X5,X7)=X7))|~(esk3_1(X5)=X5))&(![X10]:((big_f(X10,esk3_1(X5))&X10=esk5_1(X5))|(~(big_f(X10,esk3_1(X5)))&~(X10=esk5_1(X5))))|esk3_1(X5)=X5)),inference(skolemize,[status(sab)],[13])).
fof(15, negated_conjecture-derived,![X5]:![X7]:![X10]:((((~(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)))|big_f(X10,esk3_1(X5)))|esk3_1(X5)=X5)&((~(X10=esk5_1(X5))|big_f(X10,esk3_1(X5)))|esk3_1(X5)=X5))&(((~(big_f(X10,esk3_1(X5)))|X10=esk5_1(X5))|esk3_1(X5)=X5)&((~(X10=esk5_1(X5))|X10=esk5_1(X5))|esk3_1(X5)=X5)))),inference(distribute,[status(thm)],[14])).
cnf(18,negated_conjecture-derived,(esk3_1(X1)=X1|big_f(X2,esk3_1(X1))|X2!=esk5_1(X1)),inference(split_conjunct,[status(thm)],[15])).
cnf(20,negated_conjecture-derived,(esk4_2(X1,X2)=X2|big_f(esk4_2(X1,X2),esk3_1(X1))|esk3_1(X1)!=X1),inference(split_conjunct,[status(thm)],[15])).
cnf(21,negated_conjecture-derived,(esk3_1(X1)!=X1|esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),esk3_1(X1))),inference(split_conjunct,[status(thm)],[15])).
cnf(24,negated_conjecture-derived,(esk3_1(X1)=X1|big_f(esk5_1(X1),esk3_1(X1))),inference(er,[status(thm)],[18,theory(equality)])).
cnf(26,negated_conjecture-derived,(esk1_0=esk4_2(X1,X2)|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1),inference(spm,[status(thm)],[11,20,theory(equality)])).
cnf(27,negated_conjecture-derived,(esk2_0=esk3_1(X1)|esk4_2(X1,X2)=X2|esk3_1(X1)!=X1),inference(spm,[status(thm)],[10,20,theory(equality)])).
cnf(29,negated_conjecture-derived,(esk4_2(X1,X2)!=X2|esk3_1(X1)!=X1|esk1_0!=esk4_2(X1,X2)|esk2_0!=esk3_1(X1)),inference(spm,[status(thm)],[21,9,theory(equality)])).
cnf(31,negated_conjecture-derived,(esk1_0=esk5_1(X1)|esk3_1(X1)=X1),inference(spm,[status(thm)],[11,24,theory(equality)])).
cnf(32,negated_conjecture-derived,(esk2_0=esk3_1(X1)|esk3_1(X1)=X1),inference(spm,[status(thm)],[10,24,theory(equality)])).
cnf(35,negated_conjecture-derived,(esk3_1(X1)=X1|big_f(esk1_0,esk3_1(X1))),inference(spm,[status(thm)],[24,31,theory(equality)])).
cnf(36,negated_conjecture-derived,(esk3_1(X2)=X2|esk2_0!=X2),inference(ef,[status(thm)],[32,theory(equality)])).
cnf(46,negated_conjecture-derived,(esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),X1)|esk2_0!=X1),inference(spm,[status(thm)],[21,36,theory(equality)])).
cnf(54,negated_conjecture-derived,(esk2_0=X1|big_f(esk1_0,esk2_0)|esk3_1(X1)=X1),inference(spm,[status(thm)],[35,32,theory(equality)])).
cnf(60,negated_conjecture-derived,(esk4_2(X1,X2)!=X2|~big_f(esk4_2(X1,X2),X1)),inference(csr,[status(thm)],[46,10])).
cnf(71,negated_conjecture-derived,(esk3_1(X1)=X1|big_f(esk1_0,esk2_0)),inference(csr,[status(thm)],[54,36])).
cnf(76,negated_conjecture-derived,(esk3_1(X1)=esk2_0|esk4_2(X1,X2)=X2),inference(csr,[status(thm)],[27,32])).
cnf(79,negated_conjecture-derived,(esk3_1(X1)=esk2_0|~big_f(X2,X1)),inference(spm,[status(thm)],[60,76,theory(equality)])).
cnf(87,negated_conjecture-derived,(esk3_1(esk2_0)=esk2_0|esk3_1(X1)=X1),inference(spm,[status(thm)],[79,71,theory(equality)])).
cnf(101,negated_conjecture-derived,(esk3_1(esk2_0)=esk2_0),inference(ef,[status(thm)],[87,theory(equality)])).
cnf(113,negated_conjecture-derived,(esk4_2(esk2_0,X1)=esk1_0|esk4_2(esk2_0,X1)=X1),inference(spm,[status(thm)],[26,101,theory(equality)])).
cnf(114,negated_conjecture-derived,(esk4_2(esk2_0,X2)=X2|esk1_0!=X2),inference(ef,[status(thm)],[113,theory(equality)])).
cnf(143,negated_conjecture-derived,(X1!=esk1_0|esk3_1(esk2_0)!=esk2_0),inference(spm,[status(thm)],[29,114,theory(equality)])).
cnf(150,negated_conjecture-derived,(X1!=esk1_0|\$false),inference(rw,[status(thm)],[143,101,theory(equality)])).
cnf(151,negated_conjecture-derived,(X1!=esk1_0),inference(cn,[status(thm)],[150,theory(equality)])).
cnf(152,negated_conjecture-derived,(\$false),inference(er,[status(thm)],[151,theory(equality)])).
cnf(155,negated_conjecture-derived,(\$false),152,['proof']).
# Proof object ends here.
```

## Mace2 2.2

William McCune
Argonne National Laboratory, USA
mccune@mcs.anl.gov

### Sample SAT model for MGT031-1

```======================= Model #1 at 0.04 seconds:

zero: 0

greater :
| 0 1
--+----
0 | T T
1 | F F

e: 0

number_of_organizations :
| 0 1
--+----
0 | 0 0
1 | 0 0

an_organisation: 0

appear :
| 0 1
--+----
0 | 0 1
1 | 0 0

environment :
0 1
-------
F T

sk1 :
| 0 1
--+----
0 | 0 0
1 | 0 0
Dimension 3 table for subpopulation not printed

cardinality_at_time :
| 0 1
--+----
0 | 0 0
1 | 0 1

efficient_producers: 0

in_environment :
| 0 1
--+----
0 | F F
1 | F T

first_movers: 1

greater_or_equal :
| 0 1
--+----
0 | T T
1 | F T

sk2: 1
end_of_model
```

## Mace4 2004-D

William McCune
Argonne National Laboratory, USA
mccune@mcs.anl.gov

### Sample SAT model for MGT031-1

```-------- Model 1 at 0.02 seconds --------

e : 0

an_organisation : 0

zero : 0

efficient_producers : 0

first_movers : 1

sk2 : 1

appear :
| 0 1
--+----
0 | 0 1
1 | 0 0

number_of_organizations :
| 0 1
--+----
0 | 0 0
1 | 0 0

sk1 :
| 0 1
--+----
0 | 0 0
1 | 0 0

cardinality_at_time :
| 0 1
--+----
0 | 0 0
1 | 0 1

environment :
0 1
-------
0 1

greater :
| 0 1
--+----
0 | 1 1
1 | 0 0

in_environment :
| 0 1
--+----
0 | 0 0
1 | 0 1

greater_or_equal :
| 0 1
--+----
0 | 1 1
1 | 0 1
Sorry, no pretty printing yet for arity 3.
subpopulation(0,0,0) = 0.
subpopulation(0,0,1) = 0.
subpopulation(0,1,0) = 1.
subpopulation(0,1,1) = 1.
subpopulation(1,0,0) = 0.
subpopulation(1,0,1) = 0.
subpopulation(1,1,0) = 0.
subpopulation(1,1,1) = 0.

-------- end of model --------
```

## MathServ 0.62

Jürgen Zimmer
Universität des Saarlandes, German
{jzimmer,serge}@ags.uni-sb.de

```%------------------------------------------------------------------------------
% File       : Otter---3.3
% Problem    : Unknown : TPTP Unknown
% Format     : otter:hypothesis:set(auto),clear(print_given)
% Command    : otter-script %s

% Computer   : Unknown
% Model      : Unknown
% CPU        : Unknown @ Unknown
% Memory     : Unknown
% OS         : Unknown
% CPULimit   : Unknowns

% Result     : Unsatisfiable 0s
% Output     : Refutation 0s
% Statistics : Number of clauses     :   26 (  34 expanded)
%              Depth                 :    8
%              Number of atoms       :   38 (  49 expanded)
%              Maximal clause size   :    4 (   1 average)
%              Maximal term depth    :    2 (   1 average)
% Verified   :

%------------------------------------------------------------------------------
%----TSTP SOLUTION
% 1 [] -killed(agatha,agatha).
cnf(1,initial,
( ~killed(agatha,agatha) ),
file('Unknown',unknown),
[]).

% 2 [] -lives(A)|equal(A,agatha)|equal(A,butler)|equal(A,charles).
cnf(2,initial,
( ~lives(A)
| equal(A,agatha)
| equal(A,butler)
| equal(A,charles) ),
file('Unknown',unknown),
[]).

% 3 [] -killed(A,B)|hates(A,B).
cnf(3,initial,
( ~killed(A,B)
| hates(A,B) ),
file('Unknown',unknown),
[]).

% 4 [] -killed(A,B)| -richer(A,B).
cnf(4,initial,
( ~killed(A,B)
| ~richer(A,B) ),
file('Unknown',unknown),
[]).

% 5 [] -hates(agatha,A)| -hates(charles,A).
cnf(5,initial,
( ~hates(agatha,A)
| ~hates(charles,A) ),
file('Unknown',unknown),
[]).

% 6 [] -hates(agatha,A)|hates(butler,A).
cnf(6,initial,
( ~hates(agatha,A)
| hates(butler,A) ),
file('Unknown',unknown),
[]).

% 7 [] -hates(A,sk_1_y_32725(A)).
cnf(7,initial,
( ~hates(A,sk_1_y_32725(A)) ),
file('Unknown',unknown),
[]).

% 8 [] -equal(agatha,butler).
cnf(8,initial,
( ~equal(agatha,butler) ),
file('Unknown',unknown),
[]).

% 9 [copy,8,flip.1] -equal(butler,agatha).
cnf(9,derived,
( ~equal(butler,agatha) ),
inference(flip,[status(thm)],[
inference(copy,[status(thm)],[8]),theory(equality)]),
[iquote('copy,8,flip.1')]).

% 11 [] lives(sk_0_x_32715).
cnf(11,initial,
( lives(sk_0_x_32715) ),
file('Unknown',unknown),
[]).

% 12 [] killed(sk_0_x_32715,agatha).
cnf(12,initial,
( killed(sk_0_x_32715,agatha) ),
file('Unknown',unknown),
[]).

% 16 [] equal(A,butler)|hates(agatha,A).
cnf(16,initial,
( equal(A,butler)
| hates(agatha,A) ),
file('Unknown',unknown),
[]).

% 17 [] richer(A,agatha)|hates(butler,A).
cnf(17,initial,
( richer(A,agatha)
| hates(butler,A) ),
file('Unknown',unknown),
[]).

% 19 [hyper,12,3] hates(sk_0_x_32715,agatha).
cnf(19,derived,
( hates(sk_0_x_32715,agatha) ),
inference(hyper,[status(thm)],[12,3]),
[iquote('hyper,12,3')]).

% 22 [para_into,12.1.1,2.2.1,unit_del,1,11] equal(sk_0_x_32715,butler)|equal(sk_0_x_32715,charles).
cnf(22,derived,
( equal(sk_0_x_32715,butler)
| equal(sk_0_x_32715,charles) ),
inference(unit_del,[status(thm)],[
inference(para_into,[status(thm)],[12,2,theory(equality)]),1,11]),
[iquote('para_into,12.1.1,2.2.1,unit_del,1,11')]).

% 25 [hyper,16,7] equal(sk_1_y_32725(agatha),butler).
cnf(25,derived,
( equal(sk_1_y_32725(agatha),butler) ),
inference(hyper,[status(thm)],[16,7]),
[iquote('hyper,16,7')]).

% 27 [hyper,16,6] equal(A,butler)|hates(butler,A).
cnf(27,derived,
( equal(A,butler)
| hates(butler,A) ),
inference(hyper,[status(thm)],[16,6]),
[iquote('hyper,16,6')]).

% 29 [para_from,16.1.1,12.1.1] killed(butler,agatha)|hates(agatha,sk_0_x_32715).
cnf(29,derived,
( killed(butler,agatha)
| hates(agatha,sk_0_x_32715) ),
inference(para_from,[status(thm)],[16,12,theory(equality)]),
[iquote('para_from,16.1.1,12.1.1')]).

% 38 [para_from,25.1.1,7.1.2] -hates(agatha,butler).
cnf(38,derived,
( ~hates(agatha,butler) ),
inference(para_from,[status(thm)],[25,7,theory(equality)]),
[iquote('para_from,25.1.1,7.1.2')]).

% 51 [hyper,27,7] equal(sk_1_y_32725(butler),butler).
cnf(51,derived,
( equal(sk_1_y_32725(butler),butler) ),
inference(hyper,[status(thm)],[27,7]),
[iquote('hyper,27,7')]).

% 62 [para_from,51.1.1,7.1.2] -hates(butler,butler).
cnf(62,derived,
( ~hates(butler,butler) ),
inference(para_from,[status(thm)],[51,7,theory(equality)]),
[iquote('para_from,51.1.1,7.1.2')]).

% 65 [hyper,29,4,17,unit_del,62] hates(agatha,sk_0_x_32715).
cnf(65,derived,
( hates(agatha,sk_0_x_32715) ),
inference(unit_del,[status(thm)],[
inference(hyper,[status(thm)],[29,4,17]),62]),
[iquote('hyper,29,4,17,unit_del,62')]).

% 68,67 [para_into,65.1.2,22.1.1,unit_del,38] equal(sk_0_x_32715,charles).
cnf(68,derived,
( equal(sk_0_x_32715,charles) ),
inference(unit_del,[status(thm)],[
inference(para_into,[status(thm)],[65,22,theory(equality)]),38]),
[iquote('para_into,65.1.2,22.1.1,unit_del,38')]).

% 77 [back_demod,19,demod,68] hates(charles,agatha).
cnf(77,derived,
( hates(charles,agatha) ),
inference(demod,[status(thm)],[
inference(back_demod,[status(thm)],[19]),68,theory(equality)]),
[iquote('back_demod,19,demod,68')]).

% 81 [hyper,77,5,16,flip.1] equal(butler,agatha).
cnf(81,derived,
( equal(butler,agatha) ),
inference(flip,[status(thm)],[
inference(hyper,[status(thm)],[77,5,16]),theory(equality)]),
[iquote('hyper,77,5,16,flip.1')]).

% 83 [binary,81.1,9.1] \$F.
cnf(83,derived,
( \$false ),
inference(binary,[status(thm)],[81,9]),
[iquote('binary,81.1,9.1')]).
```

## Otter 3.3

William McCune
Argonne National Laboratory, USA
mccune@mcs.anl.gov

### Sample MIX proof for SYN075-1

```---------------- PROOF ----------------

1 [] -big_f(A,B)|equal(A,a).
2 [] -big_f(A,B)|equal(B,b).
3 [] -equal(A,a)| -equal(B,b)|big_f(A,B).
4 [] -big_f(A,f(B))| -equal(A,g(B))|equal(f(B),B).
5 [] -equal(A,g(B))|big_f(A,f(B))|equal(f(B),B).
8 [] -equal(f(A),A)|big_f(h(A,B),f(A))|equal(h(A,B),B).
9 [] -equal(f(A),A)| -equal(h(A,B),B)| -big_f(h(A,B),f(A)).
11 [] equal(A,A).
13 [hyper,11,5] big_f(g(A),f(A))|equal(f(A),A).
14 [hyper,11,3,11] big_f(a,b).
21 [hyper,13,3,11] big_f(g(b),f(b))|big_f(a,f(b)).
62 [hyper,21,4,11] big_f(a,f(b))|equal(f(b),b).
79 [hyper,62,3,11,factor_simp] big_f(a,f(b)).
81,80 [hyper,79,2] equal(f(b),b).
126 [hyper,80,8,demod,81] big_f(h(b,A),b)|equal(h(b,A),A).
319 [hyper,126,3,80,demod,81,factor_simp] big_f(h(b,a),b).
331,330 [hyper,319,1] equal(h(b,a),a).
335 [para_from,330.1.1,9.3.1,demod,81,331,81,unit_del,11,11,14] \$F.

------------ end of proof -------------
```

### Sample MIX proof for PUZ031-1

```---------------- PROOF ----------------

1 [] animal(A)| -wolf(A).
2 [] animal(A)| -fox(A).
3 [] animal(A)| -bird(A).
5 [] animal(A)| -snail(A).
6 [] plant(A)| -grain(A).
7 [] eats(A,B)|eats(A,C)| -animal(A)| -plant(B)| -animal(C)| -plant(D)| -much_smaller(C,A)| -eats(C,D).
9 [] much_smaller(A,B)| -snail(A)| -bird(B).
10 [] much_smaller(A,B)| -bird(A)| -fox(B).
11 [] much_smaller(A,B)| -fox(A)| -wolf(B).
13 [] -wolf(A)| -grain(B)| -eats(A,B).
15 [] -bird(A)| -snail(B)| -eats(A,B).
18 [] plant(snail_food_of(A))| -snail(A).
19 [] eats(A,snail_food_of(A))| -snail(A).
20 [] -animal(A)| -animal(B)| -grain(C)| -eats(A,B)| -eats(B,C).
23 [factor,7.4.6] eats(A,B)|eats(A,C)| -animal(A)| -plant(B)| -animal(C)| -much_smaller(C,A)| -eats(C,B).
28 [] wolf(a_wolf).
29 [] fox(a_fox).
30 [] bird(a_bird).
32 [] snail(a_snail).
33 [] grain(a_grain).
34 [hyper,28,1] animal(a_wolf).
35 [hyper,29,11,28] much_smaller(a_fox,a_wolf).
36 [hyper,29,2] animal(a_fox).
37 [hyper,30,10,29] much_smaller(a_bird,a_fox).
38 [hyper,30,3] animal(a_bird).
44 [hyper,32,19] eats(a_snail,snail_food_of(a_snail)).
45 [hyper,32,18] plant(snail_food_of(a_snail)).
46 [hyper,32,9,30] much_smaller(a_snail,a_bird).
47 [hyper,32,5] animal(a_snail).
48 [hyper,33,6] plant(a_grain).
50 [hyper,44,7,38,48,47,45,46] eats(a_bird,a_grain)|eats(a_bird,a_snail).
55 [hyper,50,15,30,32] eats(a_bird,a_grain).
56 [hyper,55,23,36,48,38,37] eats(a_fox,a_grain)|eats(a_fox,a_bird).
62 [hyper,56,20,36,38,33,55] eats(a_fox,a_grain).
63 [hyper,62,23,34,48,36,35] eats(a_wolf,a_grain)|eats(a_wolf,a_fox).
67 [hyper,63,13,28,33] eats(a_wolf,a_fox).
69 [hyper,67,20,34,36,33,62] \$F.

------------ end of proof -------------
```

Koen Claessen, Niklas Sörensson
Chalmers University of Technology and Gothenburg University, Sweden
{koen,nik}@cs.chalmers.se

### Solution Description

When it has found a model, Paradox produces a table of definitions for each constant symbol, function symbol, and predicate symbol. The table is sorted alphabetically. In the table, domain elements are represented as positive natural numbers preceded by a ' (tick).

NOTE: In order to save space in the representation of the model, sometimes, some entries in some of the definition tables are missing. This is not a bug! More detailedly, it might happen that for a model with a domain of size n, for some argument position, only a subset {'1,'2,..,'k} of all domain elements is shown, with k < n. What this means is that the entries for other domain elements 'j (with k < j <= n) occurring at that argument position look the same as entries with 'k at that position. Problem NLP041-1.p is an example where a model is represented in such a way.

### Sample Solution to MGT031-1

```an_organisation = '1

appear('1,'1) = '2
appear('1,'2) = '2
appear('2,'1) = '1
appear('2,'2) = '1

cardinality_at_time('1,'1) = '2
cardinality_at_time('1,'2) = '2
cardinality_at_time('2,'1) = '2
cardinality_at_time('2,'2) = '2

e = '1

efficient_producers = '2

environment('1) : FALSE
environment('2) : TRUE

first_movers = '2

greater('1,'1) : TRUE
greater('1,'2) : TRUE
greater('2,'1) : FALSE
greater('2,'2) : TRUE

greater_or_equal('1,'1) : TRUE
greater_or_equal('1,'2) : TRUE
greater_or_equal('2,'1) : FALSE
greater_or_equal('2,'2) : TRUE

in_environment('1,'1) : TRUE
in_environment('1,'2) : TRUE
in_environment('2,'1) : TRUE
in_environment('2,'2) : TRUE

number_of_organizations('1,'1) = '2
number_of_organizations('1,'2) = '1
number_of_organizations('2,'1) = '2
number_of_organizations('2,'2) = '2

sk1('1,'1) = '2
sk1('1,'2) = '2
sk1('2,'1) = '2
sk1('2,'2) = '2

sk2 = '2

subpopulation('1,'1,'1) : TRUE
subpopulation('1,'1,'2) : TRUE
subpopulation('1,'2,'1) : TRUE
subpopulation('1,'2,'2) : TRUE
subpopulation('2,'1,'1) : TRUE
subpopulation('2,'1,'2) : TRUE
subpopulation('2,'2,'1) : TRUE
subpopulation('2,'2,'2) : TRUE

zero = '1
```

### Sample Solution to NLP041-1

```abstraction('1,'1) : FALSE
abstraction('1,'2) : FALSE
abstraction('1,'3) : FALSE
abstraction('1,'4) : TRUE

act('1,'1) : FALSE
act('1,'2) : FALSE
act('1,'3) : TRUE
act('1,'4) : FALSE

actual_world('1) : TRUE

agent('1,'1,'1) : TRUE
agent('1,'1,'2) : TRUE
agent('1,'1,'3) : TRUE
agent('1,'1,'4) : TRUE
agent('1,'2,'1) : TRUE
agent('1,'2,'2) : TRUE
agent('1,'2,'3) : TRUE
agent('1,'2,'4) : TRUE
agent('1,'3,'1) : TRUE
agent('1,'3,'2) : FALSE
agent('1,'3,'3) : FALSE
agent('1,'3,'4) : FALSE
agent('1,'4,'1) : TRUE
agent('1,'4,'2) : TRUE
agent('1,'4,'3) : TRUE
agent('1,'4,'4) : FALSE

animate('1,'1) : TRUE
animate('1,'2) : FALSE
animate('1,'3) : FALSE
animate('1,'4) : FALSE

beverage('1,'1) : FALSE
beverage('1,'2) : TRUE
beverage('1,'3) : FALSE
beverage('1,'4) : FALSE

entity('1,'1) : TRUE
entity('1,'2) : TRUE
entity('1,'3) : FALSE
entity('1,'4) : FALSE

event('1,'1) : FALSE
event('1,'2) : FALSE
event('1,'3) : TRUE
event('1,'4) : FALSE

eventuality('1,'1) : FALSE
eventuality('1,'2) : FALSE
eventuality('1,'3) : TRUE
eventuality('1,'4) : FALSE

existent('1,'1) : TRUE
existent('1,'2) : TRUE
existent('1,'3) : FALSE
existent('1,'4) : FALSE

female('1,'1) : TRUE
female('1,'2) : FALSE
female('1,'3) : FALSE
female('1,'4) : FALSE

food('1,'1) : FALSE
food('1,'2) : TRUE
food('1,'3) : FALSE
food('1,'4) : FALSE

forename('1,'1) : FALSE
forename('1,'2) : FALSE
forename('1,'3) : FALSE
forename('1,'4) : TRUE

general('1,'1) : FALSE
general('1,'2) : FALSE
general('1,'3) : FALSE
general('1,'4) : TRUE

human('1,'1) : TRUE
human('1,'2) : FALSE
human('1,'3) : FALSE
human('1,'4) : FALSE

human_person('1,'1) : TRUE
human_person('1,'2) : FALSE
human_person('1,'3) : FALSE
human_person('1,'4) : FALSE

impartial('1,'1) : TRUE
impartial('1,'2) : TRUE
impartial('1,'3) : FALSE
impartial('1,'4) : FALSE

living('1,'1) : TRUE
living('1,'2) : FALSE
living('1,'3) : FALSE
living('1,'4) : FALSE

mia_forename('1,'1) : FALSE
mia_forename('1,'2) : FALSE
mia_forename('1,'3) : FALSE
mia_forename('1,'4) : TRUE

nonexistent('1,'1) : FALSE
nonexistent('1,'2) : FALSE
nonexistent('1,'3) : TRUE
nonexistent('1,'4) : TRUE

nonhuman('1,'1) : FALSE
nonhuman('1,'2) : TRUE
nonhuman('1,'3) : TRUE
nonhuman('1,'4) : TRUE

nonliving('1,'1) : FALSE
nonliving('1,'2) : TRUE
nonliving('1,'3) : TRUE
nonliving('1,'4) : TRUE

nonreflexive('1,'1) : FALSE
nonreflexive('1,'2) : FALSE
nonreflexive('1,'3) : TRUE
nonreflexive('1,'4) : TRUE

object('1,'1) : FALSE
object('1,'2) : TRUE
object('1,'3) : FALSE
object('1,'4) : FALSE

of('1,'1,'1) : FALSE
of('1,'1,'2) : TRUE
of('1,'1,'3) : TRUE
of('1,'1,'4) : TRUE
of('1,'2,'1) : FALSE
of('1,'2,'2) : TRUE
of('1,'2,'3) : TRUE
of('1,'2,'4) : TRUE
of('1,'3,'1) : FALSE
of('1,'3,'2) : TRUE
of('1,'3,'3) : TRUE
of('1,'3,'4) : TRUE
of('1,'4,'1) : TRUE
of('1,'4,'2) : TRUE
of('1,'4,'3) : TRUE
of('1,'4,'4) : TRUE

order('1,'1) : FALSE
order('1,'2) : FALSE
order('1,'3) : TRUE
order('1,'4) : FALSE

organism('1,'1) : TRUE
organism('1,'2) : FALSE
organism('1,'3) : FALSE
organism('1,'4) : FALSE

past('1,'1) : FALSE
past('1,'2) : FALSE
past('1,'3) : TRUE
past('1,'4) : FALSE

patient('1,'1,'1) : TRUE
patient('1,'1,'2) : TRUE
patient('1,'1,'3) : TRUE
patient('1,'1,'4) : TRUE
patient('1,'2,'1) : TRUE
patient('1,'2,'2) : TRUE
patient('1,'2,'3) : TRUE
patient('1,'2,'4) : TRUE
patient('1,'3,'1) : FALSE
patient('1,'3,'2) : TRUE
patient('1,'3,'3) : TRUE
patient('1,'3,'4) : TRUE
patient('1,'4,'1) : FALSE
patient('1,'4,'2) : FALSE
patient('1,'4,'3) : FALSE
patient('1,'4,'4) : TRUE

relation('1,'1) : FALSE
relation('1,'2) : FALSE
relation('1,'3) : FALSE
relation('1,'4) : TRUE

relname('1,'1) : FALSE
relname('1,'2) : FALSE
relname('1,'3) : FALSE
relname('1,'4) : TRUE

shake_beverage('1,'1) : FALSE
shake_beverage('1,'2) : TRUE
shake_beverage('1,'3) : FALSE
shake_beverage('1,'4) : FALSE

singleton('1,'1) : TRUE
singleton('1,'2) : TRUE
singleton('1,'3) : TRUE
singleton('1,'4) : TRUE

skc5 = '1

skc6 = '3

skc7 = '2

skc8 = '4

skc9 = '1

specific('1,'1) : TRUE
specific('1,'2) : TRUE
specific('1,'3) : TRUE
specific('1,'4) : FALSE

substance_matter('1,'1) : FALSE
substance_matter('1,'2) : TRUE
substance_matter('1,'3) : FALSE
substance_matter('1,'4) : FALSE

thing('1,'1) : TRUE
thing('1,'2) : TRUE
thing('1,'3) : TRUE
thing('1,'4) : TRUE

unisex('1,'1) : FALSE
unisex('1,'2) : TRUE
unisex('1,'3) : TRUE
unisex('1,'4) : TRUE

woman('1,'1) : TRUE
woman('1,'2) : FALSE
woman('1,'3) : FALSE
woman('1,'4) : FALSE
```

Koen Claessen, Niklas Sörensson
Chalmers University of Technology and Gothenburg University, Sweden
{koen,nik}@cs.chalmers.se

### Solution Description

When it has found a model, Paradox produces a table of definitions for each constant symbol, function symbol, and predicate symbol. The table is sorted alphabetically. In the table, domain elements are represented as positive natural numbers preceded by a ' (tick).

NOTE: In order to save space in the representation of the model, sometimes, some entries in some of the definition tables are missing. This is not a bug! More detailedly, it might happen that for a model with a domain of size n, for some argument position, only a subset {'1,'2,..,'k} of all domain elements is shown, with k < n. What this means is that the entries for other domain elements 'j (with k < j <= n) occurring at that argument position look the same as entries with 'k at that position. Problem NLP041-1.p is an example where a model is represented in such a way.

### Sample Solution to MGT031-1

```an_organisation = '1

appear('1,'1) = '2
appear('1,'2) = '2
appear('2,'1) = '1
appear('2,'2) = '1

cardinality_at_time('1,'1) = '2
cardinality_at_time('1,'2) = '2
cardinality_at_time('2,'1) = '2
cardinality_at_time('2,'2) = '2

e = '1

efficient_producers = '2

environment('1) : FALSE
environment('2) : TRUE

first_movers = '2

greater('1,'1) : TRUE
greater('1,'2) : TRUE
greater('2,'1) : FALSE
greater('2,'2) : TRUE

greater_or_equal('1,'1) : TRUE
greater_or_equal('1,'2) : TRUE
greater_or_equal('2,'1) : FALSE
greater_or_equal('2,'2) : TRUE

in_environment('1,'1) : TRUE
in_environment('1,'2) : TRUE
in_environment('2,'1) : TRUE
in_environment('2,'2) : TRUE

number_of_organizations('1,'1) = '2
number_of_organizations('1,'2) = '1
number_of_organizations('2,'1) = '2
number_of_organizations('2,'2) = '2

sk1('1,'1) = '2
sk1('1,'2) = '2
sk1('2,'1) = '2
sk1('2,'2) = '2

sk2 = '2

subpopulation('1,'1,'1) : TRUE
subpopulation('1,'1,'2) : TRUE
subpopulation('1,'2,'1) : TRUE
subpopulation('1,'2,'2) : TRUE
subpopulation('2,'1,'1) : TRUE
subpopulation('2,'1,'2) : TRUE
subpopulation('2,'2,'1) : TRUE
subpopulation('2,'2,'2) : TRUE

zero = '1
```

### Sample Solution to NLP041-1

```abstraction('1,'1) : FALSE
abstraction('1,'2) : FALSE
abstraction('1,'3) : FALSE
abstraction('1,'4) : TRUE

act('1,'1) : FALSE
act('1,'2) : FALSE
act('1,'3) : TRUE
act('1,'4) : FALSE

actual_world('1) : TRUE

agent('1,'1,'1) : TRUE
agent('1,'1,'2) : TRUE
agent('1,'1,'3) : TRUE
agent('1,'1,'4) : TRUE
agent('1,'2,'1) : TRUE
agent('1,'2,'2) : TRUE
agent('1,'2,'3) : TRUE
agent('1,'2,'4) : TRUE
agent('1,'3,'1) : TRUE
agent('1,'3,'2) : FALSE
agent('1,'3,'3) : FALSE
agent('1,'3,'4) : FALSE
agent('1,'4,'1) : TRUE
agent('1,'4,'2) : TRUE
agent('1,'4,'3) : TRUE
agent('1,'4,'4) : FALSE

animate('1,'1) : TRUE
animate('1,'2) : FALSE
animate('1,'3) : FALSE
animate('1,'4) : FALSE

beverage('1,'1) : FALSE
beverage('1,'2) : TRUE
beverage('1,'3) : FALSE
beverage('1,'4) : FALSE

entity('1,'1) : TRUE
entity('1,'2) : TRUE
entity('1,'3) : FALSE
entity('1,'4) : FALSE

event('1,'1) : FALSE
event('1,'2) : FALSE
event('1,'3) : TRUE
event('1,'4) : FALSE

eventuality('1,'1) : FALSE
eventuality('1,'2) : FALSE
eventuality('1,'3) : TRUE
eventuality('1,'4) : FALSE

existent('1,'1) : TRUE
existent('1,'2) : TRUE
existent('1,'3) : FALSE
existent('1,'4) : FALSE

female('1,'1) : TRUE
female('1,'2) : FALSE
female('1,'3) : FALSE
female('1,'4) : FALSE

food('1,'1) : FALSE
food('1,'2) : TRUE
food('1,'3) : FALSE
food('1,'4) : FALSE

forename('1,'1) : FALSE
forename('1,'2) : FALSE
forename('1,'3) : FALSE
forename('1,'4) : TRUE

general('1,'1) : FALSE
general('1,'2) : FALSE
general('1,'3) : FALSE
general('1,'4) : TRUE

human('1,'1) : TRUE
human('1,'2) : FALSE
human('1,'3) : FALSE
human('1,'4) : FALSE

human_person('1,'1) : TRUE
human_person('1,'2) : FALSE
human_person('1,'3) : FALSE
human_person('1,'4) : FALSE

impartial('1,'1) : TRUE
impartial('1,'2) : TRUE
impartial('1,'3) : FALSE
impartial('1,'4) : FALSE

living('1,'1) : TRUE
living('1,'2) : FALSE
living('1,'3) : FALSE
living('1,'4) : FALSE

mia_forename('1,'1) : FALSE
mia_forename('1,'2) : FALSE
mia_forename('1,'3) : FALSE
mia_forename('1,'4) : TRUE

nonexistent('1,'1) : FALSE
nonexistent('1,'2) : FALSE
nonexistent('1,'3) : TRUE
nonexistent('1,'4) : TRUE

nonhuman('1,'1) : FALSE
nonhuman('1,'2) : TRUE
nonhuman('1,'3) : TRUE
nonhuman('1,'4) : TRUE

nonliving('1,'1) : FALSE
nonliving('1,'2) : TRUE
nonliving('1,'3) : TRUE
nonliving('1,'4) : TRUE

nonreflexive('1,'1) : FALSE
nonreflexive('1,'2) : FALSE
nonreflexive('1,'3) : TRUE
nonreflexive('1,'4) : TRUE

object('1,'1) : FALSE
object('1,'2) : TRUE
object('1,'3) : FALSE
object('1,'4) : FALSE

of('1,'1,'1) : FALSE
of('1,'1,'2) : TRUE
of('1,'1,'3) : TRUE
of('1,'1,'4) : TRUE
of('1,'2,'1) : FALSE
of('1,'2,'2) : TRUE
of('1,'2,'3) : TRUE
of('1,'2,'4) : TRUE
of('1,'3,'1) : FALSE
of('1,'3,'2) : TRUE
of('1,'3,'3) : TRUE
of('1,'3,'4) : TRUE
of('1,'4,'1) : TRUE
of('1,'4,'2) : TRUE
of('1,'4,'3) : TRUE
of('1,'4,'4) : TRUE

order('1,'1) : FALSE
order('1,'2) : FALSE
order('1,'3) : TRUE
order('1,'4) : FALSE

organism('1,'1) : TRUE
organism('1,'2) : FALSE
organism('1,'3) : FALSE
organism('1,'4) : FALSE

past('1,'1) : FALSE
past('1,'2) : FALSE
past('1,'3) : TRUE
past('1,'4) : FALSE

patient('1,'1,'1) : TRUE
patient('1,'1,'2) : TRUE
patient('1,'1,'3) : TRUE
patient('1,'1,'4) : TRUE
patient('1,'2,'1) : TRUE
patient('1,'2,'2) : TRUE
patient('1,'2,'3) : TRUE
patient('1,'2,'4) : TRUE
patient('1,'3,'1) : FALSE
patient('1,'3,'2) : TRUE
patient('1,'3,'3) : TRUE
patient('1,'3,'4) : TRUE
patient('1,'4,'1) : FALSE
patient('1,'4,'2) : FALSE
patient('1,'4,'3) : FALSE
patient('1,'4,'4) : TRUE

relation('1,'1) : FALSE
relation('1,'2) : FALSE
relation('1,'3) : FALSE
relation('1,'4) : TRUE

relname('1,'1) : FALSE
relname('1,'2) : FALSE
relname('1,'3) : FALSE
relname('1,'4) : TRUE

shake_beverage('1,'1) : FALSE
shake_beverage('1,'2) : TRUE
shake_beverage('1,'3) : FALSE
shake_beverage('1,'4) : FALSE

singleton('1,'1) : TRUE
singleton('1,'2) : TRUE
singleton('1,'3) : TRUE
singleton('1,'4) : TRUE

skc5 = '1

skc6 = '3

skc7 = '2

skc8 = '4

skc9 = '1

specific('1,'1) : TRUE
specific('1,'2) : TRUE
specific('1,'3) : TRUE
specific('1,'4) : FALSE

substance_matter('1,'1) : FALSE
substance_matter('1,'2) : TRUE
substance_matter('1,'3) : FALSE
substance_matter('1,'4) : FALSE

thing('1,'1) : TRUE
thing('1,'2) : TRUE
thing('1,'3) : TRUE
thing('1,'4) : TRUE

unisex('1,'1) : FALSE
unisex('1,'2) : TRUE
unisex('1,'3) : TRUE
unisex('1,'4) : TRUE

woman('1,'1) : TRUE
woman('1,'2) : FALSE
woman('1,'3) : FALSE
woman('1,'4) : FALSE
```

## Prover9 July-2005

William McCune
Argonne National Laboratory, USA
mccune@mcs.anl.gov
```Prover9 (July-2005) Sample Proofs

Justifications in proofs.

Each clause is identified by an integer, and literals
are identified by [a,b,c,...].

Primary justifications (first operation in justification):

input               input clause
clausify            from transforming FOF to clauses
copy                copy a clause
resolve             binary resolution
hyper               hyperresolution (positive or negative)
ur                  unit-resulting resolution
factor              factoring
xx_res              resolution with x=x
para                paramodulation
back_demod          back demodulation
back_unit_del       back unit deletion
new_symbol          introduction of new function symbol

Secondary justifications:

demod               rewriting by a sequence of equations
flip                flip equality literal
xx                  simplification with x=x
merge               merge identical literals
unit_del            unit deletion (simplifying resolution)
```

### Sample MIX proof for SYN075-1

```-------- Proof 1 -------- (0.01 + 0.02 seconds)

-------- PROOF --------
1 - big_f(A,B) | A = a.  [input]
2 - big_f(A,B) | B = b.  [input]
3 A != a | B != b | big_f(A,B).  [input]
4 - big_f(A,f(B)) | A != g(B) | f(B) = B.  [input]
6 A != g(B) | big_f(A,f(B)) | f(B) = B.  [input]
11 - big_f(A,B) | a = A.  [copy 1 flip b]
12 - big_f(A,B) | b = B.  [copy 2 flip b]
13 a != A | b != B | big_f(A,B).  [copy 3 flip a flip b]
14 - big_f(A,f(B)) | g(B) != A | f(B) = B.  [copy 4 flip b]
15 g(A) != B | big_f(B,f(A)) | f(A) = A.  [copy 6 flip a]
18 f(A) != A | big_f(h(A,B),f(A)) | h(A,B) = B.  [input]
19 f(A) != A | h(A,B) != B | - big_f(h(A,B),f(A)).  [input]
21 b != A | big_f(a,A).  [xx_res (13 a)]
22 a != A | big_f(A,b).  [xx_res (13 b)]
23 big_f(a,b).  [xx_res (21 a)]
24 - big_f(g(A),f(A)) | f(A) = A.  [xx_res (14 b)]
25 big_f(g(A),f(A)) | f(A) = A.  [xx_res (15 a)]
27 big_f(g(b),f(b)) | big_f(a,f(b)).  [resolve (25 b 21 a_flip)]
40 big_f(a,f(b)) | f(b) = b.  [resolve (27 a 24 a)]
47 big_f(a,f(b)).  [resolve (40 b 21 a_flip) merge b]
48 f(b) = b.  [resolve (47 a 12 a) flip a]
51 big_f(h(b,A),b) | h(b,A) = A.  [resolve (18 a 48 a) demod (48)]
53 big_f(h(b,a),b).  [resolve (51 b 22 a_flip) merge b]
63 h(b,a) = a.  [resolve (53 a 11 a) flip a]
67 \$F.  [resolve (63 a 19 b) demod (48 63 48) xx a unit_del (a 23)]
-------- end of proof  -------

THEOREM PROVED
```

### Sample MIX proof for PUZ031-1

FOF problems are given to a procedure that attempts to reduce the problem to independent subproblems. In this case (SYN075-1), the procedure does not give independent subproblems. (An example that does give independent subproblems is given after this proof.) Proofs of transformation steps from FOF to independent FOF subproblems, and from FOF to clauses, are not given.
```-------- Proof 1 -------- (0.01 + 0.00 seconds)

-------- PROOF --------
1 - big_f(A,B) | A = \$c1.  [clausify]
2 - big_f(A,B) | B = \$c2.  [clausify]
3 big_f(A,B) | A != \$c1 | B != \$c2.  [clausify]
5 big_f(A,\$f1(B)) | A != \$f2(B) | \$f1(B) = B.  [clausify]
8 - big_f(A,B) | \$c1 = A.  [copy 1 flip b]
9 - big_f(A,B) | \$c2 = B.  [copy 2 flip b]
10 big_f(A,B) | \$c1 != A | \$c2 != B.  [copy 3 flip b flip c]
12 big_f(A,\$f1(B)) | \$f2(B) != A | \$f1(B) = B.  [copy 5 flip b]
13 big_f(\$f3(A,B),\$f1(A)) | \$f3(A,B) = B | \$f1(A) != A.  [clausify]
14 - big_f(\$f3(A,B),\$f1(A)) | \$f3(A,B) != B | \$f1(A) != A.  [clausify]
15 big_f(\$c1,A) | \$c2 != A.  [xx_res (10 b)]
16 big_f(A,\$c2) | \$c1 != A.  [xx_res (10 c)]
17 big_f(\$c1,\$c2).  [xx_res (15 b)]
18 big_f(\$f2(A),\$f1(A)) | \$f1(A) = A.  [xx_res (12 b)]
21 big_f(\$f2(\$c2),\$f1(\$c2)) | big_f(\$c1,\$f1(\$c2)).  [resolve (18 b 15 b_flip)]
50 big_f(\$c1,\$f1(\$c2)) | \$f1(\$c2) = \$c2.  [resolve (21 a 9 a) flip b]
54 big_f(\$c1,\$f1(\$c2)).  [resolve (50 b 15 b_flip) merge b]
64 \$f1(\$c2) = \$c2.  [resolve (54 a 9 a) flip a]
68 big_f(\$f3(\$c2,A),\$c2) | \$f3(\$c2,A) = A.  [resolve (64 a 13 c) demod (64)]
72 big_f(\$f3(\$c2,\$c1),\$c2).  [resolve (68 b 16 b_flip) merge b]
77 \$f3(\$c2,\$c1) = \$c1.  [resolve (72 a 8 a) flip a]
78 \$F.  [resolve (77 a 14 b) demod (77 64 64) xx b unit_del (a 17)]
-------- end of proof  -------

THEOREM PROVED
```
An example that demonstrates FOF problem reduction.

Problem (negated): -(a = b -> (p(a) <-> p(b))).

In the output:

```% Problem reduction gives 2 independent subproblems.

% Subproblem 1 (negated):  (=(b,a) & p(a) & - p(b)).

-------- PROOF --------
1 b = a.  [clausify]
2 p(a).  [clausify]
3 - p(b).  [clausify]
4 b = a.  [copy 1]
5 p(a).  [copy 2]
6 - p(a).  [copy 3 demod (4)]
7 \$F.  [resolve (6 a 5 a)]
-------- end of proof  -------

% Subproblem 2 (negated):  (=(b,a) & - p(a) & p(b)).

-------- PROOF --------
1 b = a.  [clausify]
2 - p(a).  [clausify]
3 p(b).  [clausify]
4 a = b.  [copy 1 flip a]
5 - p(b).  [copy 2 demod (4)]
6 p(b).  [copy 3]
7 \$F.  [resolve (6 a 5 a)]
-------- end of proof  -------

% All 2 subproblems have been proved, so we are done.

THEOREM PROVED
```

## THEO JN05

Monty Newborn
newborn@cs.mcgill.ca

### Sample MIX proof for SYN075-1

```Rating   : 0.09 v2.7.0    Status   : Unsatisfiable
Predicates: equal big_f
Functions: aC  bC  : h  f  g       Renamed predicates:  E. big_f
EQ:  12.11.2    ESAF: 7 8 9 10    ESAP: 3 4

----------------------------------------------------------------------
MODIFY THEOREM

Nodes searched last time = 0
Time taken = 1     Time to go = 599    o_maxtime = 299

Weaken clause: 19S ~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],f[x]]
Weakened to: 0 19S ~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],z] ... ?

LEVEL  CLAUSE  LITERAL POSITION     NEW   OLD HEURISTIC
0      19       3        4         2    80000101
--------------------------------------------------------------------

Axioms:
1 >~E.[x,aC] ~E.[y,bC] big_f[x,y]   2: ~E.[x,y] ~E.[y,z] E.[x,z]
3: ~big_f[x,y] ~E.[x,z] big_f[z,y]  4: ~big_f[x,y] ~E.[y,z] big_f[x,z]
5 >~big_f[x,y] E.[x,aC]             6: ~big_f[x,y] E.[y,bC]
7: ~E.[x,y] E.[h[x,z],h[y,z]]       8: ~E.[x,y] E.[h[z,x],h[z,y]]
9: ~E.[x,y] E.[f[x],f[y]]          10: ~E.[x,y] E.[g[x],g[y]]
11: ~E.[x,y] E.[y,x]                12 >E.[x,x]

Negated conclusion:
13# ~big_f[x,f[y]] E.[x,g[y]] big_f[h[y,z],f[y]] ~big_f[h[y,z],f[y]]
14S ~E.[x,g[y]] big_f[x,f[y]] big_f[h[y,z],f[y]] E.[h[y,z],z]
15S ~E.[x,g[y]] big_f[x,f[y]] ~E.[h[y,z],z] ~big_f[h[y,z],f[y]]
16#>~big_f[x,f[y]] ~E.[x,g[y]] E.[f[y],y]
17#>~E.[x,g[y]] big_f[x,f[y]] E.[f[y],y]
18S>~E.[f[x],x] big_f[h[x,y],f[x]] E.[h[x,y],y]
19S>~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],z] ... ?

---------------
Phase 0 clauses used in proof:
20S>(17b*16a) ~E.[x,g[y]] E.[f[y],y]

Phases 1 and 2 clauses used in proof:
21S>(20a,12a) E.[f[x],x]

22S>(20b,18a) ~E.[x,g[y]] big_f[h[y,z],f[y]] E.[h[y,z],z]
23S>(22b,5a)  ~E.[x,g[y]] E.[h[y,z],z] E.[h[y,z],aC]
24S>(23a,12a) E.[h[x,y],y] E.[h[x,y],aC]
25S>(24ab)    E.[h[x,aC],aC]

26S>(20a,12a) E.[f[x],x]
27S>(26a,1a)  ~E.[x,bC] big_f[f[aC],x]
28S>[27b,21a] ~E.[x,bC] big_f[aC,x]
29S>(28a,12a) big_f[aC,bC]

30S>(20b,19a) ~E.[x,g[y]] ~E.[h[y,z],z] ~big_f[h[y,z],u] ... ?
31S>(30b,5b)  ~E.[x,g[y]] ~big_f[h[y,aC],z] ~big_f[h[y,aC],u] ... ?
32S>[31b,25a] ~E.[x,g[y]] ~big_f[aC,z] ~big_f[h[y,aC],u] ... ?
33S>[32c,25a] ~E.[x,g[y]] ~big_f[aC,z] ~big_f[aC,u] ... ?
34S>(33a,12a) ~big_f[aC,x] ~big_f[aC,y] ... ?
35S>(34a,29a) ~big_f[aC,y] ... ?
36S>(35a,29a) [] ... ?

END OF WEAKENED PROOF

-----------------------------------------------------------------
RECONSIDER PROOF

Reinstated base clause: 19S>~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],f[x]] ... ?

-----------------------------------------------------------------

List of useful clauses from weakened proof:

20S (17b,16a) ~E.[x,g[y]] E.[f[y],y]
21S (20a,12a) E.[f[x],x]
22# (20b,18a) ~E.[x,g[y]] big_f[h[y,z],f[y]] E.[h[y,z],z]
23# (22b,5a)  ~E.[x,g[y]] E.[h[y,z],z] E.[h[y,z],aC]
24S (23a,12a) E.[h[x,y],y] E.[h[x,y],aC]
25S (24ab)    E.[h[x,aC],aC]
26# (20a,12a) E.[f[x],x]
27# (26a,1a)  ~E.[x,bC] big_f[f[aC],x]
28S (27b,21a) ~E.[x,bC] big_f[aC,x]
29S (28a,12a) big_f[aC,bC]
30: (20b,19a) ~E.[x,g[y]] ~E.[h[y,z],z] ~big_f[h[y,z],f[y]]
31: (30b,5b)  ~E.[x,g[y]] ~big_f[h[y,aC],f[y]] ~big_f[h[y,aC],z]

End Final ulist

--------------------------------------------------------------
ANALYSIS OF WEAKENED PROOF

Clause 19 was weakened:  19S>~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],f[x]]
Length of weakened proof is 17 inferences.
Nodes searched for weakened proof is 38.
12 clauses in weakened proof are usable when proving given theorem.
Of these clauses, 8 will be added to the base clauses.
3 of given 12 axioms used in weakened proof will be placed in the sos.
4 of given 7 clauses in sos were used in weakened proof.

Proof of weakened version may be useful.
----------------------------------------------------------------

PHASE 0: 0 s, PHASE 1: 0 s, PHASE 2: 1 s ACCUM: 0  Total Time: 1 s
NOD: 38         RES: 82         FAC: 12         T: 12  V: 6  L: 3
CTE: 73         CTH: 0          CTF: 0          CSZ: 16777216
UTE: 23         UTH: 20         UTF: 0          SBA: 5
BAS: 19         RED: 18         LEN: 1+16=17

----------------------------------------------------------------------
MODIFY THEOREM

Nodes searched last time = 38
Time taken = 2
Time to go = 598
o_maxtime = 299

Proof found with 1 weakening. Had weakened clause 19 (used).
Set weakened_clause_count to 0, o_maxtime = timeToGo

Single weakening proof found => This time none.
----------------------------------------------------------------------

Axioms:
1S ~E.[x,aC] ~E.[y,bC] big_f[x,y]   2: ~E.[x,y] ~E.[y,z] E.[x,z]
3: ~big_f[x,y] ~E.[x,z] big_f[z,y]  4: ~big_f[x,y] ~E.[y,z] big_f[x,z]
5S ~big_f[x,y] E.[x,aC]             6: ~big_f[x,y] E.[y,bC]
7: ~E.[x,y] E.[h[x,z],h[y,z]]       8: ~E.[x,y] E.[h[z,x],h[z,y]]
9: ~E.[x,y] E.[f[x],f[y]]          10: ~E.[x,y] E.[g[x],g[y]]
11: ~E.[x,y] E.[y,x]                12S E.[x,x]

Negated conclusion:
13# ~big_f[x,f[y]] E.[x,g[y]] big_f[h[y,z],f[y]] ~big_f[h[y,z],f[y]]
14S ~E.[x,g[y]] big_f[x,f[y]] big_f[h[y,z],f[y]] E.[h[y,z],z]
15# ~E.[x,g[y]] big_f[x,f[y]] ~E.[h[y,z],z] ~big_f[h[y,z],f[y]]
16# ~big_f[x,f[y]] ~E.[x,g[y]] E.[f[y],y]
17# ~E.[x,g[y]] big_f[x,f[y]] E.[f[y],y]
18# ~E.[f[x],x] big_f[h[x,y],f[x]] E.[h[x,y],y]
19#>~E.[f[x],x] ~E.[h[x,y],y] ~big_f[h[x,y],f[x]]

---------------
Weakened clauses used in proof:
20S (17b,16a) ~E.[x,g[y]] E.[f[y],y]
21S (20a,12a) E.[f[x],x]
22# (20b,18a) ~E.[x,g[y]] big_f[h[y,z],f[y]] E.[h[y,z],z]
23# (22b,5a)  ~E.[x,g[y]] E.[h[y,z],z] E.[h[y,z],aC]
24S (23a,12a) E.[h[x,y],y] E.[h[x,y],aC]
25S (24a,0b)  E.[h[x,aC],aC]
26# (20a,12a) E.[f[x],x]
27# (26a,1a)  ~E.[x,bC] big_f[f[aC],x]
28S (27b,21a) ~E.[x,bC] big_f[aC,x]
29S (28a,12a) big_f[aC,bC]

Phase 0 clauses used in proof:
21S>E.[f[x],x]    (Clause 21 in weakened proof)
23S>E.[h[x,aC],aC]    (Clause 25 in weakened proof)
25S>big_f[aC,bC]    (Clause 29 in weakened proof)
29S>(19a*21a) ~E.[h[x,y],y] ~big_f[h[x,y],f[x]]

Phases 1 and 2 clauses used in proof:
30S>(29a,23a) ~big_f[h[x,aC],f[x]]
31S>[30a,23a] ~big_f[aC,f[x]]
32S>[31a,21a] ~big_f[aC,x]
33S>(32a,25a) []

END OF PROOF

PHASE 0: 0 s, PHASE 1: 1 s, PHASE 2: -NA- ACCUM: 1  Total Time: 2 s
NOD: 1          RES: 1          FAC: 0          T: 12  V: 6  L: 3
CTE: 25         CTH: 0          CTF: 0          CSZ: 16777216
UTE: 26         UTH: 4          UTF: 0          SBA: 5
BAS: 19         RED: 24         LEN: 4+4=8
```

### Sample MIX proof for SYN075+1

```big_f(z,u) | ~equal(z,SK1()) | ~equal(u,SK2())
~equal(x,y) | ~equal(y,z) | equal(x,z)
~big_f(x,y) | ~equal(y,z) | big_f(x,z)
~big_f(x,y) | ~equal(x,z) | big_f(z,y)
~big_f(z,u) | equal(u,SK2())
~big_f(z,u) | equal(z,SK1())
~equal(x,y) | equal(y,x)
equal(x,x)

negated_conclusion

~big_f(SK5(x,v),SK3(x)) | big_f(SK5(x,v),SK3(x)) | big_f(u,SK3(x)) | ~equal(u,SK4(x))
~big_f(SK5(x,v),SK3(x)) | big_f(SK5(x,v),SK3(x)) | ~big_f(u,SK3(x)) | equal(u,SK4(x))
equal(SK5(x,v),v) | big_f(SK5(x,v),SK3(x)) | big_f(u,SK3(x)) | ~equal(u,SK4(x))
equal(SK5(x,v),v) | big_f(SK5(x,v),SK3(x)) | ~big_f(u,SK3(x)) | equal(u,SK4(x))
~big_f(SK5(x,v),SK3(x)) | ~equal(SK5(x,v),v) | big_f(u,SK3(x)) | ~equal(u,SK4(x))
~big_f(SK5(x,v),SK3(x)) | ~equal(SK5(x,v),v) | ~big_f(u,SK3(x)) | equal(u,SK4(x))
equal(SK5(x,v),v) | ~equal(SK5(x,v),v) | big_f(u,SK3(x)) | ~equal(u,SK4(x))
equal(SK5(x,v),v) | ~equal(SK5(x,v),v) | ~big_f(u,SK3(x)) | equal(u,SK4(x))
~big_f(SK5(x,v),SK3(x)) | big_f(SK5(x,v),SK3(x)) | ~equal(SK3(x),x)
equal(SK5(x,v),v) | big_f(SK5(x,v),SK3(x)) | ~equal(SK3(x),x)
~big_f(SK5(x,v),SK3(x)) | ~equal(SK5(x,v),v) | ~equal(SK3(x),x)
equal(SK5(x,v),v) | ~equal(SK5(x,v),v) | ~equal(SK3(x),x)
equal(SK3(x),x) | big_f(u,SK3(x)) | ~equal(u,SK4(x))
equal(SK3(x),x) | ~big_f(u,SK3(x)) | equal(u,SK4(x))
equal(SK3(x),x) | ~equal(SK3(x),x)

Predicates: big_f equal
Functions: SK1  SK2  : SK5  SK3  SK4
Renamed predicates:  big_f E.
EQ:  12.11.2    ESAF: 5 6 7 8    ESAP: 3 4
OPT: k1 m1 z0 h1 n1 b1  x12:X6:N5 v6 l3 t600/600

----------------------------------------------------------------------
MODIFY THEOREM

Nodes searched last time = 1
Time taken = 0
Time to go = 600
o_maxtime = 300

Weaken clause: 23S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~E.[SK3[x],x]
Weakened to: 0 23S ~big_f[SK5[x,y],z] ~E.[SK5[x,y],y] ~E.[SK3[x],x] ... ?

LEVEL  CLAUSE  LITERAL POSITION     NEW   OLD HEURISTIC
0      23       1        4         2    80000101
--------------------------------------------------------------------

0
1 {T1 N61-61 [C226 H0 h0 U38 u24 f0] E2 s16 t0 L0}
2 {T1 N218-218 [C813 H171 h0 U51 u54 f0] E5 s74 t0 L0}* .

Weakened proof obtained; details coming!!

#.@.@.1 {T1 N266-48 [C193 H0 h0 U11 u2 f0] E2 s88 t0 L0}\$

Axioms:
1 >big_f[x,y] ~E.[x,SK1] ~E.[y,SK2] 2: ~E.[x,y] ~E.[y,z] E.[x,z]
3: ~big_f[x,y] ~E.[y,z] big_f[x,z]  4: ~big_f[x,y] ~E.[x,z] big_f[z,y]
5: ~E.[x,y] E.[SK5[x,z],SK5[y,z]]   6: ~E.[x,y] E.[SK5[z,x],SK5[z,y]]
7: ~E.[x,y] E.[SK3[x],SK3[y]]       8: ~E.[x,y] E.[SK4[x],SK4[y]]
9 >~big_f[x,y] E.[y,SK2]           10 >~big_f[x,y] E.[x,SK1]
11: ~E.[x,y] E.[y,x]                12 >E.[x,x]

Negated conclusion:
13# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] big_f[z,SK3[x]] ~E.[z,SK4[x]]
14# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] ~big_f[z,SK3[x]] E.[z,SK4[x]]
15S E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] big_f[z,SK3[x]] ~E.[z,SK4[x]]
16S E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] ~big_f[z,SK3[x]] E.[z,SK4[x]]
17S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] big_f[z,SK3[x]] ~E.[z,SK4[x]]
18S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~big_f[z,SK3[x]] E.[z,SK4[x]]
19# E.[SK5[x,y],y] ~E.[SK5[x,y],y] big_f[z,SK3[x]] ~E.[z,SK4[x]]
20# E.[SK5[x,y],y] ~E.[SK5[x,y],y] ~big_f[z,SK3[x]] E.[z,SK4[x]]
21# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] ~E.[SK3[x],x]
22S>E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] ~E.[SK3[x],x]
23S>~big_f[SK5[x,y],z] ~E.[SK5[x,y],y] ~E.[SK3[x],x] ... ?
24# E.[SK5[x,y],y] ~E.[SK5[x,y],y] ~E.[SK3[x],x]
25S>E.[SK3[x],x] big_f[y,SK3[x]] ~E.[y,SK4[x]]
26S E.[SK3[x],x] ~big_f[y,SK3[x]] E.[y,SK4[x]]
27# E.[SK3[x],x] ~E.[SK3[x],x]

---------------
Phases 1 and 2 clauses used in proof:
28: (12a,1b)  big_f[SK1,x] ~E.[x,SK2]
29: (28b,12a) big_f[SK1,SK2]

30S>(25b,9a)  E.[SK3[x],x] ~E.[y,SK4[x]] E.[SK3[x],SK2]
31S>(30b,12a) E.[SK3[x],x] E.[SK3[x],SK2]
32S>(31ab)    E.[SK3[SK2],SK2]

33S>(22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
34S>(33ac)    ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
35S>(34a,32a) E.[SK5[SK2,SK1],SK1]

36S>(22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
37S>(36ac)    ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
38S>(37b*23b) ~E.[SK3[x],x] ~big_f[SK5[x,SK1],y] ... ?

39S>37 | 38 {SK2/x} ~E.[SK3[SK2],SK2] ~big_f[SK5[SK2,SK1],y] ... ?
40S>(39a,32a) ~big_f[SK5[SK2,SK1],x] ... ?
41S>[40a,35a] ~big_f[SK1,x] ... ?
42S>(41a,29a) [] ... ?

END OF WEAKENED PROOF

-----------------------------------------------------------------
RECONSIDER PROOF

Reinstated base clause: 23S>~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~E.[SK3[x],x] ... ?

-----------------------------------------------------------------

List of useful clauses from weakened proof:

28S (12a,1b)  big_f[SK1,x] ~E.[x,SK2]
29S (28b,12a) big_f[SK1,SK2]
30# (25b,9a)  E.[SK3[x],x] ~E.[y,SK4[x]] E.[SK3[x],SK2]
31S (30b,12a) E.[SK3[x],x] E.[SK3[x],SK2]
32S (31ab)    E.[SK3[SK2],SK2]
33# (22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
34S (33ac)    ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
35S (34a,32a) E.[SK5[SK2,SK1],SK1]
36# (22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
36# (22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
37S (36ac)    ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
37# (36ac)    ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
38: (37b*23b) ~E.[SK3[x],x] ~big_f[SK5[x,SK1],SK3[x]]
39# 37 | 23 {SK2/x} ~E.[SK3[SK2],SK2] ~big_f[SK5[SK2,SK1],SK3[SK2]]
40: (39a,32a) ~big_f[SK5[SK2,SK1],SK3[SK2]]

End Final ulist

-----------------------------------------------------------------
ANALYSIS OF WEAKENED PROOF

Clause 23 was weakened:  23S>~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~E.[SK3[x],x]
Length of weakened proof is 15 inferences.
Nodes searched for weakened proof is 266.
15 clauses in weakened proof are usable when proving given theorem.
Of these clauses, 9 will be added to the base clauses.
4 of given 12 axioms used in weakened proof will be placed in the sos.
3 of given 15 clauses in sos were used in weakened proof.

Proof of weakened version may be useful.

-----------------------------------------------------------------
Valid inferences derived from given clauses:

PHASE 0: 0 s, PHASE 1: 1 s, PHASE 2: 0 s ACCUM: 0  Total Time: 1 s
NOD: 266        RES: 891        FAC: 47         T: 12  V: 6  L: 3
CTE: 813        CTH: 171        CTF: 0          CSZ: 16777216
UTE: 51         UTH: 54         UTF: 0          SBA: 5
BAS: 27         RED: 27         LEN: 0+15=15

----------------------------------------------------------------------
MODIFY THEOREM

Nodes searched last time = 266
Time taken = 2    Time to go = 598    o_maxtime = 299

Proof found with 1 weakening. Had weakened clause 23 (used).
Set weakened_clause_count to 0, o_maxtime = timeToGo

Single weakening proof found => This time none.
----------------------------------------------------------------------

THE PROOF

Axioms:
1S big_f[x,y] ~E.[x,SK1] ~E.[y,SK2]
2: ~E.[x,y] ~E.[y,z] E.[x,z]
3: ~big_f[x,y] ~E.[y,z] big_f[x,z]
4 >~big_f[x,y] ~E.[x,z] big_f[z,y]
5: ~E.[x,y] E.[SK5[x,z],SK5[y,z]]
6: ~E.[x,y] E.[SK5[z,x],SK5[z,y]]
7: ~E.[x,y] E.[SK3[x],SK3[y]]
8: ~E.[x,y] E.[SK4[x],SK4[y]]
9S ~big_f[x,y] E.[y,SK2]
10S ~big_f[x,y] E.[x,SK1]
11: ~E.[x,y] E.[y,x]
12S>E.[x,x]

Negated conclusion:
13# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] big_f[z,SK3[x]] ~E.[z,SK4[x]]
14# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] ~big_f[z,SK3[x]] E.[z,SK4[x]]
15S E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] big_f[z,SK3[x]] ~E.[z,SK4[x]]
16S E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] ~big_f[z,SK3[x]] E.[z,SK4[x]]
17S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] big_f[z,SK3[x]] ~E.[z,SK4[x]]
18S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~big_f[z,SK3[x]] E.[z,SK4[x]]
19# E.[SK5[x,y],y] ~E.[SK5[x,y],y] big_f[z,SK3[x]] ~E.[z,SK4[x]]
20# E.[SK5[x,y],y] ~E.[SK5[x,y],y] ~big_f[z,SK3[x]] E.[z,SK4[x]]
21# ~big_f[SK5[x,y],SK3[x]] big_f[SK5[x,y],SK3[x]] ~E.[SK3[x],x]
22S E.[SK5[x,y],y] big_f[SK5[x,y],SK3[x]] ~E.[SK3[x],x]
23S ~big_f[SK5[x,y],SK3[x]] ~E.[SK5[x,y],y] ~E.[SK3[x],x]
24# E.[SK5[x,y],y] ~E.[SK5[x,y],y] ~E.[SK3[x],x]
25S E.[SK3[x],x] big_f[y,SK3[x]] ~E.[y,SK4[x]]
26S E.[SK3[x],x] ~big_f[y,SK3[x]] E.[y,SK4[x]]
27# E.[SK3[x],x] ~E.[SK3[x],x]

---------------
Weakened clauses used in proof:
28S (12a,1b)  big_f[SK1,x] ~E.[x,SK2]
29S (28b,12a) big_f[SK1,SK2]
30# (25b,9a)  E.[SK3[x],x] ~E.[y,SK4[x]] E.[SK3[x],SK2]
31S (30b,12a) E.[SK3[x],x] E.[SK3[x],SK2]
32S (31a,0b)  E.[SK3[SK2],SK2]
33# (22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
34S (33a,0c)  ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
35S (34a,32a) E.[SK5[SK2,SK1],SK1]
36# (22b,10a) E.[SK5[x,y],y] ~E.[SK3[x],x] E.[SK5[x,y],SK1]
37S (36a,0c)  ~E.[SK3[x],x] E.[SK5[x,SK1],SK1]
38: (37b*23b) ~E.[SK3[x],x] ~big_f[SK5[x,SK1],SK3[x]]
39# 38 | 0 {SK2/x} ~E.[SK3[SK2],SK2] ~big_f[SK5[SK2,SK1],SK3[SK2]]
40: (39a,32a) ~big_f[SK5[SK2,SK1],SK3[SK2]]

Phase 0 clauses used in proof:
29S>big_f[SK1,SK2]    (Clause 29 in weakened proof)
31S>E.[SK3[SK2],SK2]    (Clause 32 in weakened proof)
33S>E.[SK5[SK2,SK1],SK1]    (Clause 35 in weakened proof)
35S>~big_f[SK5[SK2,SK1],SK3[SK2]]    (Clause 40 in weakened proof)

Phases 1 and 2 clauses used in proof:
37S>(35a,4c)  ~big_f[x,SK3[SK2]] ~E.[x,SK5[SK2,SK1]]
38S>[37a,31a] ~big_f[x,SK2] ~E.[x,SK5[SK2,SK1]]
39S>[38b,33a] ~big_f[x,SK2] ~E.[x,SK1]
40S>(39a,29a) ~E.[SK1,SK1]
41S>(40a,12a) []

END OF PROOF

PHASE 0: 0 s, PHASE 1: 0 s, PHASE 2: -NA- ACCUM: 1  Total Time: 1 s
NOD: 6          RES: 17         FAC: 0          T: 12  V: 6  L: 3
CTE: 50         CTH: 0          CTF: 0          CSZ: 16777216
UTE: 14         UTH: 12         UTF: 0          SBA: 7
BAS: 27         RED: 36         LEN: 4+5=9
```

## Vampire 7.0

Alexandre Riazanov, Andrei Voronkov
University of Manchester, England
{riazanoa,voronkov}@cs.man.ac.uk

### Names of rules used in Vampire 7.0 proofs, and their meanings

1. "input":
Input axiom, hypothesis or the negation of conjecture
2. "choice axiom":
Additional axiom (Ax)((Ey)F(x,y) -> F(x,f(x))), where f is a Skolem function
3. "monotone replacement":
(Ax)(F(x)->F'(x)), G[F(t)] => G[F'(t)]
4. "forall-elimination":
G[(Ax)F(x)] => G[F(t)]
5. "not-and":
G[~(F1 & ... & Fn)] => G[~F1 \/ ... \/ ~Fn]
6. "not-or":
G[~(F1 \/ ... \/ Fn)] => G[~F1 & ... & ~Fn]
7. "not-implies":
G[~(F1 -> F2)] => G[F1 & ~F2]
8. "not-iff":
G[~(F1 <-> F2)] => G[F1 <~> F2]
9. "not-xor":
G[~(F1 <~> F2)] => G[F1 <-> F2]
10. "not-not":
G[~~F] => G[F]
11. "not-forall":
G[~(Ax)F] => G[(Ex)~F]
12. "not-exists":
G[~(Ex)F] => G[(Ax)~F]
13. "implies-to-or":
G[F1 -> F2] => G[~F1 \/ F2]
14. "equivalence-to-and":
G[F1 <-> F2] => G[(F1 -> F2) & (F2 -> F1)]
15. "xor-to-and":
G[F1 <~> F2] => G[(F1 \/ F2) & (~F1 \/ ~F2)]
16. "rectify":
Renaming of bound variables.
17. "dummy quantifier removal":
G[(Q x1 ... xk ... x_n)A] => G[(Q x1 ... xk-1 xk+1 ... x_n)A] where xk does not occur in A
18. "forall-and":
G[(A x1 ... xn)(F1 & ... & Fm)] => G[(A x1 ... xn)F1 & ... & (A x1 ... xn)Fm)]
19. "exists-or":
G[(E x1 ... xn)(F1 \/ ... \/ Fm)] => G[(E x1 ... xn)F1 \/ ... \/ (E x1 ... xn)Fm)]
20. "quantifier swap":
G[(Q x)(Q y)F] => G[(Q y)(Q x)F]
21. "forall-or":
G[(A x1 x2)(F1 \/ F2)] => G[(A x1)F1 \/ ... \/ (A x2)F2)], where x2 does not occur in F1. Can be applied to many variables and disjunctions of arbitrary length.
22. "exists-and":
G[(E x1 x2)(F1 & F2)] => G[(E x1)F1 & ... & (E x2)F2)], where x2 does not occur in F1. Can be applied to many variables and disjunctions of arbitrary length.
23. "permutation":
Applies symmetry of <->, <~>, \/ or &.
24. "flattening":
Applies associativity of \/ or &.
25. "equality reordering":
Applies symmetry of the equality predicate.
26. "equivalence to implication":
G[F1 <-> F2] => G[F1 -> F2], G[F1 <-> F2] => G[F2 -> F1], provided that the context G[.] is positive.
27. "miniscoping":
G[(E x) F1 \/ F2] => G[(E x) F1 \/ (E x) F2] G[(A x) F1 & F2] => G[(A x) F1 & (A x) F2]
28. "cnf transformation":
G[F1 & .. Fk-1 & Fk & Fk+1 & .. & Fn] => G[F1 & .. Fk-1 & Fk+1 & .. & Fn], where the context G[.] is positive.
29. "remove duplicate literals":
Factorises duplicate literals in a clause.
30. "resolution":
Binary resolution (on literals, not arbitrary formulas)
31. "kernel inference":
Any combination of the following rules on clauses: binary resolution, factoring, paramodulation, equality resolution, equality factoring, permutation of literals in a clause, renaming of free variables in a clause.

### Sample MIX proof for SYN075-1

```=========== Refutation ==========
*********** [3, input] ***********
X0!=a \/ X1!=b \/ big_f(X0,X1)
*********** [3->13, kernel inference] ***********
X0!=a \/ X1!=b \/ big_f(X0,X1)
-----------------------------
X1!=b \/ X2!=a \/ big_f(X2,X1)
*********** [13->22, kernel inference] ***********
X1!=b \/ X2!=a \/ big_f(X2,X1)
-----------------------------
X1!=b \/ X2!=a \/ big_f(X2,X1)
*********** [22->28, kernel inference] ***********
X1!=b \/ X2!=a \/ big_f(X2,X1)
-----------------------------
X1!=a \/ big_f(X1,b)
*********** [28->33, kernel inference] ***********
X1!=a \/ big_f(X1,b)
-----------------------------
big_f(a,b)
*********** [1, input] ***********
~big_f(X0,X1) \/ X0=a
*********** [1->11, kernel inference] ***********
~big_f(X0,X1) \/ X0=a
-----------------------------
~big_f(X1,X2) \/ X1=a
*********** [11->20, kernel inference] ***********
~big_f(X1,X2) \/ X1=a
-----------------------------
~big_f(X1,X2) \/ X1=a
*********** [9, input] ***********
f(X0)!=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
*********** [9->18, kernel inference] ***********
f(X0)!=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
-----------------------------
f(X1)!=X1 \/ h(X1,X2)=X2 \/ big_f(h(X1,X2),f(X1))
*********** [18->26, kernel inference] ***********
f(X1)!=X1 \/ h(X1,X2)=X2 \/ big_f(h(X1,X2),f(X1))
-----------------------------
f(X1)!=X1 \/ h(X1,X2)=X2 \/ big_f(h(X1,X2),f(X1))
*********** [4, input] ***********
~big_f(X1,f(X0)) \/ X1!=g(X0) \/ f(X0)=X0
*********** [4->14, kernel inference] ***********
~big_f(X1,f(X0)) \/ X1!=g(X0) \/ f(X0)=X0
-----------------------------
X1!=g(X2) \/ f(X2)=X2 \/ ~big_f(X1,f(X2))
*********** [6, input] ***********
X1!=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
*********** [14,6->15, kernel inference] ***********
X1!=g(X2) \/ f(X2)=X2 \/ ~big_f(X1,f(X2))
X1!=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
-----------------------------
X1!=g(X2) \/ f(X2)=X2
*********** [15->23, kernel inference] ***********
X1!=g(X2) \/ f(X2)=X2
-----------------------------
X1!=g(X2) \/ f(X2)=X2
*********** [23->29, kernel inference] ***********
X1!=g(X2) \/ f(X2)=X2
-----------------------------
f(X1)=X1
*********** [26,29->31, kernel inference] ***********
f(X1)!=X1 \/ h(X1,X2)=X2 \/ big_f(h(X1,X2),f(X1))
f(X1)=X1
-----------------------------
big_f(h(X1,X2),X1) \/ h(X1,X2)=X2
*********** [20,31->35, kernel inference] ***********
~big_f(X1,X2) \/ X1=a
big_f(h(X1,X2),X1) \/ h(X1,X2)=X2
-----------------------------
h(X1,X2)=a \/ h(X1,X2)=X2
*********** [35->36, kernel inference] ***********
h(X1,X2)=a \/ h(X1,X2)=X2
-----------------------------
a!=X1 \/ h(X2,X1)=X1
*********** [36->40, kernel inference] ***********
a!=X1 \/ h(X2,X1)=X1
-----------------------------
h(X1,a)=a
*********** [10, input] ***********
f(X0)!=X0 \/ h(X0,X2)!=X2 \/ ~big_f(h(X0,X2),f(X0))
*********** [10->19, kernel inference] ***********
f(X0)!=X0 \/ h(X0,X2)!=X2 \/ ~big_f(h(X0,X2),f(X0))
-----------------------------
~big_f(h(X1,X2),f(X1)) \/ h(X1,X2)!=X2 \/ f(X1)!=X1
*********** [19->27, kernel inference] ***********
~big_f(h(X1,X2),f(X1)) \/ h(X1,X2)!=X2 \/ f(X1)!=X1
-----------------------------
~big_f(h(X1,X2),f(X1)) \/ h(X1,X2)!=X2 \/ f(X1)!=X1
*********** [27,29->32, kernel inference] ***********
~big_f(h(X1,X2),f(X1)) \/ h(X1,X2)!=X2 \/ f(X1)!=X1
f(X1)=X1
-----------------------------
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),X1)
*********** [40,32,40->41, kernel inference] ***********
h(X1,a)=a
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),X1)
h(X1,a)=a
-----------------------------
~big_f(a,X1)
*********** [33,41->42, kernel inference] ***********
big_f(a,b)
~big_f(a,X1)
-----------------------------
#
======= End of refutation =======
```

### Sample FOF proof for SYN075+1

```=========== Refutation ==========
*********** [1, input] ***********
(? X1 X0)(! X3 X2)(big_f(X3,X2) <=> X3=X1 & X2=X0)
*********** [1->3, rectify] ***********
(? X1 X0)(! X3 X2)(big_f(X3,X2) <=> X3=X1 & X2=X0)
-----------------------------
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X2=X0 & X3=X1)
*********** [3->84, equivalence-to-and] ***********
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X2=X0 & X3=X1)
-----------------------------
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & (X2=X0 & X3=X1 => big_f(X2,X3)))
*********** [84->85, implies-to-or] ***********
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & (X2=X0 & X3=X1 => big_f(X2,X3)))
-----------------------------
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & (~(X2=X0 & X3=X1) \/ big_f(X2,X3)))
*********** [85->86, not-and] ***********
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & (~(X2=X0 & X3=X1) \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & ((~X2=X0 \/ ~X3=X1) \/ big_f(X2,X3)))
*********** [86->5, implies-to-or] ***********
(? X0 X1)(! X2 X3)((big_f(X2,X3) => X2=X0 & X3=X1) & ((~X2=X0 \/ ~X3=X1) \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & ((~X2=X0 \/ ~X3=X1) \/ big_f(X2,X3)))
*********** [5->6, flattening] ***********
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & ((~X2=X0 \/ ~X3=X1) \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (~X2=X0 \/ ~X3=X1 \/ big_f(X2,X3)))
*********** [6->89, forall-and] ***********
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (~X2=X0 \/ ~X3=X1 \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X2 X3)(~X2=X0 \/ ~X3=X1 \/ big_f(X2,X3)))
*********** [89->7, forall-or] ***********
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X2 X3)(~X2=X0 \/ ~X3=X1 \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X3)((! X2)(~X2=X0 \/ big_f(X2,X3)) \/ ~X3=X1))
*********** [7->8, rectify] ***********
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X3)((! X2)(~X2=X0 \/ big_f(X2,X3)) \/ ~X3=X1))
-----------------------------
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X4)((! X5)(~X5=X0 \/ big_f(X5,X4)) \/ ~X4=X1))
*********** [91, choice axiom] ***********
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X4)((! X5)(~X5=X0 \/ big_f(X5,X4)) \/ ~X4=X1)) => (! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & (! X4)((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
*********** [91,8->92, monotone replacement] ***********
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X4)((! X5)(~X5=X0 \/ big_f(X5,X4)) \/ ~X4=X1)) => (! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & (! X4)((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
(? X0 X1)((! X2 X3)(~big_f(X2,X3) \/ (X2=X0 & X3=X1)) & (! X4)((! X5)(~X5=X0 \/ big_f(X5,X4)) \/ ~X4=X1))
-----------------------------
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & (! X4)((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
*********** [92->93, forall-elimination] ***********
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & (! X4)((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
*********** [93->94, forall-elimination] ***********
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((! X5)(~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
*********** [94->9, forall-elimination] ***********
(! X2 X3)(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
*********** [9->17, cnf transformation] ***********
(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
X4!=sk1 \/ big_f(X5,X4) \/ X5!=sk0
*********** [17->26, kernel inference] ***********
X4!=sk1 \/ big_f(X5,X4) \/ X5!=sk0
-----------------------------
X1!=sk0 \/ X2!=sk1 \/ big_f(X1,X2)
*********** [26->33, kernel inference] ***********
X1!=sk0 \/ X2!=sk1 \/ big_f(X1,X2)
-----------------------------
X1!=sk0 \/ X2!=sk1 \/ big_f(X1,X2)
*********** [33->37, kernel inference] ***********
X1!=sk0 \/ X2!=sk1 \/ big_f(X1,X2)
-----------------------------
X1!=sk1 \/ big_f(sk0,X1)
*********** [37->38, kernel inference] ***********
X1!=sk1 \/ big_f(sk0,X1)
-----------------------------
big_f(sk0,sk1)
*********** [9->16, cnf transformation] ***********
(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
X3=sk1 \/ ~big_f(X2,X3)
*********** [16->27, kernel inference] ***********
X3=sk1 \/ ~big_f(X2,X3)
-----------------------------
~big_f(X1,X2) \/ X2=sk1
*********** [27->34, kernel inference] ***********
~big_f(X1,X2) \/ X2=sk1
-----------------------------
~big_f(X1,X2) \/ X2=sk1
*********** [2, input] ***********
~(? X0)(! X2)((? X1)(! X3)(big_f(X3,X2) <=> X3=X1) <=> X2=X0)
*********** [2->4, rectify] ***********
~(? X0)(! X2)((? X1)(! X3)(big_f(X3,X2) <=> X3=X1) <=> X2=X0)
-----------------------------
~(? X0)(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
*********** [4->96, not-exists] ***********
~(? X0)(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
-----------------------------
(! X0)~(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
*********** [96->97, not-forall] ***********
(! X0)~(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
-----------------------------
(! X0)(? X1)~((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
*********** [97->10, not-iff] ***********
(! X0)(? X1)~((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
-----------------------------
(! X0)(? X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <~> X1=X0)
*********** [10->99, xor-to-and] ***********
(! X0)(? X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <~> X1=X0)
-----------------------------
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & (~(? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
*********** [99->100, not-exists] ***********
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & (~(? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)~(! X3)(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
*********** [100->101, not-forall] ***********
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)~(! X3)(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)~(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
*********** [101->102, not-iff] ***********
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)~(big_f(X3,X1) <=> X3=X2) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)(big_f(X3,X1) <~> X3=X2) \/ ~X1=X0))
*********** [102->103, xor-to-and] ***********
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)(big_f(X3,X1) <~> X3=X2) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
*********** [103->104, equivalence-to-and] ***********
(! X0)(? X1)(((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)((big_f(X3,X1) => X3=X2) & (X3=X2 => big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
*********** [104->105, implies-to-or] ***********
(! X0)(? X1)(((? X2)(! X3)((big_f(X3,X1) => X3=X2) & (X3=X2 => big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)((big_f(X3,X1) => X3=X2) & (~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
*********** [105->11, implies-to-or] ***********
(! X0)(? X1)(((? X2)(! X3)((big_f(X3,X1) => X3=X2) & (~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)(! X3)((~big_f(X3,X1) \/ X3=X2) & (~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
*********** [11->12, forall-and] ***********
(! X0)(? X1)(((? X2)(! X3)((~big_f(X3,X1) \/ X3=X2) & (~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X3)(~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
*********** [12->13, rectify] ***********
(! X0)(? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X3)(~X3=X2 \/ big_f(X3,X1))) \/ X1=X0) & ((! X2)(? X3)((big_f(X3,X1) \/ X3=X2) & (~big_f(X3,X1) \/ ~X3=X2)) \/ ~X1=X0))
-----------------------------
(! X0)(? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,X1))) \/ X1=X0) & ((! X5)(? X6)((big_f(X6,X1) \/ X6=X5) & (~big_f(X6,X1) \/ ~X6=X5)) \/ ~X1=X0))
*********** [112, choice axiom] ***********
(! X0)((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) => (! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0))))
*********** [110, choice axiom] ***********
(! X0 X5)((? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) => (big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5))
*********** [108, choice axiom] ***********
(! X0)((? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,X1))) \/ X1=X0) & ((! X5)(? X6)((big_f(X6,X1) \/ X6=X5) & (~big_f(X6,X1) \/ ~X6=X5)) \/ ~X1=X0)) => ((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)(? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) \/ ~sk2(X0)=X0))
*********** [108,13->109, monotone replacement] ***********
(! X0)((? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,X1))) \/ X1=X0) & ((! X5)(? X6)((big_f(X6,X1) \/ X6=X5) & (~big_f(X6,X1) \/ ~X6=X5)) \/ ~X1=X0)) => ((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)(? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) \/ ~sk2(X0)=X0))
(! X0)(? X1)(((? X2)((! X3)(~big_f(X3,X1) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,X1))) \/ X1=X0) & ((! X5)(? X6)((big_f(X6,X1) \/ X6=X5) & (~big_f(X6,X1) \/ ~X6=X5)) \/ ~X1=X0))
-----------------------------
(! X0)(((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)(? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) \/ ~sk2(X0)=X0))
*********** [110,109->111, monotone replacement] ***********
(! X0 X5)((? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) => (big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5))
(! X0)(((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)(? X6)((big_f(X6,sk2(X0)) \/ X6=X5) & (~big_f(X6,sk2(X0)) \/ ~X6=X5)) \/ ~sk2(X0)=X0))
-----------------------------
(! X0)(((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0))
*********** [112,111->113, monotone replacement] ***********
(! X0)((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) => (! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0))))
(! X0)(((? X2)((! X3)(~big_f(X3,sk2(X0)) \/ X3=X2) & (! X4)(~X4=X2 \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0))
-----------------------------
(! X0)((((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0))
*********** [113->114, forall-elimination] ***********
(! X0)((((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0))
-----------------------------
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
*********** [114->115, forall-elimination] ***********
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & ((! X5)((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
*********** [115->116, forall-elimination] ***********
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (! X4)(~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
*********** [116->14, forall-elimination] ***********
(((! X3)(~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
(((~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
*********** [14->19, cnf transformation] ***********
(((~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
sk2(X0)=X0 \/ big_f(X4,sk2(X0)) \/ X4!=sk3(X0)
*********** [19->24, kernel inference] ***********
sk2(X0)=X0 \/ big_f(X4,sk2(X0)) \/ X4!=sk3(X0)
-----------------------------
X1!=sk3(X2) \/ sk2(X2)=X2 \/ big_f(X1,sk2(X2))
*********** [24->31, kernel inference] ***********
X1!=sk3(X2) \/ sk2(X2)=X2 \/ big_f(X1,sk2(X2))
-----------------------------
X1!=sk3(X2) \/ sk2(X2)=X2 \/ big_f(X1,sk2(X2))
*********** [31->36, kernel inference] ***********
X1!=sk3(X2) \/ sk2(X2)=X2 \/ big_f(X1,sk2(X2))
-----------------------------
big_f(sk3(X1),sk2(X1)) \/ sk2(X1)=X1
*********** [34,36->40, kernel inference] ***********
~big_f(X1,X2) \/ X2=sk1
big_f(sk3(X1),sk2(X1)) \/ sk2(X1)=X1
-----------------------------
sk2(X1)=sk1 \/ sk2(X1)=X1
*********** [40->43, kernel inference] ***********
sk2(X1)=sk1 \/ sk2(X1)=X1
-----------------------------
sk1!=X1 \/ sk2(X1)=X1
*********** [43->49, kernel inference] ***********
sk1!=X1 \/ sk2(X1)=X1
-----------------------------
sk2(sk1)=sk1
*********** [9->15, cnf transformation] ***********
(~big_f(X2,X3) \/ (X2=sk0 & X3=sk1)) & ((~X5=sk0 \/ big_f(X5,X4)) \/ ~X4=sk1)
-----------------------------
X2=sk0 \/ ~big_f(X2,X3)
*********** [15->28, kernel inference] ***********
X2=sk0 \/ ~big_f(X2,X3)
-----------------------------
~big_f(X1,X2) \/ X1=sk0
*********** [28->35, kernel inference] ***********
~big_f(X1,X2) \/ X1=sk0
-----------------------------
~big_f(X1,X2) \/ X1=sk0
*********** [14->20, cnf transformation] ***********
(((~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
sk2(X0)!=X0 \/ sk4(X0,X5)=X5 \/ big_f(sk4(X0,X5),sk2(X0))
*********** [20->23, kernel inference] ***********
sk2(X0)!=X0 \/ sk4(X0,X5)=X5 \/ big_f(sk4(X0,X5),sk2(X0))
-----------------------------
sk2(X1)!=X1 \/ sk4(X1,X2)=X2 \/ big_f(sk4(X1,X2),sk2(X1))
*********** [23->30, kernel inference] ***********
sk2(X1)!=X1 \/ sk4(X1,X2)=X2 \/ big_f(sk4(X1,X2),sk2(X1))
-----------------------------
sk2(X1)!=X1 \/ sk4(X1,X2)=X2 \/ big_f(sk4(X1,X2),sk2(X1))
*********** [49,30,49->54, kernel inference] ***********
sk2(sk1)=sk1
sk2(X1)!=X1 \/ sk4(X1,X2)=X2 \/ big_f(sk4(X1,X2),sk2(X1))
sk2(sk1)=sk1
-----------------------------
big_f(sk4(sk1,X1),sk1) \/ sk4(sk1,X1)=X1
*********** [35,54->56, kernel inference] ***********
~big_f(X1,X2) \/ X1=sk0
big_f(sk4(sk1,X1),sk1) \/ sk4(sk1,X1)=X1
-----------------------------
sk4(sk1,X1)=sk0 \/ sk4(sk1,X1)=X1
*********** [56->68, kernel inference] ***********
sk4(sk1,X1)=sk0 \/ sk4(sk1,X1)=X1
-----------------------------
sk0!=X1 \/ sk4(sk1,X1)=X1
*********** [68->75, kernel inference] ***********
sk0!=X1 \/ sk4(sk1,X1)=X1
-----------------------------
sk4(sk1,sk0)=sk0
*********** [14->21, cnf transformation] ***********
(((~big_f(X3,sk2(X0)) \/ X3=sk3(X0)) & (~X4=sk3(X0) \/ big_f(X4,sk2(X0)))) \/ sk2(X0)=X0) & (((big_f(sk4(X0,X5),sk2(X0)) \/ sk4(X0,X5)=X5) & (~big_f(sk4(X0,X5),sk2(X0)) \/ ~sk4(X0,X5)=X5)) \/ ~sk2(X0)=X0)
-----------------------------
sk2(X0)!=X0 \/ sk4(X0,X5)!=X5 \/ ~big_f(sk4(X0,X5),sk2(X0))
*********** [21->22, kernel inference] ***********
sk2(X0)!=X0 \/ sk4(X0,X5)!=X5 \/ ~big_f(sk4(X0,X5),sk2(X0))
-----------------------------
~big_f(sk4(X1,X2),sk2(X1)) \/ sk4(X1,X2)!=X2 \/ sk2(X1)!=X1
*********** [22->29, kernel inference] ***********
~big_f(sk4(X1,X2),sk2(X1)) \/ sk4(X1,X2)!=X2 \/ sk2(X1)!=X1
-----------------------------
~big_f(sk4(X1,X2),sk2(X1)) \/ sk4(X1,X2)!=X2 \/ sk2(X1)!=X1
*********** [38,49,75,49,29,75->83, kernel inference] ***********
big_f(sk0,sk1)
sk2(sk1)=sk1
sk4(sk1,sk0)=sk0
sk2(sk1)=sk1
~big_f(sk4(X1,X2),sk2(X1)) \/ sk4(X1,X2)!=X2 \/ sk2(X1)!=X1
sk4(sk1,sk0)=sk0
-----------------------------
#
======= End of refutation =======
```

## Vampire 8.0

Andrei Voronkov
University of Manchester, England
voronkov@cs.man.ac.uk

### Sample MIX proof for SYN075-1

```=========== Refutation ==========
*********** [3, input] ***********
X0!=a \/ X1!=b \/ big_f(X0,X1)
*********** [3->11, normalize] ***********
X0!=a \/ X1!=b \/ big_f(X0,X1)
-----------------------------
X1!=b \/ X0!=a \/ big_f(X0,X1)
*********** [11->28, equality resolution] ***********
X1!=b \/ X0!=a \/ big_f(X0,X1)
-----------------------------
X1!=a \/ big_f(X1,b)
*********** [28->35, equality resolution] ***********
X1!=a \/ big_f(X1,b)
-----------------------------
big_f(a,b)
*********** [1, input] ***********
~big_f(X0,X1) \/ X0=a
*********** [4, input] ***********
~big_f(X1,f(X0)) \/ X1!=g(X0) \/ f(X0)=X0
*********** [4->12, normalize] ***********
~big_f(X1,f(X0)) \/ X1!=g(X0) \/ f(X0)=X0
-----------------------------
X1!=g(X0) \/ ~big_f(X1,f(X0)) \/ X0=f(X0)
*********** [12->21, literal permutation] ***********
X1!=g(X0) \/ ~big_f(X1,f(X0)) \/ X0=f(X0)
-----------------------------
X1!=g(X2) \/ ~big_f(X1,f(X2)) \/ f(X2)=X2
*********** [6, input] ***********
X1!=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
*********** [6->14, normalize] ***********
X1!=g(X0) \/ big_f(X1,f(X0)) \/ f(X0)=X0
-----------------------------
X1!=g(X0) \/ X0=f(X0) \/ big_f(X1,f(X0))
*********** [21,14->22, forward subsumption resolution] ***********
X1!=g(X2) \/ ~big_f(X1,f(X2)) \/ f(X2)=X2
X1!=g(X0) \/ X0=f(X0) \/ big_f(X1,f(X0))
-----------------------------
X1!=g(X2) \/ f(X2)=X2
*********** [22->29, equality resolution] ***********
X1!=g(X2) \/ f(X2)=X2
-----------------------------
f(X1)=X1
*********** [9, input] ***********
f(X0)!=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
*********** [9->17, normalize] ***********
f(X0)!=X0 \/ big_f(h(X0,X2),f(X0)) \/ h(X0,X2)=X2
-----------------------------
X0!=f(X0) \/ X2=h(X0,X2) \/ big_f(h(X0,X2),f(X0))
*********** [17->25, literal permutation] ***********
X0!=f(X0) \/ X2=h(X0,X2) \/ big_f(h(X0,X2),f(X0))
-----------------------------
f(X1)!=X1 \/ big_f(h(X1,X2),f(X1)) \/ h(X1,X2)=X2
*********** [29,25->31, backward demodulation] ***********
f(X1)=X1
f(X1)!=X1 \/ big_f(h(X1,X2),f(X1)) \/ h(X1,X2)=X2
-----------------------------
big_f(h(X1,X2),X1) \/ h(X1,X2)=X2
*********** [1,31->33, resolution] ***********
~big_f(X0,X1) \/ X0=a
big_f(h(X1,X2),X1) \/ h(X1,X2)=X2
-----------------------------
h(X1,X2)=a \/ h(X1,X2)=X2
*********** [33->36, equality factoring] ***********
h(X1,X2)=a \/ h(X1,X2)=X2
-----------------------------
a!=X1 \/ h(X2,X1)=X1
*********** [36->40, equality resolution] ***********
a!=X1 \/ h(X2,X1)=X1
-----------------------------
h(X1,a)=a
*********** [10, input] ***********
f(X0)!=X0 \/ h(X0,X2)!=X2 \/ ~big_f(h(X0,X2),f(X0))
*********** [10->18, normalize] ***********
f(X0)!=X0 \/ h(X0,X2)!=X2 \/ ~big_f(h(X0,X2),f(X0))
-----------------------------
X0!=f(X0) \/ X2!=h(X0,X2) \/ ~big_f(h(X0,X2),f(X0))
*********** [18->24, literal permutation] ***********
X0!=f(X0) \/ X2!=h(X0,X2) \/ ~big_f(h(X0,X2),f(X0))
-----------------------------
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),f(X1)) \/ f(X1)!=X1
*********** [29,24->32, backward demodulation] ***********
f(X1)=X1
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),f(X1)) \/ f(X1)!=X1
-----------------------------
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),X1)
*********** [40,32,40->41, backward superposition, forward demodulation] ***********
h(X1,a)=a
h(X1,X2)!=X2 \/ ~big_f(h(X1,X2),X1)
h(X1,a)=a
-----------------------------
~big_f(a,X1)
*********** [35,41->42, resolution] ***********
big_f(a,b)
~big_f(a,X1)
-----------------------------
#
======= End of refutation =======
```

### Sample FOF proof for SYN075+1

```=========== Refutation ==========
*********** [1, input] ***********
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X2=X0 & X3=X1)
*********** [1->77, normalize] ***********
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X2=X0 & X3=X1)
-----------------------------
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X3=X1 & X2=X0)
*********** [77->84, NNF transformation] ***********
(? X0 X1)(! X2 X3)(big_f(X2,X3) <=> X3=X1 & X2=X0)
-----------------------------
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X3=X1 & X2=X0)) & ((X3!=X1 \/ X2!=X0) \/ big_f(X2,X3)))
*********** [84->85, flattening] ***********
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X3=X1 & X2=X0)) & ((X3!=X1 \/ X2!=X0) \/ big_f(X2,X3)))
-----------------------------
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X3=X1 & X2=X0)) & (X3!=X1 \/ X2!=X0 \/ big_f(X2,X3)))
*********** [85->86, skolemization] ***********
(? X0 X1)(! X2 X3)((~big_f(X2,X3) \/ (X3=X1 & X2=X0)) & (X3!=X1 \/ X2!=X0 \/ big_f(X2,X3)))
-----------------------------
(~big_f(X2,X3) \/ (X3=\$s12 & X2=\$s11)) & (X3!=\$s12 \/ X2!=\$s11 \/ big_f(X2,X3))
*********** [86->93, cnf transformation] ***********
(~big_f(X2,X3) \/ (X3=\$s12 & X2=\$s11)) & (X3!=\$s12 \/ X2!=\$s11 \/ big_f(X2,X3))
-----------------------------
big_f(X2,X3) \/ X2!=\$s11 \/ X3!=\$s12
*********** [93->116, equality resolution, passive clause reanimation] ***********
big_f(X2,X3) \/ X2!=\$s11 \/ X3!=\$s12
-----------------------------
X1!=\$s11 \/ big_f(X1,\$s12)
*********** [116->122, equality resolution, passive clause reanimation] ***********
X1!=\$s11 \/ big_f(X1,\$s12)
-----------------------------
big_f(\$s11,\$s12)
*********** [2, input] ***********
~(? X1)(! X3)((? X0)(! X2)(big_f(X2,X3) <=> X2=X0) <=> X3=X1)
*********** [2->78, rectify] ***********
~(? X1)(! X3)((? X0)(! X2)(big_f(X2,X3) <=> X2=X0) <=> X3=X1)
-----------------------------
~(? X0)(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
*********** [78->79, normalize] ***********
~(? X0)(! X1)((? X2)(! X3)(big_f(X3,X1) <=> X3=X2) <=> X1=X0)
-----------------------------
~(? X0)(! X1)(X1=X0 <=> (? X2)(! X3)(X3=X2 <=> big_f(X3,X1)))
*********** [79->80, ENNF transformation] ***********
~(? X0)(! X1)(X1=X0 <=> (? X2)(! X3)(X3=X2 <=> big_f(X3,X1)))
-----------------------------
(! X0)(? X1)(X1=X0 <~> (? X2)(! X3)(X3=X2 <=> big_f(X3,X1)))
*********** [80->81, NNF transformation] ***********
(! X0)(? X1)(X1=X0 <~> (? X2)(! X3)(X3=X2 <=> big_f(X3,X1)))
-----------------------------
(! X0)(? X1)((X1=X0 \/ (? X2)(! X3)((X3!=X2 \/ big_f(X3,X1)) & (~big_f(X3,X1) \/ X3=X2))) & (X1!=X0 \/ (! X2)(? X3)((X3=X2 \/ big_f(X3,X1)) & (X3!=X2 \/ ~big_f(X3,X1)))))
*********** [81->82, rectify] ***********
(! X0)(? X1)((X1=X0 \/ (? X2)(! X3)((X3!=X2 \/ big_f(X3,X1)) & (~big_f(X3,X1) \/ X3=X2))) & (X1!=X0 \/ (! X2)(? X3)((X3=X2 \/ big_f(X3,X1)) & (X3!=X2 \/ ~big_f(X3,X1)))))
-----------------------------
(! X0)(? X1)((X1=X0 \/ (? X2)(! X3)((X3!=X2 \/ big_f(X3,X1)) & (~big_f(X3,X1) \/ X3=X2))) & (X1!=X0 \/ (! X4)(? X5)((X5=X4 \/ big_f(X5,X1)) & (X5!=X4 \/ ~big_f(X5,X1)))))
*********** [82->83, skolemization] ***********
(! X0)(? X1)((X1=X0 \/ (? X2)(! X3)((X3!=X2 \/ big_f(X3,X1)) & (~big_f(X3,X1) \/ X3=X2))) & (X1!=X0 \/ (! X4)(? X5)((X5=X4 \/ big_f(X5,X1)) & (X5!=X4 \/ ~big_f(X5,X1)))))
-----------------------------
(\$s8(X0)=X0 \/ ((X3!=\$s9(X1) \/ big_f(X3,\$s8(X0))) & (~big_f(X3,\$s8(X0)) \/ X3=\$s9(X1)))) & (\$s8(X0)!=X0 \/ ((\$s10(X1,X4)=X4 \/ big_f(\$s10(X1,X4),\$s8(X0))) & (\$s10(X1,X4)!=X4 \/ ~big_f(\$s10(X1,X4),\$s8(X0)))))
*********** [83->87, cnf transformation] ***********
(\$s8(X0)=X0 \/ ((X3!=\$s9(X1) \/ big_f(X3,\$s8(X0))) & (~big_f(X3,\$s8(X0)) \/ X3=\$s9(X1)))) & (\$s8(X0)!=X0 \/ ((\$s10(X1,X4)=X4 \/ big_f(\$s10(X1,X4),\$s8(X0))) & (\$s10(X1,X4)!=X4 \/ ~big_f(\$s10(X1,X4),\$s8(X0)))))
-----------------------------
big_f(X3,\$s8(X0)) \/ X3!=\$s9(X1) \/ \$s8(X0)=X0
*********** [87->118, equality resolution, passive clause reanimation] ***********
big_f(X3,\$s8(X0)) \/ X3!=\$s9(X1) \/ \$s8(X0)=X0
-----------------------------
big_f(\$s9(X1),\$s8(X2)) \/ \$s8(X2)=X2
*********** [86->91, cnf transformation] ***********
(~big_f(X2,X3) \/ (X3=\$s12 & X2=\$s11)) & (X3!=\$s12 \/ X2!=\$s11 \/ big_f(X2,X3))
-----------------------------
X3=\$s12 \/ ~big_f(X2,X3)
*********** [118,91->123, resolution, passive clause reanimation] ***********
big_f(\$s9(X1),\$s8(X2)) \/ \$s8(X2)=X2
X3=\$s12 \/ ~big_f(X2,X3)
-----------------------------
\$s8(X1)=\$s12 \/ \$s8(X1)=X1
*********** [123->131, equality factoring, passive clause reanimation] ***********
\$s8(X1)=\$s12 \/ \$s8(X1)=X1
-----------------------------
\$s12!=X1 \/ \$s8(X1)=X1
*********** [131->146, equality resolution, passive clause reanimation] ***********
\$s12!=X1 \/ \$s8(X1)=X1
-----------------------------
\$s8(\$s12)=\$s12
*********** [83->89, cnf transformation] ***********
(\$s8(X0)=X0 \/ ((X3!=\$s9(X1) \/ big_f(X3,\$s8(X0))) & (~big_f(X3,\$s8(X0)) \/ X3=\$s9(X1)))) & (\$s8(X0)!=X0 \/ ((\$s10(X1,X4)=X4 \/ big_f(\$s10(X1,X4),\$s8(X0))) & (\$s10(X1,X4)!=X4 \/ ~big_f(\$s10(X1,X4),\$s8(X0)))))
-----------------------------
big_f(\$s10(X1,X4),\$s8(X0)) \/ \$s10(X1,X4)=X4 \/ \$s8(X0)!=X0
*********** [146,89,146->202, backward superposition, forward demodulation, passive clause reanimation] ***********
\$s8(\$s12)=\$s12
big_f(\$s10(X1,X4),\$s8(X0)) \/ \$s10(X1,X4)=X4 \/ \$s8(X0)!=X0
\$s8(\$s12)=\$s12
-----------------------------
big_f(\$s10(X1,X2),\$s12) \/ \$s10(X1,X2)=X2
*********** [86->92, cnf transformation] ***********
(~big_f(X2,X3) \/ (X3=\$s12 & X2=\$s11)) & (X3!=\$s12 \/ X2!=\$s11 \/ big_f(X2,X3))
-----------------------------
X2=\$s11 \/ ~big_f(X2,X3)
*********** [202,92->213, resolution, passive clause reanimation] ***********
big_f(\$s10(X1,X2),\$s12) \/ \$s10(X1,X2)=X2
X2=\$s11 \/ ~big_f(X2,X3)
-----------------------------
\$s10(X1,X2)=\$s11 \/ \$s10(X1,X2)=X2
*********** [213->296, equality factoring, passive clause reanimation] ***********
\$s10(X1,X2)=\$s11 \/ \$s10(X1,X2)=X2
-----------------------------
\$s11!=X1 \/ \$s10(X2,X1)=X1
*********** [296->320, equality resolution, passive clause reanimation] ***********
\$s11!=X1 \/ \$s10(X2,X1)=X1
-----------------------------
\$s10(X1,\$s11)=\$s11
*********** [83->90, cnf transformation] ***********
(\$s8(X0)=X0 \/ ((X3!=\$s9(X1) \/ big_f(X3,\$s8(X0))) & (~big_f(X3,\$s8(X0)) \/ X3=\$s9(X1)))) & (\$s8(X0)!=X0 \/ ((\$s10(X1,X4)=X4 \/ big_f(\$s10(X1,X4),\$s8(X0))) & (\$s10(X1,X4)!=X4 \/ ~big_f(\$s10(X1,X4),\$s8(X0)))))
-----------------------------
~big_f(\$s10(X1,X4),\$s8(X0)) \/ \$s10(X1,X4)!=X4 \/ \$s8(X0)!=X0
*********** [146,90,146->192, backward superposition, forward demodulation, passive clause reanimation] ***********
\$s8(\$s12)=\$s12
~big_f(\$s10(X1,X4),\$s8(X0)) \/ \$s10(X1,X4)!=X4 \/ \$s8(X0)!=X0
\$s8(\$s12)=\$s12
-----------------------------
\$s10(X1,X2)!=X2 \/ ~big_f(\$s10(X1,X2),\$s12)
*********** [122,320,192,320->328, backward superposition, forward demodulation, forward subsumption resolution] ***********
big_f(\$s11,\$s12)
\$s10(X1,\$s11)=\$s11
\$s10(X1,X2)!=X2 \/ ~big_f(\$s10(X1,X2),\$s12)
\$s10(X1,\$s11)=\$s11
-----------------------------
#
======= End of refutation =======
```