Entrants' Sample Solutions

iProver 2.6

Konstantin Korovin
University of Manchester, United Kingdom

Sample solution for SEU140+2

```% SZS status Theorem

% SZS output start CNFRefutation

fof(f8,axiom,(
! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (in(X2,X0) => in(X2,X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SEU/SEU140+2.p',unknown)).

fof(f77,plain,(
! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (~in(X2,X0) | in(X2,X1)))),
inference(ennf_transformation,[],[f8])).

fof(f113,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X2] : (~in(X2,X0) | in(X2,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))),
inference(nnf_transformation,[],[f77])).

fof(f115,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & ((in(sK2(X1,X0),X0) & ~in(sK2(X1,X0),X1)) | subset(X0,X1)))),
inference(skolemisation,[status(esa)],[f114])).
fof(f114,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))),
inference(rectify,[],[f113])).

fof(f149,plain,(
( ! [X0,X3,X1] : (in(X3,X1) | ~in(X3,X0) | ~subset(X0,X1)) )),
inference(cnf_transformation,[],[f115])).

fof(f43,axiom,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X2] : ~(in(X2,X0) & in(X2,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SEU/SEU140+2.p',unknown)).

fof(f70,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(rectify,[],[f43])).

fof(f71,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(flattening,[],[f70])).

fof(f131,plain,(
! [X0,X1] : ((disjoint(X0,X1) | (in(sK8(X1,X0),X0) & in(sK8(X1,X0),X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(skolemisation,[status(esa)],[f92])).
fof(f92,plain,(
! [X0,X1] : ((disjoint(X0,X1) | ? [X3] : (in(X3,X0) & in(X3,X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(ennf_transformation,[],[f71])).

fof(f198,plain,(
( ! [X2,X0,X1] : (~disjoint(X0,X1) | ~in(X2,X1) | ~in(X2,X0)) )),
inference(cnf_transformation,[],[f131])).

fof(f196,plain,(
( ! [X0,X1] : (in(sK8(X1,X0),X0) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f131])).

fof(f197,plain,(
( ! [X0,X1] : (in(sK8(X1,X0),X1) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f131])).

fof(f51,conjecture,(
! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SEU/SEU140+2.p',unknown)).

fof(f52,negated_conjecture,(
~! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
inference(negated_conjecture,[],[f51])).

fof(f97,plain,(
? [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) & ~disjoint(X0,X2))),
inference(ennf_transformation,[],[f52])).

fof(f133,plain,(
subset(sK10,sK11) & disjoint(sK11,sK12) & ~disjoint(sK10,sK12)),
inference(skolemisation,[status(esa)],[f98])).
fof(f98,plain,(
? [X0,X1,X2] : (subset(X0,X1) & disjoint(X1,X2) & ~disjoint(X0,X2))),
inference(flattening,[],[f97])).

fof(f209,plain,(
~disjoint(sK10,sK12)),
inference(cnf_transformation,[],[f133])).

fof(f208,plain,(
disjoint(sK11,sK12)),
inference(cnf_transformation,[],[f133])).

fof(f207,plain,(
subset(sK10,sK11)),
inference(cnf_transformation,[],[f133])).

cnf(c_17,plain,
( ~ in(X0_\$i,X1_\$i) | in(X0_\$i,X2_\$i) | ~ subset(X1_\$i,X2_\$i) ),
inference(cnf_transformation,[],[f149]) ).

cnf(c_262,plain,
( ~ in(sK8(sK12,sK10),sK10)
| in(sK8(sK12,sK10),X0_\$i)
| ~ subset(sK10,X0_\$i) ),
inference(instantiation,[status(thm)],[c_17]) ).

cnf(c_835,plain,
( ~ in(sK8(sK12,sK10),sK10)
| in(sK8(sK12,sK10),sK11)
| ~ subset(sK10,sK11) ),
inference(instantiation,[status(thm)],[c_262]) ).

cnf(c_62,plain,
( ~ in(X0_\$i,X1_\$i) | ~ in(X0_\$i,X2_\$i) | ~ disjoint(X2_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f198]) ).

cnf(c_243,plain,
( ~ in(sK8(sK12,sK10),sK12)
| ~ in(sK8(sK12,sK10),X0_\$i)
| ~ disjoint(X0_\$i,sK12) ),
inference(instantiation,[status(thm)],[c_62]) ).

cnf(c_760,plain,
( ~ in(sK8(sK12,sK10),sK12)
| ~ in(sK8(sK12,sK10),sK11)
| ~ disjoint(sK11,sK12) ),
inference(instantiation,[status(thm)],[c_243]) ).

cnf(c_64,plain,
( in(sK8(X0_\$i,X1_\$i),X1_\$i) | disjoint(X1_\$i,X0_\$i) ),
inference(cnf_transformation,[],[f196]) ).

cnf(c_210,plain,
( in(sK8(sK12,sK10),sK10) | disjoint(sK10,sK12) ),
inference(instantiation,[status(thm)],[c_64]) ).

cnf(c_63,plain,
( in(sK8(X0_\$i,X1_\$i),X0_\$i) | disjoint(X1_\$i,X0_\$i) ),
inference(cnf_transformation,[],[f197]) ).

cnf(c_209,plain,
( in(sK8(sK12,sK10),sK12) | disjoint(sK10,sK12) ),
inference(instantiation,[status(thm)],[c_63]) ).

cnf(c_72,negated_conjecture,
( ~ disjoint(sK10,sK12) ),
inference(cnf_transformation,[],[f209]) ).

cnf(c_73,negated_conjecture,
( disjoint(sK11,sK12) ),
inference(cnf_transformation,[],[f208]) ).

cnf(c_74,negated_conjecture,
( subset(sK10,sK11) ),
inference(cnf_transformation,[],[f207]) ).

( \$false ),
inference(minisat,
[status(thm)],
[c_835,c_760,c_210,c_209,c_72,c_73,c_74]) ).

% SZS output end CNFRefutation
```

Sample solution for NLP042+1

