%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM424+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 : n008.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:15 PM UTC 2026
% Result : Theorem 262.92s 41.34s
% Output : Refutation 262.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 134 ( 22 unt; 5 def)
% Number of atoms : 376 ( 95 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 420 ( 178 ~; 167 |; 57 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 102 ( 0 sgn 93 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntOne) ).
fof(f4,axiom,
! [X0] :
( aInteger0(X0)
=> aInteger0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntNeg) ).
fof(f5,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntPlus) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(f8,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(f9,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(f10,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddNeg) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
fof(f12,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDistrib) ).
fof(f16,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulMinOne) ).
fof(f21,axiom,
( aInteger0(xa)
& aInteger0(xb)
& aInteger0(xq)
& xq != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__704) ).
fof(f22,conjecture,
( ( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) )
=> ( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xb,smndt0(xa)) )
| aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(xb,xa,xq) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f23,negated_conjecture,
~ ( ( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) )
=> ( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xb,smndt0(xa)) )
| aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(xb,xa,xq) ) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
fof(f25,plain,
~ ( ( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) )
=> ( ? [X1] :
( aInteger0(X1)
& sdtpldt0(xb,smndt0(xa)) = sdtasdt0(xq,X1) )
| aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
| sdteqdtlpzmzozddtrp0(xb,xa,xq) ) ),
inference(rectify,[],[f23]) ).
fof(f26,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f27,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f28,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f27]) ).
fof(f31,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f32,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f34,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f36,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f37,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f37]) ).
fof(f39,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f39]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f42]) ).
fof(f45,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f53,plain,
( ! [X1] :
( ~ aInteger0(X1)
| sdtpldt0(xb,smndt0(xa)) != sdtasdt0(xq,X1) )
& ~ aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
& ~ sdteqdtlpzmzozddtrp0(xb,xa,xq)
& ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) ),
inference(ennf_transformation,[],[f25]) ).
fof(f54,plain,
( ! [X1] :
( ~ aInteger0(X1)
| sdtpldt0(xb,smndt0(xa)) != sdtasdt0(xq,X1) )
& ~ aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
& ~ sdteqdtlpzmzozddtrp0(xb,xa,xq)
& ? [X0] :
( aInteger0(X0)
& sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) ),
inference(flattening,[],[f53]) ).
fof(f60,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(xq,X0) != sdtpldt0(xb,smndt0(xa)) )
& ~ aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
& ~ sdteqdtlpzmzozddtrp0(xb,xa,xq)
& ? [X1] :
( aInteger0(X1)
& sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,X1) )
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) ),
inference(rectify,[],[f54]) ).
fof(f61,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(xq,X0) != sdtpldt0(xb,smndt0(xa)) )
& ~ aDivisorOf0(xq,sdtpldt0(xb,smndt0(xa)))
& ~ sdteqdtlpzmzozddtrp0(xb,xa,xq)
& aInteger0(sK1)
& sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sK1)
& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))
& sdteqdtlpzmzozddtrp0(xa,xb,xq) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1)],[f60]) ).
fof(f63,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f64,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f26]) ).
fof(f65,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f28]) ).
fof(f67,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
inference(cnf_transformation,[],[f32]) ).
fof(f68,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f69,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f35]) ).
fof(f70,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(cnf_transformation,[],[f35]) ).
fof(f71,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(smndt0(X0),X0) ),
inference(cnf_transformation,[],[f36]) ).
fof(f73,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f74,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f78,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f43]) ).
fof(f82,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sdtasdt0(smndt0(sz10),X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f93,plain,
aInteger0(xq),
inference(cnf_transformation,[],[f21]) ).
fof(f94,plain,
aInteger0(xb),
inference(cnf_transformation,[],[f21]) ).
fof(f95,plain,
aInteger0(xa),
inference(cnf_transformation,[],[f21]) ).
fof(f98,plain,
sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sK1),
inference(cnf_transformation,[],[f61]) ).
fof(f99,plain,
aInteger0(sK1),
inference(cnf_transformation,[],[f61]) ).
fof(f102,plain,
! [X0] :
( sdtasdt0(xq,X0) != sdtpldt0(xb,smndt0(xa))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f110,plain,
xb = sdtpldt0(sz00,xb),
inference(resolution,[],[f69,f94]) ).
fof(f115,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sdtpldt0(smndt0(X0),sz00) ),
inference(resolution,[],[f70,f64]) ).
fof(f156,plain,
( aInteger0(sdtasdt0(xq,sK1))
| ~ aInteger0(xa)
| ~ aInteger0(smndt0(xb)) ),
inference(superposition,[],[f65,f98]) ).
fof(f158,plain,
( aInteger0(sdtasdt0(xq,sK1))
| ~ aInteger0(smndt0(xb)) ),
inference(forward_subsumption_resolution,[],[f156,f95]) ).
fof(f160,definition,
( spl2_1
<=> aInteger0(smndt0(xb)) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f161,plain,
( aInteger0(smndt0(xb))
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f162,plain,
( ~ aInteger0(smndt0(xb))
| spl2_1 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f164,definition,
( spl2_2
<=> aInteger0(sdtasdt0(xq,sK1)) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f166,plain,
( aInteger0(sdtasdt0(xq,sK1))
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f167,plain,
( ~ spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f158,f164,f160]) ).
fof(f180,plain,
sz00 = sdtpldt0(smndt0(xb),xb),
inference(resolution,[],[f71,f94]) ).
fof(f192,plain,
( ~ aInteger0(xb)
| spl2_1 ),
inference(resolution,[],[f162,f64]) ).
fof(f193,plain,
( $false
| spl2_1 ),
inference(forward_subsumption_resolution,[],[f192,f94]) ).
fof(f194,plain,
spl2_1,
inference(avatar_contradiction_clause,[],[f193]) ).
fof(f209,plain,
smndt0(xa) = sdtasdt0(smndt0(sz10),xa),
inference(resolution,[],[f82,f95]) ).
fof(f212,plain,
smndt0(sK1) = sdtasdt0(smndt0(sz10),sK1),
inference(resolution,[],[f82,f99]) ).
fof(f228,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,xa) = sdtpldt0(xa,X0) ),
inference(resolution,[],[f68,f95]) ).
fof(f240,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(xq,X0) = sdtasdt0(X0,xq) ),
inference(resolution,[],[f74,f93]) ).
fof(f242,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sK1) = sdtasdt0(sK1,X0) ),
inference(resolution,[],[f74,f99]) ).
fof(f250,plain,
( sz00 = sdtpldt0(smndt0(smndt0(xb)),smndt0(xb))
| ~ spl2_1 ),
inference(resolution,[],[f161,f71]) ).
fof(f258,plain,
( smndt0(smndt0(xb)) = sdtasdt0(smndt0(sz10),smndt0(xb))
| ~ spl2_1 ),
inference(resolution,[],[f161,f82]) ).
fof(f273,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(X1,xb)) = sdtpldt0(sdtpldt0(X0,X1),xb) ),
inference(resolution,[],[f67,f94]) ).
fof(f285,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,sdtasdt0(X1,xq)) = sdtasdt0(sdtasdt0(X0,X1),xq) ),
inference(resolution,[],[f73,f93]) ).
fof(f305,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(X1,xa)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xa)) ),
inference(resolution,[],[f78,f95]) ).
fof(f338,plain,
( smndt0(sdtasdt0(xq,sK1)) = sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1))
| ~ spl2_2 ),
inference(resolution,[],[f166,f82]) ).
fof(f396,definition,
( spl2_8
<=> aInteger0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f397,plain,
( aInteger0(smndt0(sz10))
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f398,plain,
( ~ aInteger0(smndt0(sz10))
| spl2_8 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f445,plain,
sdtasdt0(xq,sK1) = sdtasdt0(sK1,xq),
inference(resolution,[],[f242,f93]) ).
fof(f742,plain,
( ~ aInteger0(sz10)
| spl2_8 ),
inference(resolution,[],[f398,f64]) ).
fof(f743,plain,
( $false
| spl2_8 ),
inference(forward_subsumption_resolution,[],[f742,f63]) ).
fof(f744,plain,
spl2_8,
inference(avatar_contradiction_clause,[],[f743]) ).
fof(f881,plain,
( sdtpldt0(xa,smndt0(xb)) = sdtpldt0(smndt0(xb),xa)
| ~ spl2_1 ),
inference(resolution,[],[f228,f161]) ).
fof(f1071,plain,
( smndt0(smndt0(xb)) = sdtpldt0(smndt0(smndt0(xb)),sz00)
| ~ spl2_1 ),
inference(resolution,[],[f115,f161]) ).
fof(f2116,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(smndt0(xb),xb)) = sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb) )
| ~ spl2_1 ),
inference(resolution,[],[f273,f161]) ).
fof(f2286,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtasdt0(sK1,xq)) = sdtasdt0(sdtasdt0(X0,sK1),xq) ),
inference(resolution,[],[f285,f99]) ).
fof(f2806,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(smndt0(xb),xa)) = sdtpldt0(sdtasdt0(X0,smndt0(xb)),sdtasdt0(X0,xa)) )
| ~ spl2_1 ),
inference(resolution,[],[f305,f161]) ).
fof(f4310,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz00) = sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb) )
| ~ spl2_1 ),
inference(forward_demodulation,[],[f2116,f180]) ).
fof(f4360,definition,
( spl2_23
<=> aInteger0(smndt0(smndt0(xb))) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f4361,plain,
( aInteger0(smndt0(smndt0(xb)))
| ~ spl2_23 ),
inference(avatar_component_clause,[],[f4360]) ).
fof(f4362,plain,
( ~ aInteger0(smndt0(smndt0(xb)))
| spl2_23 ),
inference(avatar_component_clause,[],[f4360]) ).
fof(f5660,plain,
( sdtasdt0(xq,sK1) = sdtpldt0(smndt0(xb),xa)
| ~ spl2_1 ),
inference(forward_demodulation,[],[f881,f98]) ).
fof(f9097,plain,
( sdtasdt0(smndt0(sz10),sdtpldt0(smndt0(xb),xa)) = sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xb)),sdtasdt0(smndt0(sz10),xa))
| ~ spl2_1
| ~ spl2_8 ),
inference(resolution,[],[f2806,f397]) ).
fof(f9124,plain,
( sdtasdt0(smndt0(sz10),sdtpldt0(smndt0(xb),xa)) = sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xb)),smndt0(xa))
| ~ spl2_1
| ~ spl2_8 ),
inference(forward_demodulation,[],[f9097,f209]) ).
fof(f12066,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtasdt0(xq,sK1)) = sdtasdt0(sdtasdt0(X0,sK1),xq) ),
inference(forward_demodulation,[],[f2286,f445]) ).
fof(f12555,definition,
( spl2_72
<=> aInteger0(smndt0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f12556,plain,
( aInteger0(smndt0(sK1))
| ~ spl2_72 ),
inference(avatar_component_clause,[],[f12555]) ).
fof(f12557,plain,
( ~ aInteger0(smndt0(sK1))
| spl2_72 ),
inference(avatar_component_clause,[],[f12555]) ).
fof(f12633,plain,
( ~ aInteger0(sK1)
| spl2_72 ),
inference(resolution,[],[f12557,f64]) ).
fof(f12634,plain,
( $false
| spl2_72 ),
inference(forward_subsumption_resolution,[],[f12633,f99]) ).
fof(f12635,plain,
spl2_72,
inference(avatar_contradiction_clause,[],[f12634]) ).
fof(f12698,plain,
( sdtasdt0(xq,smndt0(sK1)) = sdtasdt0(smndt0(sK1),xq)
| ~ spl2_72 ),
inference(resolution,[],[f12556,f240]) ).
fof(f16400,plain,
( ~ aInteger0(smndt0(xb))
| spl2_23 ),
inference(resolution,[],[f4362,f64]) ).
fof(f16401,plain,
( $false
| ~ spl2_1
| spl2_23 ),
inference(forward_subsumption_resolution,[],[f16400,f161]) ).
fof(f16402,plain,
( ~ spl2_1
| spl2_23 ),
inference(avatar_contradiction_clause,[],[f16401]) ).
fof(f16428,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1)) = sdtasdt0(sdtasdt0(smndt0(sz10),sK1),xq)
| ~ spl2_8 ),
inference(resolution,[],[f12066,f397]) ).
fof(f16462,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1)) = sdtasdt0(smndt0(sK1),xq)
| ~ spl2_8 ),
inference(forward_demodulation,[],[f16428,f212]) ).
fof(f16478,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1)) = sdtasdt0(xq,smndt0(sK1))
| ~ spl2_8
| ~ spl2_72 ),
inference(forward_demodulation,[],[f16462,f12698]) ).
fof(f16492,plain,
( smndt0(sdtasdt0(xq,sK1)) = sdtasdt0(xq,smndt0(sK1))
| ~ spl2_2
| ~ spl2_8
| ~ spl2_72 ),
inference(forward_demodulation,[],[f16478,f338]) ).
fof(f16987,plain,
( sdtpldt0(smndt0(smndt0(xb)),sz00) = sdtpldt0(sdtpldt0(smndt0(smndt0(xb)),smndt0(xb)),xb)
| ~ spl2_1
| ~ spl2_23 ),
inference(resolution,[],[f4361,f4310]) ).
fof(f17030,plain,
( sdtpldt0(sz00,xb) = sdtpldt0(smndt0(smndt0(xb)),sz00)
| ~ spl2_1
| ~ spl2_23 ),
inference(forward_demodulation,[],[f16987,f250]) ).
fof(f17156,plain,
( sdtpldt0(sz00,xb) = smndt0(smndt0(xb))
| ~ spl2_1
| ~ spl2_23 ),
inference(forward_demodulation,[],[f17030,f1071]) ).
fof(f17192,plain,
( xb = smndt0(smndt0(xb))
| ~ spl2_1
| ~ spl2_23 ),
inference(forward_demodulation,[],[f17156,f110]) ).
fof(f77800,plain,
( sdtpldt0(smndt0(smndt0(xb)),smndt0(xa)) = sdtasdt0(smndt0(sz10),sdtpldt0(smndt0(xb),xa))
| ~ spl2_1
| ~ spl2_8 ),
inference(forward_demodulation,[],[f9124,f258]) ).
fof(f80916,plain,
( sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1)) = sdtpldt0(smndt0(smndt0(xb)),smndt0(xa))
| ~ spl2_1
| ~ spl2_8 ),
inference(forward_demodulation,[],[f77800,f5660]) ).
fof(f82148,plain,
( sdtpldt0(xb,smndt0(xa)) = sdtasdt0(smndt0(sz10),sdtasdt0(xq,sK1))
| ~ spl2_1
| ~ spl2_8
| ~ spl2_23 ),
inference(forward_demodulation,[],[f80916,f17192]) ).
fof(f82482,plain,
( sdtpldt0(xb,smndt0(xa)) = smndt0(sdtasdt0(xq,sK1))
| ~ spl2_1
| ~ spl2_2
| ~ spl2_8
| ~ spl2_23 ),
inference(forward_demodulation,[],[f82148,f338]) ).
fof(f110289,plain,
( sdtpldt0(xb,smndt0(xa)) != smndt0(sdtasdt0(xq,sK1))
| ~ aInteger0(smndt0(sK1))
| ~ spl2_2
| ~ spl2_8
| ~ spl2_72 ),
inference(superposition,[],[f102,f16492]) ).
fof(f110294,plain,
( ~ aInteger0(smndt0(sK1))
| ~ spl2_1
| ~ spl2_2
| ~ spl2_8
| ~ spl2_23
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f110289,f82482]) ).
fof(f110296,plain,
( $false
| ~ spl2_1
| ~ spl2_2
| ~ spl2_8
| ~ spl2_23
| ~ spl2_72 ),
inference(forward_subsumption_resolution,[],[f110294,f12556]) ).
fof(f110297,plain,
( ~ spl2_1
| ~ spl2_2
| ~ spl2_8
| ~ spl2_23
| ~ spl2_72 ),
inference(avatar_contradiction_clause,[],[f110296]) ).
cnf(s87,plain,
( ~ spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f167]) ).
cnf(s113,plain,
spl2_1,
inference(sat_conversion,[],[f194]) ).
cnf(s325,plain,
spl2_8,
inference(sat_conversion,[],[f744]) ).
cnf(s3687,plain,
spl2_72,
inference(sat_conversion,[],[f12635]) ).
cnf(s4697,plain,
( ~ spl2_1
| spl2_23 ),
inference(sat_conversion,[],[f16402]) ).
cnf(s32420,plain,
( ~ spl2_1
| ~ spl2_2
| ~ spl2_8
| ~ spl2_23
| ~ spl2_72 ),
inference(sat_conversion,[],[f110297]) ).
cnf(s32448,plain,
spl2_23,
inference(rat,[],[s4697,s113]) ).
cnf(s32453,plain,
~ spl2_2,
inference(rat,[],[s32420,s3687,s113,s325,s32448]) ).
cnf(s32455,plain,
$false,
inference(rat,[],[s87,s32453,s113]) ).
fof(f110300,plain,
$false,
inference(avatar_sat_refutation,[],[s32455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM424+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 % Computer : n008.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 19:51:10 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 15.30/2.67 % (1559292)Will run a generic schedule for satisfiability detection.
% 15.30/2.67 % (1559299)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3371051861:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.30/2.67 % (1559298)% WARNING: option uhcvi not known.
% 15.30/2.67 % (1559297)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3453971206_2999 on theBenchmark for (2999ds/0Mi)
% 15.30/2.67 % (1559302)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3612400643:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.30/2.67 % (1559301)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=467748779:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.30/2.67 % (1559298)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1280932567:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.30/2.67 % (1559300)dis+10_1_sil=32000:sp=arity:random_seed=1493957271:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.30/2.67 % (1559303)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2359106302:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.30/2.67 % TRYING [1]
% 15.30/2.67 % TRYING [2]
% 15.30/2.67 % TRYING [3]
% 15.30/2.67 % TRYING [4]
% 15.30/2.67 % TRYING [5]
% 15.30/2.67 % (1559300)Instruction limit reached!
% 15.30/2.67 % (1559300)------------------------------
% 15.30/2.67 % (1559300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.67 % (1559300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.67 % (1559300)CaDiCaL version: 2.1.3
% 15.30/2.67 % (1559300)Termination reason: Instruction limit
% 15.30/2.67 % (1559300)Termination phase: Saturation
% 15.30/2.67 % (1559300)Time elapsed: 0.060 s
% 15.30/2.67 % (1559300)Peak memory usage: 13 MB
% 15.30/2.67 % (1559300)Instructions burned: 103 (million)
% 15.30/2.67 % (1559301)Instruction limit reached!
% 15.30/2.67 % (1559301)------------------------------
% 15.30/2.67 % (1559301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.67 % (1559301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.67 % (1559301)CaDiCaL version: 2.1.3
% 15.30/2.67 % (1559301)Termination reason: Instruction limit
% 15.30/2.67 % (1559301)Termination phase: Saturation
% 15.30/2.67 % (1559301)Time elapsed: 0.063 s
% 15.30/2.67 % (1559301)Peak memory usage: 13 MB
% 15.30/2.67 % (1559301)Instructions burned: 116 (million)
% 15.30/2.67 % (1559302)Instruction limit reached!
% 15.30/2.67 % (1559302)------------------------------
% 15.30/2.67 % (1559302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.67 % (1559302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.67 % (1559302)CaDiCaL version: 2.1.3
% 15.30/2.67 % (1559302)Termination reason: Instruction limit
% 15.30/2.67 % (1559302)Termination phase: Saturation
% 15.30/2.67 % (1559302)Time elapsed: 0.067 s
% 15.30/2.67 % (1559302)Peak memory usage: 13 MB
% 15.30/2.67 % (1559302)Instructions burned: 131 (million)
% 15.30/2.67 % (1559311)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3012024841:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.30/2.67 % (1559312)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2004753122:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.30/2.67 % TRYING [1]
% 15.30/2.67 % TRYING [2]
% 15.30/2.67 % TRYING [3]
% 15.30/2.67 % (1559313)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=1543912858:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.30/2.67 % TRYING [4]
% 15.30/2.67 % (1559303)Instruction limit reached!
% 15.30/2.67 % (1559303)------------------------------
% 15.30/2.67 % (1559303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.67 % (1559303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.67 % (1559303)CaDiCaL version: 2.1.3
% 15.30/2.67 % (1559303)Termination reason: Instruction limit
% 15.30/2.67 % (1559303)Termination phase: Saturation
% 15.30/2.67 % (1559303)Time elapsed: 0.105 s
% 15.30/2.67 % (1559303)Peak memory usage: 14 MB
% 15.30/2.67 % (1559303)Instructions burned: 159 (million)
% 15.30/2.67 % TRYING [5]
% 15.30/2.67 % TRYING [6]
% 15.30/2.67 % (1559317)ott-21_1_sil=16000:fs=off:random_seed=852738802:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.30/2.67 % (1559312)Instruction limit reached!
% 15.30/2.67 % (1559312)------------------------------
% 15.30/2.67 % (1559312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.05 % (1559312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.05 % (1559312)CaDiCaL version: 2.1.3
% 46.73/7.05 % (1559312)Termination reason: Instruction limit
% 46.73/7.05 % (1559312)Termination phase: Saturation
% 46.73/7.05 % (1559312)Time elapsed: 0.067 s
% 46.73/7.05 % (1559312)Peak memory usage: 12 MB
% 46.73/7.05 % (1559312)Instructions burned: 131 (million)
% 46.73/7.05 % (1559319)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1071949808:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 46.73/7.05 % TRYING [6]
% 46.73/7.05 % (1559317)Instruction limit reached!
% 46.73/7.05 % (1559317)------------------------------
% 46.73/7.05 % (1559317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.05 % (1559317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.05 % (1559317)CaDiCaL version: 2.1.3
% 46.73/7.05 % (1559317)Termination reason: Instruction limit
% 46.73/7.05 % (1559317)Termination phase: Saturation
% 46.73/7.05 % (1559317)Time elapsed: 0.089 s
% 46.73/7.05 % (1559317)Peak memory usage: 13 MB
% 46.73/7.05 % (1559317)Instructions burned: 180 (million)
% 46.73/7.06 % (1559321)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4185024546:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.73/7.06 % TRYING [1]
% 46.73/7.06 % TRYING [2]
% 46.73/7.06 % TRYING [3]
% 46.73/7.06 % TRYING [4]
% 46.73/7.06 % TRYING [5]
% 46.73/7.06 % TRYING [7]
% 46.73/7.06 % (1559311)Instruction limit reached!
% 46.73/7.06 % (1559311)------------------------------
% 46.73/7.06 % (1559311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.06 % (1559311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.06 % (1559311)CaDiCaL version: 2.1.3
% 46.73/7.06 % (1559311)Termination reason: Instruction limit
% 46.73/7.06 % (1559311)Termination phase: Finite model building constraint generation
% 46.73/7.06 % (1559311)Time elapsed: 0.320 s
% 46.73/7.06 % (1559311)Peak memory usage: 31 MB
% 46.73/7.06 % (1559311)Instructions burned: 715 (million)
% 46.73/7.06 % TRYING [7]
% 46.73/7.06 % (1559323)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2782086494:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 46.73/7.06 % (1559319)Instruction limit reached!
% 46.73/7.06 % (1559319)------------------------------
% 46.73/7.06 % (1559319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.06 % (1559319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.06 % (1559319)CaDiCaL version: 2.1.3
% 46.73/7.06 % (1559319)Termination reason: Instruction limit
% 46.73/7.06 % (1559319)Termination phase: Saturation
% 46.73/7.06 % (1559319)Time elapsed: 0.300 s
% 46.73/7.06 % (1559319)Peak memory usage: 14 MB
% 46.73/7.06 % (1559319)Instructions burned: 477 (million)
% 46.73/7.06 % (1559313)Instruction limit reached!
% 46.73/7.06 % (1559313)------------------------------
% 46.73/7.06 % (1559313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.06 % (1559313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.06 % (1559313)CaDiCaL version: 2.1.3
% 46.73/7.06 % (1559313)Termination reason: Instruction limit
% 46.73/7.06 % (1559313)Termination phase: Saturation
% 46.73/7.06 % (1559313)Time elapsed: 0.384 s
% 46.73/7.06 % (1559313)Peak memory usage: 20 MB
% 46.73/7.06 % (1559313)Instructions burned: 684 (million)
% 46.73/7.06 % (1559325)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2715714419:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 46.73/7.06 % (1559326)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=4139278510: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)
% 46.73/7.06 % TRYING [6]
% 46.73/7.06 % (1559321)Instruction limit reached!
% 46.73/7.06 % (1559321)------------------------------
% 46.73/7.06 % (1559321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.73/7.06 % (1559321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.73/7.06 % (1559321)CaDiCaL version: 2.1.3
% 46.73/7.06 % (1559321)Termination reason: Instruction limit
% 46.73/7.06 % (1559321)Termination phase: Finite model building constraint generation
% 46.73/7.06 % (1559321)Time elapsed: 0.328 s
% 46.73/7.06 % (1559321)Peak memory usage: 22 MB
% 46.73/7.06 % (1559321)Instructions burned: 867 (million)
% 46.73/7.06 % (1559329)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1683211618:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 94.73/13.82 % TRYING [14]
% 94.73/13.82 % (1559325)Instruction limit reached!
% 94.73/13.82 % (1559325)------------------------------
% 94.73/13.82 % (1559325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559325)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559325)Termination reason: Instruction limit
% 94.73/13.82 % (1559325)Termination phase: Finite model building constraint generation
% 94.73/13.82 % (1559325)Time elapsed: 0.330 s
% 94.73/13.82 % (1559325)Peak memory usage: 74 MB
% 94.73/13.82 % (1559325)Instructions burned: 890 (million)
% 94.73/13.82 % (1559331)fmb+10_1_sil=64000:random_seed=2742282565:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 94.73/13.82 % TRYING [1]
% 94.73/13.82 % TRYING [2]
% 94.73/13.82 % (1559326)Instruction limit reached!
% 94.73/13.82 % (1559326)------------------------------
% 94.73/13.82 % (1559326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559326)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559326)Termination reason: Instruction limit
% 94.73/13.82 % (1559326)Termination phase: Saturation
% 94.73/13.82 % (1559326)Time elapsed: 0.362 s
% 94.73/13.82 % (1559326)Peak memory usage: 16 MB
% 94.73/13.82 % (1559326)Instructions burned: 692 (million)
% 94.73/13.82 % TRYING [3]
% 94.73/13.82 % TRYING [4]
% 94.73/13.82 % (1559333)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3238726137:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 94.73/13.82 % TRYING [20]
% 94.73/13.82 % TRYING [5]
% 94.73/13.82 % (1559323)Instruction limit reached!
% 94.73/13.82 % (1559323)------------------------------
% 94.73/13.82 % (1559323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559323)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559323)Termination reason: Instruction limit
% 94.73/13.82 % (1559323)Termination phase: Saturation
% 94.73/13.82 % (1559323)Time elapsed: 0.609 s
% 94.73/13.82 % (1559323)Peak memory usage: 28 MB
% 94.73/13.82 % (1559323)Instructions burned: 1180 (million)
% 94.73/13.82 % (1559335)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=280240599:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 94.73/13.82 % TRYING [8]
% 94.73/13.82 % (1559329)Instruction limit reached!
% 94.73/13.82 % (1559329)------------------------------
% 94.73/13.82 % (1559329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559329)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559329)Termination reason: Instruction limit
% 94.73/13.82 % (1559329)Termination phase: Saturation
% 94.73/13.82 % (1559329)Time elapsed: 0.510 s
% 94.73/13.82 % (1559329)Peak memory usage: 20 MB
% 94.73/13.82 % (1559329)Instructions burned: 880 (million)
% 94.73/13.82 % TRYING [6]
% 94.73/13.82 % (1559337)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3929712758:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 94.73/13.82 % (1559335)Instruction limit reached!
% 94.73/13.82 % (1559335)------------------------------
% 94.73/13.82 % (1559335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559335)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559335)Termination reason: Instruction limit
% 94.73/13.82 % (1559335)Termination phase: Finite model building constraint generation
% 94.73/13.82 % (1559335)Time elapsed: 0.342 s
% 94.73/13.82 % (1559335)Peak memory usage: 67 MB
% 94.73/13.82 % (1559335)Instructions burned: 921 (million)
% 94.73/13.82 % (1559339)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2271895390:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 94.73/13.82 % TRYING [7]
% 94.73/13.82 % (1559339)Instruction limit reached!
% 94.73/13.82 % (1559339)------------------------------
% 94.73/13.82 % (1559339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.73/13.82 % (1559339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.73/13.82 % (1559339)CaDiCaL version: 2.1.3
% 94.73/13.82 % (1559339)Termination reason: Instruction limit
% 94.73/13.82 % (1559339)Termination phase: Saturation
% 94.73/13.82 % (1559339)Time elapsed: 0.753 s
% 94.73/13.82 % (1559339)Peak memory usage: 34 MB
% 94.73/13.82 % (1559339)Instructions burned: 1473 (million)
% 94.73/13.82 % (1559341)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=179877464:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 218.14/31.23 % TRYING [77]
% 218.14/31.23 % TRYING [8]
% 218.14/31.23 % TRYING [8]
% 218.14/31.23 % (1559337)Instruction limit reached!
% 218.14/31.23 % (1559337)------------------------------
% 218.14/31.23 % (1559337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559337)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559337)Termination reason: Instruction limit
% 218.14/31.23 % (1559337)Termination phase: Saturation
% 218.14/31.23 % (1559337)Time elapsed: 2.609 s
% 218.14/31.23 % (1559337)Peak memory usage: 57 MB
% 218.14/31.23 % (1559337)Instructions burned: 5133 (million)
% 218.14/31.23 % (1559343)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2501216020:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 218.14/31.23 % TRYING [16]
% 218.14/31.23 % (1559333)Instruction limit reached!
% 218.14/31.23 % (1559333)------------------------------
% 218.14/31.23 % (1559333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559333)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559333)Termination reason: Instruction limit
% 218.14/31.23 % (1559333)Termination phase: Finite model building constraint generation
% 218.14/31.23 % (1559333)Time elapsed: 3.302 s
% 218.14/31.23 % (1559333)Peak memory usage: 578 MB
% 218.14/31.23 % (1559333)Instructions burned: 9517 (million)
% 218.14/31.23 % (1559345)ott-2_1_sil=16000:newcnf=on:random_seed=1902807451:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 218.14/31.23 % (1559341)Instruction limit reached!
% 218.14/31.23 % (1559341)------------------------------
% 218.14/31.23 % (1559341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559341)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559341)Termination reason: Instruction limit
% 218.14/31.23 % (1559341)Termination phase: Finite model building constraint generation
% 218.14/31.23 % (1559341)Time elapsed: 2.156 s
% 218.14/31.23 % (1559341)Peak memory usage: 374 MB
% 218.14/31.23 % (1559341)Instructions burned: 6324 (million)
% 218.14/31.23 % (1559347)ott+10_1_sil=32000:tgt=ground:random_seed=736763096:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 218.14/31.23 % (1559343)Instruction limit reached!
% 218.14/31.23 % (1559343)------------------------------
% 218.14/31.23 % (1559343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559343)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559343)Termination reason: Instruction limit
% 218.14/31.23 % (1559343)Termination phase: Finite model building constraint generation
% 218.14/31.23 % (1559343)Time elapsed: 0.752 s
% 218.14/31.23 % (1559343)Peak memory usage: 146 MB
% 218.14/31.23 % (1559343)Instructions burned: 2176 (million)
% 218.14/31.23 % (1559349)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3427230874:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 218.14/31.23 % TRYING [1]
% 218.14/31.23 % TRYING [2]
% 218.14/31.23 % TRYING [3]
% 218.14/31.23 % TRYING [4]
% 218.14/31.23 % TRYING [5]
% 218.14/31.23 % TRYING [6]
% 218.14/31.23 % (1559345)Instruction limit reached!
% 218.14/31.23 % (1559345)------------------------------
% 218.14/31.23 % (1559345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559345)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559345)Termination reason: Instruction limit
% 218.14/31.23 % (1559345)Termination phase: Saturation
% 218.14/31.23 % (1559345)Time elapsed: 0.470 s
% 218.14/31.23 % (1559345)Peak memory usage: 23 MB
% 218.14/31.23 % (1559345)Instructions burned: 869 (million)
% 218.14/31.23 % (1559351)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4161114988:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 218.14/31.23 % TRYING [7]
% 218.14/31.23 % (1559351)Instruction limit reached!
% 218.14/31.23 % (1559351)------------------------------
% 218.14/31.23 % (1559351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.14/31.23 % (1559351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.14/31.23 % (1559351)CaDiCaL version: 2.1.3
% 218.14/31.23 % (1559351)Termination reason: Instruction limit
% 218.14/31.23 % (1559351)Termination phase: Saturation
% 218.14/31.23 % (1559351)Time elapsed: 1.823 s
% 218.14/31.23 % (1559351)Peak memory usage: 41 MB
% 218.14/31.23 % (1559351)Instructions burned: 3514 (million)
% 262.92/41.34 % (1559353)dis+21_1_sil=32000:sas=cadical:random_seed=3605319302:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 262.92/41.34 % TRYING [8]
% 262.92/41.34 % (1559347)Instruction limit reached!
% 262.92/41.34 % (1559347)------------------------------
% 262.92/41.34 % (1559347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559347)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559347)Termination reason: Instruction limit
% 262.92/41.34 % (1559347)Termination phase: Saturation
% 262.92/41.34 % (1559347)Time elapsed: 2.678 s
% 262.92/41.34 % (1559347)Peak memory usage: 80 MB
% 262.92/41.34 % (1559347)Instructions burned: 5115 (million)
% 262.92/41.34 % (1559355)ott+11_1_sil=16000:gs=on:random_seed=168175445:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2928 on theBenchmark for (2928ds/2251Mi)
% 262.92/41.34 % (1559355)Instruction limit reached!
% 262.92/41.34 % (1559355)------------------------------
% 262.92/41.34 % (1559355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559355)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559355)Termination reason: Instruction limit
% 262.92/41.34 % (1559355)Termination phase: Saturation
% 262.92/41.34 % (1559355)Time elapsed: 0.884 s
% 262.92/41.34 % (1559355)Peak memory usage: 13 MB
% 262.92/41.34 % (1559355)Instructions burned: 2253 (million)
% 262.92/41.34 % (1559357)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3707915502:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 262.92/41.34 % TRYING [7]
% 262.92/41.34 % TRYING [9]
% 262.92/41.34 % (1559353)Instruction limit reached!
% 262.92/41.34 % (1559353)------------------------------
% 262.92/41.34 % (1559353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559353)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559353)Termination reason: Instruction limit
% 262.92/41.34 % (1559353)Termination phase: Saturation
% 262.92/41.34 % (1559353)Time elapsed: 1.910 s
% 262.92/41.34 % (1559353)Peak memory usage: 50 MB
% 262.92/41.34 % (1559353)Instructions burned: 3775 (million)
% 262.92/41.34 % (1559359)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1592835634:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2914 on theBenchmark for (2914ds/4591Mi)
% 262.92/41.34 % TRYING [8]
% 262.92/41.34 % (1559331)Instruction limit reached!
% 262.92/41.34 % (1559331)------------------------------
% 262.92/41.34 % (1559331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559331)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559331)Termination reason: Instruction limit
% 262.92/41.34 % (1559331)Termination phase: Finite model building SAT solving
% 262.92/41.34 % (1559331)Time elapsed: 9.735 s
% 262.92/41.34 % (1559331)Peak memory usage: 138 MB
% 262.92/41.34 % (1559331)Instructions burned: 22064 (million)
% 262.92/41.34 % (1559361)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2407320997:i=29340_2893 on theBenchmark for (2893ds/29340Mi)
% 262.92/41.34 % (1559359)Instruction limit reached!
% 262.92/41.34 % (1559359)------------------------------
% 262.92/41.34 % (1559359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559359)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559359)Termination reason: Instruction limit
% 262.92/41.34 % (1559359)Termination phase: Saturation
% 262.92/41.34 % (1559359)Time elapsed: 2.141 s
% 262.92/41.34 % (1559359)Peak memory usage: 48 MB
% 262.92/41.34 % (1559359)Instructions burned: 4592 (million)
% 262.92/41.34 % (1559363)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3499268435:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 262.92/41.34 % TRYING [9]
% 262.92/41.34 % (1559363)Instruction limit reached!
% 262.92/41.34 % (1559363)------------------------------
% 262.92/41.34 % (1559363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559363)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559363)Termination reason: Instruction limit
% 262.92/41.34 % (1559363)Termination phase: Saturation
% 262.92/41.34 % (1559363)Time elapsed: 2.635 s
% 262.92/41.34 % (1559363)Peak memory usage: 58 MB
% 262.92/41.34 % (1559363)Instructions burned: 5211 (million)
% 262.92/41.34 % (1559365)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3012053412:i=5497:nm=2_2866 on theBenchmark for (2866ds/5497Mi)
% 262.92/41.34 % TRYING [17]
% 262.92/41.34 % TRYING [9]
% 262.92/41.34 % (1559365)Instruction limit reached!
% 262.92/41.34 % (1559365)------------------------------
% 262.92/41.34 % (1559365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559365)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559365)Termination reason: Instruction limit
% 262.92/41.34 % (1559365)Termination phase: Finite model building constraint generation
% 262.92/41.34 % (1559365)Time elapsed: 1.898 s
% 262.92/41.34 % (1559365)Peak memory usage: 339 MB
% 262.92/41.34 % (1559365)Instructions burned: 5499 (million)
% 262.92/41.34 % (1559367)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=956415633:fmbsr=2:i=46332_2846 on theBenchmark for (2846ds/46332Mi)
% 262.92/41.34 % TRYING [15]
% 262.92/41.34 % (1559299)Instruction limit reached!
% 262.92/41.34 % (1559299)------------------------------
% 262.92/41.34 % (1559299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559299)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559299)Termination reason: Instruction limit
% 262.92/41.34 % (1559299)Termination phase: Saturation
% 262.92/41.34 % (1559299)Time elapsed: 18.311 s
% 262.92/41.34 % (1559299)Peak memory usage: 71 MB
% 262.92/41.34 % (1559299)Instructions burned: 88025 (million)
% 262.92/41.34 % (1559369)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=610308290:i=14071_2816 on theBenchmark for (2816ds/14071Mi)
% 262.92/41.34 % TRYING [12]
% 262.92/41.34 % TRYING [9]
% 262.92/41.34 % (1559369)Instruction limit reached!
% 262.92/41.34 % (1559369)------------------------------
% 262.92/41.34 % (1559369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559369)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559369)Termination reason: Instruction limit
% 262.92/41.34 % (1559369)Termination phase: Finite model building SAT solving
% 262.92/41.34 % (1559369)Time elapsed: 5.802 s
% 262.92/41.34 % (1559369)Peak memory usage: 570 MB
% 262.92/41.34 % (1559369)Instructions burned: 14072 (million)
% 262.92/41.34 % (1559361)Instruction limit reached!
% 262.92/41.34 % (1559361)------------------------------
% 262.92/41.34 % (1559361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559361)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559361)Termination reason: Instruction limit
% 262.92/41.34 % (1559361)Termination phase: Saturation
% 262.92/41.34 % (1559361)Time elapsed: 13.542 s
% 262.92/41.34 % (1559361)Peak memory usage: 310 MB
% 262.92/41.34 % (1559361)Instructions burned: 29343 (million)
% 262.92/41.34 % (1559371)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=912935248:i=22565:add=on:rawr=on_2757 on theBenchmark for (2757ds/22565Mi)
% 262.92/41.34 % (1559373)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2453524646:i=8173:av=off_2757 on theBenchmark for (2757ds/8173Mi)
% 262.92/41.34 % (1559373)Instruction limit reached!
% 262.92/41.34 % (1559373)------------------------------
% 262.92/41.34 % (1559373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559373)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559373)Termination reason: Instruction limit
% 262.92/41.34 % (1559373)Termination phase: Saturation
% 262.92/41.34 % (1559373)Time elapsed: 3.483 s
% 262.92/41.34 % (1559373)Peak memory usage: 56 MB
% 262.92/41.34 % (1559373)Instructions burned: 8176 (million)
% 262.92/41.34 % (1559375)dis+10_16:1_sil=16000:random_seed=3045452965:i=9155:fsr=off_2722 on theBenchmark for (2722ds/9155Mi)
% 262.92/41.34 % (1559371)Instruction limit reached!
% 262.92/41.34 % (1559371)------------------------------
% 262.92/41.34 % (1559371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559371)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559371)Termination reason: Instruction limit
% 262.92/41.34 % (1559371)Termination phase: Saturation
% 262.92/41.34 % (1559371)Time elapsed: 6.575 s
% 262.92/41.34 % (1559371)Peak memory usage: 286 MB
% 262.92/41.34 % (1559371)Instructions burned: 22568 (million)
% 262.92/41.34 % (1559377)ott-3_8_sil=64000:random_seed=2409258330:i=20139:bs=on_2691 on theBenchmark for (2691ds/20139Mi)
% 262.92/41.34 % (1559375)Instruction limit reached!
% 262.92/41.34 % (1559375)------------------------------
% 262.92/41.34 % (1559375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559375)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559375)Termination reason: Instruction limit
% 262.92/41.34 % (1559375)Termination phase: Saturation
% 262.92/41.34 % (1559375)Time elapsed: 4.480 s
% 262.92/41.34 % (1559375)Peak memory usage: 90 MB
% 262.92/41.34 % (1559375)Instructions burned: 9159 (million)
% 262.92/41.34 % (1559379)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1618177857:fmbsr=2:i=32576_2677 on theBenchmark for (2677ds/32576Mi)
% 262.92/41.34 % TRYING [9]
% 262.92/41.34 % TRYING [10]
% 262.92/41.34 % (1559377)Instruction limit reached!
% 262.92/41.34 % (1559377)------------------------------
% 262.92/41.34 % (1559377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559377)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559377)Termination reason: Instruction limit
% 262.92/41.34 % (1559377)Termination phase: Saturation
% 262.92/41.34 % (1559377)Time elapsed: 7.077 s
% 262.92/41.34 % (1559377)Peak memory usage: 142 MB
% 262.92/41.34 % (1559377)Instructions burned: 20139 (million)
% 262.92/41.34 % (1559381)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=685219758:i=11404_2620 on theBenchmark for (2620ds/11404Mi)
% 262.92/41.34 % (1559381) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1559292-1559381"...
% 262.92/41.34 % (1559381)...printing done.
% 262.92/41.34 % (1559381)Refutation found. Thanks to Tanya!
% 262.92/41.34 % SZS status Theorem for theBenchmark
% 262.92/41.34 % SZS output start Proof for theBenchmark
% See solution above
% 262.92/41.34 % (1559381)------------------------------
% 262.92/41.34 % (1559381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 262.92/41.34 % (1559381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 262.92/41.34 % (1559381)CaDiCaL version: 2.1.3
% 262.92/41.34 % (1559381)Termination reason: Refutation
% 262.92/41.34 % (1559381)Time elapsed: 2.681 s
% 262.92/41.34 % (1559381)Peak memory usage: 75 MB
% 262.92/41.34 % (1559381)Instructions burned: 10892 (million)
% 262.92/41.34 % (1559292)Success in time 40.9 s
% 262.92/41.34 % Vampire exiting
%------------------------------------------------------------------------------