Entrants' Sample Solutions


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.0

Michael Färber
Universität Innsbruck, Austria

Sample solution for SET014^4

% SZS output start Proof
thf(ty$i, type, $i : $tType).
thf(tyeigen__3, type, eigen__3 : $i).
thf(tyeigen__2, type, eigen__2 : ($i>$o)).
thf(tyeigen__1, type, eigen__1 : ($i>$o)).
thf(tyeigen__0, type, eigen__0 : ($i>$o)).
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_negation,[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,(~((((![X1:$i]:((eigen__0 @ X1) => (eigen__2 @ X1))) & (![X1:$i]:((eigen__1 @ X1) => (eigen__2 @ X1)))) => (![X1:$i]:(((eigen__0 @ X1) | (eigen__1 @ X1)) => (eigen__2 @ X1)))))),introduced(assumption,[])).
thf(h4,assumption,((![X1:$i]:((eigen__0 @ X1) => (eigen__2 @ X1))) & (![X1:$i]:((eigen__1 @ X1) => (eigen__2 @ X1)))),introduced(assumption,[])).
thf(h5,assumption,(~((![X1:$i]:(((eigen__0 @ X1) | (eigen__1 @ X1)) => (eigen__2 @ X1))))),introduced(assumption,[])).
thf(h6,assumption,(![X1:$i]:((eigen__0 @ X1) => (eigen__2 @ X1))),introduced(assumption,[])).
thf(h7,assumption,(![X1:$i]:((eigen__1 @ X1) => (eigen__2 @ X1))),introduced(assumption,[])).
thf(h8,assumption,(~((((eigen__0 @ eigen__3) | (eigen__1 @ eigen__3)) => (eigen__2 @ eigen__3)))),introduced(assumption,[])).
thf(h9,assumption,((eigen__0 @ eigen__3) | (eigen__1 @ eigen__3)),introduced(assumption,[])).
thf(h10,assumption,(~((eigen__2 @ eigen__3))),introduced(assumption,[])).
thf(h11,assumption,(eigen__0 @ eigen__3),introduced(assumption,[])).
thf(h12,assumption,(eigen__1 @ eigen__3),introduced(assumption,[])).
thf(h13,assumption,((eigen__0 @ eigen__3) => (eigen__2 @ eigen__3)),introduced(assumption,[])).
thf(h14,assumption,(~((eigen__0 @ eigen__3))),introduced(assumption,[])).
thf(h15,assumption,(eigen__2 @ eigen__3),introduced(assumption,[])).
thf(11,plain,$false,inference(tab_conflict,[status(thm),assumptions([h14,h13,h11,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0])],[h11,h14])).
thf(12,plain,$false,inference(tab_conflict,[status(thm),assumptions([h15,h13,h11,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0])],[h15,h10])).
thf(10,plain,$false,inference(tab_imp,[status(thm),assumptions([h13,h11,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_imp(discharge,[h14]),tab_imp(discharge,[h15])],[h13,11,12,h14,h15])).
thf(9,plain,$false,inference(tab_all,[status(thm),assumptions([h11,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_all(discharge,[h13])],[h6:[bind(X1,$thf(eigen__3))],10,h13])).
thf(h16,assumption,((eigen__1 @ eigen__3) => (eigen__2 @ eigen__3)),introduced(assumption,[])).
thf(h17,assumption,(~((eigen__1 @ eigen__3))),introduced(assumption,[])).
thf(15,plain,$false,inference(tab_conflict,[status(thm),assumptions([h17,h16,h12,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0])],[h12,h17])).
thf(16,plain,$false,inference(tab_conflict,[status(thm),assumptions([h15,h16,h12,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0])],[h15,h10])).
thf(14,plain,$false,inference(tab_imp,[status(thm),assumptions([h16,h12,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_imp(discharge,[h17]),tab_imp(discharge,[h15])],[h16,15,16,h17,h15])).
thf(13,plain,$false,inference(tab_all,[status(thm),assumptions([h12,h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_all(discharge,[h16])],[h7:[bind(X1,$thf(eigen__3))],14,h16])).
thf(8,plain,$false,inference(tab_or,[status(thm),assumptions([h9,h10,h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_or(discharge,[h11]),tab_or(discharge,[h12])],[h9,9,13,h11,h12])).
thf(7,plain,$false,inference(tab_negimp,[status(thm),assumptions([h8,h6,h7,h4,h5,h3,h2,h1,h0]),tab_negimp(discharge,[h9,h10])],[h8,8,h9,h10])).
thf(6,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,7,h8])).
thf(5,plain,$false,inference(tab_and,[status(thm),assumptions([h4,h5,h3,h2,h1,h0]),tab_and(discharge,[h6,h7])],[h4,6,h6,h7])).
thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h2,h1,h0]),tab_negimp(discharge,[h4,h5])],[h3,5,h4,h5])).
thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h2,h1,h0]),tab_negall(discharge,[h3]),tab_negall(eigenvar,eigen__2)],[h2,4,h3])).
thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,3,h2])).
thf(1,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,2,h1])).
thf(0,theorem,(![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(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% SZS output end Proof

Sample solution for SYO553^1

% SZS output start Proof
thf(ty$i, type, $i : $tType).
thf(tyeigen__2, type, eigen__2 : $i).
thf(claim,conjecture,(?[X1:$i>$i>$i]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) = X3))))).
thf(h0,negated_conjecture,(~(?[X1:$i>$i>$i]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) = X3))))),inference(assume_negation,[status(cth)],[claim])).
thf(h1,assumption,(~((![X1:$i]:(![X2:$i]:(X2 = X2))))),introduced(assumption,[])).
thf(h2,assumption,(~((![X1:$i]:(X1 = X1)))),introduced(assumption,[])).
thf(h3,assumption,(~((eigen__2 = eigen__2))),introduced(assumption,[])).
thf(4,plain,$false,inference(tab_refl,[status(thm),assumptions([h3,h2,h1,h0])],[h3])).
thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h2,h1,h0]),tab_negall(discharge,[h3]),tab_negall(eigenvar,eigen__2)],[h2,4,h3])).
thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,3,h2])).
thf(1,plain,$false,inference(tab_negex,[status(thm),assumptions([h0]),tab_negex(discharge,[h1])],[h0:[bind(X1,$thf((^[X1:$i]:(^[X2:$i]:X2))))],2,h1])).
thf(0,theorem,(?[X1:$i>$i>$i]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) = X3)))),inference(contra,[status(thm),contra(discharge,[h0])],[1,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)

).