```% SZS status CounterSatisfiable

% SZS output start Saturation

fof(f43,axiom,(
! [X0,X1,X2] : ((entity(X0,X1) & forename(X0,X2) & of(X0,X2,X1)) => ~? [X3] : (forename(X0,X3) & X2 != X3 & of(X0,X3,X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f98,plain,(
! [X0,X1,X2] : ((~entity(X0,X1) | ~forename(X0,X2) | ~of(X0,X2,X1)) | ! [X3] : (~forename(X0,X3) | X2 = X3 | ~of(X0,X3,X1)))),
inference(ennf_transformation,[],[f43])).

fof(f99,plain,(
! [X0,X1,X2] : (~entity(X0,X1) | ~forename(X0,X2) | ~of(X0,X2,X1) | ! [X3] : (~forename(X0,X3) | X2 = X3 | ~of(X0,X3,X1)))),
inference(flattening,[],[f98])).

fof(f139,plain,(
( ! [X2,X0,X3,X1] : (~of(X0,X3,X1) | X2 = X3 | ~forename(X0,X3) | ~of(X0,X2,X1) | ~forename(X0,X2) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f99])).

fof(f45,conjecture,(
~? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f46,negated_conjecture,(
~~? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(negated_conjecture,[],[f45])).

fof(f53,plain,(
? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & past(X0,X4) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(flattening,[],[f46])).

fof(f54,plain,(
? [X0] : (actual_world(X0) & ? [X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & nonreflexive(X0,X4) & order(X0,X4)))),
inference(pure_predicate_removal,[],[f53])).

fof(f102,plain,(
of(sK0,sK2,sK1) & woman(sK0,sK1) & mia_forename(sK0,sK2) & forename(sK0,sK2) & shake_beverage(sK0,sK3) & event(sK0,sK4) & agent(sK0,sK4,sK1) & patient(sK0,sK4,sK3) & nonreflexive(sK0,sK4) & order(sK0,sK4)),
inference(skolemisation,[status(esa)],[f55])).
fof(f55,plain,(
? [X0,X1,X2,X3,X4] : (of(X0,X2,X1) & woman(X0,X1) & mia_forename(X0,X2) & forename(X0,X2) & shake_beverage(X0,X3) & event(X0,X4) & agent(X0,X4,X1) & patient(X0,X4,X3) & nonreflexive(X0,X4) & order(X0,X4))),
inference(pure_predicate_removal,[],[f54])).

fof(f141,plain,(
of(sK0,sK2,sK1)),
inference(cnf_transformation,[],[f102])).

fof(f144,plain,(
forename(sK0,sK2)),
inference(cnf_transformation,[],[f102])).

fof(f44,axiom,(
! [X0,X1,X2,X3] : ((nonreflexive(X0,X1) & agent(X0,X1,X2) & patient(X0,X1,X3)) => X2 != X3)),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f100,plain,(
! [X0,X1,X2,X3] : ((~nonreflexive(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3)) | X2 != X3)),
inference(ennf_transformation,[],[f44])).

fof(f101,plain,(
! [X0,X1,X2,X3] : (~nonreflexive(X0,X1) | ~agent(X0,X1,X2) | ~patient(X0,X1,X3) | X2 != X3)),
inference(flattening,[],[f100])).

fof(f140,plain,(
( ! [X2,X0,X3,X1] : (X2 != X3 | ~patient(X0,X1,X3) | ~agent(X0,X1,X2) | ~nonreflexive(X0,X1)) )),
inference(cnf_transformation,[],[f101])).

fof(f151,plain,(
( ! [X0,X3,X1] : (~patient(X0,X1,X3) | ~agent(X0,X1,X3) | ~nonreflexive(X0,X1)) )),
inference(equality_resolution,[],[f140])).

fof(f147,plain,(
agent(sK0,sK4,sK1)),
inference(cnf_transformation,[],[f102])).

fof(f149,plain,(
nonreflexive(sK0,sK4)),
inference(cnf_transformation,[],[f102])).

fof(f27,axiom,(
! [X0,X1] : (shake_beverage(X0,X1) => beverage(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f84,plain,(
! [X0,X1] : (~shake_beverage(X0,X1) | beverage(X0,X1))),
inference(ennf_transformation,[],[f27])).

fof(f125,plain,(
( ! [X0,X1] : (beverage(X0,X1) | ~shake_beverage(X0,X1)) )),
inference(cnf_transformation,[],[f84])).

fof(f26,axiom,(
! [X0,X1] : (beverage(X0,X1) => food(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f83,plain,(
! [X0,X1] : (~beverage(X0,X1) | food(X0,X1))),
inference(ennf_transformation,[],[f26])).

fof(f124,plain,(
( ! [X0,X1] : (food(X0,X1) | ~beverage(X0,X1)) )),
inference(cnf_transformation,[],[f83])).

fof(f25,axiom,(
! [X0,X1] : (food(X0,X1) => substance_matter(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f82,plain,(
! [X0,X1] : (~food(X0,X1) | substance_matter(X0,X1))),
inference(ennf_transformation,[],[f25])).

fof(f123,plain,(
( ! [X0,X1] : (substance_matter(X0,X1) | ~food(X0,X1)) )),
inference(cnf_transformation,[],[f82])).

fof(f24,axiom,(
! [X0,X1] : (substance_matter(X0,X1) => object(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f81,plain,(
! [X0,X1] : (~substance_matter(X0,X1) | object(X0,X1))),
inference(ennf_transformation,[],[f24])).

fof(f122,plain,(
( ! [X0,X1] : (object(X0,X1) | ~substance_matter(X0,X1)) )),
inference(cnf_transformation,[],[f81])).

fof(f8,axiom,(
! [X0,X1] : (woman(X0,X1) => human_person(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f68,plain,(
! [X0,X1] : (~woman(X0,X1) | human_person(X0,X1))),
inference(ennf_transformation,[],[f8])).

fof(f109,plain,(
( ! [X0,X1] : (human_person(X0,X1) | ~woman(X0,X1)) )),
inference(cnf_transformation,[],[f68])).

fof(f19,axiom,(
! [X0,X1] : (object(X0,X1) => nonliving(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f77,plain,(
! [X0,X1] : (~object(X0,X1) | nonliving(X0,X1))),
inference(ennf_transformation,[],[f19])).

fof(f118,plain,(
( ! [X0,X1] : (nonliving(X0,X1) | ~object(X0,X1)) )),
inference(cnf_transformation,[],[f77])).

fof(f2,axiom,(
! [X0,X1] : (human_person(X0,X1) => animate(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f63,plain,(
! [X0,X1] : (~human_person(X0,X1) | animate(X0,X1))),
inference(ennf_transformation,[],[f2])).

fof(f104,plain,(
( ! [X0,X1] : (animate(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f63])).

fof(f37,axiom,(
! [X0,X1] : (animate(X0,X1) => ~nonliving(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f47,plain,(
! [X0,X1] : (animate(X0,X1) => ~nonliving(X0,X1))),
inference(flattening,[],[f37])).

fof(f92,plain,(
! [X0,X1] : (~animate(X0,X1) | ~nonliving(X0,X1))),
inference(ennf_transformation,[],[f47])).

fof(f133,plain,(
( ! [X0,X1] : (~nonliving(X0,X1) | ~animate(X0,X1)) )),
inference(cnf_transformation,[],[f92])).

fof(f145,plain,(
shake_beverage(sK0,sK3)),
inference(cnf_transformation,[],[f102])).

fof(f16,axiom,(
! [X0,X1] : (forename(X0,X1) => relname(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f75,plain,(
! [X0,X1] : (~forename(X0,X1) | relname(X0,X1))),
inference(ennf_transformation,[],[f16])).

fof(f116,plain,(
( ! [X0,X1] : (relname(X0,X1) | ~forename(X0,X1)) )),
inference(cnf_transformation,[],[f75])).

fof(f15,axiom,(
! [X0,X1] : (relname(X0,X1) => relation(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f74,plain,(
! [X0,X1] : (~relname(X0,X1) | relation(X0,X1))),
inference(ennf_transformation,[],[f15])).

fof(f115,plain,(
( ! [X0,X1] : (relation(X0,X1) | ~relname(X0,X1)) )),
inference(cnf_transformation,[],[f74])).

fof(f14,axiom,(
! [X0,X1] : (relation(X0,X1) => abstraction(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f73,plain,(
! [X0,X1] : (~relation(X0,X1) | abstraction(X0,X1))),
inference(ennf_transformation,[],[f14])).

fof(f114,plain,(
( ! [X0,X1] : (abstraction(X0,X1) | ~relation(X0,X1)) )),
inference(cnf_transformation,[],[f73])).

fof(f21,axiom,(
! [X0,X1] : (entity(X0,X1) => specific(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f79,plain,(
! [X0,X1] : (~entity(X0,X1) | specific(X0,X1))),
inference(ennf_transformation,[],[f21])).

fof(f120,plain,(
( ! [X0,X1] : (specific(X0,X1) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f79])).

fof(f11,axiom,(
! [X0,X1] : (abstraction(X0,X1) => general(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f71,plain,(
! [X0,X1] : (~abstraction(X0,X1) | general(X0,X1))),
inference(ennf_transformation,[],[f11])).

fof(f112,plain,(
( ! [X0,X1] : (general(X0,X1) | ~abstraction(X0,X1)) )),
inference(cnf_transformation,[],[f71])).

fof(f41,axiom,(
! [X0,X1] : (specific(X0,X1) => ~general(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f51,plain,(
! [X0,X1] : (specific(X0,X1) => ~general(X0,X1))),
inference(flattening,[],[f41])).

fof(f96,plain,(
! [X0,X1] : (~specific(X0,X1) | ~general(X0,X1))),
inference(ennf_transformation,[],[f51])).

fof(f137,plain,(
( ! [X0,X1] : (~general(X0,X1) | ~specific(X0,X1)) )),
inference(cnf_transformation,[],[f96])).

fof(f7,axiom,(
! [X0,X1] : (human_person(X0,X1) => organism(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f67,plain,(
! [X0,X1] : (~human_person(X0,X1) | organism(X0,X1))),
inference(ennf_transformation,[],[f7])).

fof(f108,plain,(
( ! [X0,X1] : (organism(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f67])).

fof(f6,axiom,(
! [X0,X1] : (organism(X0,X1) => entity(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f66,plain,(
! [X0,X1] : (~organism(X0,X1) | entity(X0,X1))),
inference(ennf_transformation,[],[f6])).

fof(f107,plain,(
( ! [X0,X1] : (entity(X0,X1) | ~organism(X0,X1)) )),
inference(cnf_transformation,[],[f66])).

fof(f34,axiom,(
! [X0,X1] : (event(X0,X1) => eventuality(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f89,plain,(
! [X0,X1] : (~event(X0,X1) | eventuality(X0,X1))),
inference(ennf_transformation,[],[f34])).

fof(f130,plain,(
( ! [X0,X1] : (eventuality(X0,X1) | ~event(X0,X1)) )),
inference(cnf_transformation,[],[f89])).

fof(f31,axiom,(
! [X0,X1] : (eventuality(X0,X1) => specific(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f88,plain,(
! [X0,X1] : (~eventuality(X0,X1) | specific(X0,X1))),
inference(ennf_transformation,[],[f31])).

fof(f129,plain,(
( ! [X0,X1] : (specific(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f88])).

fof(f146,plain,(
event(sK0,sK4)),
inference(cnf_transformation,[],[f102])).

fof(f30,axiom,(
! [X0,X1] : (eventuality(X0,X1) => nonexistent(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f87,plain,(
! [X0,X1] : (~eventuality(X0,X1) | nonexistent(X0,X1))),
inference(ennf_transformation,[],[f30])).

fof(f128,plain,(
( ! [X0,X1] : (nonexistent(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f87])).

fof(f20,axiom,(
! [X0,X1] : (entity(X0,X1) => existent(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f78,plain,(
! [X0,X1] : (~entity(X0,X1) | existent(X0,X1))),
inference(ennf_transformation,[],[f20])).

fof(f119,plain,(
( ! [X0,X1] : (existent(X0,X1) | ~entity(X0,X1)) )),
inference(cnf_transformation,[],[f78])).

fof(f38,axiom,(
! [X0,X1] : (existent(X0,X1) => ~nonexistent(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f48,plain,(
! [X0,X1] : (existent(X0,X1) => ~nonexistent(X0,X1))),
inference(flattening,[],[f38])).

fof(f93,plain,(
! [X0,X1] : (~existent(X0,X1) | ~nonexistent(X0,X1))),
inference(ennf_transformation,[],[f48])).

fof(f134,plain,(
( ! [X0,X1] : (~nonexistent(X0,X1) | ~existent(X0,X1)) )),
inference(cnf_transformation,[],[f93])).

fof(f23,axiom,(
! [X0,X1] : (object(X0,X1) => entity(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f80,plain,(
! [X0,X1] : (~object(X0,X1) | entity(X0,X1))),
inference(ennf_transformation,[],[f23])).

fof(f121,plain,(
( ! [X0,X1] : (entity(X0,X1) | ~object(X0,X1)) )),
inference(cnf_transformation,[],[f80])).

fof(f9,axiom,(
! [X0,X1] : (mia_forename(X0,X1) => forename(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f69,plain,(
! [X0,X1] : (~mia_forename(X0,X1) | forename(X0,X1))),
inference(ennf_transformation,[],[f9])).

fof(f110,plain,(
( ! [X0,X1] : (forename(X0,X1) | ~mia_forename(X0,X1)) )),
inference(cnf_transformation,[],[f69])).

fof(f28,axiom,(
! [X0,X1] : (order(X0,X1) => event(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f85,plain,(
! [X0,X1] : (~order(X0,X1) | event(X0,X1))),
inference(ennf_transformation,[],[f28])).

fof(f126,plain,(
( ! [X0,X1] : (event(X0,X1) | ~order(X0,X1)) )),
inference(cnf_transformation,[],[f85])).

fof(f12,axiom,(
! [X0,X1] : (abstraction(X0,X1) => nonhuman(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f72,plain,(
! [X0,X1] : (~abstraction(X0,X1) | nonhuman(X0,X1))),
inference(ennf_transformation,[],[f12])).

fof(f113,plain,(
( ! [X0,X1] : (nonhuman(X0,X1) | ~abstraction(X0,X1)) )),
inference(cnf_transformation,[],[f72])).

fof(f3,axiom,(
! [X0,X1] : (human_person(X0,X1) => human(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f64,plain,(
! [X0,X1] : (~human_person(X0,X1) | human(X0,X1))),
inference(ennf_transformation,[],[f3])).

fof(f105,plain,(
( ! [X0,X1] : (human(X0,X1) | ~human_person(X0,X1)) )),
inference(cnf_transformation,[],[f64])).

fof(f39,axiom,(
! [X0,X1] : (nonhuman(X0,X1) => ~human(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f49,plain,(
! [X0,X1] : (nonhuman(X0,X1) => ~human(X0,X1))),
inference(flattening,[],[f39])).

fof(f94,plain,(
! [X0,X1] : (~nonhuman(X0,X1) | ~human(X0,X1))),
inference(ennf_transformation,[],[f49])).

fof(f135,plain,(
( ! [X0,X1] : (~human(X0,X1) | ~nonhuman(X0,X1)) )),
inference(cnf_transformation,[],[f94])).

fof(f29,axiom,(
! [X0,X1] : (eventuality(X0,X1) => unisex(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f86,plain,(
! [X0,X1] : (~eventuality(X0,X1) | unisex(X0,X1))),
inference(ennf_transformation,[],[f29])).

fof(f127,plain,(
( ! [X0,X1] : (unisex(X0,X1) | ~eventuality(X0,X1)) )),
inference(cnf_transformation,[],[f86])).

fof(f1,axiom,(
! [X0,X1] : (woman(X0,X1) => female(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f62,plain,(
! [X0,X1] : (~woman(X0,X1) | female(X0,X1))),
inference(ennf_transformation,[],[f1])).

fof(f103,plain,(
( ! [X0,X1] : (female(X0,X1) | ~woman(X0,X1)) )),
inference(cnf_transformation,[],[f62])).

fof(f42,axiom,(
! [X0,X1] : (unisex(X0,X1) => ~female(X0,X1))),
file('/Users/korovin/TPTP-v6.1.0/Problems/NLP/NLP042+1.p',unknown)).

fof(f52,plain,(
! [X0,X1] : (unisex(X0,X1) => ~female(X0,X1))),
inference(flattening,[],[f42])).

fof(f97,plain,(
! [X0,X1] : (~unisex(X0,X1) | ~female(X0,X1))),
inference(ennf_transformation,[],[f52])).

fof(f138,plain,(
( ! [X0,X1] : (~female(X0,X1) | ~unisex(X0,X1)) )),
inference(cnf_transformation,[],[f97])).

fof(f142,plain,(
woman(sK0,sK1)),
inference(cnf_transformation,[],[f102])).

fof(f143,plain,(
mia_forename(sK0,sK2)),
inference(cnf_transformation,[],[f102])).

fof(f148,plain,(
patient(sK0,sK4,sK3)),
inference(cnf_transformation,[],[f102])).

fof(f150,plain,(
order(sK0,sK4)),
inference(cnf_transformation,[],[f102])).

cnf(c_36,plain,
( ~ entity(X0_\$i,X1_\$i)
| ~ forename(X0_\$i,X2_\$i)
| ~ forename(X0_\$i,X3_\$i)
| ~ of(X0_\$i,X2_\$i,X1_\$i)
| ~ of(X0_\$i,X3_\$i,X1_\$i)
| X3_\$i = X2_\$i ),
inference(cnf_transformation,[],[f139]) ).

cnf(c_495,plain,
( ~ entity(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ forename(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| ~ forename(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i)
| ~ of(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i,X0_\$\$iProver_event_2_\$i)
| ~ of(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X0_\$\$iProver_event_2_\$i)
| X2_\$\$iProver_event_2_\$i = X1_\$\$iProver_event_2_\$i ),
inference(subtyping,[status(esa)],[c_36]) ).

cnf(c_47,negated_conjecture,
( of(sK0,sK2,sK1) ),
inference(cnf_transformation,[],[f141]) ).

cnf(c_484,negated_conjecture,
( of(sK0,sK2,sK1) ),
inference(subtyping,[status(esa)],[c_47]) ).

cnf(c_649,plain,
( ~ entity(sK0,sK1)
| ~ forename(sK0,sK2)
| ~ forename(sK0,X0_\$\$iProver_event_2_\$i)
| ~ of(sK0,X0_\$\$iProver_event_2_\$i,sK1)
| sK2 = X0_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_495,c_484]) ).

cnf(c_44,negated_conjecture,
( forename(sK0,sK2) ),
inference(cnf_transformation,[],[f144]) ).

cnf(c_650,plain,
( ~ entity(sK0,sK1)
| ~ forename(sK0,X0_\$\$iProver_event_2_\$i)
| ~ of(sK0,X0_\$\$iProver_event_2_\$i,sK1)
| sK2 = X0_\$\$iProver_event_2_\$i ),
inference(global_propositional_subsumption,[status(thm)],[c_649,c_44]) ).

cnf(c_663,plain,
( ~ entity(sK0,sK1) | ~ forename(sK0,sK2) | sK2 = sK2 ),
inference(resolution,[status(thm)],[c_650,c_484]) ).

cnf(c_664,plain,
( ~ entity(sK0,sK1) | sK2 = sK2 ),
inference(global_propositional_subsumption,[status(thm)],[c_663,c_44]) ).

cnf(c_498,plain,
( X0_\$\$iProver_event_2_\$i = X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_667,plain,
( sK2 = sK2 ),
inference(forward_subsumption_resolution,[status(thm)],[c_664,c_498]) ).

cnf(c_508,plain,
( agent(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ agent(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X3_\$\$iProver_event_2_\$i)
| X0_\$\$iProver_event_2_\$i != X2_\$\$iProver_event_2_\$i
| X1_\$\$iProver_event_2_\$i != X3_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_684,plain,
( agent(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,sK2)
| ~ agent(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i,sK2)
| X0_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_667,c_508]) ).

cnf(c_507,plain,
( patient(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ patient(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X3_\$\$iProver_event_2_\$i)
| X0_\$\$iProver_event_2_\$i != X2_\$\$iProver_event_2_\$i
| X1_\$\$iProver_event_2_\$i != X3_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_683,plain,
( patient(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,sK2)
| ~ patient(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i,sK2)
| X0_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_667,c_507]) ).

cnf(c_506,plain,
( of(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ of(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X3_\$\$iProver_event_2_\$i)
| X0_\$\$iProver_event_2_\$i != X2_\$\$iProver_event_2_\$i
| X1_\$\$iProver_event_2_\$i != X3_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_682,plain,
( of(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,sK2)
| ~ of(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i,sK2)
| X0_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_667,c_506]) ).

cnf(c_499,plain,
( X0_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i
| X2_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i
| X2_\$\$iProver_event_2_\$i = X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_671,plain,
( sK2 = X0_\$\$iProver_event_2_\$i | X0_\$\$iProver_event_2_\$i != sK2 ),
inference(resolution,[status(thm)],[c_667,c_499]) ).

cnf(c_638,plain,
( agent(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ agent(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| X0_\$\$iProver_event_2_\$i != X2_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_508,c_498]) ).

cnf(c_629,plain,
( patient(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ patient(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| X0_\$\$iProver_event_2_\$i != X2_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_507,c_498]) ).

cnf(c_620,plain,
( ~ of(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| of(X0_\$\$iProver_event_1_\$i,X2_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| X2_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_506,c_498]) ).

cnf(c_612,plain,
( X0_\$\$iProver_event_2_\$i != X1_\$\$iProver_event_2_\$i
| X1_\$\$iProver_event_2_\$i = X0_\$\$iProver_event_2_\$i ),
inference(resolution,[status(thm)],[c_499,c_498]) ).

cnf(c_37,plain,
( ~ patient(X0_\$i,X1_\$i,X2_\$i)
| ~ agent(X0_\$i,X1_\$i,X2_\$i)
| ~ nonreflexive(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f151]) ).

cnf(c_494,plain,
( ~ patient(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ agent(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i,X1_\$\$iProver_event_2_\$i)
| ~ nonreflexive(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_37]) ).

cnf(c_41,negated_conjecture,
( agent(sK0,sK4,sK1) ),
inference(cnf_transformation,[],[f147]) ).

cnf(c_490,negated_conjecture,
( agent(sK0,sK4,sK1) ),
inference(subtyping,[status(esa)],[c_41]) ).

cnf(c_604,plain,
( ~ patient(sK0,sK4,sK1) | ~ nonreflexive(sK0,sK4) ),
inference(resolution,[status(thm)],[c_494,c_490]) ).

cnf(c_39,negated_conjecture,
( nonreflexive(sK0,sK4) ),
inference(cnf_transformation,[],[f149]) ).

cnf(c_605,plain,
( ~ patient(sK0,sK4,sK1) ),
inference(global_propositional_subsumption,[status(thm)],[c_604,c_39]) ).

cnf(c_22,plain,
( beverage(X0_\$i,X1_\$i) | ~ shake_beverage(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f125]) ).

cnf(c_21,plain,
( food(X0_\$i,X1_\$i) | ~ beverage(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f124]) ).

cnf(c_20,plain,
( substance_matter(X0_\$i,X1_\$i) | ~ food(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f123]) ).

cnf(c_19,plain,
( object(X0_\$i,X1_\$i) | ~ substance_matter(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f122]) ).

cnf(c_176,plain,
( object(X0_\$i,X1_\$i) | ~ food(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_20,c_19]) ).

cnf(c_186,plain,
( object(X0_\$i,X1_\$i) | ~ beverage(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_21,c_176]) ).

cnf(c_196,plain,
( object(X0_\$i,X1_\$i) | ~ shake_beverage(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_22,c_186]) ).

cnf(c_6,plain,
( ~ woman(X0_\$i,X1_\$i) | human_person(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f109]) ).

cnf(c_15,plain,
( ~ object(X0_\$i,X1_\$i) | nonliving(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f118]) ).

cnf(c_1,plain,
( animate(X0_\$i,X1_\$i) | ~ human_person(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f104]) ).

cnf(c_30,plain,
( ~ animate(X0_\$i,X1_\$i) | ~ nonliving(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f133]) ).

cnf(c_96,plain,
( ~ human_person(X0_\$i,X1_\$i) | ~ nonliving(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_1,c_30]) ).

cnf(c_228,plain,
( ~ human_person(X0_\$i,X1_\$i) | ~ object(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_15,c_96]) ).

cnf(c_258,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ object(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_6,c_228]) ).

cnf(c_300,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ shake_beverage(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_196,c_258]) ).

cnf(c_482,plain,
( ~ woman(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ shake_beverage(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_300]) ).

cnf(c_43,negated_conjecture,
( shake_beverage(sK0,sK3) ),
inference(cnf_transformation,[],[f145]) ).

cnf(c_488,negated_conjecture,
( shake_beverage(sK0,sK3) ),
inference(subtyping,[status(esa)],[c_43]) ).

cnf(c_575,plain,
( ~ woman(sK0,sK3) ),
inference(resolution,[status(thm)],[c_482,c_488]) ).

cnf(c_13,plain,
( ~ forename(X0_\$i,X1_\$i) | relname(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f116]) ).

cnf(c_12,plain,
( relation(X0_\$i,X1_\$i) | ~ relname(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f115]) ).

cnf(c_11,plain,
( abstraction(X0_\$i,X1_\$i) | ~ relation(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f114]) ).

cnf(c_146,plain,
( abstraction(X0_\$i,X1_\$i) | ~ relname(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_12,c_11]) ).

cnf(c_156,plain,
( ~ forename(X0_\$i,X1_\$i) | abstraction(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_13,c_146]) ).

cnf(c_17,plain,
( ~ entity(X0_\$i,X1_\$i) | specific(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f120]) ).

cnf(c_9,plain,
( ~ abstraction(X0_\$i,X1_\$i) | general(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f112]) ).

cnf(c_34,plain,
( ~ general(X0_\$i,X1_\$i) | ~ specific(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f137]) ).

cnf(c_126,plain,
( ~ abstraction(X0_\$i,X1_\$i) | ~ specific(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_9,c_34]) ).

cnf(c_246,plain,
( ~ entity(X0_\$i,X1_\$i) | ~ abstraction(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_17,c_126]) ).

cnf(c_328,plain,
( ~ entity(X0_\$i,X1_\$i) | ~ forename(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_156,c_246]) ).

cnf(c_479,plain,
( ~ entity(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_328]) ).

cnf(c_487,negated_conjecture,
( forename(sK0,sK2) ),
inference(subtyping,[status(esa)],[c_44]) ).

cnf(c_566,plain,
( ~ entity(sK0,sK2) ),
inference(resolution,[status(thm)],[c_479,c_487]) ).

cnf(c_5,plain,
( ~ human_person(X0_\$i,X1_\$i) | organism(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f108]) ).

cnf(c_4,plain,
( ~ organism(X0_\$i,X1_\$i) | entity(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f107]) ).

cnf(c_218,plain,
( ~ human_person(X0_\$i,X1_\$i) | entity(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_5,c_4]) ).

cnf(c_266,plain,
( ~ woman(X0_\$i,X1_\$i) | entity(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_6,c_218]) ).

cnf(c_483,plain,
( ~ woman(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| entity(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_266]) ).

cnf(c_568,plain,
( ~ woman(sK0,sK2) ),
inference(resolution,[status(thm)],[c_566,c_483]) ).

cnf(c_27,plain,
( ~ event(X0_\$i,X1_\$i) | eventuality(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f130]) ).

cnf(c_26,plain,
( specific(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f129]) ).

cnf(c_238,plain,
( ~ abstraction(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_26,c_126]) ).

cnf(c_336,plain,
( ~ forename(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_156,c_238]) ).

cnf(c_350,plain,
( ~ forename(X0_\$i,X1_\$i) | ~ event(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_27,c_336]) ).

cnf(c_478,plain,
( ~ forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ event(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_350]) ).

cnf(c_42,negated_conjecture,
( event(sK0,sK4) ),
inference(cnf_transformation,[],[f146]) ).

cnf(c_489,negated_conjecture,
( event(sK0,sK4) ),
inference(subtyping,[status(esa)],[c_42]) ).

cnf(c_562,plain,
( ~ forename(sK0,sK4) ),
inference(resolution,[status(thm)],[c_478,c_489]) ).

cnf(c_25,plain,
( ~ eventuality(X0_\$i,X1_\$i) | nonexistent(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f128]) ).

cnf(c_16,plain,
( ~ entity(X0_\$i,X1_\$i) | existent(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f119]) ).

cnf(c_31,plain,
( ~ existent(X0_\$i,X1_\$i) | ~ nonexistent(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f134]) ).

cnf(c_166,plain,
( ~ entity(X0_\$i,X1_\$i) | ~ nonexistent(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_16,c_31]) ).

cnf(c_206,plain,
( ~ entity(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_25,c_166]) ).

cnf(c_366,plain,
( ~ entity(X0_\$i,X1_\$i) | ~ event(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_27,c_206]) ).

cnf(c_476,plain,
( ~ entity(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ event(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_366]) ).

cnf(c_549,plain,
( ~ entity(sK0,sK4) ),
inference(resolution,[status(thm)],[c_476,c_489]) ).

cnf(c_551,plain,
( ~ woman(sK0,sK4) ),
inference(resolution,[status(thm)],[c_549,c_483]) ).

cnf(c_18,plain,
( entity(X0_\$i,X1_\$i) | ~ object(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f121]) ).

cnf(c_308,plain,
( entity(X0_\$i,X1_\$i) | ~ shake_beverage(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_196,c_18]) ).

cnf(c_481,plain,
( entity(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ shake_beverage(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_308]) ).

cnf(c_537,plain,
( entity(sK0,sK3) ),
inference(resolution,[status(thm)],[c_481,c_488]) ).

cnf(c_509,plain,
( ~ nonreflexive(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| nonreflexive(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_505,plain,
( ~ order(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| order(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_504,plain,
( ~ event(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| event(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_503,plain,
( ~ shake_beverage(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| shake_beverage(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_502,plain,
( ~ mia_forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| mia_forename(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_501,plain,
( ~ forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| forename(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_500,plain,
( ~ woman(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| woman(X0_\$\$iProver_event_1_\$i,X1_\$\$iProver_event_2_\$i)
| X1_\$\$iProver_event_2_\$i != X0_\$\$iProver_event_2_\$i ),
theory(equality) ).

cnf(c_7,plain,
( forename(X0_\$i,X1_\$i) | ~ mia_forename(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f110]) ).

cnf(c_497,plain,
( forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ mia_forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_7]) ).

cnf(c_23,plain,
( event(X0_\$i,X1_\$i) | ~ order(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f126]) ).

cnf(c_496,plain,
( event(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ order(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_23]) ).

cnf(c_10,plain,
( ~ abstraction(X0_\$i,X1_\$i) | nonhuman(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f113]) ).

cnf(c_2,plain,
( ~ human_person(X0_\$i,X1_\$i) | human(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f105]) ).

cnf(c_32,plain,
( ~ human(X0_\$i,X1_\$i) | ~ nonhuman(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f135]) ).

cnf(c_106,plain,
( ~ human_person(X0_\$i,X1_\$i) | ~ nonhuman(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_2,c_32]) ).

cnf(c_136,plain,
( ~ human_person(X0_\$i,X1_\$i) | ~ abstraction(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_10,c_106]) ).

cnf(c_274,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ abstraction(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_6,c_136]) ).

cnf(c_320,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ forename(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_156,c_274]) ).

cnf(c_480,plain,
( ~ woman(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ forename(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_320]) ).

cnf(c_24,plain,
( unisex(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f127]) ).

cnf(c_0,plain,
( female(X0_\$i,X1_\$i) | ~ woman(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f103]) ).

cnf(c_35,plain,
( ~ female(X0_\$i,X1_\$i) | ~ unisex(X0_\$i,X1_\$i) ),
inference(cnf_transformation,[],[f138]) ).

cnf(c_86,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ unisex(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_0,c_35]) ).

cnf(c_288,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ eventuality(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_24,c_86]) ).

cnf(c_358,plain,
( ~ woman(X0_\$i,X1_\$i) | ~ event(X0_\$i,X1_\$i) ),
inference(resolution,[status(thm)],[c_27,c_288]) ).

cnf(c_477,plain,
( ~ woman(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i)
| ~ event(X0_\$\$iProver_event_1_\$i,X0_\$\$iProver_event_2_\$i) ),
inference(subtyping,[status(esa)],[c_358]) ).

cnf(c_46,negated_conjecture,
( woman(sK0,sK1) ),
inference(cnf_transformation,[],[f142]) ).

cnf(c_485,negated_conjecture,
( woman(sK0,sK1) ),
inference(subtyping,[status(esa)],[c_46]) ).

cnf(c_45,negated_conjecture,
( mia_forename(sK0,sK2) ),
inference(cnf_transformation,[],[f143]) ).

cnf(c_486,negated_conjecture,
( mia_forename(sK0,sK2) ),
inference(subtyping,[status(esa)],[c_45]) ).

cnf(c_40,negated_conjecture,
( patient(sK0,sK4,sK3) ),
inference(cnf_transformation,[],[f148]) ).

cnf(c_491,negated_conjecture,
( patient(sK0,sK4,sK3) ),
inference(subtyping,[status(esa)],[c_40]) ).

cnf(c_492,negated_conjecture,
( nonreflexive(sK0,sK4) ),
inference(subtyping,[status(esa)],[c_39]) ).

cnf(c_38,negated_conjecture,
( order(sK0,sK4) ),
inference(cnf_transformation,[],[f150]) ).

cnf(c_493,negated_conjecture,
( order(sK0,sK4) ),
inference(subtyping,[status(esa)],[c_38]) ).

% SZS output end Saturation
```

