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]) ).

cnf(contradiction,plain,
    ( $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(t,X0_$i,triple(encrypt(quadruple(X1_$i,X2_$i,generate_key(X2_$i),X3_$i),X4_$i),encrypt(triple(X0_$i,generate_key(X2_$i),X3_$i),X5_$i),X6_$i)))
    | ~ 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(t,X0_$$iProver_fresh_intruder_nonce_1_$i,triple(encrypt(quadruple(X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,generate_key(X2_$$iProver_fresh_intruder_nonce_1_$i),X3_$$iProver_fresh_intruder_nonce_1_$i),X4_$$iProver_fresh_intruder_nonce_1_$i),encrypt(triple(X0_$$iProver_fresh_intruder_nonce_1_$i,generate_key(X2_$$iProver_fresh_intruder_nonce_1_$i),X3_$$iProver_fresh_intruder_nonce_1_$i),X5_$$iProver_fresh_intruder_nonce_1_$i),X6_$$iProver_fresh_intruder_nonce_1_$i)))
    | ~ 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(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
    | intruder_message(X3_$i) ),
    inference(cnf_transformation,[],[f89]) ).

cnf(c_222,plain,
    ( ~ intruder_message(quadruple(X0_$$iProver_fresh_intruder_nonce_1_$i,X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,X3_$$iProver_fresh_intruder_nonce_1_$i))
    | intruder_message(X3_$$iProver_fresh_intruder_nonce_1_$i) ),
    inference(subtyping,[status(esa)],[c_17]) ).

cnf(c_18,plain,
    ( ~ intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
    | intruder_message(X2_$i) ),
    inference(cnf_transformation,[],[f88]) ).

cnf(c_221,plain,
    ( ~ intruder_message(quadruple(X0_$$iProver_fresh_intruder_nonce_1_$i,X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,X3_$$iProver_fresh_intruder_nonce_1_$i))
    | intruder_message(X2_$$iProver_fresh_intruder_nonce_1_$i) ),
    inference(subtyping,[status(esa)],[c_18]) ).

cnf(c_19,plain,
    ( ~ intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
    | intruder_message(X1_$i) ),
    inference(cnf_transformation,[],[f87]) ).

cnf(c_220,plain,
    ( ~ intruder_message(quadruple(X0_$$iProver_fresh_intruder_nonce_1_$i,X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,X3_$$iProver_fresh_intruder_nonce_1_$i))
    | intruder_message(X1_$$iProver_fresh_intruder_nonce_1_$i) ),
    inference(subtyping,[status(esa)],[c_19]) ).

cnf(c_20,plain,
    ( ~ intruder_message(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
    | intruder_message(X0_$i) ),
    inference(cnf_transformation,[],[f86]) ).

cnf(c_219,plain,
    ( ~ intruder_message(quadruple(X0_$$iProver_fresh_intruder_nonce_1_$i,X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,X3_$$iProver_fresh_intruder_nonce_1_$i))
    | 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(quadruple(X0_$i,X1_$i,X2_$i,X3_$i))
    | ~ 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(quadruple(X0_$$iProver_fresh_intruder_nonce_1_$i,X1_$$iProver_fresh_intruder_nonce_1_$i,X2_$$iProver_fresh_intruder_nonce_1_$i,X3_$$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)
    | ~ 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))))
    | ~ message(sent(t,a,triple(encrypt(quadruple(X0_$i,X4_$i,X3_$i,X5_$i),at),X1_$i,X2_$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,(
  ~$less(0,read(sK0,sK3))),
  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),
  inference(AVATAR_contradiction_clause,[],[f2484,f131])).
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),
  inference(AVATAR_contradiction_clause,[],[f2995,f137])).
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).
tff(function_quadruple,axiom,
           quadruple(at,at,at,at) = at
         & 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,(
  ~$less(0,read(sK0,sK3))),
  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),
  inference(avatar_contradiction_clause,[],[f2479])).
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),
  inference(avatar_contradiction_clause,[],[f2994])).
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).
tff(function_quadruple,axiom,
           quadruple(at,at,at,at) = t
         & 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)

).