%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM496+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:24:32 PM UTC 2026
% Result : Theorem 28.95s 5.22s
% Output : Refutation 28.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 11
% Syntax : Number of formulae : 82 ( 14 unt; 1 def)
% Number of atoms : 404 ( 146 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 485 ( 163 ~; 192 |; 118 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 91 ( 65 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f32,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( doDivides0(X0,X1)
& doDivides0(X1,X2) )
=> doDivides0(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivTrans) ).
fof(f33,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( doDivides0(X0,X1)
& doDivides0(X0,X2) )
=> doDivides0(X0,sdtpldt0(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivSum) ).
fof(f37,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& doDivides0(X1,X0) )
=> ( X1 = sz10
| X1 = X0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefPrime) ).
fof(f38,axiom,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ? [X1] :
( aNaturalNumber0(X1)
& doDivides0(X1,X0)
& isPrime0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPrimDiv) ).
fof(f39,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1837) ).
fof(f41,axiom,
( xp != sz00
& xp != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtasdt0(X0,X1) )
| doDivides0(X0,xp) ) )
=> ( X0 = sz10
| X0 = xp ) )
& isPrime0(xp)
& ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X0) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1860) ).
fof(f43,axiom,
( aNaturalNumber0(xr)
& sdtpldt0(xp,xr) = xn
& xr = sdtmndt0(xn,xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1883) ).
fof(f46,axiom,
( ( ? [X0] :
( aNaturalNumber0(X0)
& xr = sdtasdt0(xp,X0) )
& doDivides0(xp,xr) )
| ( ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
& doDivides0(xp,xm) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2027) ).
fof(f47,conjecture,
( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
| doDivides0(xp,xn)
| ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
| doDivides0(xp,xm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f48,negated_conjecture,
~ ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
| doDivides0(xp,xn)
| ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
| doDivides0(xp,xm) ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f52,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtasdt0(X0,X1) )
| doDivides0(X0,xp) ) )
=> ( X0 = sz10
| X0 = xp ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(rectify,[],[f41]) ).
fof(f53,plain,
( ( ? [X0] :
( aNaturalNumber0(X0)
& xr = sdtasdt0(xp,X0) )
& doDivides0(xp,xr) )
| ( ? [X1] :
( aNaturalNumber0(X1)
& xm = sdtasdt0(xp,X1) )
& doDivides0(xp,xm) ) ),
inference(rectify,[],[f46]) ).
fof(f54,plain,
~ ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
| doDivides0(xp,xn)
| ? [X1] :
( aNaturalNumber0(X1)
& xm = sdtasdt0(xp,X1) )
| doDivides0(xp,xm) ),
inference(rectify,[],[f48]) ).
fof(f105,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f106,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| ~ doDivides0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f33]) ).
fof(f108,plain,
! [X0,X1,X2] :
( doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| ~ doDivides0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f107]) ).
fof(f115,plain,
! [X0] :
( ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) ) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f116,plain,
! [X0] :
( ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) ) )
| ~ aNaturalNumber0(X0) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& doDivides0(X1,X0)
& isPrime0(X1) )
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(ennf_transformation,[],[f38]) ).
fof(f118,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& doDivides0(X1,X0)
& isPrime0(X1) )
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(flattening,[],[f117]) ).
fof(f121,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(ennf_transformation,[],[f52]) ).
fof(f122,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtasdt0(xp,X0) )
& ~ doDivides0(xp,xn)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| xm != sdtasdt0(xp,X1) )
& ~ doDivides0(xp,xm) ),
inference(ennf_transformation,[],[f54]) ).
fof(f127,definition,
( ( ? [X1] :
( aNaturalNumber0(X1)
& xm = sdtasdt0(xp,X1) )
& doDivides0(xp,xm) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f128,plain,
( ( ? [X0] :
( aNaturalNumber0(X0)
& xr = sdtasdt0(xp,X0) )
& doDivides0(xp,xr) )
| sP2 ),
inference(definition_folding,[],[f53,f127]) ).
fof(f139,plain,
! [X0] :
( ( ( isPrime0(X0)
| sz00 = X0
| sz10 = X0
| ? [X1] :
( sz10 != X1
& X0 != X1
& aNaturalNumber0(X1)
& doDivides0(X1,X0) ) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) )
| ~ isPrime0(X0) ) )
| ~ aNaturalNumber0(X0) ),
inference(nnf_transformation,[],[f116]) ).
fof(f140,plain,
! [X0] :
( ( ( isPrime0(X0)
| sz00 = X0
| sz10 = X0
| ? [X1] :
( sz10 != X1
& X0 != X1
& aNaturalNumber0(X1)
& doDivides0(X1,X0) ) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) )
| ~ isPrime0(X0) ) )
| ~ aNaturalNumber0(X0) ),
inference(flattening,[],[f139]) ).
fof(f141,plain,
! [X0] :
( ( ( isPrime0(X0)
| sz00 = X0
| sz10 = X0
| ? [X1] :
( sz10 != X1
& X0 != X1
& aNaturalNumber0(X1)
& doDivides0(X1,X0) ) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X2] :
( sz10 = X2
| X0 = X2
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X0) ) )
| ~ isPrime0(X0) ) )
| ~ aNaturalNumber0(X0) ),
inference(rectify,[],[f140]) ).
fof(f142,plain,
! [X0] :
( ( ( isPrime0(X0)
| sz00 = X0
| sz10 = X0
| ( sz10 != sK5(X0)
& sK5(X0) != X0
& aNaturalNumber0(sK5(X0))
& doDivides0(sK5(X0),X0) ) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X2] :
( sz10 = X2
| X0 = X2
| ~ aNaturalNumber0(X2)
| ~ doDivides0(X2,X0) ) )
| ~ isPrime0(X0) ) )
| ~ aNaturalNumber0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X1,sK5(X0))],[f141]) ).
fof(f143,plain,
! [X0] :
( ( aNaturalNumber0(sK6(X0))
& doDivides0(sK6(X0),X0)
& isPrime0(sK6(X0)) )
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X1,sK6(X0))],[f118]) ).
fof(f152,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& aNaturalNumber0(sK11)
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK11)
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11)],[f122]) ).
fof(f156,plain,
( ( ? [X1] :
( aNaturalNumber0(X1)
& xm = sdtasdt0(xp,X1) )
& doDivides0(xp,xm) )
| ~ sP2 ),
inference(nnf_transformation,[],[f127]) ).
fof(f157,plain,
( ( ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
& doDivides0(xp,xm) )
| ~ sP2 ),
inference(rectify,[],[f156]) ).
fof(f158,plain,
( ( aNaturalNumber0(sK15)
& xm = sdtasdt0(xp,sK15)
& doDivides0(xp,xm) )
| ~ sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X0,sK15)],[f157]) ).
fof(f159,plain,
( ( aNaturalNumber0(sK16)
& xr = sdtasdt0(xp,sK16)
& doDivides0(xp,xr) )
| sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X0,sK16)],[f128]) ).
fof(f162,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| doDivides0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f106]) ).
fof(f214,plain,
! [X2,X0,X1] :
( doDivides0(X0,sdtpldt0(X1,X2))
| ~ doDivides0(X0,X1)
| ~ doDivides0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f108]) ).
fof(f219,plain,
! [X0] :
( sz10 != X0
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f225,plain,
! [X0] :
( isPrime0(sK6(X0))
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(cnf_transformation,[],[f143]) ).
fof(f226,plain,
! [X0] :
( doDivides0(sK6(X0),X0)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(cnf_transformation,[],[f143]) ).
fof(f227,plain,
! [X0] :
( aNaturalNumber0(sK6(X0))
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(cnf_transformation,[],[f143]) ).
fof(f228,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f39]) ).
fof(f251,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| xp = X0
| ~ aNaturalNumber0(X0)
| sz10 = X0 ),
inference(cnf_transformation,[],[f152]) ).
fof(f253,plain,
sz10 != xp,
inference(cnf_transformation,[],[f152]) ).
fof(f254,plain,
sz00 != xp,
inference(cnf_transformation,[],[f152]) ).
fof(f259,plain,
xn = sdtpldt0(xp,xr),
inference(cnf_transformation,[],[f43]) ).
fof(f260,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[],[f43]) ).
fof(f268,plain,
( doDivides0(xp,xm)
| ~ sP2 ),
inference(cnf_transformation,[],[f158]) ).
fof(f271,plain,
( doDivides0(xp,xr)
| sP2 ),
inference(cnf_transformation,[],[f159]) ).
fof(f274,plain,
~ doDivides0(xp,xm),
inference(cnf_transformation,[],[f123]) ).
fof(f276,plain,
~ doDivides0(xp,xn),
inference(cnf_transformation,[],[f123]) ).
fof(f289,plain,
( ~ isPrime0(sz10)
| ~ aNaturalNumber0(sz10) ),
inference(equality_resolution,[],[f219]) ).
fof(f291,plain,
~ sP2,
inference(forward_subsumption_resolution,[],[f268,f274]) ).
fof(f628,plain,
( ~ aNaturalNumber0(xp)
| sz00 = xp
| sz10 = xp
| xp = sK6(xp)
| ~ aNaturalNumber0(sK6(xp))
| sz10 = sK6(xp) ),
inference(resolution,[],[f226,f251]) ).
fof(f629,plain,
( ~ aNaturalNumber0(xp)
| sz00 = xp
| sz10 = xp
| xp = sK6(xp)
| sz10 = sK6(xp) ),
inference(forward_subsumption_resolution,[],[f628,f227]) ).
fof(f630,plain,
( sz00 = xp
| sz10 = xp
| xp = sK6(xp)
| sz10 = sK6(xp) ),
inference(forward_subsumption_resolution,[],[f629,f228]) ).
fof(f631,plain,
( sz10 = xp
| xp = sK6(xp)
| sz10 = sK6(xp) ),
inference(forward_subsumption_resolution,[],[f630,f254]) ).
fof(f632,plain,
( xp = sK6(xp)
| sz10 = sK6(xp) ),
inference(forward_subsumption_resolution,[],[f631,f253]) ).
fof(f1087,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| doDivides0(X0,xr)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| sP2 ),
inference(resolution,[],[f213,f271]) ).
fof(f1115,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| doDivides0(X0,xr)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| sP2 ),
inference(forward_subsumption_resolution,[],[f1087,f228]) ).
fof(f1123,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| doDivides0(X0,xr)
| ~ aNaturalNumber0(X0)
| sP2 ),
inference(forward_subsumption_resolution,[],[f1115,f260]) ).
fof(f1125,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| doDivides0(X0,xr)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1123,f291]) ).
fof(f1435,plain,
! [X0] :
( doDivides0(X0,xn)
| ~ doDivides0(X0,xp)
| ~ doDivides0(X0,xr)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr) ),
inference(superposition,[],[f214,f259]) ).
fof(f1452,plain,
! [X0] :
( doDivides0(X0,xn)
| ~ doDivides0(X0,xp)
| ~ doDivides0(X0,xr)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr) ),
inference(forward_subsumption_resolution,[],[f1435,f228]) ).
fof(f1459,plain,
! [X0] :
( doDivides0(X0,xn)
| ~ doDivides0(X0,xp)
| ~ doDivides0(X0,xr)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1452,f260]) ).
fof(f1461,plain,
! [X0] :
( ~ doDivides0(X0,xp)
| doDivides0(X0,xn)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1459,f1125]) ).
fof(f1463,plain,
( doDivides0(sK6(xp),xn)
| ~ aNaturalNumber0(sK6(xp))
| ~ aNaturalNumber0(xp)
| sz00 = xp
| sz10 = xp ),
inference(resolution,[],[f1461,f226]) ).
fof(f1466,plain,
( doDivides0(sK6(xp),xn)
| ~ aNaturalNumber0(xp)
| sz00 = xp
| sz10 = xp ),
inference(forward_subsumption_resolution,[],[f1463,f227]) ).
fof(f1468,plain,
( doDivides0(sK6(xp),xn)
| sz00 = xp
| sz10 = xp ),
inference(forward_subsumption_resolution,[],[f1466,f228]) ).
fof(f1469,plain,
( doDivides0(sK6(xp),xn)
| sz10 = xp ),
inference(forward_subsumption_resolution,[],[f1468,f254]) ).
fof(f1470,plain,
doDivides0(sK6(xp),xn),
inference(forward_subsumption_resolution,[],[f1469,f253]) ).
fof(f7301,plain,
( doDivides0(xp,xn)
| sz10 = sK6(xp) ),
inference(superposition,[],[f1470,f632]) ).
fof(f7311,plain,
sz10 = sK6(xp),
inference(forward_subsumption_resolution,[],[f7301,f276]) ).
fof(f7322,plain,
( isPrime0(sz10)
| ~ aNaturalNumber0(xp)
| sz00 = xp
| sz10 = xp ),
inference(superposition,[],[f225,f7311]) ).
fof(f7323,plain,
( isPrime0(sz10)
| sz00 = xp
| sz10 = xp ),
inference(forward_subsumption_resolution,[],[f7322,f228]) ).
fof(f7326,plain,
( isPrime0(sz10)
| sz10 = xp ),
inference(forward_subsumption_resolution,[],[f7323,f254]) ).
fof(f7328,plain,
isPrime0(sz10),
inference(forward_subsumption_resolution,[],[f7326,f253]) ).
fof(f7330,plain,
~ aNaturalNumber0(sz10),
inference(resolution,[],[f7328,f289]) ).
fof(f7331,plain,
$false,
inference(forward_subsumption_resolution,[],[f7330,f162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM496+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 20:11:36 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.67/2.51 % (521135)Will run a generic schedule for satisfiability detection.
% 14.67/2.51 % (521142)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2031420305:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.67/2.51 % (521141)% WARNING: option uhcvi not known.
% 14.67/2.51 % (521140)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2055991944_2999 on theBenchmark for (2999ds/0Mi)
% 14.67/2.51 % (521143)dis+10_1_sil=32000:sp=arity:random_seed=1444543694:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.67/2.51 % (521141)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=24703645:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.67/2.51 % (521144)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=649873145:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.67/2.51 % (521145)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2983024311:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.67/2.51 % (521146)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1973059270:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.67/2.51 % Detected minimum model sizes of [3]
% 14.67/2.51 % Detected maximum model sizes of [max]
% 14.67/2.51 % TRYING [3]
% 14.67/2.51 % TRYING [4]
% 14.67/2.51 % TRYING [5]
% 14.67/2.51 % (521143)Instruction limit reached!
% 14.67/2.51 % (521143)------------------------------
% 14.67/2.51 % (521143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.51 % (521143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.51 % (521143)CaDiCaL version: 2.1.3
% 14.67/2.51 % (521143)Termination reason: Instruction limit
% 14.67/2.51 % (521143)Termination phase: Saturation
% 14.67/2.51 % (521143)Time elapsed: 0.057 s
% 14.67/2.51 % (521143)Peak memory usage: 12 MB
% 14.67/2.51 % (521143)Instructions burned: 103 (million)
% 14.67/2.51 % (521144)Instruction limit reached!
% 14.67/2.51 % (521144)------------------------------
% 14.67/2.51 % (521144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.51 % (521144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.51 % (521144)CaDiCaL version: 2.1.3
% 14.67/2.51 % (521144)Termination reason: Instruction limit
% 14.67/2.51 % (521144)Termination phase: Saturation
% 14.67/2.51 % (521144)Time elapsed: 0.062 s
% 14.67/2.51 % (521144)Peak memory usage: 13 MB
% 14.67/2.51 % (521144)Instructions burned: 117 (million)
% 14.67/2.51 % (521145)Instruction limit reached!
% 14.67/2.51 % (521145)------------------------------
% 14.67/2.51 % (521145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.51 % (521145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.51 % (521145)CaDiCaL version: 2.1.3
% 14.67/2.51 % (521145)Termination reason: Instruction limit
% 14.67/2.51 % (521145)Termination phase: Saturation
% 14.67/2.51 % (521145)Time elapsed: 0.072 s
% 14.67/2.51 % (521145)Peak memory usage: 13 MB
% 14.67/2.51 % (521145)Instructions burned: 132 (million)
% 14.67/2.51 % (521154)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3274559191:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.67/2.51 % (521155)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2211498484:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.67/2.51 % Detected minimum model sizes of [3]
% 14.67/2.51 % Detected maximum model sizes of [max]
% 14.67/2.51 % TRYING [3]
% 14.67/2.51 % (521156)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=592797708:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.67/2.51 % (521146)Instruction limit reached!
% 14.67/2.51 % (521146)------------------------------
% 14.67/2.51 % (521146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.51 % (521146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.51 % (521146)CaDiCaL version: 2.1.3
% 14.67/2.51 % (521146)Termination reason: Instruction limit
% 14.67/2.51 % (521146)Termination phase: Saturation
% 14.67/2.51 % (521146)Time elapsed: 0.096 s
% 14.67/2.51 % (521146)Peak memory usage: 14 MB
% 14.67/2.51 % (521146)Instructions burned: 160 (million)
% 14.67/2.51 % TRYING [4]
% 14.67/2.51 % (521160)ott-21_1_sil=16000:fs=off:random_seed=345548912:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.67/2.51 % TRYING [5]
% 14.67/2.51 % TRYING [6]
% 14.67/2.51 % (521155)Instruction limit reached!
% 14.67/2.51 % (521155)------------------------------
% 14.67/2.51 % (521155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521155)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521155)Termination reason: Instruction limit
% 28.95/5.22 % (521155)Termination phase: Saturation
% 28.95/5.22 % (521155)Time elapsed: 0.064 s
% 28.95/5.22 % (521155)Peak memory usage: 12 MB
% 28.95/5.22 % (521155)Instructions burned: 132 (million)
% 28.95/5.22 % (521162)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=778430302:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 28.95/5.22 % (521160)Instruction limit reached!
% 28.95/5.22 % (521160)------------------------------
% 28.95/5.22 % (521160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521160)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521160)Termination reason: Instruction limit
% 28.95/5.22 % (521160)Termination phase: Saturation
% 28.95/5.22 % (521160)Time elapsed: 0.093 s
% 28.95/5.22 % (521160)Peak memory usage: 13 MB
% 28.95/5.22 % (521160)Instructions burned: 180 (million)
% 28.95/5.22 % TRYING [6]
% 28.95/5.22 % (521164)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2523308806:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [3]
% 28.95/5.22 % TRYING [4]
% 28.95/5.22 % (521154)Instruction limit reached!
% 28.95/5.22 % (521154)------------------------------
% 28.95/5.22 % (521154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521154)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521154)Termination reason: Instruction limit
% 28.95/5.22 % (521154)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521154)Time elapsed: 0.255 s
% 28.95/5.22 % (521154)Peak memory usage: 32 MB
% 28.95/5.22 % (521154)Instructions burned: 715 (million)
% 28.95/5.22 % TRYING [7]
% 28.95/5.22 % (521166)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2607509745:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 28.95/5.22 % TRYING [5]
% 28.95/5.22 % (521156)Instruction limit reached!
% 28.95/5.22 % (521156)------------------------------
% 28.95/5.22 % (521156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521156)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521156)Termination reason: Instruction limit
% 28.95/5.22 % (521156)Termination phase: Saturation
% 28.95/5.22 % (521156)Time elapsed: 0.383 s
% 28.95/5.22 % (521156)Peak memory usage: 20 MB
% 28.95/5.22 % (521156)Instructions burned: 684 (million)
% 28.95/5.22 % (521162)Instruction limit reached!
% 28.95/5.22 % (521162)------------------------------
% 28.95/5.22 % (521162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521162)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521162)Termination reason: Instruction limit
% 28.95/5.22 % (521162)Termination phase: Saturation
% 28.95/5.22 % (521162)Time elapsed: 0.314 s
% 28.95/5.22 % (521162)Peak memory usage: 15 MB
% 28.95/5.22 % (521162)Instructions burned: 478 (million)
% 28.95/5.22 % (521168)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1172588682:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 28.95/5.22 % (521169)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4268969749:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 28.95/5.22 % (521164)Instruction limit reached!
% 28.95/5.22 % (521164)------------------------------
% 28.95/5.22 % (521164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521164)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521164)Termination reason: Instruction limit
% 28.95/5.22 % (521164)Termination phase: Finite model building SAT solving
% 28.95/5.22 % (521164)Time elapsed: 0.353 s
% 28.95/5.22 % (521164)Peak memory usage: 23 MB
% 28.95/5.22 % (521164)Instructions burned: 866 (million)
% 28.95/5.22 % (521172)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=842299835:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 28.95/5.22 % TRYING [14]
% 28.95/5.22 % TRYING [8]
% 28.95/5.22 % (521168)Instruction limit reached!
% 28.95/5.22 % (521168)------------------------------
% 28.95/5.22 % (521168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521168)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521168)Termination reason: Instruction limit
% 28.95/5.22 % (521168)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521168)Time elapsed: 0.338 s
% 28.95/5.22 % (521168)Peak memory usage: 76 MB
% 28.95/5.22 % (521168)Instructions burned: 890 (million)
% 28.95/5.22 % (521174)fmb+10_1_sil=64000:random_seed=3457719055:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [3]
% 28.95/5.22 % (521169)Instruction limit reached!
% 28.95/5.22 % (521169)------------------------------
% 28.95/5.22 % (521169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521169)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521169)Termination reason: Instruction limit
% 28.95/5.22 % (521169)Termination phase: Saturation
% 28.95/5.22 % (521169)Time elapsed: 0.373 s
% 28.95/5.22 % (521169)Peak memory usage: 21 MB
% 28.95/5.22 % (521169)Instructions burned: 694 (million)
% 28.95/5.22 % (521176)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=456067332:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 28.95/5.22 % TRYING [4]
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [20]
% 28.95/5.22 % TRYING [5]
% 28.95/5.22 % (521166)Instruction limit reached!
% 28.95/5.22 % (521166)------------------------------
% 28.95/5.22 % (521166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521166)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521166)Termination reason: Instruction limit
% 28.95/5.22 % (521166)Termination phase: Saturation
% 28.95/5.22 % (521166)Time elapsed: 0.657 s
% 28.95/5.22 % (521166)Peak memory usage: 22 MB
% 28.95/5.22 % (521166)Instructions burned: 1180 (million)
% 28.95/5.22 % (521178)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4215511039:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [8]
% 28.95/5.22 % (521172)Instruction limit reached!
% 28.95/5.22 % (521172)------------------------------
% 28.95/5.22 % (521172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521172)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521172)Termination reason: Instruction limit
% 28.95/5.22 % (521172)Termination phase: Saturation
% 28.95/5.22 % (521172)Time elapsed: 0.505 s
% 28.95/5.22 % (521172)Peak memory usage: 20 MB
% 28.95/5.22 % (521172)Instructions burned: 881 (million)
% 28.95/5.22 % (521180)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2366911285:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 28.95/5.22 % TRYING [6]
% 28.95/5.22 % (521178)Instruction limit reached!
% 28.95/5.22 % (521178)------------------------------
% 28.95/5.22 % (521178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521178)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521178)Termination reason: Instruction limit
% 28.95/5.22 % (521178)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521178)Time elapsed: 0.339 s
% 28.95/5.22 % (521178)Peak memory usage: 69 MB
% 28.95/5.22 % (521178)Instructions burned: 922 (million)
% 28.95/5.22 % (521182)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2217733205:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 28.95/5.22 % TRYING [9]
% 28.95/5.22 % TRYING [7]
% 28.95/5.22 % (521182)Instruction limit reached!
% 28.95/5.22 % (521182)------------------------------
% 28.95/5.22 % (521182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521182)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521182)Termination reason: Instruction limit
% 28.95/5.22 % (521182)Termination phase: Saturation
% 28.95/5.22 % (521182)Time elapsed: 0.650 s
% 28.95/5.22 % (521182)Peak memory usage: 15 MB
% 28.95/5.22 % (521182)Instructions burned: 1472 (million)
% 28.95/5.22 % (521184)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2089430144:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [77]
% 28.95/5.22 % TRYING [10]
% 28.95/5.22 % TRYING [8]
% 28.95/5.22 % (521180)Instruction limit reached!
% 28.95/5.22 % (521180)------------------------------
% 28.95/5.22 % (521180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521180)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521180)Termination reason: Instruction limit
% 28.95/5.22 % (521180)Termination phase: Saturation
% 28.95/5.22 % (521180)Time elapsed: 2.695 s
% 28.95/5.22 % (521180)Peak memory usage: 40 MB
% 28.95/5.22 % (521180)Instructions burned: 5132 (million)
% 28.95/5.22 % (521186)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2883984964:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [16]
% 28.95/5.22 % (521176)Instruction limit reached!
% 28.95/5.22 % (521176)------------------------------
% 28.95/5.22 % (521176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521176)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521176)Termination reason: Instruction limit
% 28.95/5.22 % (521176)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521176)Time elapsed: 3.275 s
% 28.95/5.22 % (521176)Peak memory usage: 577 MB
% 28.95/5.22 % (521176)Instructions burned: 9517 (million)
% 28.95/5.22 % (521188)ott-2_1_sil=16000:newcnf=on:random_seed=3295494349:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 28.95/5.22 % (521184)Instruction limit reached!
% 28.95/5.22 % (521184)------------------------------
% 28.95/5.22 % (521184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521184)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521184)Termination reason: Instruction limit
% 28.95/5.22 % (521184)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521184)Time elapsed: 2.362 s
% 28.95/5.22 % (521184)Peak memory usage: 523 MB
% 28.95/5.22 % (521184)Instructions burned: 6325 (million)
% 28.95/5.22 % (521190)ott+10_1_sil=32000:tgt=ground:random_seed=3471723937:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 28.95/5.22 % (521186)Instruction limit reached!
% 28.95/5.22 % (521186)------------------------------
% 28.95/5.22 % (521186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521186)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521186)Termination reason: Instruction limit
% 28.95/5.22 % (521186)Termination phase: Finite model building constraint generation
% 28.95/5.22 % (521186)Time elapsed: 0.766 s
% 28.95/5.22 % (521186)Peak memory usage: 146 MB
% 28.95/5.22 % (521186)Instructions burned: 2177 (million)
% 28.95/5.22 % (521192)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=968396373:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 28.95/5.22 % Detected minimum model sizes of [3]
% 28.95/5.22 % Detected maximum model sizes of [max]
% 28.95/5.22 % TRYING [3]
% 28.95/5.22 % TRYING [4]
% 28.95/5.22 % (521190) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-521135-521190"...
% 28.95/5.22 % (521188)Instruction limit reached!
% 28.95/5.22 % (521188)------------------------------
% 28.95/5.22 % (521188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521188)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521188)Termination reason: Instruction limit
% 28.95/5.22 % (521188)Termination phase: Saturation
% 28.95/5.22 % (521188)Time elapsed: 0.451 s
% 28.95/5.22 % (521188)Peak memory usage: 23 MB
% 28.95/5.22 % (521188)Instructions burned: 871 (million)
% 28.95/5.22 % (521190)...printing done.
% 28.95/5.22 % (521190)Refutation found. Thanks to Tanya!
% 28.95/5.22 % SZS status Theorem for theBenchmark
% 28.95/5.22 % SZS output start Proof for theBenchmark
% See solution above
% 28.95/5.22 % (521190)------------------------------
% 28.95/5.22 % (521190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.95/5.22 % (521190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.95/5.22 % (521190)CaDiCaL version: 2.1.3
% 28.95/5.22 % (521190)Termination reason: Refutation
% 28.95/5.22 % (521190)Time elapsed: 0.192 s
% 28.95/5.22 % (521190)Peak memory usage: 15 MB
% 28.95/5.22 % (521190)Instructions burned: 350 (million)
% 28.95/5.22 % (521135)Success in time 4.798 s
% 28.95/5.22 % Vampire exiting
%------------------------------------------------------------------------------