Sample solution for SWV017+1

```% SZS status Satisfiable

% SZS output start Saturation

fof(f9,axiom,(
! [X0,X1] : ((message(sent(X0,b,pair(X0,X1))) & fresh_to_b(X1)) => (message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))) & b_stored(pair(X0,X1))))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f39,plain,(
! [X0,X1] : ((message(sent(X0,b,pair(X0,X1))) & fresh_to_b(X1)) => message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))),
inference(pure_predicate_removal,[],[f9])).

fof(f44,plain,(
! [X0,X1] : ((~message(sent(X0,b,pair(X0,X1))) | ~fresh_to_b(X1)) | message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))),
inference(ennf_transformation,[],[f39])).

fof(f45,plain,(
! [X0,X1] : (~message(sent(X0,b,pair(X0,X1))) | ~fresh_to_b(X1) | message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))))),
inference(flattening,[],[f44])).

fof(f75,plain,(
( ! [X0,X1] : (message(sent(b,t,triple(b,generate_b_nonce(X1),encrypt(triple(X0,X1,generate_expiration_time(X1)),bt)))) | ~fresh_to_b(X1) | ~message(sent(X0,b,pair(X0,X1)))) )),
inference(cnf_transformation,[],[f45])).

fof(f14,axiom,(
! [X0,X1,X2,X3,X4,X5,X6] : ((message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) & t_holds(key(X5,X0)) & t_holds(key(X6,X2)) & a_nonce(X3)) => message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f46,plain,(
! [X0,X1,X2,X3,X4,X5,X6] : ((~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) | ~t_holds(key(X5,X0)) | ~t_holds(key(X6,X2)) | ~a_nonce(X3)) | message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))),
inference(ennf_transformation,[],[f14])).

fof(f47,plain,(
! [X0,X1,X2,X3,X4,X5,X6] : (~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5)))) | ~t_holds(key(X5,X0)) | ~t_holds(key(X6,X2)) | ~a_nonce(X3) | message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))))),
inference(flattening,[],[f46])).

fof(f79,plain,(
( ! [X6,X4,X2,X0,X5,X3,X1] : (message(sent(t,X2,triple(encrypt(quadruple(X0,X3,generate_key(X3),X4),X6),encrypt(triple(X2,generate_key(X3),X4),X5),X1))) | ~a_nonce(X3) | ~t_holds(key(X6,X2)) | ~t_holds(key(X5,X0)) | ~message(sent(X0,t,triple(X0,X1,encrypt(triple(X2,X3,X4),X5))))) )),
inference(cnf_transformation,[],[f47])).

fof(f15,axiom,(
! [X0,X1,X2] : (message(sent(X0,X1,X2)) => intruder_message(X2))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f48,plain,(
! [X0,X1,X2] : (~message(sent(X0,X1,X2)) | intruder_message(X2))),
inference(ennf_transformation,[],[f15])).

fof(f80,plain,(
( ! [X2,X0,X1] : (intruder_message(X2) | ~message(sent(X0,X1,X2))) )),
inference(cnf_transformation,[],[f48])).

fof(f16,axiom,(
! [X0,X1] : (intruder_message(pair(X0,X1)) => (intruder_message(X0) & intruder_message(X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f49,plain,(
! [X0,X1] : (~intruder_message(pair(X0,X1)) | (intruder_message(X0) & intruder_message(X1)))),
inference(ennf_transformation,[],[f16])).

fof(f82,plain,(
( ! [X0,X1] : (intruder_message(X1) | ~intruder_message(pair(X0,X1))) )),
inference(cnf_transformation,[],[f49])).

fof(f81,plain,(
( ! [X0,X1] : (intruder_message(X0) | ~intruder_message(pair(X0,X1))) )),
inference(cnf_transformation,[],[f49])).

fof(f17,axiom,(
! [X0,X1,X2] : (intruder_message(triple(X0,X1,X2)) => (intruder_message(X0) & intruder_message(X1) & intruder_message(X2)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f50,plain,(
! [X0,X1,X2] : (~intruder_message(triple(X0,X1,X2)) | (intruder_message(X0) & intruder_message(X1) & intruder_message(X2)))),
inference(ennf_transformation,[],[f17])).

fof(f85,plain,(
( ! [X2,X0,X1] : (intruder_message(X2) | ~intruder_message(triple(X0,X1,X2))) )),
inference(cnf_transformation,[],[f50])).

fof(f84,plain,(
( ! [X2,X0,X1] : (intruder_message(X1) | ~intruder_message(triple(X0,X1,X2))) )),
inference(cnf_transformation,[],[f50])).

fof(f83,plain,(
( ! [X2,X0,X1] : (intruder_message(X0) | ~intruder_message(triple(X0,X1,X2))) )),
inference(cnf_transformation,[],[f50])).

fof(f18,axiom,(
! [X0,X1,X2,X3] : (intruder_message(quadruple(X0,X1,X2,X3)) => (intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f51,plain,(
! [X0,X1,X2,X3] : (~intruder_message(quadruple(X0,X1,X2,X3)) | (intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)))),
inference(ennf_transformation,[],[f18])).

fof(f89,plain,(
( ! [X2,X0,X3,X1] : (intruder_message(X3) | ~intruder_message(quadruple(X0,X1,X2,X3))) )),
inference(cnf_transformation,[],[f51])).

fof(f88,plain,(
( ! [X2,X0,X3,X1] : (intruder_message(X2) | ~intruder_message(quadruple(X0,X1,X2,X3))) )),
inference(cnf_transformation,[],[f51])).

fof(f87,plain,(
( ! [X2,X0,X3,X1] : (intruder_message(X1) | ~intruder_message(quadruple(X0,X1,X2,X3))) )),
inference(cnf_transformation,[],[f51])).

fof(f86,plain,(
( ! [X2,X0,X3,X1] : (intruder_message(X0) | ~intruder_message(quadruple(X0,X1,X2,X3))) )),
inference(cnf_transformation,[],[f51])).

fof(f19,axiom,(
! [X0,X1] : ((intruder_message(X0) & intruder_message(X1)) => intruder_message(pair(X0,X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f52,plain,(
! [X0,X1] : ((~intruder_message(X0) | ~intruder_message(X1)) | intruder_message(pair(X0,X1)))),
inference(ennf_transformation,[],[f19])).

fof(f53,plain,(
! [X0,X1] : (~intruder_message(X0) | ~intruder_message(X1) | intruder_message(pair(X0,X1)))),
inference(flattening,[],[f52])).

fof(f90,plain,(
( ! [X0,X1] : (intruder_message(pair(X0,X1)) | ~intruder_message(X1) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f53])).

fof(f20,axiom,(
! [X0,X1,X2] : ((intruder_message(X0) & intruder_message(X1) & intruder_message(X2)) => intruder_message(triple(X0,X1,X2)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f54,plain,(
! [X0,X1,X2] : ((~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2)) | intruder_message(triple(X0,X1,X2)))),
inference(ennf_transformation,[],[f20])).

fof(f55,plain,(
! [X0,X1,X2] : (~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | intruder_message(triple(X0,X1,X2)))),
inference(flattening,[],[f54])).

fof(f91,plain,(
( ! [X2,X0,X1] : (intruder_message(triple(X0,X1,X2)) | ~intruder_message(X2) | ~intruder_message(X1) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f55])).

fof(f21,axiom,(
! [X0,X1,X2,X3] : ((intruder_message(X0) & intruder_message(X1) & intruder_message(X2) & intruder_message(X3)) => intruder_message(quadruple(X0,X1,X2,X3)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f56,plain,(
! [X0,X1,X2,X3] : ((~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | ~intruder_message(X3)) | intruder_message(quadruple(X0,X1,X2,X3)))),
inference(ennf_transformation,[],[f21])).

fof(f57,plain,(
! [X0,X1,X2,X3] : (~intruder_message(X0) | ~intruder_message(X1) | ~intruder_message(X2) | ~intruder_message(X3) | intruder_message(quadruple(X0,X1,X2,X3)))),
inference(flattening,[],[f56])).

fof(f92,plain,(
( ! [X2,X0,X3,X1] : (intruder_message(quadruple(X0,X1,X2,X3)) | ~intruder_message(X3) | ~intruder_message(X2) | ~intruder_message(X1) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f57])).

fof(f23,axiom,(
! [X0,X1,X2] : ((intruder_message(X0) & party_of_protocol(X1) & party_of_protocol(X2)) => message(sent(X1,X2,X0)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f60,plain,(
! [X0,X1,X2] : ((~intruder_message(X0) | ~party_of_protocol(X1) | ~party_of_protocol(X2)) | message(sent(X1,X2,X0)))),
inference(ennf_transformation,[],[f23])).

fof(f61,plain,(
! [X0,X1,X2] : (~intruder_message(X0) | ~party_of_protocol(X1) | ~party_of_protocol(X2) | message(sent(X1,X2,X0)))),
inference(flattening,[],[f60])).

fof(f94,plain,(
( ! [X2,X0,X1] : (message(sent(X1,X2,X0)) | ~party_of_protocol(X2) | ~party_of_protocol(X1) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f61])).

fof(f27,axiom,(
! [X0] : ~a_nonce(generate_key(X0))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f36,plain,(
! [X0] : ~a_nonce(generate_key(X0))),
inference(flattening,[],[f27])).

fof(f98,plain,(
( ! [X0] : (~a_nonce(generate_key(X0))) )),
inference(cnf_transformation,[],[f36])).

fof(f28,axiom,(
! [X0] : (a_nonce(generate_expiration_time(X0)) & a_nonce(generate_b_nonce(X0)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f100,plain,(
( ! [X0] : (a_nonce(generate_b_nonce(X0))) )),
inference(cnf_transformation,[],[f28])).

fof(f99,plain,(
( ! [X0] : (a_nonce(generate_expiration_time(X0))) )),
inference(cnf_transformation,[],[f28])).

fof(f32,axiom,(
! [X0] : (fresh_intruder_nonce(X0) => fresh_intruder_nonce(generate_intruder_nonce(X0)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f67,plain,(
! [X0] : (~fresh_intruder_nonce(X0) | fresh_intruder_nonce(generate_intruder_nonce(X0)))),
inference(ennf_transformation,[],[f32])).

fof(f104,plain,(
( ! [X0] : (fresh_intruder_nonce(generate_intruder_nonce(X0)) | ~fresh_intruder_nonce(X0)) )),
inference(cnf_transformation,[],[f67])).

fof(f33,axiom,(
! [X0] : (fresh_intruder_nonce(X0) => (fresh_to_b(X0) & intruder_message(X0)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f68,plain,(
! [X0] : (~fresh_intruder_nonce(X0) | (fresh_to_b(X0) & intruder_message(X0)))),
inference(ennf_transformation,[],[f33])).

fof(f106,plain,(
( ! [X0] : (intruder_message(X0) | ~fresh_intruder_nonce(X0)) )),
inference(cnf_transformation,[],[f68])).

fof(f105,plain,(
( ! [X0] : (fresh_to_b(X0) | ~fresh_intruder_nonce(X0)) )),
inference(cnf_transformation,[],[f68])).

fof(f4,axiom,(
a_stored(pair(b,an_a_nonce))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f71,plain,(
a_stored(pair(b,an_a_nonce))),
inference(cnf_transformation,[],[f4])).

fof(f5,axiom,(
! [X0,X1,X2,X3,X4,X5] : ((message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) & a_stored(pair(X4,X5))) => (message(sent(a,X4,pair(X3,encrypt(X0,X2)))) & a_holds(key(X2,X4))))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f40,plain,(
! [X0,X1,X2,X3,X4,X5] : ((message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) & a_stored(pair(X4,X5))) => message(sent(a,X4,pair(X3,encrypt(X0,X2)))))),
inference(pure_predicate_removal,[],[f5])).

fof(f42,plain,(
! [X0,X1,X2,X3,X4,X5] : ((~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) | ~a_stored(pair(X4,X5))) | message(sent(a,X4,pair(X3,encrypt(X0,X2)))))),
inference(ennf_transformation,[],[f40])).

fof(f43,plain,(
! [X0,X1,X2,X3,X4,X5] : (~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0))) | ~a_stored(pair(X4,X5)) | message(sent(a,X4,pair(X3,encrypt(X0,X2)))))),
inference(flattening,[],[f42])).

fof(f72,plain,(
( ! [X4,X2,X0,X5,X3,X1] : (message(sent(a,X4,pair(X3,encrypt(X0,X2)))) | ~a_stored(pair(X4,X5)) | ~message(sent(t,a,triple(encrypt(quadruple(X4,X5,X2,X1),at),X3,X0)))) )),
inference(cnf_transformation,[],[f43])).

fof(f25,axiom,(
! [X0,X1,X2] : ((intruder_message(X0) & intruder_holds(key(X1,X2)) & party_of_protocol(X2)) => intruder_message(encrypt(X0,X1)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f64,plain,(
! [X0,X1,X2] : ((~intruder_message(X0) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2)) | intruder_message(encrypt(X0,X1)))),
inference(ennf_transformation,[],[f25])).

fof(f65,plain,(
! [X0,X1,X2] : (~intruder_message(X0) | ~intruder_holds(key(X1,X2)) | ~party_of_protocol(X2) | intruder_message(encrypt(X0,X1)))),
inference(flattening,[],[f64])).

fof(f96,plain,(
( ! [X2,X0,X1] : (intruder_message(encrypt(X0,X1)) | ~party_of_protocol(X2) | ~intruder_holds(key(X1,X2)) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f65])).

fof(f24,axiom,(
! [X1,X2] : ((intruder_message(X1) & party_of_protocol(X2)) => intruder_holds(key(X1,X2)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f35,plain,(
! [X0,X1] : ((intruder_message(X0) & party_of_protocol(X1)) => intruder_holds(key(X0,X1)))),
inference(rectify,[],[f24])).

fof(f62,plain,(
! [X0,X1] : ((~intruder_message(X0) | ~party_of_protocol(X1)) | intruder_holds(key(X0,X1)))),
inference(ennf_transformation,[],[f35])).

fof(f63,plain,(
! [X0,X1] : (~intruder_message(X0) | ~party_of_protocol(X1) | intruder_holds(key(X0,X1)))),
inference(flattening,[],[f62])).

fof(f95,plain,(
( ! [X0,X1] : (intruder_holds(key(X0,X1)) | ~party_of_protocol(X1) | ~intruder_message(X0)) )),
inference(cnf_transformation,[],[f63])).

fof(f31,axiom,(
fresh_intruder_nonce(an_intruder_nonce)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f103,plain,(
fresh_intruder_nonce(an_intruder_nonce)),
inference(cnf_transformation,[],[f31])).

fof(f26,axiom,(
a_nonce(an_a_nonce)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f97,plain,(
a_nonce(an_a_nonce)),
inference(cnf_transformation,[],[f26])).

fof(f13,axiom,(
party_of_protocol(t)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f78,plain,(
party_of_protocol(t)),
inference(cnf_transformation,[],[f13])).

fof(f12,axiom,(
t_holds(key(bt,b))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f77,plain,(
t_holds(key(bt,b))),
inference(cnf_transformation,[],[f12])).

fof(f11,axiom,(
t_holds(key(at,a))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f76,plain,(
t_holds(key(at,a))),
inference(cnf_transformation,[],[f11])).

fof(f8,axiom,(
fresh_to_b(an_a_nonce)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f74,plain,(
fresh_to_b(an_a_nonce)),
inference(cnf_transformation,[],[f8])).

fof(f7,axiom,(
party_of_protocol(b)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f73,plain,(
party_of_protocol(b)),
inference(cnf_transformation,[],[f7])).

fof(f3,axiom,(
message(sent(a,b,pair(a,an_a_nonce)))),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f70,plain,(
message(sent(a,b,pair(a,an_a_nonce)))),
inference(cnf_transformation,[],[f3])).

fof(f2,axiom,(
party_of_protocol(a)),
file('/Users/korovin/TPTP-v6.1.0/Problems/SWV/SWV017+1.p',unknown)).

fof(f69,plain,(
party_of_protocol(a)),
inference(cnf_transformation,[],[f2])).

cnf(c_6,plain,
( message(sent(b,t,triple(b,generate_b_nonce(X0_\$i),encrypt(triple(X1_\$i,X0_\$i,generate_expiration_time(X0_\$i)),bt))))
| ~ message(sent(X1_\$i,b,pair(X1_\$i,X0_\$i)))
| ~ fresh_to_b(X0_\$i) ),
inference(cnf_transformation,[],[f75]) ).

cnf(c_233,plain,
( message(sent(b,t,triple(b,generate_b_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i),encrypt(triple(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X0_\$\$iProver_fresh_intruder_nonce_1_\$i,generate_expiration_time(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)),bt))))
| ~ message(sent(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,b,pair(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X0_\$\$iProver_fresh_intruder_nonce_1_\$i)))
| ~ fresh_to_b(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_6]) ).

cnf(c_10,plain,
| ~ message(sent(X1_\$i,t,triple(X1_\$i,X6_\$i,encrypt(triple(X0_\$i,X2_\$i,X3_\$i),X5_\$i))))
| ~ t_holds(key(X4_\$i,X0_\$i))
| ~ t_holds(key(X5_\$i,X1_\$i))
| ~ a_nonce(X2_\$i) ),
inference(cnf_transformation,[],[f79]) ).

cnf(c_229,plain,
| ~ message(sent(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,t,triple(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X6_\$\$iProver_fresh_intruder_nonce_1_\$i,encrypt(triple(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i,X3_\$\$iProver_fresh_intruder_nonce_1_\$i),X5_\$\$iProver_fresh_intruder_nonce_1_\$i))))
| ~ t_holds(key(X4_\$\$iProver_fresh_intruder_nonce_1_\$i,X0_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ t_holds(key(X5_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ a_nonce(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_10]) ).

cnf(c_11,plain,
( ~ message(sent(X0_\$i,X1_\$i,X2_\$i)) | intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f80]) ).

cnf(c_228,plain,
( ~ message(sent(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_11]) ).

cnf(c_12,plain,
( ~ intruder_message(pair(X0_\$i,X1_\$i)) | intruder_message(X1_\$i) ),
inference(cnf_transformation,[],[f82]) ).

cnf(c_227,plain,
( ~ intruder_message(pair(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_12]) ).

cnf(c_13,plain,
( ~ intruder_message(pair(X0_\$i,X1_\$i)) | intruder_message(X0_\$i) ),
inference(cnf_transformation,[],[f81]) ).

cnf(c_226,plain,
( ~ intruder_message(pair(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_13]) ).

cnf(c_14,plain,
( ~ intruder_message(triple(X0_\$i,X1_\$i,X2_\$i))
| intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f85]) ).

cnf(c_225,plain,
( ~ intruder_message(triple(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_14]) ).

cnf(c_15,plain,
( ~ intruder_message(triple(X0_\$i,X1_\$i,X2_\$i))
| intruder_message(X1_\$i) ),
inference(cnf_transformation,[],[f84]) ).

cnf(c_224,plain,
( ~ intruder_message(triple(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_15]) ).

cnf(c_16,plain,
( ~ intruder_message(triple(X0_\$i,X1_\$i,X2_\$i))
| intruder_message(X0_\$i) ),
inference(cnf_transformation,[],[f83]) ).

cnf(c_223,plain,
( ~ intruder_message(triple(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_16]) ).

cnf(c_17,plain,
| intruder_message(X3_\$i) ),
inference(cnf_transformation,[],[f89]) ).

cnf(c_222,plain,
| intruder_message(X3_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_17]) ).

cnf(c_18,plain,
| intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f88]) ).

cnf(c_221,plain,
| intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_18]) ).

cnf(c_19,plain,
| intruder_message(X1_\$i) ),
inference(cnf_transformation,[],[f87]) ).

cnf(c_220,plain,
| intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_19]) ).

cnf(c_20,plain,
| intruder_message(X0_\$i) ),
inference(cnf_transformation,[],[f86]) ).

cnf(c_219,plain,
| intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_20]) ).

cnf(c_21,plain,
( intruder_message(pair(X0_\$i,X1_\$i))
| ~ intruder_message(X1_\$i)
| ~ intruder_message(X0_\$i) ),
inference(cnf_transformation,[],[f90]) ).

cnf(c_218,plain,
( intruder_message(pair(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_21]) ).

cnf(c_22,plain,
( intruder_message(triple(X0_\$i,X1_\$i,X2_\$i))
| ~ intruder_message(X1_\$i)
| ~ intruder_message(X0_\$i)
| ~ intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f91]) ).

cnf(c_217,plain,
( intruder_message(triple(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_22]) ).

cnf(c_23,plain,
| ~ intruder_message(X1_\$i)
| ~ intruder_message(X0_\$i)
| ~ intruder_message(X3_\$i)
| ~ intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f92]) ).

cnf(c_216,plain,
| ~ intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X3_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_23]) ).

cnf(c_25,plain,
( ~ party_of_protocol(X0_\$i)
| ~ party_of_protocol(X1_\$i)
| message(sent(X1_\$i,X0_\$i,X2_\$i))
| ~ intruder_message(X2_\$i) ),
inference(cnf_transformation,[],[f94]) ).

cnf(c_215,plain,
( ~ party_of_protocol(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ party_of_protocol(X1_\$\$iProver_fresh_intruder_nonce_1_\$i)
| message(sent(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ intruder_message(X2_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_25]) ).

cnf(c_29,plain,
( ~ a_nonce(generate_key(X0_\$i)) ),
inference(cnf_transformation,[],[f98]) ).

cnf(c_213,plain,
( ~ a_nonce(generate_key(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)) ),
inference(subtyping,[status(esa)],[c_29]) ).

cnf(c_30,plain,
( a_nonce(generate_b_nonce(X0_\$i)) ),
inference(cnf_transformation,[],[f100]) ).

cnf(c_212,plain,
( a_nonce(generate_b_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)) ),
inference(subtyping,[status(esa)],[c_30]) ).

cnf(c_31,plain,
( a_nonce(generate_expiration_time(X0_\$i)) ),
inference(cnf_transformation,[],[f99]) ).

cnf(c_211,plain,
( a_nonce(generate_expiration_time(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)) ),
inference(subtyping,[status(esa)],[c_31]) ).

cnf(c_35,plain,
( fresh_intruder_nonce(generate_intruder_nonce(X0_\$i))
| ~ fresh_intruder_nonce(X0_\$i) ),
inference(cnf_transformation,[],[f104]) ).

cnf(c_209,plain,
( fresh_intruder_nonce(generate_intruder_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ fresh_intruder_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_35]) ).

cnf(c_36,plain,
( intruder_message(X0_\$i) | ~ fresh_intruder_nonce(X0_\$i) ),
inference(cnf_transformation,[],[f106]) ).

cnf(c_208,plain,
( intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ fresh_intruder_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_36]) ).

cnf(c_37,plain,
( fresh_to_b(X0_\$i) | ~ fresh_intruder_nonce(X0_\$i) ),
inference(cnf_transformation,[],[f105]) ).

cnf(c_207,plain,
( fresh_to_b(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ fresh_intruder_nonce(X0_\$\$iProver_fresh_intruder_nonce_1_\$i) ),
inference(subtyping,[status(esa)],[c_37]) ).

cnf(c_2,plain,
( a_stored(pair(b,an_a_nonce)) ),
inference(cnf_transformation,[],[f71]) ).

cnf(c_3,plain,
( message(sent(a,X0_\$i,pair(X1_\$i,encrypt(X2_\$i,X3_\$i))))
| ~ a_stored(pair(X0_\$i,X4_\$i)) ),
inference(cnf_transformation,[],[f72]) ).

cnf(c_61,plain,
( message(sent(a,b,pair(X0_\$i,encrypt(X1_\$i,X2_\$i))))
| ~ message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,X2_\$i,X3_\$i),at),X0_\$i,X1_\$i))) ),
inference(resolution,[status(thm)],[c_2,c_3]) ).

cnf(c_206,plain,
( message(sent(a,b,pair(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,encrypt(X1_\$\$iProver_fresh_intruder_nonce_1_\$i,X2_\$\$iProver_fresh_intruder_nonce_1_\$i))))
| ~ message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,X2_\$\$iProver_fresh_intruder_nonce_1_\$i,X3_\$\$iProver_fresh_intruder_nonce_1_\$i),at),X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))) ),
inference(subtyping,[status(esa)],[c_61]) ).

cnf(c_27,plain,
( ~ party_of_protocol(X0_\$i)
| intruder_message(encrypt(X1_\$i,X2_\$i))
| ~ intruder_message(X1_\$i)
| ~ intruder_holds(key(X2_\$i,X0_\$i)) ),
inference(cnf_transformation,[],[f96]) ).

cnf(c_26,plain,
( ~ party_of_protocol(X0_\$i)
| ~ intruder_message(X1_\$i)
| intruder_holds(key(X1_\$i,X0_\$i)) ),
inference(cnf_transformation,[],[f95]) ).

cnf(c_95,plain,
( ~ party_of_protocol(X0_\$i)
| intruder_message(encrypt(X1_\$i,X2_\$i))
| ~ intruder_message(X2_\$i)
| ~ intruder_message(X1_\$i) ),
inference(resolution,[status(thm)],[c_27,c_26]) ).

cnf(c_168,plain,
( ~ party_of_protocol(X0_\$i) | ~ sP0_iProver_split ),
inference(splitting,
[splitting(split),new_symbols(definition,[~ sP0_iProver_split])],
[c_95]) ).

cnf(c_205,plain,
( ~ party_of_protocol(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ sP0_iProver_split ),
inference(subtyping,[status(esa)],[c_168]) ).

cnf(c_169,plain,
( intruder_message(encrypt(X0_\$i,X1_\$i))
| ~ intruder_message(X1_\$i)
| ~ intruder_message(X0_\$i)
| sP0_iProver_split ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_95]) ).

cnf(c_204,plain,
( intruder_message(encrypt(X0_\$\$iProver_fresh_intruder_nonce_1_\$i,X1_\$\$iProver_fresh_intruder_nonce_1_\$i))
| ~ intruder_message(X1_\$\$iProver_fresh_intruder_nonce_1_\$i)
| ~ intruder_message(X0_\$\$iProver_fresh_intruder_nonce_1_\$i)
| sP0_iProver_split ),
inference(subtyping,[status(esa)],[c_169]) ).

cnf(c_34,plain,
( fresh_intruder_nonce(an_intruder_nonce) ),
inference(cnf_transformation,[],[f103]) ).

cnf(c_210,plain,
( fresh_intruder_nonce(an_intruder_nonce) ),
inference(subtyping,[status(esa)],[c_34]) ).

cnf(c_28,plain,
( a_nonce(an_a_nonce) ),
inference(cnf_transformation,[],[f97]) ).

cnf(c_214,plain,
( a_nonce(an_a_nonce) ),
inference(subtyping,[status(esa)],[c_28]) ).

cnf(c_9,plain,
( party_of_protocol(t) ),
inference(cnf_transformation,[],[f78]) ).

cnf(c_230,plain,
( party_of_protocol(t) ),
inference(subtyping,[status(esa)],[c_9]) ).

cnf(c_8,plain,
( t_holds(key(bt,b)) ),
inference(cnf_transformation,[],[f77]) ).

cnf(c_231,plain,
( t_holds(key(bt,b)) ),
inference(subtyping,[status(esa)],[c_8]) ).

cnf(c_7,plain,
( t_holds(key(at,a)) ),
inference(cnf_transformation,[],[f76]) ).

cnf(c_232,plain,
( t_holds(key(at,a)) ),
inference(subtyping,[status(esa)],[c_7]) ).

cnf(c_5,plain,
( fresh_to_b(an_a_nonce) ),
inference(cnf_transformation,[],[f74]) ).

cnf(c_234,plain,
( fresh_to_b(an_a_nonce) ),
inference(subtyping,[status(esa)],[c_5]) ).

cnf(c_4,plain,
( party_of_protocol(b) ),
inference(cnf_transformation,[],[f73]) ).

cnf(c_235,plain,
( party_of_protocol(b) ),
inference(subtyping,[status(esa)],[c_4]) ).

cnf(c_1,plain,
( message(sent(a,b,pair(a,an_a_nonce))) ),
inference(cnf_transformation,[],[f70]) ).

cnf(c_236,plain,
( message(sent(a,b,pair(a,an_a_nonce))) ),
inference(subtyping,[status(esa)],[c_1]) ).

cnf(c_0,plain,
( party_of_protocol(a) ),
inference(cnf_transformation,[],[f69]) ).

cnf(c_237,plain,
( party_of_protocol(a) ),
inference(subtyping,[status(esa)],[c_0]) ).

% SZS output end Saturation
```

