%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM566+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:24:50 PM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : Refutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 26
% Syntax : Number of formulae : 182 ( 42 unt; 11 def)
% Number of atoms : 506 ( 67 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 558 ( 234 ~; 268 |; 23 &)
% ( 23 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 12 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 124 ( 0 sgn 118 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ~ ? [X1] : aElementOf0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefEmp) ).
fof(f10,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> aElementOf0(X2,X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(f12,axiom,
! [X0] :
( aSet0(X0)
=> aSubsetOf0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubRefl) ).
fof(f23,axiom,
( aSet0(szNzAzT0)
& isCountable0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNATSet) ).
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroNum) ).
fof(f42,axiom,
! [X0] :
( aSet0(X0)
=> ( sbrdtbr0(X0) = sz00
<=> X0 = slcrc0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCardEmpty) ).
fof(f57,axiom,
! [X0,X1] :
( ( aSet0(X0)
& aElementOf0(X1,szNzAzT0) )
=> ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSel) ).
fof(f69,axiom,
! [X0] :
( aFunction0(X0)
=> ! [X1] :
( aElementOf0(X1,szDzozmdt0(X0))
=> aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mImgRng) ).
fof(f73,axiom,
( aSet0(xT)
& isFinite0(xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3291) ).
fof(f75,axiom,
( aSubsetOf0(xS,szNzAzT0)
& isCountable0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3435) ).
fof(f76,axiom,
( aFunction0(xc)
& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)
& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3453) ).
fof(f78,axiom,
xK = sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3462) ).
fof(f79,axiom,
aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3476) ).
fof(f80,axiom,
! [X0] :
( aElementOf0(X0,slbdtsldtrb0(xS,sz00))
=> sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__3507) ).
fof(f81,conjecture,
? [X0] :
( aElementOf0(X0,xT)
& ? [X1] :
( aSubsetOf0(X1,xS)
& isCountable0(X1)
& ! [X2] :
( aElementOf0(X2,slbdtsldtrb0(X1,xK))
=> sdtlpdtrp0(xc,X2) = X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f82,negated_conjecture,
~ ? [X0] :
( aElementOf0(X0,xT)
& ? [X1] :
( aSubsetOf0(X1,xS)
& isCountable0(X1)
& ! [X2] :
( aElementOf0(X2,slbdtsldtrb0(X1,xK))
=> sdtlpdtrp0(xc,X2) = X0 ) ) ),
inference(negated_conjecture,[status(cth)],[f81]) ).
fof(f88,plain,
! [X0] :
( X0 = slcrc0
<=> ( aSet0(X0)
& ! [X1] : ~ aElementOf0(X1,X0) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f95,plain,
! [X0] :
( ! [X1] :
( aSubsetOf0(X1,X0)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1) ) ) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f98,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f143,plain,
! [X0] :
( ( sbrdtbr0(X0) = sz00
<=> X0 = slcrc0 )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f167,plain,
! [X0,X1] :
( ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f168,plain,
! [X0,X1] :
( ! [X2] :
( X2 = slbdtsldtrb0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aSubsetOf0(X3,X0)
& sbrdtbr0(X3) = X1 ) ) ) )
| ~ aSet0(X0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(flattening,[],[f167]) ).
fof(f187,plain,
! [X0] :
( ! [X1] :
( aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))
| ~ aElementOf0(X1,szDzozmdt0(X0)) )
| ~ aFunction0(X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f195,plain,
! [X0] :
( sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0)
| ~ aElementOf0(X0,slbdtsldtrb0(xS,sz00)) ),
inference(ennf_transformation,[],[f80]) ).
fof(f196,plain,
! [X0] :
( ~ aElementOf0(X0,xT)
| ! [X1] :
( ~ aSubsetOf0(X1,xS)
| ~ isCountable0(X1)
| ? [X2] :
( sdtlpdtrp0(xc,X2) != X0
& aElementOf0(X2,slbdtsldtrb0(X1,xK)) ) ) ),
inference(ennf_transformation,[],[f82]) ).
fof(f198,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f88]) ).
fof(f199,plain,
! [X0] :
( aSet0(X0)
| slcrc0 != X0 ),
inference(cnf_transformation,[],[f88]) ).
fof(f200,plain,
! [X0] :
( aElementOf0(sK0(X0),X0)
| ~ aSet0(X0)
| slcrc0 = X0 ),
inference(cnf_transformation,[],[f88]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ aSet0(X0)
| ~ aElementOf0(X2,X1)
| aElementOf0(X2,X0)
| ~ aSubsetOf0(X1,X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f207,plain,
! [X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aSet0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f209,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f237,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[],[f23]) ).
fof(f238,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[],[f24]) ).
fof(f259,plain,
! [X0] :
( ~ aSet0(X0)
| slcrc0 = X0
| sz00 != sbrdtbr0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f291,plain,
! [X2,X3,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| sbrdtbr0(X3) = X1
| ~ aElementOf0(X3,X2)
| slbdtsldtrb0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f168]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| aSubsetOf0(X3,X0)
| ~ aElementOf0(X3,X2)
| slbdtsldtrb0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f168]) ).
fof(f322,plain,
! [X0,X1] :
( ~ aFunction0(X0)
| ~ aElementOf0(X1,szDzozmdt0(X0))
| aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0))) ),
inference(cnf_transformation,[],[f187]) ).
fof(f335,plain,
aSet0(xT),
inference(cnf_transformation,[],[f73]) ).
fof(f337,plain,
isCountable0(xS),
inference(cnf_transformation,[],[f75]) ).
fof(f338,plain,
aSubsetOf0(xS,szNzAzT0),
inference(cnf_transformation,[],[f75]) ).
fof(f339,plain,
aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT),
inference(cnf_transformation,[],[f76]) ).
fof(f340,plain,
szDzozmdt0(xc) = slbdtsldtrb0(xS,xK),
inference(cnf_transformation,[],[f76]) ).
fof(f341,plain,
aFunction0(xc),
inference(cnf_transformation,[],[f76]) ).
fof(f346,plain,
sz00 = xK,
inference(cnf_transformation,[],[f78]) ).
fof(f347,plain,
aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)),
inference(cnf_transformation,[],[f79]) ).
fof(f348,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xS,sz00))
| sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0) ),
inference(cnf_transformation,[],[f195]) ).
fof(f349,plain,
! [X0,X1] :
( aElementOf0(sK21(X0,X1),slbdtsldtrb0(X1,xK))
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f196]) ).
fof(f350,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK21(X0,X1)) != X0
| ~ isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[],[f196]) ).
fof(f351,plain,
aElementOf0(xK,szNzAzT0),
inference(definition_unfolding,[],[f238,f346]) ).
fof(f357,plain,
! [X0] :
( sbrdtbr0(X0) != xK
| slcrc0 = X0
| ~ aSet0(X0) ),
inference(definition_unfolding,[],[f259,f346]) ).
fof(f362,plain,
aElementOf0(slcrc0,slbdtsldtrb0(xS,xK)),
inference(definition_unfolding,[],[f347,f346]) ).
fof(f363,plain,
! [X0] :
( ~ aElementOf0(X0,slbdtsldtrb0(xS,xK))
| sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0) ),
inference(definition_unfolding,[],[f348,f346]) ).
fof(f364,plain,
aSet0(slcrc0),
inference(equality_resolution,[],[f199]) ).
fof(f365,plain,
! [X1] : ~ aElementOf0(X1,slcrc0),
inference(equality_resolution,[],[f198]) ).
fof(f392,plain,
! [X3,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| aSubsetOf0(X3,X0)
| ~ aElementOf0(X3,slbdtsldtrb0(X0,X1)) ),
inference(equality_resolution,[],[f292]) ).
fof(f393,plain,
! [X3,X0,X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aSet0(X0)
| sbrdtbr0(X3) = X1
| ~ aElementOf0(X3,slbdtsldtrb0(X0,X1)) ),
inference(equality_resolution,[],[f291]) ).
fof(f410,plain,
! [X0] :
( ~ aElementOf0(sK0(X0),X0)
| ~ aSet0(X0)
| slcrc0 = X0 ),
inference(consistent_polarity_flipping,[],[f200]) ).
fof(f411,plain,
! [X1] : aElementOf0(X1,slcrc0),
inference(consistent_polarity_flipping,[],[f365]) ).
fof(f414,plain,
! [X2,X0,X1] :
( ~ aSubsetOf0(X1,X0)
| aElementOf0(X2,X1)
| ~ aElementOf0(X2,X0)
| ~ aSet0(X0) ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f438,plain,
~ aElementOf0(xK,szNzAzT0),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f490,plain,
! [X3,X0,X1] :
( aElementOf0(X3,slbdtsldtrb0(X0,X1))
| ~ aSet0(X0)
| aSubsetOf0(X3,X0)
| aElementOf0(X1,szNzAzT0) ),
inference(consistent_polarity_flipping,[],[f392]) ).
fof(f491,plain,
! [X3,X0,X1] :
( aElementOf0(X3,slbdtsldtrb0(X0,X1))
| ~ aSet0(X0)
| sbrdtbr0(X3) = X1
| aElementOf0(X1,szNzAzT0) ),
inference(consistent_polarity_flipping,[],[f393]) ).
fof(f516,plain,
! [X0,X1] :
( ~ aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))
| aElementOf0(X1,szDzozmdt0(X0))
| aFunction0(X0) ),
inference(consistent_polarity_flipping,[],[f322]) ).
fof(f529,plain,
~ isCountable0(xS),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f530,plain,
~ aFunction0(xc),
inference(consistent_polarity_flipping,[],[f341]) ).
fof(f535,plain,
~ aElementOf0(slcrc0,slbdtsldtrb0(xS,xK)),
inference(consistent_polarity_flipping,[],[f362]) ).
fof(f536,plain,
! [X0] :
( aElementOf0(X0,slbdtsldtrb0(xS,xK))
| sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0) ),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f537,plain,
! [X0,X1] :
( sdtlpdtrp0(xc,sK21(X0,X1)) != X0
| isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| aElementOf0(X0,xT) ),
inference(consistent_polarity_flipping,[],[f350]) ).
fof(f538,plain,
! [X0,X1] :
( ~ aElementOf0(sK21(X0,X1),slbdtsldtrb0(X1,xK))
| isCountable0(X1)
| ~ aSubsetOf0(X1,xS)
| aElementOf0(X0,xT) ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f546,definition,
( spl22_2
<=> aSet0(slcrc0) ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f547,plain,
( aSet0(slcrc0)
| ~ spl22_2 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f555,plain,
spl22_2,
inference(avatar_split_clause,[],[f364,f546]) ).
fof(f558,plain,
~ aElementOf0(slcrc0,szDzozmdt0(xc)),
inference(superposition,[],[f535,f340]) ).
fof(f559,plain,
! [X0] :
( ~ aElementOf0(sK21(X0,xS),szDzozmdt0(xc))
| isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| aElementOf0(X0,xT) ),
inference(superposition,[],[f538,f340]) ).
fof(f560,plain,
! [X0] :
( ~ aElementOf0(sK21(X0,xS),szDzozmdt0(xc))
| ~ aSubsetOf0(xS,xS)
| aElementOf0(X0,xT) ),
inference(forward_subsumption_resolution,[],[f559,f529]) ).
fof(f562,definition,
( spl22_4
<=> aSubsetOf0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f563,plain,
( aSubsetOf0(xS,xS)
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f564,plain,
( ~ aSubsetOf0(xS,xS)
| spl22_4 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl22_5
<=> ! [X0] :
( ~ aElementOf0(sK21(X0,xS),szDzozmdt0(xc))
| aElementOf0(X0,xT) ) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f567,plain,
( ! [X0] :
( ~ aElementOf0(sK21(X0,xS),szDzozmdt0(xc))
| aElementOf0(X0,xT) )
| ~ spl22_5 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f568,plain,
( ~ spl22_4
| spl22_5 ),
inference(avatar_split_clause,[],[f560,f566,f562]) ).
fof(f569,plain,
( ~ aSet0(xS)
| spl22_4 ),
inference(resolution,[],[f564,f209]) ).
fof(f575,plain,
( aSet0(xS)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[],[f207,f338]) ).
fof(f577,plain,
( aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aSet0(xT) ),
inference(resolution,[],[f207,f339]) ).
fof(f579,plain,
aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))),
inference(forward_subsumption_resolution,[],[f577,f335]) ).
fof(f580,plain,
( ~ aSet0(szNzAzT0)
| spl22_4 ),
inference(forward_subsumption_resolution,[],[f575,f569]) ).
fof(f581,plain,
( $false
| spl22_4 ),
inference(forward_subsumption_resolution,[],[f580,f237]) ).
fof(f582,plain,
spl22_4,
inference(avatar_contradiction_clause,[],[f581]) ).
fof(f588,definition,
( spl22_7
<=> aSet0(xS) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f589,plain,
( aSet0(xS)
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f592,plain,
aSet0(xS),
inference(forward_subsumption_resolution,[],[f575,f237]) ).
fof(f593,plain,
spl22_7,
inference(avatar_split_clause,[],[f592,f588]) ).
fof(f733,plain,
! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X0,xT)
| ~ aSet0(xT) ),
inference(resolution,[],[f414,f339]) ).
fof(f738,plain,
! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X0,xT) ),
inference(forward_subsumption_resolution,[],[f733,f335]) ).
fof(f791,plain,
! [X0] :
( aElementOf0(X0,szDzozmdt0(xc))
| sdtlpdtrp0(xc,X0) = sdtlpdtrp0(xc,slcrc0) ),
inference(forward_demodulation,[],[f536,f340]) ).
fof(f811,plain,
( ! [X0] :
( aElementOf0(X0,xT)
| sdtlpdtrp0(xc,slcrc0) = sdtlpdtrp0(xc,sK21(X0,xS)) )
| ~ spl22_5 ),
inference(resolution,[],[f791,f567]) ).
fof(f826,plain,
( sdtlpdtrp0(xc,slcrc0) = sdtlpdtrp0(xc,sK21(sK0(xT),xS))
| ~ aSet0(xT)
| slcrc0 = xT
| ~ spl22_5 ),
inference(resolution,[],[f811,f410]) ).
fof(f827,plain,
( sdtlpdtrp0(xc,slcrc0) = sdtlpdtrp0(xc,sK21(sK0(xT),xS))
| slcrc0 = xT
| ~ spl22_5 ),
inference(forward_subsumption_resolution,[],[f826,f335]) ).
fof(f829,definition,
( spl22_25
<=> slcrc0 = xT ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f831,plain,
( slcrc0 = xT
| ~ spl22_25 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f833,definition,
( spl22_26
<=> sdtlpdtrp0(xc,slcrc0) = sdtlpdtrp0(xc,sK21(sK0(xT),xS)) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f835,plain,
( sdtlpdtrp0(xc,slcrc0) = sdtlpdtrp0(xc,sK21(sK0(xT),xS))
| ~ spl22_26 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f836,plain,
( spl22_25
| spl22_26
| ~ spl22_5 ),
inference(avatar_split_clause,[],[f827,f566,f833,f829]) ).
fof(f841,plain,
( aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),slcrc0)
| ~ spl22_25 ),
inference(superposition,[],[f339,f831]) ).
fof(f867,plain,
( ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X0,slcrc0)
| ~ aSet0(slcrc0) )
| ~ spl22_25 ),
inference(resolution,[],[f841,f414]) ).
fof(f869,plain,
( ! [X0] :
( aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ aElementOf0(X0,slcrc0) )
| ~ spl22_2
| ~ spl22_25 ),
inference(forward_subsumption_resolution,[],[f867,f547]) ).
fof(f870,plain,
( ! [X0] : aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ spl22_2
| ~ spl22_25 ),
inference(forward_subsumption_resolution,[],[f869,f411]) ).
fof(f922,definition,
( spl22_29
<=> slcrc0 = sdtlcdtrc0(xc,szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f924,plain,
( slcrc0 = sdtlcdtrc0(xc,szDzozmdt0(xc))
| ~ spl22_29 ),
inference(avatar_component_clause,[],[f922]) ).
fof(f935,plain,
( ~ aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc)))
| slcrc0 = sdtlcdtrc0(xc,szDzozmdt0(xc))
| ~ spl22_2
| ~ spl22_25 ),
inference(resolution,[],[f870,f410]) ).
fof(f938,plain,
( slcrc0 = sdtlcdtrc0(xc,szDzozmdt0(xc))
| ~ spl22_2
| ~ spl22_25 ),
inference(forward_subsumption_resolution,[],[f935,f579]) ).
fof(f939,plain,
( spl22_29
| ~ spl22_2
| ~ spl22_25 ),
inference(avatar_split_clause,[],[f938,f829,f546,f922]) ).
fof(f953,plain,
! [X0,X1] :
( ~ aSet0(X0)
| aSubsetOf0(sK21(X1,X0),X0)
| aElementOf0(xK,szNzAzT0)
| isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| aElementOf0(X1,xT) ),
inference(resolution,[],[f490,f538]) ).
fof(f956,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,xS)
| aSubsetOf0(sK21(X1,X0),X0)
| isCountable0(X0)
| ~ aSet0(X0)
| aElementOf0(X1,xT) ),
inference(forward_subsumption_resolution,[],[f953,f438]) ).
fof(f967,definition,
( spl22_33
<=> aElementOf0(sK21(sK0(xT),xS),szDzozmdt0(xc)) ),
introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).
fof(f968,plain,
( ~ aElementOf0(sK21(sK0(xT),xS),szDzozmdt0(xc))
| spl22_33 ),
inference(avatar_component_clause,[],[f967]) ).
fof(f969,plain,
( aElementOf0(sK21(sK0(xT),xS),szDzozmdt0(xc))
| ~ spl22_33 ),
inference(avatar_component_clause,[],[f967]) ).
fof(f977,definition,
( spl22_35
<=> aElementOf0(sK0(xT),xT) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f979,plain,
( aElementOf0(sK0(xT),xT)
| ~ spl22_35 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f1097,plain,
! [X0,X1] :
( ~ aSet0(X0)
| xK = sbrdtbr0(sK21(X1,X0))
| aElementOf0(xK,szNzAzT0)
| isCountable0(X0)
| ~ aSubsetOf0(X0,xS)
| aElementOf0(X1,xT) ),
inference(resolution,[],[f491,f538]) ).
fof(f1100,plain,
! [X0,X1] :
( ~ aSubsetOf0(X0,xS)
| xK = sbrdtbr0(sK21(X1,X0))
| isCountable0(X0)
| ~ aSet0(X0)
| aElementOf0(X1,xT) ),
inference(forward_subsumption_resolution,[],[f1097,f438]) ).
fof(f1109,plain,
( ! [X0] :
( ~ aElementOf0(sdtlpdtrp0(xc,X0),slcrc0)
| aElementOf0(X0,szDzozmdt0(xc))
| aFunction0(xc) )
| ~ spl22_29 ),
inference(superposition,[],[f516,f924]) ).
fof(f1110,plain,
( ! [X0] :
( ~ aElementOf0(sdtlpdtrp0(xc,X0),slcrc0)
| aElementOf0(X0,szDzozmdt0(xc)) )
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f1109,f530]) ).
fof(f1111,plain,
( ! [X0] : aElementOf0(X0,szDzozmdt0(xc))
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f1110,f411]) ).
fof(f1188,plain,
( aElementOf0(sK0(xT),xT)
| ~ spl22_5
| ~ spl22_33 ),
inference(resolution,[],[f969,f567]) ).
fof(f1189,plain,
( spl22_35
| ~ spl22_5
| ~ spl22_33 ),
inference(avatar_split_clause,[],[f1188,f967,f566,f977]) ).
fof(f1190,plain,
( ~ aSet0(xT)
| slcrc0 = xT
| ~ spl22_35 ),
inference(resolution,[],[f979,f410]) ).
fof(f1191,plain,
( slcrc0 = xT
| ~ spl22_35 ),
inference(forward_subsumption_resolution,[],[f1190,f335]) ).
fof(f1281,plain,
( ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aElementOf0(sK21(sK0(xT),xS),szDzozmdt0(xc))
| aFunction0(xc)
| ~ spl22_26 ),
inference(superposition,[],[f516,f835]) ).
fof(f1283,plain,
( ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| aFunction0(xc)
| ~ spl22_26
| spl22_33 ),
inference(forward_subsumption_resolution,[],[f1281,f968]) ).
fof(f1286,plain,
( ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),sdtlcdtrc0(xc,szDzozmdt0(xc)))
| ~ spl22_26
| spl22_33 ),
inference(forward_subsumption_resolution,[],[f1283,f530]) ).
fof(f1316,plain,
( ! [X0] :
( aSubsetOf0(sK21(X0,xS),xS)
| isCountable0(xS)
| ~ aSet0(xS)
| aElementOf0(X0,xT) )
| ~ spl22_4 ),
inference(resolution,[],[f956,f563]) ).
fof(f1318,plain,
( ! [X0] :
( aSubsetOf0(sK21(X0,xS),xS)
| ~ aSet0(xS)
| aElementOf0(X0,xT) )
| ~ spl22_4 ),
inference(forward_subsumption_resolution,[],[f1316,f529]) ).
fof(f1320,plain,
( ! [X0] :
( aSubsetOf0(sK21(X0,xS),xS)
| aElementOf0(X0,xT) )
| ~ spl22_4
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f1318,f589]) ).
fof(f1344,plain,
( ! [X0] :
( aElementOf0(X0,xT)
| aSet0(sK21(X0,xS))
| ~ aSet0(xS) )
| ~ spl22_4
| ~ spl22_7 ),
inference(resolution,[],[f1320,f207]) ).
fof(f1345,plain,
( ! [X0] :
( aSet0(sK21(X0,xS))
| aElementOf0(X0,xT) )
| ~ spl22_4
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f1344,f589]) ).
fof(f1664,plain,
( ! [X0] :
( xK = sbrdtbr0(sK21(X0,xS))
| isCountable0(xS)
| ~ aSet0(xS)
| aElementOf0(X0,xT) )
| ~ spl22_4 ),
inference(resolution,[],[f1100,f563]) ).
fof(f1668,plain,
( ! [X0] :
( xK = sbrdtbr0(sK21(X0,xS))
| ~ aSet0(xS)
| aElementOf0(X0,xT) )
| ~ spl22_4 ),
inference(forward_subsumption_resolution,[],[f1664,f529]) ).
fof(f1670,plain,
( ! [X0] :
( aElementOf0(X0,xT)
| xK = sbrdtbr0(sK21(X0,xS)) )
| ~ spl22_4
| ~ spl22_7 ),
inference(forward_subsumption_resolution,[],[f1668,f589]) ).
fof(f1869,plain,
( ~ aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_26
| spl22_33 ),
inference(resolution,[],[f738,f1286]) ).
fof(f1912,plain,
( xK = sbrdtbr0(sK21(sdtlpdtrp0(xc,slcrc0),xS))
| ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33 ),
inference(resolution,[],[f1869,f1670]) ).
fof(f2965,plain,
( xK != xK
| slcrc0 = sK21(sdtlpdtrp0(xc,slcrc0),xS)
| ~ aSet0(sK21(sdtlpdtrp0(xc,slcrc0),xS))
| ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33 ),
inference(superposition,[],[f357,f1912]) ).
fof(f2971,plain,
( slcrc0 = sK21(sdtlpdtrp0(xc,slcrc0),xS)
| ~ aSet0(sK21(sdtlpdtrp0(xc,slcrc0),xS))
| ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33 ),
inference(trivial_inequality_removal,[],[f2965]) ).
fof(f2973,definition,
( spl22_145
<=> aSet0(sK21(sdtlpdtrp0(xc,slcrc0),xS)) ),
introduced(definition,[new_symbols(definition,[spl22_145])],[avatar_definition]) ).
fof(f2975,plain,
( ~ aSet0(sK21(sdtlpdtrp0(xc,slcrc0),xS))
| spl22_145 ),
inference(avatar_component_clause,[],[f2973]) ).
fof(f2987,definition,
( spl22_148
<=> slcrc0 = sK21(sdtlpdtrp0(xc,slcrc0),xS) ),
introduced(definition,[new_symbols(definition,[spl22_148])],[avatar_definition]) ).
fof(f2989,plain,
( slcrc0 = sK21(sdtlpdtrp0(xc,slcrc0),xS)
| ~ spl22_148 ),
inference(avatar_component_clause,[],[f2987]) ).
fof(f2990,plain,
( ~ spl22_145
| spl22_148
| ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33 ),
inference(avatar_split_clause,[],[f2971,f967,f833,f588,f562,f2987,f2973]) ).
fof(f3037,plain,
( aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_4
| ~ spl22_7
| spl22_145 ),
inference(resolution,[],[f2975,f1345]) ).
fof(f3038,plain,
( $false
| ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33
| spl22_145 ),
inference(forward_subsumption_resolution,[],[f3037,f1869]) ).
fof(f3039,plain,
( ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33
| spl22_145 ),
inference(avatar_contradiction_clause,[],[f3038]) ).
fof(f3292,plain,
( sdtlpdtrp0(xc,slcrc0) != sdtlpdtrp0(xc,slcrc0)
| isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_148 ),
inference(superposition,[],[f537,f2989]) ).
fof(f3293,plain,
( isCountable0(xS)
| ~ aSubsetOf0(xS,xS)
| aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_148 ),
inference(trivial_inequality_removal,[],[f3292]) ).
fof(f3294,plain,
( ~ aSubsetOf0(xS,xS)
| aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_148 ),
inference(forward_subsumption_resolution,[],[f3293,f529]) ).
fof(f3295,plain,
( aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)
| ~ spl22_4
| ~ spl22_148 ),
inference(forward_subsumption_resolution,[],[f3294,f563]) ).
fof(f3296,plain,
( $false
| ~ spl22_4
| ~ spl22_26
| spl22_33
| ~ spl22_148 ),
inference(forward_subsumption_resolution,[],[f3295,f1869]) ).
fof(f3297,plain,
( ~ spl22_4
| ~ spl22_26
| spl22_33
| ~ spl22_148 ),
inference(avatar_contradiction_clause,[],[f3296]) ).
fof(f3311,plain,
( spl22_25
| ~ spl22_35 ),
inference(avatar_split_clause,[],[f1191,f977,f829]) ).
fof(f3500,plain,
( $false
| ~ spl22_29 ),
inference(backward_subsumption_resolution,[],[f558,f1111]) ).
fof(f3507,plain,
~ spl22_29,
inference(avatar_contradiction_clause,[],[f3500]) ).
cnf(s3,plain,
spl22_2,
inference(sat_conversion,[],[f555]) ).
cnf(s4,plain,
( ~ spl22_4
| spl22_5 ),
inference(sat_conversion,[],[f568]) ).
cnf(s5,plain,
spl22_4,
inference(sat_conversion,[],[f582]) ).
cnf(s7,plain,
spl22_7,
inference(sat_conversion,[],[f593]) ).
cnf(s25,plain,
( ~ spl22_5
| spl22_25
| spl22_26 ),
inference(sat_conversion,[],[f836]) ).
cnf(s30,plain,
( ~ spl22_2
| ~ spl22_25
| spl22_29 ),
inference(sat_conversion,[],[f939]) ).
cnf(s43,plain,
( ~ spl22_5
| ~ spl22_33
| spl22_35 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s134,plain,
( ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33
| ~ spl22_145
| spl22_148 ),
inference(sat_conversion,[],[f2990]) ).
cnf(s137,plain,
( ~ spl22_4
| ~ spl22_7
| ~ spl22_26
| spl22_33
| spl22_145 ),
inference(sat_conversion,[],[f3039]) ).
cnf(s150,plain,
( ~ spl22_4
| ~ spl22_26
| spl22_33
| ~ spl22_148 ),
inference(sat_conversion,[],[f3297]) ).
cnf(s156,plain,
( spl22_25
| ~ spl22_35 ),
inference(sat_conversion,[],[f3311]) ).
cnf(s185,plain,
~ spl22_29,
inference(sat_conversion,[],[f3507]) ).
cnf(s191,plain,
( ~ spl22_2
| ~ spl22_25 ),
inference(rat,[],[s30,s185]) ).
cnf(s208,plain,
spl22_5,
inference(rat,[],[s4,s5]) ).
cnf(s211,plain,
~ spl22_25,
inference(rat,[],[s191,s3]) ).
cnf(s215,plain,
~ spl22_35,
inference(rat,[],[s156,s211]) ).
cnf(s216,plain,
spl22_26,
inference(rat,[],[s25,s208,s211]) ).
cnf(s218,plain,
~ spl22_33,
inference(rat,[],[s43,s208,s215]) ).
cnf(s224,plain,
~ spl22_148,
inference(rat,[],[s150,s216,s5,s218]) ).
cnf(s225,plain,
spl22_145,
inference(rat,[],[s137,s216,s5,s7,s218]) ).
cnf(s226,plain,
$false,
inference(rat,[],[s134,s224,s216,s5,s7,s225,s218]) ).
fof(f3516,plain,
$false,
inference(avatar_sat_refutation,[],[s226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM566+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 20:31:19 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.32 Running first-order model finding
% 0.08/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.41 % (2712027)Will run a generic schedule for satisfiability detection.
% 0.08/0.41 % (2712033)% WARNING: option uhcvi not known.
% 0.08/0.41 % (2712038)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2599821801:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.41 % (2712037)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2069580739:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.41 % (2712035)dis+10_1_sil=32000:sp=arity:random_seed=3889472044:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.41 % (2712032)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2374829299_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.41 % (2712034)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2222850504:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.41 % (2712033)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=197953457:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.41 % (2712036)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3691517982:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.41 % TRYING [1]
% 0.08/0.41 % TRYING [2]
% 0.08/0.41 % TRYING [3]
% 0.08/0.41 % TRYING [4]
% 0.08/0.41 % (2712035)Instruction limit reached!
% 0.08/0.41 % (2712035)------------------------------
% 0.08/0.41 % (2712035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.41 % (2712035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.41 % (2712035)CaDiCaL version: 2.1.3
% 0.08/0.41 % (2712035)Termination reason: Instruction limit
% 0.08/0.41 % (2712035)Termination phase: Saturation
% 0.08/0.41 % (2712035)Time elapsed: 0.038 s
% 0.08/0.41 % (2712035)Peak memory usage: 13 MB
% 0.08/0.41 % (2712035)Instructions burned: 103 (million)
% 0.08/0.41 % (2712036)Instruction limit reached!
% 0.08/0.41 % (2712036)------------------------------
% 0.08/0.41 % (2712036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.41 % (2712036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.41 % (2712036)CaDiCaL version: 2.1.3
% 0.08/0.41 % (2712036)Termination reason: Instruction limit
% 0.08/0.41 % (2712036)Termination phase: Saturation
% 0.08/0.41 % (2712036)Time elapsed: 0.041 s
% 0.08/0.41 % (2712036)Peak memory usage: 13 MB
% 0.08/0.41 % (2712036)Instructions burned: 117 (million)
% 0.08/0.41 % (2712037)Instruction limit reached!
% 0.08/0.41 % (2712037)------------------------------
% 0.08/0.41 % (2712037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.41 % (2712037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.41 % (2712037)CaDiCaL version: 2.1.3
% 0.08/0.41 % (2712037)Termination reason: Instruction limit
% 0.08/0.41 % (2712037)Termination phase: Saturation
% 0.08/0.41 % (2712037)Time elapsed: 0.046 s
% 0.08/0.41 % (2712037)Peak memory usage: 13 MB
% 0.08/0.41 % (2712037)Instructions burned: 132 (million)
% 0.08/0.41 % (2712033) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2712027-2712033"...
% 0.08/0.41 % (2712046)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1169329649:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.08/0.41 % (2712033)...printing done.
% 0.08/0.41 % (2712033)Refutation found. Thanks to Tanya!
% 0.08/0.41 % SZS status Theorem for theBenchmark
% 0.08/0.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/0.41 % (2712033)------------------------------
% 0.08/0.41 % (2712033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.41 % (2712033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.41 % (2712033)CaDiCaL version: 2.1.3
% 0.08/0.41 % (2712033)Termination reason: Refutation
% 0.08/0.41 % (2712033)Time elapsed: 0.051 s
% 0.08/0.41 % (2712033)Peak memory usage: 14 MB
% 0.08/0.41 % (2712033)Instructions burned: 124 (million)
% 0.08/0.41 % (2712027)Success in time 0.079 s
% 0.08/0.41 % Vampire exiting
%------------------------------------------------------------------------------