%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM612+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:15:59 PM UTC 2026
% Result : Theorem 1.39s 1.21s
% Output : Refutation 3.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 22
% Syntax : Number of formulae : 137 ( 25 unt; 6 def)
% Number of atoms : 498 ( 86 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 560 ( 199 ~; 199 |; 126 &)
% ( 19 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 7 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 10 con; 0-2 aty)
% Number of variables : 106 ( 0 sgn 97 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> sdtpldt0(sdtmndt0(X0,X1),X1) = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mConsDiff) ).
fof(f22,axiom,
! [X0] :
( aElement0(X0)
=> ! [X1] :
( ( aSet0(X1)
& isFinite0(X1) )
=> isFinite0(sdtmndt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mFDiffSet) ).
fof(f40,axiom,
! [X0] :
( aSet0(X0)
=> aElement0(sbrdtbr0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardS) ).
fof(f41,axiom,
! [X0] :
( aSet0(X0)
=> ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardNum) ).
fof(f43,axiom,
! [X0] :
( ( aSet0(X0)
& isFinite0(X0) )
=> ! [X1] :
( aElement0(X1)
=> ( ~ aElementOf0(X1,X0)
=> sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardCons) ).
fof(f50,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefSeg) ).
fof(f56,axiom,
! [X0] :
( aElementOf0(X0,szNzAzT0)
=> sbrdtbr0(slbdtrb0(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mCardSeg) ).
fof(f74,axiom,
aElementOf0(xK,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3418) ).
fof(f75,axiom,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,xS)
=> aElementOf0(X0,szNzAzT0) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3435) ).
fof(f95,axiom,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) ) )
& ! [X0] :
( aElementOf0(X0,xO)
<=> ? [X1] :
( aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X1) = X0 ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4891) ).
fof(f98,axiom,
( ! [X0] :
( aElementOf0(X0,xO)
=> aElementOf0(X0,xS) )
& aSubsetOf0(xO,xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__4998) ).
fof(f99,axiom,
( aSet0(xQ)
& ! [X0] :
( aElementOf0(X0,xQ)
=> aElementOf0(X0,xO) )
& aSubsetOf0(xQ,xO)
& sbrdtbr0(xQ) = xK
& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5078) ).
fof(f103,axiom,
( aElementOf0(xp,xQ)
& ! [X0] :
( aElementOf0(X0,xQ)
=> sdtlseqdt0(xp,X0) )
& xp = szmzizndt0(xQ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5147) ).
fof(f104,axiom,
( aSet0(xP)
& ! [X0] :
( aElementOf0(X0,xQ)
=> sdtlseqdt0(szmzizndt0(xQ),X0) )
& ! [X0] :
( aElementOf0(X0,xP)
<=> ( aElement0(X0)
& aElementOf0(X0,xQ)
& X0 != szmzizndt0(xQ) ) )
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5164) ).
fof(f106,axiom,
? [X0] :
( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X0) = xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__5182) ).
fof(f109,conjecture,
( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
& aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f110,negated_conjecture,
~ ( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)
& aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(negated_conjecture,[status(cth)],[f109]) ).
fof(f128,plain,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
<=> ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) ) )
& ! [X1] :
( aElementOf0(X1,xO)
<=> ? [X2] :
( aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X2) = X1 ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(rectify,[],[f95]) ).
fof(f132,plain,
( aSet0(xP)
& ! [X0] :
( aElementOf0(X0,xQ)
=> sdtlseqdt0(szmzizndt0(xQ),X0) )
& ! [X1] :
( aElementOf0(X1,xP)
<=> ( aElement0(X1)
& aElementOf0(X1,xQ)
& szmzizndt0(xQ) != X1 ) )
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
inference(rectify,[],[f104]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f160,plain,
! [X0] :
( ! [X1] :
( isFinite0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isFinite0(X1) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f161,plain,
! [X0] :
( ! [X1] :
( isFinite0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isFinite0(X1) )
| ~ aElement0(X0) ),
inference(flattening,[],[f160]) ).
fof(f181,plain,
! [X0] :
( aElement0(sbrdtbr0(X0))
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f182,plain,
! [X0] :
( ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
<=> isFinite0(X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f184,plain,
! [X0] :
( ! [X1] :
( sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0))
| aElementOf0(X1,X0)
| ~ aElement0(X1) )
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f185,plain,
! [X0] :
( ! [X1] :
( sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0))
| aElementOf0(X1,X0)
| ~ aElement0(X1) )
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(flattening,[],[f184]) ).
fof(f198,plain,
! [X0] :
( ! [X1] :
( X1 = slbdtrb0(X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
<=> ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) ) ) ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f206,plain,
! [X0] :
( sbrdtbr0(slbdtrb0(X0)) = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f232,plain,
( aSet0(xS)
& ! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xS) )
& aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
inference(ennf_transformation,[],[f75]) ).
fof(f260,plain,
( ! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xO) )
& aSubsetOf0(xO,xS) ),
inference(ennf_transformation,[],[f98]) ).
fof(f261,plain,
( aSet0(xQ)
& ! [X0] :
( aElementOf0(X0,xO)
| ~ aElementOf0(X0,xQ) )
& aSubsetOf0(xQ,xO)
& sbrdtbr0(xQ) = xK
& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ),
inference(ennf_transformation,[],[f99]) ).
fof(f266,plain,
( aElementOf0(xp,xQ)
& ! [X0] :
( sdtlseqdt0(xp,X0)
| ~ aElementOf0(X0,xQ) )
& xp = szmzizndt0(xQ) ),
inference(ennf_transformation,[],[f103]) ).
fof(f267,plain,
( aSet0(xP)
& ! [X0] :
( sdtlseqdt0(szmzizndt0(xQ),X0)
| ~ aElementOf0(X0,xQ) )
& ! [X1] :
( aElementOf0(X1,xP)
<=> ( aElement0(X1)
& aElementOf0(X1,xQ)
& szmzizndt0(xQ) != X1 ) )
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
inference(ennf_transformation,[],[f132]) ).
fof(f270,plain,
( sbrdtbr0(xQ) != szszuzczcdt0(sbrdtbr0(xP))
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(ennf_transformation,[],[f110]) ).
fof(f326,plain,
! [X0] :
( ( ( aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ isFinite0(X0) )
& ( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0) ) )
| ~ aSet0(X0) ),
inference(nnf_transformation,[],[f182]) ).
fof(f337,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X2] :
( ( aElementOf0(X2,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| ~ aElementOf0(X2,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(nnf_transformation,[],[f198]) ).
fof(f338,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X2] :
( ( aElementOf0(X2,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| ~ aElementOf0(X2,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(flattening,[],[f337]) ).
fof(f339,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ? [X2] :
( ( ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),X0)
| ~ aElementOf0(X2,X1) )
& ( ( aElementOf0(X2,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X2),X0) )
| aElementOf0(X2,X1) ) ) )
& ( ( aSet0(X1)
& ! [X3] :
( ( aElementOf0(X3,X1)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X0) )
& ( ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X0) )
| ~ aElementOf0(X3,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(rectify,[],[f338]) ).
fof(f340,plain,
! [X0] :
( ! [X1] :
( ( X1 = slbdtrb0(X0)
| ~ aSet0(X1)
| ( ( ~ aElementOf0(sK33(X0,X1),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(sK33(X0,X1)),X0)
| ~ aElementOf0(sK33(X0,X1),X1) )
& ( ( aElementOf0(sK33(X0,X1),szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(sK33(X0,X1)),X0) )
| aElementOf0(sK33(X0,X1),X1) ) ) )
& ( ( aSet0(X1)
& ! [X3] :
( ( aElementOf0(X3,X1)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X0) )
& ( ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X0) )
| ~ aElementOf0(X3,X1) ) ) )
| slbdtrb0(X0) != X1 ) )
| ~ aElementOf0(X0,szNzAzT0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X2,sK33(X0,X1))],[f339]) ).
fof(f445,plain,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( ( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X0,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X0) != szDzizrdt0(xd) )
& ( ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) )
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [X1] :
( ( aElementOf0(X1,xO)
| ! [X2] :
( ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,X2) != X1 ) )
& ( ? [X2] :
( aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X2) = X1 )
| ~ aElementOf0(X1,xO) ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(nnf_transformation,[],[f128]) ).
fof(f446,plain,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( ( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X0,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X0) != szDzizrdt0(xd) )
& ( ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) )
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [X1] :
( ( aElementOf0(X1,xO)
| ! [X2] :
( ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,X2) != X1 ) )
& ( ? [X2] :
( aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X2) = X1 )
| ~ aElementOf0(X1,xO) ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(flattening,[],[f445]) ).
fof(f447,plain,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( ( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X0,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X0) != szDzizrdt0(xd) )
& ( ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) )
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [X1] :
( ( aElementOf0(X1,xO)
| ! [X2] :
( ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,X2) != X1 ) )
& ( ? [X3] :
( aElementOf0(X3,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,X3) = X1 )
| ~ aElementOf0(X1,xO) ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(rectify,[],[f446]) ).
fof(f448,plain,
( aSet0(xO)
& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))
& ! [X0] :
( ( aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| ~ aElementOf0(X0,szDzozmdt0(xd))
| sdtlpdtrp0(xd,X0) != szDzizrdt0(xd) )
& ( ( aElementOf0(X0,szDzozmdt0(xd))
& sdtlpdtrp0(xd,X0) = szDzizrdt0(xd) )
| ~ aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) )
& ! [X1] :
( ( aElementOf0(X1,xO)
| ! [X2] :
( ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,X2) != X1 ) )
& ( ( aElementOf0(sK69(X1),sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xe,sK69(X1)) = X1 )
| ~ aElementOf0(X1,xO) ) )
& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(X3,sK69(X1))],[f447]) ).
fof(f452,plain,
( aSet0(xP)
& ! [X0] :
( sdtlseqdt0(szmzizndt0(xQ),X0)
| ~ aElementOf0(X0,xQ) )
& ! [X1] :
( ( aElementOf0(X1,xP)
| ~ aElement0(X1)
| ~ aElementOf0(X1,xQ)
| szmzizndt0(xQ) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,xQ)
& szmzizndt0(xQ) != X1 )
| ~ aElementOf0(X1,xP) ) )
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
inference(nnf_transformation,[],[f267]) ).
fof(f453,plain,
( aSet0(xP)
& ! [X0] :
( sdtlseqdt0(szmzizndt0(xQ),X0)
| ~ aElementOf0(X0,xQ) )
& ! [X1] :
( ( aElementOf0(X1,xP)
| ~ aElement0(X1)
| ~ aElementOf0(X1,xQ)
| szmzizndt0(xQ) = X1 )
& ( ( aElement0(X1)
& aElementOf0(X1,xQ)
& szmzizndt0(xQ) != X1 )
| ~ aElementOf0(X1,xP) ) )
& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ),
inference(flattening,[],[f452]) ).
fof(f454,plain,
( aElementOf0(sK72,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& xp = sdtlpdtrp0(xe,sK72) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(X0,sK72)],[f106]) ).
fof(f494,plain,
! [X0,X1] :
( sdtpldt0(sdtmndt0(X0,X1),X1) = X0
| ~ aElementOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f499,plain,
! [X0,X1] :
( isFinite0(sdtmndt0(X1,X0))
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f519,plain,
! [X0] :
( aElement0(sbrdtbr0(X0))
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f520,plain,
! [X0] :
( isFinite0(X0)
| ~ aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f326]) ).
fof(f521,plain,
! [X0] :
( aElementOf0(sbrdtbr0(X0),szNzAzT0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f326]) ).
fof(f524,plain,
! [X0,X1] :
( sbrdtbr0(sdtpldt0(X0,X1)) = szszuzczcdt0(sbrdtbr0(X0))
| aElementOf0(X1,X0)
| ~ aElement0(X1)
| ~ aSet0(X0)
| ~ isFinite0(X0) ),
inference(cnf_transformation,[],[f185]) ).
fof(f541,plain,
! [X0,X1] :
( aSet0(X1)
| slbdtrb0(X0) != X1
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f340]) ).
fof(f554,plain,
! [X0] :
( sbrdtbr0(slbdtrb0(X0)) = X0
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f600,plain,
aElementOf0(xK,szNzAzT0),
inference(cnf_transformation,[],[f74]) ).
fof(f603,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[],[f232]) ).
fof(f829,plain,
! [X2,X1] :
( aElementOf0(X1,xO)
| ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| sdtlpdtrp0(xe,X2) != X1 ),
inference(cnf_transformation,[],[f448]) ).
fof(f846,plain,
! [X0] :
( aElementOf0(X0,xS)
| ~ aElementOf0(X0,xO) ),
inference(cnf_transformation,[],[f260]) ).
fof(f848,plain,
xK = sbrdtbr0(xQ),
inference(cnf_transformation,[],[f261]) ).
fof(f851,plain,
aSet0(xQ),
inference(cnf_transformation,[],[f261]) ).
fof(f862,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[],[f266]) ).
fof(f864,plain,
aElementOf0(xp,xQ),
inference(cnf_transformation,[],[f266]) ).
fof(f865,plain,
xP = sdtmndt0(xQ,szmzizndt0(xQ)),
inference(cnf_transformation,[],[f453]) ).
fof(f866,plain,
! [X1] :
( szmzizndt0(xQ) != X1
| ~ aElementOf0(X1,xP) ),
inference(cnf_transformation,[],[f453]) ).
fof(f871,plain,
aSet0(xP),
inference(cnf_transformation,[],[f453]) ).
fof(f873,plain,
xp = sdtlpdtrp0(xe,sK72),
inference(cnf_transformation,[],[f454]) ).
fof(f874,plain,
aElementOf0(sK72,sdtlbdtrb0(xd,szDzizrdt0(xd))),
inference(cnf_transformation,[],[f454]) ).
fof(f879,plain,
( sbrdtbr0(xQ) != szszuzczcdt0(sbrdtbr0(xP))
| ~ aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
inference(cnf_transformation,[],[f270]) ).
fof(f892,plain,
! [X0] :
( aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(equality_resolution,[],[f541]) ).
fof(f933,plain,
! [X2] :
( aElementOf0(sdtlpdtrp0(xe,X2),xO)
| ~ aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(equality_resolution,[],[f829]) ).
fof(f938,plain,
~ aElementOf0(szmzizndt0(xQ),xP),
inference(equality_resolution,[],[f866]) ).
fof(f941,definition,
( spl73_1
<=> aElementOf0(sbrdtbr0(xP),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl73_1])],[avatar_definition]) ).
fof(f943,plain,
( ~ aElementOf0(sbrdtbr0(xP),szNzAzT0)
| spl73_1 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f945,definition,
( spl73_2
<=> sbrdtbr0(xQ) = szszuzczcdt0(sbrdtbr0(xP)) ),
introduced(definition,[new_symbols(definition,[spl73_2])],[avatar_definition]) ).
fof(f947,plain,
( sbrdtbr0(xQ) != szszuzczcdt0(sbrdtbr0(xP))
| spl73_2 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f948,plain,
( ~ spl73_1
| ~ spl73_2 ),
inference(avatar_split_clause,[],[f879,f945,f941]) ).
fof(f964,plain,
~ aElementOf0(xp,xP),
inference(forward_demodulation,[],[f938,f862]) ).
fof(f977,plain,
xP = sdtmndt0(xQ,xp),
inference(forward_demodulation,[],[f865,f862]) ).
fof(f980,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xO) ),
inference(resolution,[],[f846,f603]) ).
fof(f1007,plain,
( ~ isFinite0(xP)
| ~ aSet0(xP)
| spl73_1 ),
inference(resolution,[],[f521,f943]) ).
fof(f1010,plain,
( ~ isFinite0(xP)
| spl73_1 ),
inference(forward_subsumption_resolution,[],[f1007,f871]) ).
fof(f1014,plain,
! [X0] :
( aElement0(X0)
| ~ aSet0(slbdtrb0(X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(superposition,[],[f519,f554]) ).
fof(f1015,plain,
! [X0] :
( aElement0(X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(forward_subsumption_resolution,[],[f1014,f892]) ).
fof(f1224,plain,
( aElementOf0(xp,xO)
| ~ aElementOf0(sK72,sdtlbdtrb0(xd,szDzizrdt0(xd))) ),
inference(superposition,[],[f933,f873]) ).
fof(f1227,plain,
aElementOf0(xp,xO),
inference(forward_subsumption_resolution,[],[f1224,f874]) ).
fof(f1337,plain,
( xK != szszuzczcdt0(sbrdtbr0(xP))
| spl73_2 ),
inference(forward_demodulation,[],[f947,f848]) ).
fof(f1378,plain,
( xQ = sdtpldt0(xP,xp)
| ~ aElementOf0(xp,xQ)
| ~ aSet0(xQ) ),
inference(superposition,[],[f494,f977]) ).
fof(f1379,plain,
( xQ = sdtpldt0(xP,xp)
| ~ aSet0(xQ) ),
inference(forward_subsumption_resolution,[],[f1378,f864]) ).
fof(f1380,plain,
xQ = sdtpldt0(xP,xp),
inference(forward_subsumption_resolution,[],[f1379,f851]) ).
fof(f1415,definition,
( spl73_38
<=> isFinite0(xQ) ),
introduced(definition,[new_symbols(definition,[spl73_38])],[avatar_definition]) ).
fof(f1416,plain,
( isFinite0(xQ)
| ~ spl73_38 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1417,plain,
( ~ isFinite0(xQ)
| spl73_38 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1433,plain,
( ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0)
| ~ aSet0(xQ)
| spl73_38 ),
inference(resolution,[],[f1417,f520]) ).
fof(f1434,plain,
( ~ aElementOf0(sbrdtbr0(xQ),szNzAzT0)
| spl73_38 ),
inference(forward_subsumption_resolution,[],[f1433,f851]) ).
fof(f1435,plain,
( ~ aElementOf0(xK,szNzAzT0)
| spl73_38 ),
inference(forward_demodulation,[],[f1434,f848]) ).
fof(f1436,plain,
( $false
| spl73_38 ),
inference(forward_subsumption_resolution,[],[f1435,f600]) ).
fof(f1437,plain,
spl73_38,
inference(avatar_contradiction_clause,[],[f1436]) ).
fof(f1745,definition,
( spl73_64
<=> aElementOf0(xp,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[spl73_64])],[avatar_definition]) ).
fof(f1746,plain,
( aElementOf0(xp,szNzAzT0)
| ~ spl73_64 ),
inference(avatar_component_clause,[],[f1745]) ).
fof(f1747,plain,
( ~ aElementOf0(xp,szNzAzT0)
| spl73_64 ),
inference(avatar_component_clause,[],[f1745]) ).
fof(f1756,plain,
( ~ aElementOf0(xp,xO)
| spl73_64 ),
inference(resolution,[],[f1747,f980]) ).
fof(f1760,plain,
( $false
| spl73_64 ),
inference(forward_subsumption_resolution,[],[f1756,f1227]) ).
fof(f1761,plain,
spl73_64,
inference(avatar_contradiction_clause,[],[f1760]) ).
fof(f3159,plain,
( sbrdtbr0(xQ) = szszuzczcdt0(sbrdtbr0(xP))
| aElementOf0(xp,xP)
| ~ aElement0(xp)
| ~ aSet0(xP)
| ~ isFinite0(xP) ),
inference(superposition,[],[f524,f1380]) ).
fof(f3161,plain,
( sbrdtbr0(xQ) = szszuzczcdt0(sbrdtbr0(xP))
| ~ aElement0(xp)
| ~ aSet0(xP)
| ~ isFinite0(xP) ),
inference(forward_subsumption_resolution,[],[f3159,f964]) ).
fof(f3162,plain,
( sbrdtbr0(xQ) = szszuzczcdt0(sbrdtbr0(xP))
| ~ aElement0(xp)
| ~ isFinite0(xP) ),
inference(forward_subsumption_resolution,[],[f3161,f871]) ).
fof(f3163,plain,
( xK = szszuzczcdt0(sbrdtbr0(xP))
| ~ aElement0(xp)
| ~ isFinite0(xP) ),
inference(forward_demodulation,[],[f3162,f848]) ).
fof(f3164,plain,
( ~ aElement0(xp)
| ~ isFinite0(xP)
| spl73_2 ),
inference(forward_subsumption_resolution,[],[f3163,f1337]) ).
fof(f3166,definition,
( spl73_141
<=> isFinite0(xP) ),
introduced(definition,[new_symbols(definition,[spl73_141])],[avatar_definition]) ).
fof(f3168,plain,
( ~ isFinite0(xP)
| spl73_141 ),
inference(avatar_component_clause,[],[f3166]) ).
fof(f3170,definition,
( spl73_142
<=> aElement0(xp) ),
introduced(definition,[new_symbols(definition,[spl73_142])],[avatar_definition]) ).
fof(f3171,plain,
( aElement0(xp)
| ~ spl73_142 ),
inference(avatar_component_clause,[],[f3170]) ).
fof(f3172,plain,
( ~ aElement0(xp)
| spl73_142 ),
inference(avatar_component_clause,[],[f3170]) ).
fof(f3173,plain,
( ~ spl73_141
| ~ spl73_142
| spl73_2 ),
inference(avatar_split_clause,[],[f3164,f945,f3170,f3166]) ).
fof(f3187,plain,
( ~ aElementOf0(xp,szNzAzT0)
| spl73_142 ),
inference(resolution,[],[f3172,f1015]) ).
fof(f3189,plain,
( $false
| ~ spl73_64
| spl73_142 ),
inference(forward_subsumption_resolution,[],[f3187,f1746]) ).
fof(f3190,plain,
( ~ spl73_64
| spl73_142 ),
inference(avatar_contradiction_clause,[],[f3189]) ).
fof(f3191,plain,
( ~ spl73_141
| spl73_1 ),
inference(avatar_split_clause,[],[f1010,f941,f3166]) ).
fof(f3879,plain,
( isFinite0(xP)
| ~ aSet0(xQ)
| ~ isFinite0(xQ)
| ~ aElement0(xp) ),
inference(superposition,[],[f499,f977]) ).
fof(f3882,plain,
( ~ aSet0(xQ)
| ~ isFinite0(xQ)
| ~ aElement0(xp)
| spl73_141 ),
inference(forward_subsumption_resolution,[],[f3879,f3168]) ).
fof(f3883,plain,
( ~ isFinite0(xQ)
| ~ aElement0(xp)
| spl73_141 ),
inference(forward_subsumption_resolution,[],[f3882,f851]) ).
fof(f3884,plain,
( ~ aElement0(xp)
| ~ spl73_38
| spl73_141 ),
inference(forward_subsumption_resolution,[],[f3883,f1416]) ).
fof(f3885,plain,
( $false
| ~ spl73_38
| spl73_141
| ~ spl73_142 ),
inference(forward_subsumption_resolution,[],[f3884,f3171]) ).
fof(f3886,plain,
( ~ spl73_38
| spl73_141
| ~ spl73_142 ),
inference(avatar_contradiction_clause,[],[f3885]) ).
cnf(s1,plain,
( ~ spl73_1
| ~ spl73_2 ),
inference(sat_conversion,[],[f948]) ).
cnf(s33,plain,
spl73_38,
inference(sat_conversion,[],[f1437]) ).
cnf(s50,plain,
spl73_64,
inference(sat_conversion,[],[f1761]) ).
cnf(s122,plain,
( spl73_2
| ~ spl73_141
| ~ spl73_142 ),
inference(sat_conversion,[],[f3173]) ).
cnf(s125,plain,
( ~ spl73_64
| spl73_142 ),
inference(sat_conversion,[],[f3190]) ).
cnf(s126,plain,
( spl73_1
| ~ spl73_141 ),
inference(sat_conversion,[],[f3191]) ).
cnf(s166,plain,
( ~ spl73_38
| spl73_141
| ~ spl73_142 ),
inference(sat_conversion,[],[f3886]) ).
cnf(s182,plain,
spl73_142,
inference(rat,[],[s125,s50]) ).
cnf(s186,plain,
spl73_141,
inference(rat,[],[s166,s182,s33]) ).
cnf(s187,plain,
spl73_1,
inference(rat,[],[s126,s186]) ).
cnf(s188,plain,
spl73_2,
inference(rat,[],[s122,s182,s186]) ).
cnf(s204,plain,
$false,
inference(rat,[],[s1,s188,s187]) ).
fof(f3887,plain,
$false,
inference(avatar_sat_refutation,[],[s204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM612+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n013.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 20:44:51 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.39/1.21 % (534395)Detected formulas, will run a generic FOF schedule.
% 1.39/1.21 % (534437)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=508262846:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.39/1.21 % (534436)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=520217386:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.39/1.21 % (534434)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2542725346:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.39/1.21 % (534432)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=739247737:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.39/1.21 % (534435)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1197849338:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.39/1.21 % (534437)First to succeed.
% 1.39/1.21 % (534437)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-534395"
% 1.39/1.21 % (534438)dis-21_1_sil=8000:lcm=predicate:random_seed=3014378592:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.39/1.21 % (534436)Also succeeded, but the first one will report.
% 1.39/1.21 % (534433)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=960969069:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.39/1.21 % (534435)Instruction limit reached!
% 1.39/1.21 % (534435)------------------------------
% 1.39/1.21 % (534435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.39/1.21 % (534435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/1.21 % (534435)CaDiCaL version: 2.1.3
% 1.39/1.21 % (534435)Termination reason: Instruction limit
% 1.39/1.21 % (534435)Termination phase: Saturation
% 1.39/1.21 % (534435)Time elapsed: 0.067 s
% 1.39/1.21 % (534435)Peak memory usage: 90 MB
% 1.39/1.21 % (534435)Instructions burned: 109 (million)
% 1.39/1.21 % (534438)Instruction limit reached!
% 1.39/1.21 % (534438)------------------------------
% 1.39/1.21 % (534438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.39/1.21 % (534438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/1.21 % (534438)CaDiCaL version: 2.1.3
% 1.39/1.21 % (534438)Termination reason: Instruction limit
% 1.39/1.21 % (534438)Termination phase: Saturation
% 1.39/1.21 % (534438)Time elapsed: 0.068 s
% 1.39/1.21 % (534438)Peak memory usage: 90 MB
% 1.39/1.21 % (534438)Instructions burned: 130 (million)
% 1.39/1.21 % (534437)Refutation found. Thanks to Tanya!
% 1.39/1.21 % SZS status Theorem for theBenchmark
% 1.39/1.21 % SZS output start Proof for theBenchmark
% See solution above
% 3.02/1.41 % (534437)------------------------------
% 3.02/1.41 % (534437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.02/1.41 % (534437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.02/1.41 % (534437)CaDiCaL version: 2.1.3
% 3.02/1.41 % (534437)Termination reason: Refutation
% 3.02/1.41 % (534437)Time elapsed: 0.051 s
% 3.02/1.41 % (534437)Peak memory usage: 92 MB
% 3.02/1.41 % (534437)Instructions burned: 130 (million)
% 3.02/1.41 % (534437)------------------------------
% 3.02/1.41 % (534437)------------------------------
% 3.02/1.41 % (534395)Success in time 0.355 s
% 3.02/1.41 % Vampire exiting
%------------------------------------------------------------------------------