Prover9 2009-11A

William McCune, Bob Veroff
University of New Mexico, USA

Sample solution for SEU140+2

```8 (all A all B (subset(A,B) <-> (all C (in(C,A) -> in(C,B))))) # label(d3_tarski) # label(axiom) # label(non_clause).  [assumption].
26 (all A all B (disjoint(A,B) -> disjoint(B,A))) # label(symmetry_r1_xboole_0) # label(axiom) # label(non_clause).  [assumption].
42 (all A all B (-(-disjoint(A,B) & (all C -(in(C,A) & in(C,B)))) & -((exists C (in(C,A) & in(C,B))) & disjoint(A,B)))) # label(t3_xboole_0) # label(lemma) # label(non_clause).  [assumption].
55 -(all A all B all C (subset(A,B) & disjoint(B,C) -> disjoint(A,C))) # label(t63_xboole_1) # label(negated_conjecture) # label(non_clause).  [assumption].
60 subset(c3,c4) # label(t63_xboole_1) # label(negated_conjecture).  [clausify(55)].
61 disjoint(c4,c5) # label(t63_xboole_1) # label(negated_conjecture).  [clausify(55)].
75 disjoint(A,B) | in(f7(A,B),A) # label(t3_xboole_0) # label(lemma).  [clausify(42)].
76 disjoint(A,B) | in(f7(A,B),B) # label(t3_xboole_0) # label(lemma).  [clausify(42)].
92 -disjoint(c3,c5) # label(t63_xboole_1) # label(negated_conjecture).  [clausify(55)].
101 -in(A,B) | -in(A,C) | -disjoint(B,C) # label(t3_xboole_0) # label(lemma).  [clausify(42)].
109 -disjoint(A,B) | disjoint(B,A) # label(symmetry_r1_xboole_0) # label(axiom).  [clausify(26)].
123 -subset(A,B) | -in(C,A) | in(C,B) # label(d3_tarski) # label(axiom).  [clausify(8)].
273 -disjoint(c5,c3).  [ur(109,b,92,a)].
300 -in(A,c3) | in(A,c4).  [resolve(123,a,60,a)].
959 in(f7(c5,c3),c3).  [resolve(273,a,76,a)].
960 in(f7(c5,c3),c5).  [resolve(273,a,75,a)].
1084 -in(f7(c5,c3),c4).  [ur(101,b,960,a,c,61,a)].
1292 \$F.  [resolve(300,a,959,a),unit_del(a,1084)].
```

Satallax 3.2

Michael Färber
Universität Innsbruck, Austria

Sample solution for SET014^4

```% SZS output start Proof
thf(ty_\$i, type, \$i : \$tType).
thf(ty_eigen__2, type, eigen__2 : (\$i>\$o)).
thf(ty_eigen__1, type, eigen__1 : (\$i>\$o)).
thf(ty_eigen__0, type, eigen__0 : (\$i>\$o)).
thf(ty_eigen__3, type, eigen__3 : \$i).
thf(sP1,plain,(sP1 <=> (eigen__0 @ eigen__3),introduced(definition,[new_symbols(
definition,[sP1])]))).
thf(sP2,plain,(sP2 <=> (sP1 => (eigen__2 @ eigen__3)),introduced(definition,[new
_symbols(definition,[sP2])]))).
thf(sP3,plain,(sP3 <=> (eigen__1 @ eigen__3),introduced(definition,[new_symbols(
definition,[sP3])]))).
thf(sP4,plain,(sP4 <=> (sP3 => (eigen__2 @ eigen__3)),introduced(definition,[new
_symbols(definition,[sP4])]))).
thf(sP5,plain,(sP5 <=> (![X1:\$i]:((eigen__1 @ X1) => (eigen__2 @ X1))),introduce
d(definition,[new_symbols(definition,[sP5])]))).
thf(sP6,plain,(sP6 <=> (eigen__2 @ eigen__3),introduced(definition,[new_symbols(
definition,[sP6])]))).
thf(sP7,plain,(sP7 <=> (![X1:\$i]:((eigen__0 @ X1) => (eigen__2 @ X1))),introduce
d(definition,[new_symbols(definition,[sP7])]))).
thf(def_in,definition,(in = (^[X1:\$i]:(^[X2:\$i>\$o]:(X2 @ X1))))).
thf(def_is_a,definition,(is_a = (^[X1:\$i]:(^[X2:\$i>\$o]:(X2 @ X1))))).
thf(def_emptyset,definition,(emptyset = (^[X1:\$i]:\$false))).
thf(def_unord_pair,definition,(unord_pair = (^[X1:\$i]:(^[X2:\$i]:(^[X3:\$i]:((~((X
3 = X1))) => (X3 = X2))))))).
thf(def_singleton,definition,(singleton = (^[X1:\$i]:(^[X2:\$i]:(X2 = X1))))).
thf(def_union,definition,(union = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(^[X3:\$i]:((~((X1 @
X3))) => (X2 @ X3))))))).
thf(def_excl_union,definition,(excl_union = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(^[X3:\$i]:
(((X1 @ X3) => (X2 @ X3)) => (~(((~((X1 @ X3))) => (~((X2 @ X3)))))))))))).
thf(def_intersection,definition,(intersection = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(^[X3:
\$i]:(~(((X1 @ X3) => (~((X2 @ X3))))))))))).
thf(def_setminus,definition,(setminus = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(^[X3:\$i]:(~((
(X1 @ X3) => (X2 @ X3))))))))).
thf(def_complement,definition,(complement = (^[X1:\$i>\$o]:(^[X2:\$i]:(~((X1 @ X2))
))))).
thf(def_disjoint,definition,(disjoint = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(((intersectio
n @ X1) @ X2) = emptyset))))).
thf(def_subset,definition,(subset = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(![X3:\$i]:((X1 @ X
3) => (X2 @ X3))))))).
thf(def_meets,definition,(meets = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(~((![X3:\$i]:((X1 @
X3) => (~((X2 @ X3))))))))))).
thf(def_misses,definition,(misses = (^[X1:\$i>\$o]:(^[X2:\$i>\$o]:(![X3:\$i]:((X1 @ X
3) => (~((X2 @ X3))))))))).
thf(thm,conjecture,(![X1:\$i>\$o]:(![X2:\$i>\$o]:(![X3:\$i>\$o]:((~(((![X4:\$i]:((X1 @
X4) => (X3 @ X4))) => (~((![X4:\$i]:((X2 @ X4) => (X3 @ X4)))))))) => (![X4:\$i]:(
((~((X1 @ X4))) => (X2 @ X4)) => (X3 @ X4)))))))).
thf(h0,negated_conjecture,(~((![X1:\$i>\$o]:(![X2:\$i>\$o]:(![X3:\$i>\$o]:((~(((![X4:\$
i]:((X1 @ X4) => (X3 @ X4))) => (~((![X4:\$i]:((X2 @ X4) => (X3 @ X4)))))))) => (
![X4:\$i]:(((~((X1 @ X4))) => (X2 @ X4)) => (X3 @ X4))))))))),inference(assume_ne
gation,[status(cth)],[thm])).
thf(h1,assumption,(~((![X1:\$i>\$o]:(![X2:\$i>\$o]:((~(((![X3:\$i]:((eigen__0 @ X3) =
> (X2 @ X3))) => (~((![X3:\$i]:((X1 @ X3) => (X2 @ X3)))))))) => (![X3:\$i]:(((~((
eigen__0 @ X3))) => (X1 @ X3)) => (X2 @ X3)))))))),introduced(assumption,[])).
thf(h2,assumption,(~((![X1:\$i>\$o]:((~(((![X2:\$i]:((eigen__0 @ X2) => (X1 @ X2)))
=> (~((![X2:\$i]:((eigen__1 @ X2) => (X1 @ X2)))))))) => (![X2:\$i]:(((~((eigen__
0 @ X2))) => (eigen__1 @ X2)) => (X1 @ X2))))))),introduced(assumption,[])).
thf(h3,assumption,(~(((~((sP7 => (~(sP5))))) => (![X1:\$i]:(((~((eigen__0 @ X1)))
=> (eigen__1 @ X1)) => (eigen__2 @ X1)))))),introduced(assumption,[])).
thf(h4,assumption,(~((sP7 => (~(sP5))))),introduced(assumption,[])).
thf(h5,assumption,(~((![X1:\$i]:(((~((eigen__0 @ X1))) => (eigen__1 @ X1)) => (ei
gen__2 @ X1))))),introduced(assumption,[])).
thf(h6,assumption,sP7,introduced(assumption,[])).
thf(h7,assumption,sP5,introduced(assumption,[])).
thf(h8,assumption,(~((((~(sP1)) => sP3) => sP6))),introduced(assumption,[])).
thf(h9,assumption,((~(sP1)) => sP3),introduced(assumption,[])).
thf(h10,assumption,(~(sP6)),introduced(assumption,[])).
thf(h11,assumption,sP1,introduced(assumption,[])).
thf(h12,assumption,sP3,introduced(assumption,[])).
thf(1,plain,((~(sP2) | ~(sP1)) | sP6),inference(prop_rule,[status(thm)],[])).
thf(2,plain,(~(sP7) | sP2),inference(all_rule,[status(thm)],[])).
thf(3,plain,\$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h10,h8,
h6,h7,h4,h5,h3,h2,h1,h0])],[h10,h11,h6,1,2])).
thf(4,plain,((~(sP4) | ~(sP3)) | sP6),inference(prop_rule,[status(thm)],[])).
thf(5,plain,(~(sP5) | sP4),inference(all_rule,[status(thm)],[])).
thf(6,plain,\$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h10,h8,
h6,h7,h4,h5,h3,h2,h1,h0])],[h10,h12,h7,4,5])).
thf(7,plain,\$false,inference(tab_imp,[status(thm),assumptions([h9,h10,h8,h6,h7,h
4,h5,h3,h2,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,3,6,h1
1,h12])).
thf(8,plain,\$false,inference(tab_negimp,[status(thm),assumptions([h8,h6,h7,h4,h5
,h3,h2,h1,h0]),tab_negimp(discharge,[h9,h10])],[h8,7,h9,h10])).
thf(9,plain,\$false,inference(tab_negall,[status(thm),assumptions([h6,h7,h4,h5,h3
,h2,h1,h0]),tab_negall(discharge,[h8]),tab_negall(eigenvar,eigen__3)],[h5,8,h8])
).
thf(10,plain,\$false,inference(tab_negimp,[status(thm),assumptions([h4,h5,h3,h2,h
1,h0]),tab_negimp(discharge,[h6,h7])],[h4,9,h6,h7])).
thf(11,plain,\$false,inference(tab_negimp,[status(thm),assumptions([h3,h2,h1,h0])
,tab_negimp(discharge,[h4,h5])],[h3,10,h4,h5])).
thf(12,plain,\$false,inference(tab_negall,[status(thm),assumptions([h2,h1,h0]),ta
b_negall(discharge,[h3]),tab_negall(eigenvar,eigen__2)],[h2,11,h3])).
thf(13,plain,\$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_n
egall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,12,h2])).
thf(14,plain,\$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_nega
ll(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,13,h1])).
% SZS output end Proof
```

Sample solution for SYO553^1

```% SZS output start Proof
thf(ty_\$i, type, \$i : \$tType).
thf(ty_eigen__2, type, eigen__2 : \$i).
thf(h0, assumption, (![X1:\$i>\$o]:(![X2:\$i]:((X1 @ X2) => (X1 @ (eps__0 @ X1)))))
,introduced(assumption,[])).
thf(eigendef_eigen__1, definition, (eigen__1 = (eps__0 @ (^[X1:\$i]:(~((![X2:\$i]:
(X2 = X2))))))), introduced(definition,[new_symbols(definition,[eigen__1]))).
thf(eigendef_eigen__2, definition, (eigen__2 = (eps__0 @ (^[X1:\$i]:(~((X1 = X1))
)))), introduced(definition,[new_symbols(definition,[eigen__2]))).
thf(sP1,plain,(sP1 <=> (![X1:\$i]:(![X2:\$i]:(X2 = X2))),introduced(definition,[ne
w_symbols(definition,[sP1])]))).
thf(sP2,plain,(sP2 <=> (![X1:\$i]:(X1 = X1)),introduced(definition,[new_symbols(d
efinition,[sP2])]))).
thf(sP3,plain,(sP3 <=> (![X1:\$i>\$i>\$i]:(~((![X2:\$i]:(![X3:\$i]:(((X1 @ X2) @ X3)
= X3)))))),introduced(definition,[new_symbols(definition,[sP3])]))).
thf(sP4,plain,(sP4 <=> (eigen__2 = eigen__2),introduced(definition,[new_symbols(
definition,[sP4])]))).
thf(claim,conjecture,(~(sP3))).
thf(h1,negated_conjecture,sP3,inference(assume_negation,[status(cth)],[claim])).
thf(1,plain,(~(sP3) | ~(sP1)),inference(all_rule,[status(thm)],[])).
thf(2,plain,(sP1 | ~(sP2)),inference(eigen_choice_rule,[status(thm),assumptions(
[h0])],[h0,eigendef_eigen__1])).
thf(3,plain,(sP2 | ~(sP4)),inference(eigen_choice_rule,[status(thm),assumptions(
[h0])],[h0,eigendef_eigen__2])).
thf(4,plain,sP4,inference(prop_rule,[status(thm)],[])).
thf(5,plain,\$false,inference(prop_unsat,[status(thm),assumptions([h1,h0])],[h1,1
,2,3,4])).
thf(6,plain,\$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eige
nvar_choice(discharge,[h0])],[5,h0])).
% SZS output end Proof
```

Vampire 4.0

Giles Reger
University of Manchester, United Kingdom

Sample solution for SEU140+2

```% SZS status Theorem for SEU140+2
% SZS output start Proof for SEU140+2
fof(f6,axiom,(
! [X0] : (empty_set = X0 <=> ! [X1] : ~in(X1,X0))),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',d1_xboole_0)).
fof(f8,axiom,(
! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (in(X2,X0) => in(X2,X1)))),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',d3_tarski)).
fof(f9,axiom,(
! [X0,X1,X2] : (set_intersection2(X0,X1) = X2 <=> ! [X3] : (in(X3,X2) <=> (in(X3,X0) & in(X3,X1))))),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',d3_xboole_0)).
fof(f11,axiom,(
! [X0,X1] : (disjoint(X0,X1) <=> set_intersection2(X0,X1) = empty_set)),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',d7_xboole_0)).
fof(f43,axiom,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X2] : ~(in(X2,X0) & in(X2,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',t3_xboole_0)).
fof(f51,conjecture,(
! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
file('/tmp/SystemOnTPTP11775/SEU140+2.tptp',t63_xboole_1)).
fof(f52,negated_conjecture,(
~! [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) => disjoint(X0,X2))),
inference(negated_conjecture,[],[f51])).
fof(f60,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(rectify,[],[f43])).
fof(f61,plain,(
! [X0,X1] : (~(~disjoint(X0,X1) & ! [X3] : ~(in(X3,X0) & in(X3,X1))) & ~(? [X2] : (in(X2,X0) & in(X2,X1)) & disjoint(X0,X1)))),
inference(flattening,[],[f60])).
fof(f63,plain,(
! [X0] : (empty_set = X0 <=> ! [X1] : ~in(X1,X0))),
inference(flattening,[],[f6])).
fof(f74,plain,(
? [X0,X1,X2] : ((subset(X0,X1) & disjoint(X1,X2)) & ~disjoint(X0,X2))),
inference(ennf_transformation,[],[f52])).
fof(f75,plain,(
? [X0,X1,X2] : (subset(X0,X1) & disjoint(X1,X2) & ~disjoint(X0,X2))),
inference(flattening,[],[f74])).
fof(f78,plain,(
! [X0,X1] : ((disjoint(X0,X1) | ? [X3] : (in(X3,X0) & in(X3,X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(ennf_transformation,[],[f61])).
fof(f96,plain,(
! [X0,X1] : (subset(X0,X1) <=> ! [X2] : (~in(X2,X0) | in(X2,X1)))),
inference(ennf_transformation,[],[f8])).
fof(f101,plain,(
subset(sK0,sK1) & disjoint(sK1,sK2) & ~disjoint(sK0,sK2)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f75])).
fof(f103,plain,(
! [X0,X1] : ((disjoint(X0,X1) | (in(sK4(X1,X0),X0) & in(sK4(X1,X0),X1))) & (! [X2] : (~in(X2,X0) | ~in(X2,X1)) | ~disjoint(X0,X1)))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK4])],[f78])).
fof(f106,plain,(
! [X0,X1] : ((~disjoint(X0,X1) | set_intersection2(X0,X1) = empty_set) & (set_intersection2(X0,X1) != empty_set | disjoint(X0,X1)))),
inference(nnf_transformation,[],[f11])).
fof(f109,plain,(
! [X0] : ((empty_set != X0 | ! [X1] : ~in(X1,X0)) & (? [X1] : in(X1,X0) | empty_set = X0))),
inference(nnf_transformation,[],[f63])).
fof(f110,plain,(
! [X0] : ((empty_set != X0 | ! [X2] : ~in(X2,X0)) & (? [X1] : in(X1,X0) | empty_set = X0))),
inference(rectify,[],[f109])).
fof(f111,plain,(
! [X0] : ((empty_set != X0 | ! [X2] : ~in(X2,X0)) & (in(sK5(X0),X0) | empty_set = X0))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK5])],[f110])).
fof(f116,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & ((~in(X3,X0) | ~in(X3,X1)) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | (~in(X3,X0) | ~in(X3,X1)))) | set_intersection2(X0,X1) = X2))),
inference(nnf_transformation,[],[f9])).
fof(f117,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X3] : ((~in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X0) | ~in(X3,X1) | in(X3,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))),
inference(flattening,[],[f116])).
fof(f118,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (? [X3] : ((in(X3,X2) | (in(X3,X0) & in(X3,X1))) & (~in(X3,X2) | ~in(X3,X0) | ~in(X3,X1))) | set_intersection2(X0,X1) = X2))),
inference(rectify,[],[f117])).
fof(f119,plain,(
! [X0,X1,X2] : ((set_intersection2(X0,X1) != X2 | ! [X4] : ((~in(X4,X2) | (in(X4,X0) & in(X4,X1))) & (~in(X4,X0) | ~in(X4,X1) | in(X4,X2)))) & (((in(sK7(X2,X1,X0),X2) | (in(sK7(X2,X1,X0),X0) & in(sK7(X2,X1,X0),X1))) & (~in(sK7(X2,X1,X0),X2) | ~in(sK7(X2,X1,X0),X0) | ~in(sK7(X2,X1,X0),X1))) | set_intersection2(X0,X1) = X2))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK7])],[f118])).
fof(f124,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X2] : (~in(X2,X0) | in(X2,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))),
inference(nnf_transformation,[],[f96])).
fof(f125,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & (? [X2] : (in(X2,X0) & ~in(X2,X1)) | subset(X0,X1)))),
inference(rectify,[],[f124])).
fof(f126,plain,(
! [X0,X1] : ((~subset(X0,X1) | ! [X3] : (~in(X3,X0) | in(X3,X1))) & ((in(sK9(X1,X0),X0) & ~in(sK9(X1,X0),X1)) | subset(X0,X1)))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK9])],[f125])).
fof(f133,plain,(
subset(sK0,sK1)),
inference(cnf_transformation,[],[f101])).
fof(f134,plain,(
disjoint(sK1,sK2)),
inference(cnf_transformation,[],[f101])).
fof(f135,plain,(
~disjoint(sK0,sK2)),
inference(cnf_transformation,[],[f101])).
fof(f146,plain,(
( ! [X0,X1] : (in(sK4(X1,X0),X0) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f103])).
fof(f147,plain,(
( ! [X0,X1] : (in(sK4(X1,X0),X1) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f103])).
fof(f162,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = empty_set | ~disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f106])).
fof(f169,plain,(
( ! [X2,X0] : (~in(X2,X0) | empty_set != X0) )),
inference(cnf_transformation,[],[f111])).
fof(f189,plain,(
( ! [X4,X2,X0,X1] : (in(X4,X2) | ~in(X4,X1) | ~in(X4,X0) | set_intersection2(X0,X1) != X2) )),
inference(cnf_transformation,[],[f119])).
fof(f202,plain,(
( ! [X0,X3,X1] : (~subset(X0,X1) | ~in(X3,X0) | in(X3,X1)) )),
inference(cnf_transformation,[],[f126])).
fof(f218,plain,(
( ! [X2] : (~in(X2,empty_set)) )),
inference(equality_resolution,[],[f169])).
fof(f222,plain,(
( ! [X4,X0,X1] : (in(X4,set_intersection2(X0,X1)) | ~in(X4,X1) | ~in(X4,X0)) )),
inference(equality_resolution,[],[f189])).
fof(f234,plain,(
set_intersection2(sK1,sK2) = empty_set),
inference(unit_resulting_resolution,[],[f134,f162])).
fof(f467,plain,(
in(sK4(sK2,sK0),sK0)),
inference(unit_resulting_resolution,[],[f135,f146])).
fof(f480,plain,(
in(sK4(sK2,sK0),sK1)),
inference(unit_resulting_resolution,[],[f133,f467,f202])).
fof(f513,plain,(
in(sK4(sK2,sK0),sK2)),
inference(unit_resulting_resolution,[],[f135,f147])).
fof(f857,plain,(
in(sK4(sK2,sK0),set_intersection2(sK1,sK2))),
inference(unit_resulting_resolution,[],[f513,f480,f222])).
fof(f865,plain,(
in(sK4(sK2,sK0),empty_set)),
inference(forward_demodulation,[],[f857,f234])).
fof(f866,plain,(
\$false),
inference(subsumption_resolution,[],[f865,f218])).
% SZS output end Proof for SEU140+2
```

Vampire 4.1

Giles Reger
University of Manchester, United Kingdom

Sample solution for DAT013=1

```tff(type_def_6, type, array: \$tType).
tff(func_def_0, type, read: (array * \$int) > \$int).
tff(func_def_1, type, write: (array * \$int * \$int) > array).
tff(func_def_7, type, sK0: array).
tff(func_def_8, type, sK1: \$int).
tff(func_def_9, type, sK2: \$int).
tff(func_def_10, type, sK3: \$int).
tff(f3,conjecture,(
! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((\$lesseq(X3,X2) & \$lesseq(X1,X3)) => \$greater(read(X0,X3),0)) => ! [X4 : \$int] : ((\$lesseq(X4,X2) & \$lesseq(\$sum(X1,3),X4)) => \$greater(read(X0,X4),0)))),
file('/Users/giles/TPTP/TPTP-v6.2.0/Problems/DAT/DAT013=1.p',unknown)).
tff(f4,negated_conjecture,(
~! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((\$lesseq(X3,X2) & \$lesseq(X1,X3)) => \$greater(read(X0,X3),0)) => ! [X4 : \$int] : ((\$lesseq(X4,X2) & \$lesseq(\$sum(X1,3),X4)) => \$greater(read(X0,X4),0)))),
inference(negated_conjecture,[],[f3])).
tff(f6,plain,(
~! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((~\$less(X2,X3) & ~\$less(X3,X1)) => \$less(0,read(X0,X3))) => ! [X4 : \$int] : ((~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3))) => \$less(0,read(X0,X4))))),
inference(evaluation,[],[f4])).
tff(f7,plain,(
( ! [X0:\$int,X1:\$int] : (\$sum(X0,X1) = \$sum(X1,X0)) )),
introduced(theory_axiom,[])).
tff(f9,plain,(
( ! [X0:\$int] : (\$sum(X0,0) = X0) )),
introduced(theory_axiom,[])).
tff(f12,plain,(
( ! [X0:\$int] : (~\$less(X0,X0)) )),
introduced(theory_axiom,[])).
tff(f13,plain,(
( ! [X2:\$int,X0:\$int,X1:\$int] : (~\$less(X1,X2) | ~\$less(X0,X1) | \$less(X0,X2)) )),
introduced(theory_axiom,[])).
tff(f14,plain,(
( ! [X0:\$int,X1:\$int] : (\$less(X1,X0) | \$less(X0,X1) | X0 = X1) )),
introduced(theory_axiom,[])).
tff(f15,plain,(
( ! [X2:\$int,X0:\$int,X1:\$int] : (\$less(\$sum(X0,X2),\$sum(X1,X2)) | ~\$less(X0,X1)) )),
introduced(theory_axiom,[])).
tff(f20,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X4 : \$int] : (~\$less(0,read(X0,X4)) & (~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3)))) & ! [X3 : \$int] : (\$less(0,read(X0,X3)) | (\$less(X2,X3) | \$less(X3,X1))))),
inference(ennf_transformation,[],[f6])).
tff(f21,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X4 : \$int] : (~\$less(0,read(X0,X4)) & ~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3))) & ! [X3 : \$int] : (\$less(0,read(X0,X3)) | \$less(X2,X3) | \$less(X3,X1)))),
inference(flattening,[],[f20])).
tff(f22,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) & ! [X4 : \$int] : (\$less(0,read(X0,X4)) | \$less(X2,X4) | \$less(X4,X1)))),
inference(rectify,[],[f21])).
tff(f23,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) & ! [X4 : \$int] : (\$less(0,read(X0,X4)) | \$less(X2,X4) | \$less(X4,X1))) => (? [X3 : \$int] : (~\$less(0,read(sK0,X3)) & ~\$less(sK2,X3) & ~\$less(X3,\$sum(sK1,3))) & ! [X4 : \$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1)))),
introduced(choice_axiom,[])).
tff(f24,plain,(
( ! [X2:\$int,X0:array,X1:\$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) => (~\$less(0,read(X0,sK3)) & ~\$less(X2,sK3) & ~\$less(sK3,\$sum(X1,3)))) )),
introduced(choice_axiom,[])).
tff(f25,plain,(
(~\$less(0,read(sK0,sK3)) & ~\$less(sK2,sK3) & ~\$less(sK3,\$sum(sK1,3))) & ! [X4 : \$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f22,f24,f23])).
tff(f29,plain,(
( ! [X4:\$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1)) )),
inference(cnf_transformation,[],[f25])).
tff(f30,plain,(
~\$less(sK3,\$sum(sK1,3))),
inference(cnf_transformation,[],[f25])).
tff(f31,plain,(
~\$less(sK2,sK3)),
inference(cnf_transformation,[],[f25])).
tff(f32,plain,(
inference(cnf_transformation,[],[f25])).
tff(f33,plain,(
~\$less(sK3,\$sum(3,sK1))),
inference(forward_demodulation,[],[f30,f7])).
tff(f98,plain,(
\$less(\$sum(3,sK1),sK3) | \$sum(3,sK1) = sK3),
inference(resolution,[],[f14,f33])).
tff(f131,plain,(
spl4_8 <=> \$sum(3,sK1) = sK3),
introduced(AVATAR_definition,[new_symbols(naming,[spl4_8])])).
tff(f132,plain,(
\$sum(3,sK1) = sK3 | ~spl4_8),
inference(AVATAR_component_clause,[],[f131])).
tff(f137,plain,(
spl4_10 <=> \$less(\$sum(3,sK1),sK3)),
introduced(AVATAR_definition,[new_symbols(naming,[spl4_10])])).
tff(f138,plain,(
\$less(\$sum(3,sK1),sK3) | ~spl4_10),
inference(AVATAR_component_clause,[],[f137])).
tff(f142,plain,(
spl4_8 | spl4_10),
inference(AVATAR_split_clause,[],[f98,f137,f131])).
tff(f172,plain,(
( ! [X6:\$int,X4:\$int,X5:\$int] : (\$less(\$sum(X5,X4),\$sum(X6,X5)) | ~\$less(X4,X6)) )),
inference(superposition,[],[f15,f7])).
tff(f489,plain,(
( ! [X6:\$int,X7:\$int] : (\$less(X6,\$sum(X7,X6)) | ~\$less(0,X7)) )),
inference(superposition,[],[f172,f9])).
tff(f659,plain,(
\$less(sK2,sK3) | \$less(sK3,sK1)),
inference(resolution,[],[f29,f32])).
tff(f662,plain,(
\$less(sK3,sK1)),
inference(subsumption_resolution,[],[f659,f31])).
tff(f664,plain,(
( ! [X0:\$int] : (~\$less(X0,sK3) | \$less(X0,sK1)) )),
inference(resolution,[],[f662,f13])).
tff(f673,plain,(
( ! [X4:\$int] : (\$less(\$sum(sK1,X4),sK3) | ~\$less(X4,3)) ) | ~spl4_8),
inference(superposition,[],[f172,f132])).
tff(f2473,plain,(
\$less(sK1,sK3) | ~\$less(0,3) | ~spl4_8),
inference(superposition,[],[f673,f9])).
tff(f2478,plain,(
\$less(sK1,sK3) | ~spl4_8),
inference(evaluation,[],[f2473])).
tff(f2480,plain,(
\$less(sK1,sK1) | ~spl4_8),
inference(resolution,[],[f2478,f664])).
tff(f2484,plain,(
\$false | ~spl4_8),
inference(subsumption_resolution,[],[f2480,f12])).
tff(f2485,plain,(
~spl4_8),
tff(f2513,plain,(
( ! [X2:\$int] : (~\$less(X2,\$sum(3,sK1)) | \$less(X2,sK3)) ) | ~spl4_10),
inference(resolution,[],[f138,f13])).
tff(f2962,plain,(
~\$less(0,3) | \$less(sK1,sK3) | ~spl4_10),
inference(resolution,[],[f489,f2513])).
tff(f2989,plain,(
\$less(sK1,sK3) | ~spl4_10),
inference(evaluation,[],[f2962])).
tff(f2991,plain,(
\$less(sK1,sK1) | ~spl4_10),
inference(resolution,[],[f2989,f664])).
tff(f2995,plain,(
\$false | ~spl4_10),
inference(subsumption_resolution,[],[f2991,f12])).
tff(f2996,plain,(
~spl4_10),
tff(f2997,plain,(
\$false),
inference(AVATAR_sat_refutation,[],[f142,f2485,f2996])).
```

Sample solution for NLP042+1

```# SZS output start Saturation.
tff(u283,axiom,
(![X1, X0] : ((~woman(X0,X1) | human_person(X0,X1))))).

tff(u282,axiom,
(![X1, X0] : ((~woman(X0,X1) | female(X0,X1))))).

tff(u281,negated_conjecture,
woman(sK0,sK1)).

tff(u280,negated_conjecture,
~female(sK0,sK4)).

tff(u279,negated_conjecture,
~female(sK0,sK2)).

tff(u278,negated_conjecture,
~female(sK0,sK3)).

tff(u277,negated_conjecture,
female(sK0,sK1)).

tff(u276,axiom,
(![X1, X0] : ((~human_person(X0,X1) | organism(X0,X1))))).

tff(u275,axiom,
(![X1, X0] : ((~human_person(X0,X1) | human(X0,X1))))).

tff(u274,axiom,
(![X1, X0] : ((~human_person(X0,X1) | animate(X0,X1))))).

tff(u273,negated_conjecture,
human_person(sK0,sK1)).

tff(u272,negated_conjecture,
~animate(sK0,sK3)).

tff(u271,negated_conjecture,
animate(sK0,sK1)).

tff(u270,negated_conjecture,
~human(sK0,sK2)).

tff(u269,negated_conjecture,
human(sK0,sK1)).

tff(u268,axiom,
(![X1, X0] : ((~organism(X0,X1) | entity(X0,X1))))).

tff(u267,axiom,
(![X1, X0] : ((~organism(X0,X1) | living(X0,X1))))).

tff(u266,negated_conjecture,
organism(sK0,sK1)).

tff(u265,negated_conjecture,
~living(sK0,sK3)).

tff(u264,negated_conjecture,
living(sK0,sK1)).

tff(u263,axiom,
(![X1, X0] : ((~entity(X0,X1) | specific(X0,X1))))).

tff(u262,axiom,
(![X1, X0] : ((~entity(X0,X1) | existent(X0,X1))))).

tff(u261,negated_conjecture,
entity(sK0,sK1)).

tff(u260,negated_conjecture,
entity(sK0,sK3)).

tff(u259,axiom,
(![X1, X0] : ((~mia_forename(X0,X1) | forename(X0,X1))))).

tff(u258,negated_conjecture,
mia_forename(sK0,sK2)).

tff(u257,axiom,
(![X1, X0] : ((~forename(X0,X1) | relname(X0,X1))))).

tff(u256,negated_conjecture,
forename(sK0,sK2)).

tff(u255,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | nonhuman(X0,X1))))).

tff(u254,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | general(X0,X1))))).

tff(u253,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | unisex(X0,X1))))).

tff(u252,negated_conjecture,
abstraction(sK0,sK2)).

tff(u251,axiom,
(![X1, X0] : ((~unisex(X0,X1) | ~female(X0,X1))))).

tff(u250,negated_conjecture,
unisex(sK0,sK2)).

tff(u249,negated_conjecture,
unisex(sK0,sK4)).

tff(u248,negated_conjecture,
unisex(sK0,sK3)).

tff(u247,negated_conjecture,
~general(sK0,sK4)).

tff(u246,negated_conjecture,
~general(sK0,sK1)).

tff(u245,negated_conjecture,
~general(sK0,sK3)).

tff(u244,negated_conjecture,
general(sK0,sK2)).

tff(u243,axiom,
(![X1, X0] : ((~nonhuman(X0,X1) | ~human(X0,X1))))).

tff(u242,negated_conjecture,
nonhuman(sK0,sK2)).

tff(u241,axiom,
(![X1, X0] : ((~relation(X0,X1) | abstraction(X0,X1))))).

tff(u240,negated_conjecture,
relation(sK0,sK2)).

tff(u239,axiom,
(![X1, X0] : ((~relname(X0,X1) | relation(X0,X1))))).

tff(u238,negated_conjecture,
relname(sK0,sK2)).

tff(u237,axiom,
(![X1, X0] : ((~object(X0,X1) | entity(X0,X1))))).

tff(u236,axiom,
(![X1, X0] : ((~object(X0,X1) | nonliving(X0,X1))))).

tff(u235,axiom,
(![X1, X0] : ((~object(X0,X1) | unisex(X0,X1))))).

tff(u234,negated_conjecture,
object(sK0,sK3)).

tff(u233,axiom,
(![X1, X0] : ((~nonliving(X0,X1) | ~living(X0,X1))))).

tff(u232,axiom,
(![X1, X0] : ((~nonliving(X0,X1) | ~animate(X0,X1))))).

tff(u231,negated_conjecture,
nonliving(sK0,sK3)).

tff(u230,negated_conjecture,
~existent(sK0,sK4)).

tff(u229,negated_conjecture,
existent(sK0,sK1)).

tff(u228,negated_conjecture,
existent(sK0,sK3)).

tff(u227,axiom,
(![X1, X0] : ((~specific(X0,X1) | ~general(X0,X1))))).

tff(u226,negated_conjecture,
specific(sK0,sK1)).

tff(u225,negated_conjecture,
specific(sK0,sK4)).

tff(u224,negated_conjecture,
specific(sK0,sK3)).

tff(u223,axiom,
(![X1, X0] : ((~substance_matter(X0,X1) | object(X0,X1))))).

tff(u222,negated_conjecture,
substance_matter(sK0,sK3)).

tff(u221,axiom,
(![X1, X0] : ((~food(X0,X1) | substance_matter(X0,X1))))).

tff(u220,negated_conjecture,
food(sK0,sK3)).

tff(u219,axiom,
(![X1, X0] : ((~beverage(X0,X1) | food(X0,X1))))).

tff(u218,negated_conjecture,
beverage(sK0,sK3)).

tff(u217,axiom,
(![X1, X0] : ((~shake_beverage(X0,X1) | beverage(X0,X1))))).

tff(u216,negated_conjecture,
shake_beverage(sK0,sK3)).

tff(u215,axiom,
(![X1, X0] : ((~order(X0,X1) | act(X0,X1))))).

tff(u214,axiom,
(![X1, X0] : ((~order(X0,X1) | event(X0,X1))))).

tff(u213,negated_conjecture,
order(sK0,sK4)).

tff(u212,axiom,
(![X1, X0] : ((~event(X0,X1) | eventuality(X0,X1))))).

tff(u211,negated_conjecture,
event(sK0,sK4)).

tff(u210,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | specific(X0,X1))))).

tff(u209,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | nonexistent(X0,X1))))).

tff(u208,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | unisex(X0,X1))))).

tff(u207,negated_conjecture,
eventuality(sK0,sK4)).

tff(u206,axiom,
(![X1, X0] : ((~nonexistent(X0,X1) | ~existent(X0,X1))))).

tff(u205,negated_conjecture,
nonexistent(sK0,sK4)).

tff(u204,axiom,
(![X1, X0] : ((~act(X0,X1) | event(X0,X1))))).

tff(u203,negated_conjecture,
act(sK0,sK4)).

tff(u202,axiom,
(![X1, X3, X0, X2] : ((~of(X0,X3,X1) | (X2 = X3) | ~forename(X0,X3) | ~of(X0,X2,X1) | ~forename(X0,X2) | ~entity(X0,X1))))).

tff(u201,negated_conjecture,
(![X0] : ((~of(sK0,X0,sK1) | (sK2 = X0) | ~forename(sK0,X0))))).

tff(u200,negated_conjecture,
of(sK0,sK2,sK1)).

tff(u199,negated_conjecture,
nonreflexive(sK0,sK4)).

tff(u198,negated_conjecture,
~agent(sK0,sK4,sK3)).

tff(u197,negated_conjecture,
agent(sK0,sK4,sK1)).

tff(u196,axiom,
(![X1, X3, X0] : ((~patient(X0,X1,X3) | ~agent(X0,X1,X3) | ~nonreflexive(X0,X1))))).

tff(u195,negated_conjecture,
patient(sK0,sK4,sK3)).

# SZS output end Saturation.
```

Sample solution for SWV017+1

```tff(declare\$i,type,\$i:\$tType).
tff(declare_\$i1,type,at:\$i).
tff(declare_\$i2,type,an_a_nonce:\$i).
tff(finite_domain,axiom,
! [X:\$i] : (
X = at | X = an_a_nonce
) ).

tff(distinct_domain,axiom,
at != an_a_nonce
).

tff(declare_t,type,t:\$i).
tff(t_definition,axiom,t = at).
tff(declare_a,type,a:\$i).
tff(a_definition,axiom,a = at).
tff(declare_b,type,b:\$i).
tff(b_definition,axiom,b = at).
tff(declare_bt,type,bt:\$i).
tff(bt_definition,axiom,bt = an_a_nonce).
tff(declare_an_intruder_nonce,type,an_intruder_nonce:\$i).
tff(an_intruder_nonce_definition,axiom,an_intruder_nonce = an_a_nonce).
tff(declare_key,type,key: \$i * \$i > \$i).
tff(function_key,axiom,
key(at,at) = at
& key(at,an_a_nonce) = at
& key(an_a_nonce,at) = at
& key(an_a_nonce,an_a_nonce) = an_a_nonce

).

tff(declare_pair,type,pair: \$i * \$i > \$i).
tff(function_pair,axiom,
pair(at,at) = at
& pair(at,an_a_nonce) = an_a_nonce
& pair(an_a_nonce,at) = at
& pair(an_a_nonce,an_a_nonce) = at

).

tff(declare_sent,type,sent: \$i * \$i * \$i > \$i).
tff(function_sent,axiom,
sent(at,at,at) = at
& sent(at,at,an_a_nonce) = at
& sent(at,an_a_nonce,at) = at
& sent(at,an_a_nonce,an_a_nonce) = an_a_nonce
& sent(an_a_nonce,at,at) = at
& sent(an_a_nonce,at,an_a_nonce) = at
& sent(an_a_nonce,an_a_nonce,at) = at
& sent(an_a_nonce,an_a_nonce,an_a_nonce) = at

).

tff(declare_quadruple,type,quadruple: \$i * \$i * \$i * \$i > \$i).
& quadruple(at,at,at,an_a_nonce) = at
& quadruple(at,at,an_a_nonce,at) = at
& quadruple(at,at,an_a_nonce,an_a_nonce) = at
& quadruple(at,an_a_nonce,at,at) = at
& quadruple(at,an_a_nonce,at,an_a_nonce) = at
& quadruple(at,an_a_nonce,an_a_nonce,at) = at
& quadruple(at,an_a_nonce,an_a_nonce,an_a_nonce) = at
& quadruple(an_a_nonce,at,at,at) = at
& quadruple(an_a_nonce,at,at,an_a_nonce) = an_a_nonce
& quadruple(an_a_nonce,at,an_a_nonce,at) = an_a_nonce
& quadruple(an_a_nonce,at,an_a_nonce,an_a_nonce) = an_a_nonce
& quadruple(an_a_nonce,an_a_nonce,at,at) = an_a_nonce
& quadruple(an_a_nonce,an_a_nonce,at,an_a_nonce) = at
& quadruple(an_a_nonce,an_a_nonce,an_a_nonce,at) = an_a_nonce
& quadruple(an_a_nonce,an_a_nonce,an_a_nonce,an_a_nonce) = an_a_nonce

).

tff(declare_encrypt,type,encrypt: \$i * \$i > \$i).
tff(function_encrypt,axiom,
encrypt(at,at) = an_a_nonce
& encrypt(at,an_a_nonce) = an_a_nonce
& encrypt(an_a_nonce,at) = at
& encrypt(an_a_nonce,an_a_nonce) = at

).

tff(declare_triple,type,triple: \$i * \$i * \$i > \$i).
tff(function_triple,axiom,
triple(at,at,at) = at
& triple(at,at,an_a_nonce) = an_a_nonce
& triple(at,an_a_nonce,at) = at
& triple(at,an_a_nonce,an_a_nonce) = at
& triple(an_a_nonce,at,at) = at
& triple(an_a_nonce,at,an_a_nonce) = an_a_nonce
& triple(an_a_nonce,an_a_nonce,at) = at
& triple(an_a_nonce,an_a_nonce,an_a_nonce) = an_a_nonce

).

tff(declare_generate_b_nonce,type,generate_b_nonce: \$i > \$i).
tff(function_generate_b_nonce,axiom,
generate_b_nonce(at) = an_a_nonce
& generate_b_nonce(an_a_nonce) = an_a_nonce

).

tff(declare_generate_expiration_time,type,generate_expiration_time: \$i > \$i).
tff(function_generate_expiration_time,axiom,
generate_expiration_time(at) = an_a_nonce
& generate_expiration_time(an_a_nonce) = an_a_nonce

).

tff(declare_generate_key,type,generate_key: \$i > \$i).
tff(function_generate_key,axiom,
generate_key(at) = at
& generate_key(an_a_nonce) = at

).

tff(declare_generate_intruder_nonce,type,generate_intruder_nonce: \$i > \$i).
tff(function_generate_intruder_nonce,axiom,
generate_intruder_nonce(at) = at
& generate_intruder_nonce(an_a_nonce) = an_a_nonce

).

tff(declare_a_holds,type,a_holds: \$i > \$o ).
fof(predicate_a_holds,axiom,
a_holds(at)
& a_holds(an_a_nonce)

).

tff(declare_party_of_protocol,type,party_of_protocol: \$i > \$o ).
fof(predicate_party_of_protocol,axiom,
party_of_protocol(at)
& party_of_protocol(an_a_nonce)

).

tff(declare_message,type,message: \$i > \$o ).
fof(predicate_message,axiom,
message(at)
& message(an_a_nonce)

).

tff(declare_a_stored,type,a_stored: \$i > \$o ).
fof(predicate_a_stored,axiom,
~a_stored(at)
& a_stored(an_a_nonce)

).

tff(declare_b_holds,type,b_holds: \$i > \$o ).
fof(predicate_b_holds,axiom,
b_holds(at)
& b_holds(an_a_nonce)

).

tff(declare_fresh_to_b,type,fresh_to_b: \$i > \$o ).
fof(predicate_fresh_to_b,axiom,
fresh_to_b(at)
& fresh_to_b(an_a_nonce)

).

tff(declare_b_stored,type,b_stored: \$i > \$o ).
fof(predicate_b_stored,axiom,
b_stored(at)
& b_stored(an_a_nonce)

).

tff(declare_a_key,type,a_key: \$i > \$o ).
fof(predicate_a_key,axiom,
a_key(at)
& ~a_key(an_a_nonce)

).

tff(declare_t_holds,type,t_holds: \$i > \$o ).
fof(predicate_t_holds,axiom,
t_holds(at)
& ~t_holds(an_a_nonce)

).

tff(declare_a_nonce,type,a_nonce: \$i > \$o ).
fof(predicate_a_nonce,axiom,
~a_nonce(at)
& a_nonce(an_a_nonce)

).

tff(declare_intruder_message,type,intruder_message: \$i > \$o ).
fof(predicate_intruder_message,axiom,
intruder_message(at)
& intruder_message(an_a_nonce)

).

tff(declare_intruder_holds,type,intruder_holds: \$i > \$o ).
fof(predicate_intruder_holds,axiom,
intruder_holds(at)
& intruder_holds(an_a_nonce)

).

tff(declare_fresh_intruder_nonce,type,fresh_intruder_nonce: \$i > \$o ).
fof(predicate_fresh_intruder_nonce,axiom,
~fresh_intruder_nonce(at)
& fresh_intruder_nonce(an_a_nonce)

).
```

Vampire 4.2

Giles Reger
University of Manchester, United Kingdom

Sample solution for DAT013=1

```tff(type_def_5, type, array: \$tType).
tff(func_def_0, type, read: (array * \$int) > \$int).
tff(func_def_1, type, write: (array * \$int * \$int) > array).
tff(func_def_7, type, sK0: array).
tff(func_def_8, type, sK1: \$int).
tff(func_def_9, type, sK2: \$int).
tff(func_def_10, type, sK3: \$int).
tff(f3,conjecture,(
! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((\$lesseq(X3,X2) & \$lesseq(X1,X3)) => \$greater(read(X0,X3),0)) => ! [X4 : \$int] : ((\$lesseq(X4,X2) & \$lesseq(\$sum(X1,3),X4)) => \$greater(read(X0,X4),0)))),
file('TPTP/TPTP-v6.4.0/Problems/DAT/DAT013=1.p',unknown)).
tff(f4,negated_conjecture,(
~! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((\$lesseq(X3,X2) & \$lesseq(X1,X3)) => \$greater(read(X0,X3),0)) => ! [X4 : \$int] : ((\$lesseq(X4,X2) & \$lesseq(\$sum(X1,3),X4)) => \$greater(read(X0,X4),0)))),
inference(negated_conjecture,[],[f3])).
tff(f6,plain,(
~! [X0 : array,X1 : \$int,X2 : \$int] : (! [X3 : \$int] : ((~\$less(X2,X3) & ~\$less(X3,X1)) => \$less(0,read(X0,X3))) => ! [X4 : \$int] : ((~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3))) => \$less(0,read(X0,X4))))),
inference(evaluation,[],[f4])).
tff(f7,plain,(
( ! [X0:\$int,X1:\$int] : (\$sum(X0,X1) = \$sum(X1,X0)) )),
introduced(theory_axiom,[])).
tff(f9,plain,(
( ! [X0:\$int] : (\$sum(X0,0) = X0) )),
introduced(theory_axiom,[])).
tff(f12,plain,(
( ! [X0:\$int] : (~\$less(X0,X0)) )),
introduced(theory_axiom,[])).
tff(f13,plain,(
( ! [X2:\$int,X0:\$int,X1:\$int] : (~\$less(X1,X2) | ~\$less(X0,X1) | \$less(X0,X2)) )),
introduced(theory_axiom,[])).
tff(f14,plain,(
( ! [X0:\$int,X1:\$int] : (\$less(X1,X0) | \$less(X0,X1) | X0 = X1) )),
introduced(theory_axiom,[])).
tff(f15,plain,(
( ! [X2:\$int,X0:\$int,X1:\$int] : (\$less(\$sum(X0,X2),\$sum(X1,X2)) | ~\$less(X0,X1)) )),
introduced(theory_axiom,[])).
tff(f20,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X4 : \$int] : (~\$less(0,read(X0,X4)) & (~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3)))) & ! [X3 : \$int] : (\$less(0,read(X0,X3)) | (\$less(X2,X3) | \$less(X3,X1))))),
inference(ennf_transformation,[],[f6])).
tff(f21,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X4 : \$int] : (~\$less(0,read(X0,X4)) & ~\$less(X2,X4) & ~\$less(X4,\$sum(X1,3))) & ! [X3 : \$int] : (\$less(0,read(X0,X3)) | \$less(X2,X3) | \$less(X3,X1)))),
inference(flattening,[],[f20])).
tff(f22,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) & ! [X4 : \$int] : (\$less(0,read(X0,X4)) | \$less(X2,X4) | \$less(X4,X1)))),
inference(rectify,[],[f21])).
tff(f23,plain,(
? [X0 : array,X1 : \$int,X2 : \$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) & ! [X4 : \$int] : (\$less(0,read(X0,X4)) | \$less(X2,X4) | \$less(X4,X1))) => (? [X3 : \$int] : (~\$less(0,read(sK0,X3)) & ~\$less(sK2,X3) & ~\$less(X3,\$sum(sK1,3))) & ! [X4 : \$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1)))),
introduced(choice_axiom,[])).
tff(f24,plain,(
( ! [X2:\$int,X0:array,X1:\$int] : (? [X3 : \$int] : (~\$less(0,read(X0,X3)) & ~\$less(X2,X3) & ~\$less(X3,\$sum(X1,3))) => (~\$less(0,read(X0,sK3)) & ~\$less(X2,sK3) & ~\$less(sK3,\$sum(X1,3)))) )),
introduced(choice_axiom,[])).
tff(f25,plain,(
(~\$less(0,read(sK0,sK3)) & ~\$less(sK2,sK3) & ~\$less(sK3,\$sum(sK1,3))) & ! [X4 : \$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f22,f24,f23])).
tff(f29,plain,(
( ! [X4:\$int] : (\$less(0,read(sK0,X4)) | \$less(sK2,X4) | \$less(X4,sK1)) )),
inference(cnf_transformation,[],[f25])).
tff(f30,plain,(
~\$less(sK3,\$sum(sK1,3))),
inference(cnf_transformation,[],[f25])).
tff(f31,plain,(
~\$less(sK2,sK3)),
inference(cnf_transformation,[],[f25])).
tff(f32,plain,(
inference(cnf_transformation,[],[f25])).
tff(f33,plain,(
~\$less(sK3,\$sum(3,sK1))),
inference(forward_demodulation,[],[f30,f7])).
tff(f98,plain,(
\$less(\$sum(3,sK1),sK3) | \$sum(3,sK1) = sK3),
inference(resolution,[],[f14,f33])).
tff(f131,plain,(
spl4_8 <=> \$sum(3,sK1) = sK3),
introduced(avatar_definition,[new_symbols(naming,[spl4_8])])).
tff(f132,plain,(
\$sum(3,sK1) = sK3 | ~spl4_8),
inference(avatar_component_clause,[],[f131])).
tff(f137,plain,(
spl4_10 <=> \$less(\$sum(3,sK1),sK3)),
introduced(avatar_definition,[new_symbols(naming,[spl4_10])])).
tff(f138,plain,(
\$less(\$sum(3,sK1),sK3) | ~spl4_10),
inference(avatar_component_clause,[],[f137])).
tff(f142,plain,(
spl4_8 | spl4_10),
inference(avatar_split_clause,[],[f98,f137,f131])).
tff(f172,plain,(
( ! [X6:\$int,X4:\$int,X5:\$int] : (\$less(\$sum(X5,X4),\$sum(X6,X5)) | ~\$less(X4,X6)) )),
inference(superposition,[],[f15,f7])).
tff(f489,plain,(
( ! [X6:\$int,X7:\$int] : (\$less(X6,\$sum(X7,X6)) | ~\$less(0,X7)) )),
inference(superposition,[],[f172,f9])).
tff(f659,plain,(
\$less(sK2,sK3) | \$less(sK3,sK1)),
inference(resolution,[],[f29,f32])).
tff(f662,plain,(
\$less(sK3,sK1)),
inference(subsumption_resolution,[],[f659,f31])).
tff(f664,plain,(
( ! [X0:\$int] : (~\$less(X0,sK3) | \$less(X0,sK1)) )),
inference(resolution,[],[f662,f13])).
tff(f673,plain,(
( ! [X4:\$int] : (\$less(\$sum(sK1,X4),sK3) | ~\$less(X4,3)) ) | ~spl4_8),
inference(superposition,[],[f172,f132])).
tff(f2468,plain,(
\$less(sK1,sK3) | ~\$less(0,3) | ~spl4_8),
inference(superposition,[],[f673,f9])).
tff(f2473,plain,(
\$less(sK1,sK3) | ~spl4_8),
inference(evaluation,[],[f2468])).
tff(f2475,plain,(
\$less(sK1,sK1) | ~spl4_8),
inference(resolution,[],[f2473,f664])).
tff(f2479,plain,(
\$false | ~spl4_8),
inference(subsumption_resolution,[],[f2475,f12])).
tff(f2480,plain,(
~spl4_8),
tff(f2508,plain,(
( ! [X2:\$int] : (~\$less(X2,\$sum(3,sK1)) | \$less(X2,sK3)) ) | ~spl4_10),
inference(resolution,[],[f138,f13])).
tff(f2961,plain,(
~\$less(0,3) | \$less(sK1,sK3) | ~spl4_10),
inference(resolution,[],[f489,f2508])).
tff(f2988,plain,(
\$less(sK1,sK3) | ~spl4_10),
inference(evaluation,[],[f2961])).
tff(f2990,plain,(
\$less(sK1,sK1) | ~spl4_10),
inference(resolution,[],[f2988,f664])).
tff(f2994,plain,(
\$false | ~spl4_10),
inference(subsumption_resolution,[],[f2990,f12])).
tff(f2995,plain,(
~spl4_10),
tff(f2996,plain,(
\$false),
inference(avatar_sat_refutation,[],[f142,f2480,f2995])).
```

Sample solution for SEU140+2

```fof(f3,axiom,(
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f4,axiom,(
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f10,axiom,(
! [X0,X1,X2] : (set_difference(X0,X1) = X2 <=> ! [X3] : (in(X3,X2) <=> (~in(X3,X1) & in(X3,X0))))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f11,axiom,(
! [X0,X1] : (disjoint(X0,X1) <=> set_intersection2(X0,X1) = empty_set)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f20,axiom,(
! [X0,X1] : set_union2(X0,X0) = X0),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f23,axiom,(
! [X0,X1] : (empty_set = set_difference(X0,X1) <=> subset(X0,X1))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f28,axiom,(
! [X0,X1] : (subset(X0,X1) => set_union2(X0,X1) = X1)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f31,axiom,(
! [X0] : set_union2(X0,empty_set) = X0),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f39,axiom,(
! [X0,X1] : subset(set_difference(X0,X1),X0)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f41,axiom,(
! [X0,X1] : set_union2(X0,X1) = set_union2(X0,set_difference(X1,X0))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f42,axiom,(
! [X0] : set_difference(X0,empty_set) = X0),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f43,axiom,(
! [X0,X1] : (~(disjoint(X0,X1) & ? [X2] : (in(X2,X1) & in(X2,X0))) & ~(! [X2] : ~(in(X2,X1) & in(X2,X0)) & ~disjoint(X0,X1)))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f45,axiom,(
! [X0,X1] : set_difference(X0,X1) = set_difference(set_union2(X0,X1),X1)),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f47,axiom,(
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f51,conjecture,(
! [X0,X1,X2] : ((disjoint(X1,X2) & subset(X0,X1)) => disjoint(X0,X2))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f52,negated_conjecture,(
~! [X0,X1,X2] : ((disjoint(X1,X2) & subset(X0,X1)) => disjoint(X0,X2))),
inference(negated_conjecture,[],[f51])).
fof(f55,axiom,(
! [X0,X1] : subset(X0,set_union2(X0,X1))),
file('TPTP/TPTP-v6.4.0/Problems/SEU/SEU140+2.p',unknown)).
fof(f58,plain,(
! [X0] : set_union2(X0,X0) = X0),
inference(rectify,[],[f20])).
fof(f62,plain,(
! [X0,X1] : (~(disjoint(X0,X1) & ? [X2] : (in(X2,X1) & in(X2,X0))) & ~(! [X3] : ~(in(X3,X1) & in(X3,X0)) & ~disjoint(X0,X1)))),
inference(rectify,[],[f43])).
fof(f73,plain,(
! [X0,X1] : (set_union2(X0,X1) = X1 | ~subset(X0,X1))),
inference(ennf_transformation,[],[f28])).
fof(f82,plain,(
! [X0,X1] : ((~disjoint(X0,X1) | ! [X2] : (~in(X2,X1) | ~in(X2,X0))) & (? [X3] : (in(X3,X1) & in(X3,X0)) | disjoint(X0,X1)))),
inference(ennf_transformation,[],[f62])).
fof(f87,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & (disjoint(X1,X2) & subset(X0,X1)))),
inference(ennf_transformation,[],[f52])).
fof(f88,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & disjoint(X1,X2) & subset(X0,X1))),
inference(flattening,[],[f87])).
fof(f114,plain,(
! [X0,X1,X2] : ((set_difference(X0,X1) = X2 | ? [X3] : (((in(X3,X1) | ~in(X3,X0)) | ~in(X3,X2)) & ((~in(X3,X1) & in(X3,X0)) | in(X3,X2)))) & (! [X3] : ((in(X3,X2) | (in(X3,X1) | ~in(X3,X0))) & ((~in(X3,X1) & in(X3,X0)) | ~in(X3,X2))) | set_difference(X0,X1) != X2))),
inference(nnf_transformation,[],[f10])).
fof(f115,plain,(
! [X0,X1,X2] : ((set_difference(X0,X1) = X2 | ? [X3] : ((in(X3,X1) | ~in(X3,X0) | ~in(X3,X2)) & ((~in(X3,X1) & in(X3,X0)) | in(X3,X2)))) & (! [X3] : ((in(X3,X2) | in(X3,X1) | ~in(X3,X0)) & ((~in(X3,X1) & in(X3,X0)) | ~in(X3,X2))) | set_difference(X0,X1) != X2))),
inference(flattening,[],[f114])).
fof(f116,plain,(
! [X0,X1,X2] : ((set_difference(X0,X1) = X2 | ? [X3] : ((in(X3,X1) | ~in(X3,X0) | ~in(X3,X2)) & ((~in(X3,X1) & in(X3,X0)) | in(X3,X2)))) & (! [X4] : ((in(X4,X2) | in(X4,X1) | ~in(X4,X0)) & ((~in(X4,X1) & in(X4,X0)) | ~in(X4,X2))) | set_difference(X0,X1) != X2))),
inference(rectify,[],[f115])).
fof(f117,plain,(
! [X2,X1,X0] : (? [X3] : ((in(X3,X1) | ~in(X3,X0) | ~in(X3,X2)) & ((~in(X3,X1) & in(X3,X0)) | in(X3,X2))) => ((in(sK4(X0,X1,X2),X1) | ~in(sK4(X0,X1,X2),X0) | ~in(sK4(X0,X1,X2),X2)) & ((~in(sK4(X0,X1,X2),X1) & in(sK4(X0,X1,X2),X0)) | in(sK4(X0,X1,X2),X2))))),
introduced(choice_axiom,[])).
fof(f118,plain,(
! [X0,X1,X2] : ((set_difference(X0,X1) = X2 | ((in(sK4(X0,X1,X2),X1) | ~in(sK4(X0,X1,X2),X0) | ~in(sK4(X0,X1,X2),X2)) & ((~in(sK4(X0,X1,X2),X1) & in(sK4(X0,X1,X2),X0)) | in(sK4(X0,X1,X2),X2)))) & (! [X4] : ((in(X4,X2) | in(X4,X1) | ~in(X4,X0)) & ((~in(X4,X1) & in(X4,X0)) | ~in(X4,X2))) | set_difference(X0,X1) != X2))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK4])],[f116,f117])).
fof(f119,plain,(
! [X0,X1] : ((disjoint(X0,X1) | set_intersection2(X0,X1) != empty_set) & (set_intersection2(X0,X1) = empty_set | ~disjoint(X0,X1)))),
inference(nnf_transformation,[],[f11])).
fof(f120,plain,(
! [X0,X1] : ((empty_set = set_difference(X0,X1) | ~subset(X0,X1)) & (subset(X0,X1) | empty_set != set_difference(X0,X1)))),
inference(nnf_transformation,[],[f23])).
fof(f129,plain,(
! [X1,X0] : (? [X3] : (in(X3,X1) & in(X3,X0)) => (in(sK8(X0,X1),X1) & in(sK8(X0,X1),X0)))),
introduced(choice_axiom,[])).
fof(f130,plain,(
! [X0,X1] : ((~disjoint(X0,X1) | ! [X2] : (~in(X2,X1) | ~in(X2,X0))) & ((in(sK8(X0,X1),X1) & in(sK8(X0,X1),X0)) | disjoint(X0,X1)))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK8])],[f82,f129])).
fof(f133,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & disjoint(X1,X2) & subset(X0,X1)) => (~disjoint(sK10,sK12) & disjoint(sK11,sK12) & subset(sK10,sK11))),
introduced(choice_axiom,[])).
fof(f134,plain,(
~disjoint(sK10,sK12) & disjoint(sK11,sK12) & subset(sK10,sK11)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK10,sK11,sK12])],[f88,f133])).
fof(f137,plain,(
( ! [X0,X1] : (set_union2(X0,X1) = set_union2(X1,X0)) )),
inference(cnf_transformation,[],[f3])).
fof(f138,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = set_intersection2(X1,X0)) )),
inference(cnf_transformation,[],[f4])).
fof(f159,plain,(
( ! [X4,X2,X0,X1] : (in(X4,X0) | ~in(X4,X2) | set_difference(X0,X1) != X2) )),
inference(cnf_transformation,[],[f118])).
fof(f160,plain,(
( ! [X4,X2,X0,X1] : (~in(X4,X1) | ~in(X4,X2) | set_difference(X0,X1) != X2) )),
inference(cnf_transformation,[],[f118])).
fof(f165,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = empty_set | ~disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f119])).
fof(f171,plain,(
( ! [X0] : (set_union2(X0,X0) = X0) )),
inference(cnf_transformation,[],[f58])).
fof(f175,plain,(
( ! [X0,X1] : (~subset(X0,X1) | empty_set = set_difference(X0,X1)) )),
inference(cnf_transformation,[],[f120])).
fof(f180,plain,(
( ! [X0,X1] : (~subset(X0,X1) | set_union2(X0,X1) = X1) )),
inference(cnf_transformation,[],[f73])).
fof(f183,plain,(
( ! [X0] : (set_union2(X0,empty_set) = X0) )),
inference(cnf_transformation,[],[f31])).
fof(f192,plain,(
( ! [X0,X1] : (subset(set_difference(X0,X1),X0)) )),
inference(cnf_transformation,[],[f39])).
fof(f195,plain,(
( ! [X0,X1] : (set_union2(X0,X1) = set_union2(X0,set_difference(X1,X0))) )),
inference(cnf_transformation,[],[f41])).
fof(f196,plain,(
( ! [X0] : (set_difference(X0,empty_set) = X0) )),
inference(cnf_transformation,[],[f42])).
fof(f197,plain,(
( ! [X0,X1] : (in(sK8(X0,X1),X0) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f130])).
fof(f198,plain,(
( ! [X0,X1] : (in(sK8(X0,X1),X1) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f130])).
fof(f201,plain,(
( ! [X0,X1] : (set_difference(X0,X1) = set_difference(set_union2(X0,X1),X1)) )),
inference(cnf_transformation,[],[f45])).
fof(f203,plain,(
( ! [X0,X1] : (set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1))) )),
inference(cnf_transformation,[],[f47])).
fof(f208,plain,(
subset(sK10,sK11)),
inference(cnf_transformation,[],[f134])).
fof(f209,plain,(
disjoint(sK11,sK12)),
inference(cnf_transformation,[],[f134])).
fof(f210,plain,(
~disjoint(sK10,sK12)),
inference(cnf_transformation,[],[f134])).
fof(f213,plain,(
( ! [X0,X1] : (subset(X0,set_union2(X0,X1))) )),
inference(cnf_transformation,[],[f55])).
fof(f216,plain,(
( ! [X0,X1] : (set_difference(X0,set_difference(X0,X1)) = set_difference(X1,set_difference(X1,X0))) )),
inference(definition_unfolding,[],[f138,f203,f203])).
fof(f224,plain,(
( ! [X0,X1] : (~disjoint(X0,X1) | empty_set = set_difference(X0,set_difference(X0,X1))) )),
inference(definition_unfolding,[],[f165,f203])).
fof(f243,plain,(
( ! [X4,X0,X1] : (~in(X4,set_difference(X0,X1)) | ~in(X4,X1)) )),
inference(equality_resolution,[],[f160])).
fof(f244,plain,(
( ! [X4,X0,X1] : (~in(X4,set_difference(X0,X1)) | in(X4,X0)) )),
inference(equality_resolution,[],[f159])).
fof(f281,plain,(
( ! [X1] : (set_union2(empty_set,X1) = X1) )),
inference(superposition,[],[f137,f183])).
fof(f286,plain,(
( ! [X6,X7] : (subset(X6,set_union2(X7,X6))) )),
inference(superposition,[],[f213,f137])).
fof(f324,plain,(
( ! [X4,X3] : (empty_set = set_difference(X3,set_union2(X4,X3))) )),
inference(resolution,[],[f175,f286])).
fof(f326,plain,(
( ! [X6,X7] : (empty_set = set_difference(set_difference(X6,X7),X6)) )),
inference(resolution,[],[f175,f192])).
fof(f340,plain,(
set_union2(sK10,sK11) = sK11),
inference(resolution,[],[f180,f208])).
fof(f399,plain,(
( ! [X10,X8,X9] : (~in(sK8(X8,set_difference(X9,X10)),X10) | disjoint(X8,set_difference(X9,X10))) )),
inference(resolution,[],[f243,f198])).
fof(f405,plain,(
( ! [X4,X2,X3] : (in(sK8(set_difference(X2,X3),X4),X2) | disjoint(set_difference(X2,X3),X4)) )),
inference(resolution,[],[f244,f197])).
fof(f468,plain,(
( ! [X4,X5] : (set_union2(X5,set_union2(X4,X5)) = set_union2(X5,set_difference(X4,X5))) )),
inference(superposition,[],[f195,f201])).
fof(f477,plain,(
( ! [X4,X5] : (set_union2(X5,X4) = set_union2(X5,set_union2(X4,X5))) )),
inference(forward_demodulation,[],[f468,f195])).
fof(f615,plain,(
empty_set = set_difference(sK11,set_difference(sK11,sK12))),
inference(resolution,[],[f224,f209])).
fof(f726,plain,(
( ! [X6,X7] : (set_difference(X7,set_difference(X7,set_union2(X6,X7))) = set_difference(set_union2(X6,X7),set_difference(X6,X7))) )),
inference(superposition,[],[f216,f201])).
fof(f772,plain,(
( ! [X6,X7] : (set_difference(X7,empty_set) = set_difference(set_union2(X6,X7),set_difference(X6,X7))) )),
inference(forward_demodulation,[],[f726,f324])).
fof(f773,plain,(
( ! [X6,X7] : (set_difference(set_union2(X6,X7),set_difference(X6,X7)) = X7) )),
inference(forward_demodulation,[],[f772,f196])).
fof(f1209,plain,(
set_union2(set_difference(sK11,sK12),empty_set) = set_union2(set_difference(sK11,sK12),sK11)),
inference(superposition,[],[f195,f615])).
fof(f1226,plain,(
set_union2(set_difference(sK11,sK12),empty_set) = set_union2(sK11,set_difference(sK11,sK12))),
inference(forward_demodulation,[],[f1209,f137])).
fof(f1227,plain,(
set_union2(empty_set,set_difference(sK11,sK12)) = set_union2(sK11,set_difference(sK11,sK12))),
inference(forward_demodulation,[],[f1226,f137])).
fof(f1228,plain,(
set_union2(sK11,set_difference(sK11,sK12)) = set_difference(sK11,sK12)),
inference(forward_demodulation,[],[f1227,f281])).
fof(f1312,plain,(
( ! [X10,X11] : (set_union2(X10,empty_set) = set_union2(X10,set_difference(X10,X11))) )),
inference(superposition,[],[f195,f326])).
fof(f1331,plain,(
( ! [X10,X11] : (set_union2(X10,set_difference(X10,X11)) = X10) )),
inference(forward_demodulation,[],[f1312,f183])).
fof(f1333,plain,(
set_difference(sK11,sK12) = sK11),
inference(backward_demodulation,[],[f1331,f1228])).
fof(f2114,plain,(
set_union2(sK11,sK10) = set_union2(sK11,sK11)),
inference(superposition,[],[f477,f340])).
fof(f2148,plain,(
set_union2(sK11,sK10) = sK11),
inference(forward_demodulation,[],[f2114,f171])).
fof(f2201,plain,(
set_difference(sK11,set_difference(sK11,sK10)) = sK10),
inference(superposition,[],[f773,f2148])).
fof(f2214,plain,(
set_difference(set_union2(sK11,sK12),sK11) = sK12),
inference(superposition,[],[f773,f1333])).
fof(f4504,plain,(
( ! [X4,X2,X3] : (disjoint(set_difference(X2,X3),set_difference(X4,X2)) | disjoint(set_difference(X2,X3),set_difference(X4,X2))) )),
inference(resolution,[],[f405,f399])).
fof(f4539,plain,(
( ! [X4,X2,X3] : (disjoint(set_difference(X2,X3),set_difference(X4,X2))) )),
inference(duplicate_literal_removal,[],[f4504])).
fof(f4747,plain,(
( ! [X41] : (disjoint(sK10,set_difference(X41,sK11))) )),
inference(superposition,[],[f4539,f2201])).
fof(f4918,plain,(
disjoint(sK10,sK12)),
inference(superposition,[],[f4747,f2214])).
fof(f4925,plain,(
\$false),
inference(subsumption_resolution,[],[f4918,f210])).
```

Sample solution for NLP042+1

```tff(u283,axiom,
(![X1, X0] : ((~woman(X0,X1) | human_person(X0,X1))))).

tff(u282,axiom,
(![X1, X0] : ((~woman(X0,X1) | female(X0,X1))))).

tff(u281,negated_conjecture,
woman(sK0,sK1)).

tff(u280,negated_conjecture,
~female(sK0,sK4)).

tff(u279,negated_conjecture,
~female(sK0,sK2)).

tff(u278,negated_conjecture,
~female(sK0,sK3)).

tff(u277,negated_conjecture,
female(sK0,sK1)).

tff(u276,axiom,
(![X1, X0] : ((~human_person(X0,X1) | organism(X0,X1))))).

tff(u275,axiom,
(![X1, X0] : ((~human_person(X0,X1) | human(X0,X1))))).

tff(u274,axiom,
(![X1, X0] : ((~human_person(X0,X1) | animate(X0,X1))))).

tff(u273,negated_conjecture,
human_person(sK0,sK1)).

tff(u272,negated_conjecture,
~animate(sK0,sK3)).

tff(u271,negated_conjecture,
animate(sK0,sK1)).

tff(u270,negated_conjecture,
~human(sK0,sK2)).

tff(u269,negated_conjecture,
human(sK0,sK1)).

tff(u268,axiom,
(![X1, X0] : ((~organism(X0,X1) | entity(X0,X1))))).

tff(u267,axiom,
(![X1, X0] : ((~organism(X0,X1) | living(X0,X1))))).

tff(u266,negated_conjecture,
organism(sK0,sK1)).

tff(u265,negated_conjecture,
~living(sK0,sK3)).

tff(u264,negated_conjecture,
living(sK0,sK1)).

tff(u263,axiom,
(![X1, X0] : ((~entity(X0,X1) | specific(X0,X1))))).

tff(u262,axiom,
(![X1, X0] : ((~entity(X0,X1) | existent(X0,X1))))).

tff(u261,negated_conjecture,
entity(sK0,sK1)).

tff(u260,negated_conjecture,
entity(sK0,sK3)).

tff(u259,axiom,
(![X1, X0] : ((~mia_forename(X0,X1) | forename(X0,X1))))).

tff(u258,negated_conjecture,
mia_forename(sK0,sK2)).

tff(u257,axiom,
(![X1, X0] : ((~forename(X0,X1) | relname(X0,X1))))).

tff(u256,negated_conjecture,
forename(sK0,sK2)).

tff(u255,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | nonhuman(X0,X1))))).

tff(u254,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | general(X0,X1))))).

tff(u253,axiom,
(![X1, X0] : ((~abstraction(X0,X1) | unisex(X0,X1))))).

tff(u252,negated_conjecture,
abstraction(sK0,sK2)).

tff(u251,axiom,
(![X1, X0] : ((~unisex(X0,X1) | ~female(X0,X1))))).

tff(u250,negated_conjecture,
unisex(sK0,sK2)).

tff(u249,negated_conjecture,
unisex(sK0,sK4)).

tff(u248,negated_conjecture,
unisex(sK0,sK3)).

tff(u247,negated_conjecture,
~general(sK0,sK4)).

tff(u246,negated_conjecture,
~general(sK0,sK1)).

tff(u245,negated_conjecture,
~general(sK0,sK3)).

tff(u244,negated_conjecture,
general(sK0,sK2)).

tff(u243,axiom,
(![X1, X0] : ((~nonhuman(X0,X1) | ~human(X0,X1))))).

tff(u242,negated_conjecture,
nonhuman(sK0,sK2)).

tff(u241,axiom,
(![X1, X0] : ((~relation(X0,X1) | abstraction(X0,X1))))).

tff(u240,negated_conjecture,
relation(sK0,sK2)).

tff(u239,axiom,
(![X1, X0] : ((~relname(X0,X1) | relation(X0,X1))))).

tff(u238,negated_conjecture,
relname(sK0,sK2)).

tff(u237,axiom,
(![X1, X0] : ((~object(X0,X1) | entity(X0,X1))))).

tff(u236,axiom,
(![X1, X0] : ((~object(X0,X1) | nonliving(X0,X1))))).

tff(u235,axiom,
(![X1, X0] : ((~object(X0,X1) | unisex(X0,X1))))).

tff(u234,negated_conjecture,
object(sK0,sK3)).

tff(u233,axiom,
(![X1, X0] : ((~nonliving(X0,X1) | ~living(X0,X1))))).

tff(u232,axiom,
(![X1, X0] : ((~nonliving(X0,X1) | ~animate(X0,X1))))).

tff(u231,negated_conjecture,
nonliving(sK0,sK3)).

tff(u230,negated_conjecture,
~existent(sK0,sK4)).

tff(u229,negated_conjecture,
existent(sK0,sK1)).

tff(u228,negated_conjecture,
existent(sK0,sK3)).

tff(u227,axiom,
(![X1, X0] : ((~specific(X0,X1) | ~general(X0,X1))))).

tff(u226,negated_conjecture,
specific(sK0,sK1)).

tff(u225,negated_conjecture,
specific(sK0,sK4)).

tff(u224,negated_conjecture,
specific(sK0,sK3)).

tff(u223,axiom,
(![X1, X0] : ((~substance_matter(X0,X1) | object(X0,X1))))).

tff(u222,negated_conjecture,
substance_matter(sK0,sK3)).

tff(u221,axiom,
(![X1, X0] : ((~food(X0,X1) | substance_matter(X0,X1))))).

tff(u220,negated_conjecture,
food(sK0,sK3)).

tff(u219,axiom,
(![X1, X0] : ((~beverage(X0,X1) | food(X0,X1))))).

tff(u218,negated_conjecture,
beverage(sK0,sK3)).

tff(u217,axiom,
(![X1, X0] : ((~shake_beverage(X0,X1) | beverage(X0,X1))))).

tff(u216,negated_conjecture,
shake_beverage(sK0,sK3)).

tff(u215,axiom,
(![X1, X0] : ((~order(X0,X1) | act(X0,X1))))).

tff(u214,axiom,
(![X1, X0] : ((~order(X0,X1) | event(X0,X1))))).

tff(u213,negated_conjecture,
order(sK0,sK4)).

tff(u212,axiom,
(![X1, X0] : ((~event(X0,X1) | eventuality(X0,X1))))).

tff(u211,negated_conjecture,
event(sK0,sK4)).

tff(u210,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | specific(X0,X1))))).

tff(u209,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | nonexistent(X0,X1))))).

tff(u208,axiom,
(![X1, X0] : ((~eventuality(X0,X1) | unisex(X0,X1))))).

tff(u207,negated_conjecture,
eventuality(sK0,sK4)).

tff(u206,axiom,
(![X1, X0] : ((~nonexistent(X0,X1) | ~existent(X0,X1))))).

tff(u205,negated_conjecture,
nonexistent(sK0,sK4)).

tff(u204,axiom,
(![X1, X0] : ((~act(X0,X1) | event(X0,X1))))).

tff(u203,negated_conjecture,
act(sK0,sK4)).

tff(u202,axiom,
(![X1, X3, X0, X2] : ((~of(X0,X3,X1) | (X2 = X3) | ~forename(X0,X3) | ~of(X0,X2,X1) | ~forename(X0,X2) | ~entity(X0,X1))))).

tff(u201,negated_conjecture,
(![X0] : ((~of(sK0,X0,sK1) | (sK2 = X0) | ~forename(sK0,X0))))).

tff(u200,negated_conjecture,
of(sK0,sK2,sK1)).

tff(u199,negated_conjecture,
nonreflexive(sK0,sK4)).

tff(u198,negated_conjecture,
~agent(sK0,sK4,sK3)).

tff(u197,negated_conjecture,
agent(sK0,sK4,sK1)).

tff(u196,axiom,
(![X1, X3, X0] : ((~patient(X0,X1,X3) | ~agent(X0,X1,X3) | ~nonreflexive(X0,X1))))).

tff(u195,negated_conjecture,
patient(sK0,sK4,sK3)).

```

Sample solution for SWV017+1

```tff(declare_\$i,type,\$i:\$tType).
tff(declare_\$i1,type,at:\$i).
tff(declare_\$i2,type,t:\$i).
tff(finite_domain,axiom,
! [X:\$i] : (
X = at | X = t
) ).

tff(distinct_domain,axiom,
at != t
).

tff(declare_a,type,a:\$i).
tff(a_definition,axiom,a = at).
tff(declare_b,type,b:\$i).
tff(b_definition,axiom,b = at).
tff(declare_an_a_nonce,type,an_a_nonce:\$i).
tff(an_a_nonce_definition,axiom,an_a_nonce = t).
tff(declare_bt,type,bt:\$i).
tff(bt_definition,axiom,bt = at).
tff(declare_an_intruder_nonce,type,an_intruder_nonce:\$i).
tff(an_intruder_nonce_definition,axiom,an_intruder_nonce = at).
tff(declare_key,type,key: \$i * \$i > \$i).
tff(function_key,axiom,
key(at,at) = at
& key(at,t) = t
& key(t,at) = t
& key(t,t) = t

).

tff(declare_pair,type,pair: \$i * \$i > \$i).
tff(function_pair,axiom,
pair(at,at) = at
& pair(at,t) = t
& pair(t,at) = at
& pair(t,t) = at

).

tff(declare_sent,type,sent: \$i * \$i * \$i > \$i).
tff(function_sent,axiom,
sent(at,at,at) = at
& sent(at,at,t) = at
& sent(at,t,at) = at
& sent(at,t,t) = at
& sent(t,at,at) = at
& sent(t,at,t) = at
& sent(t,t,at) = at
& sent(t,t,t) = at

).

tff(declare_quadruple,type,quadruple: \$i * \$i * \$i * \$i > \$i).
& quadruple(at,at,at,t) = at
& quadruple(at,at,t,at) = t
& quadruple(at,at,t,t) = t
& quadruple(at,t,at,at) = t
& quadruple(at,t,at,t) = at
& quadruple(at,t,t,at) = at
& quadruple(at,t,t,t) = at
& quadruple(t,at,at,at) = t
& quadruple(t,at,at,t) = at
& quadruple(t,at,t,at) = t
& quadruple(t,at,t,t) = t
& quadruple(t,t,at,at) = t
& quadruple(t,t,at,t) = at
& quadruple(t,t,t,at) = t
& quadruple(t,t,t,t) = t

).

tff(declare_encrypt,type,encrypt: \$i * \$i > \$i).
tff(function_encrypt,axiom,
encrypt(at,at) = at
& encrypt(at,t) = at
& encrypt(t,at) = at
& encrypt(t,t) = t

).

tff(declare_triple,type,triple: \$i * \$i * \$i > \$i).
tff(function_triple,axiom,
triple(at,at,at) = t
& triple(at,at,t) = at
& triple(at,t,at) = at
& triple(at,t,t) = at
& triple(t,at,at) = t
& triple(t,at,t) = t
& triple(t,t,at) = at
& triple(t,t,t) = at

).

tff(declare_generate_b_nonce,type,generate_b_nonce: \$i > \$i).
tff(function_generate_b_nonce,axiom,
generate_b_nonce(at) = t
& generate_b_nonce(t) = t

).

tff(declare_generate_expiration_time,type,generate_expiration_time: \$i > \$i).
tff(function_generate_expiration_time,axiom,
generate_expiration_time(at) = t
& generate_expiration_time(t) = t

).

tff(declare_generate_key,type,generate_key: \$i > \$i).
tff(function_generate_key,axiom,
generate_key(at) = at
& generate_key(t) = at

).

tff(declare_generate_intruder_nonce,type,generate_intruder_nonce: \$i > \$i).
tff(function_generate_intruder_nonce,axiom,
generate_intruder_nonce(at) = at
& generate_intruder_nonce(t) = t

).

tff(declare_a_holds,type,a_holds: \$i > \$o ).
tff(predicate_a_holds,axiom,
%         a_holds(at) undefined in model
%         a_holds(t) undefined in model

).

tff(declare_party_of_protocol,type,party_of_protocol: \$i > \$o ).
tff(predicate_party_of_protocol,axiom,
party_of_protocol(at)
& party_of_protocol(t)

).

tff(declare_message,type,message: \$i > \$o ).
tff(predicate_message,axiom,
message(at)
& ~message(t)

).

tff(declare_a_stored,type,a_stored: \$i > \$o ).
tff(predicate_a_stored,axiom,
~a_stored(at)
& a_stored(t)

).

tff(declare_b_holds,type,b_holds: \$i > \$o ).
tff(predicate_b_holds,axiom,
%         b_holds(at) undefined in model
%         b_holds(t) undefined in model

).

tff(declare_fresh_to_b,type,fresh_to_b: \$i > \$o ).
tff(predicate_fresh_to_b,axiom,
fresh_to_b(at)
& fresh_to_b(t)

).

tff(declare_b_stored,type,b_stored: \$i > \$o ).
tff(predicate_b_stored,axiom,
%         b_stored(at) undefined in model
%         b_stored(t) undefined in model

).

tff(declare_a_key,type,a_key: \$i > \$o ).
tff(predicate_a_key,axiom,
a_key(at)
& ~a_key(t)

).

tff(declare_t_holds,type,t_holds: \$i > \$o ).
tff(predicate_t_holds,axiom,
t_holds(at)
& ~t_holds(t)

).

tff(declare_a_nonce,type,a_nonce: \$i > \$o ).
tff(predicate_a_nonce,axiom,
~a_nonce(at)
& a_nonce(t)

).

tff(declare_intruder_message,type,intruder_message: \$i > \$o ).
tff(predicate_intruder_message,axiom,
intruder_message(at)
& intruder_message(t)

).

tff(declare_intruder_holds,type,intruder_holds: \$i > \$o ).
tff(predicate_intruder_holds,axiom,
intruder_holds(at)
& intruder_holds(t)

).

tff(declare_fresh_intruder_nonce,type,fresh_intruder_nonce: \$i > \$o ).
tff(predicate_fresh_intruder_nonce,axiom,
fresh_intruder_nonce(at)
& ~fresh_intruder_nonce(t)

).
```