%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM480+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:24:29 PM UTC 2026
% Result : Theorem 20.48s 3.38s
% Output : Refutation 20.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 13
% Syntax : Number of formulae : 85 ( 34 unt; 4 def)
% Number of atoms : 261 ( 95 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 306 ( 130 ~; 139 |; 25 &)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 96 ( 91 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f9,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulAsso) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
fof(f36,axiom,
( aNaturalNumber0(xl)
& aNaturalNumber0(xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1524) ).
fof(f37,axiom,
( xl != sz00
& doDivides0(xl,xm) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1524_04) ).
fof(f38,axiom,
aNaturalNumber0(xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1553) ).
fof(f40,conjecture,
sdtasdt0(xn,sdtsldt0(xm,xl)) = sdtsldt0(sdtasdt0(xn,xm),xl),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f41,negated_conjecture,
sdtasdt0(xn,sdtsldt0(xm,xl)) != sdtsldt0(sdtasdt0(xn,xm),xl),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f44,plain,
sdtsldt0(sdtasdt0(xn,xm),xl) != sdtasdt0(xn,sdtsldt0(xm,xl)),
inference(flattening,[],[f41]) ).
fof(f48,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f49,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f48]) ).
fof(f55,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f56,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f58,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f57]) ).
fof(f90,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f91,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f93,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f92]) ).
fof(f107,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(nnf_transformation,[],[f91]) ).
fof(f108,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X0,X3) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(rectify,[],[f107]) ).
fof(f109,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ( aNaturalNumber0(sK1(X0,X1))
& sdtasdt0(X0,sK1(X0,X1)) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1))],[f108]) ).
fof(f110,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = sdtsldt0(X1,X0)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 )
& ( ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| sdtsldt0(X1,X0) != X2 ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(nnf_transformation,[],[f93]) ).
fof(f111,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = sdtsldt0(X1,X0)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 )
& ( ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| sdtsldt0(X1,X0) != X2 ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f110]) ).
fof(f116,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f121,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f122,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(cnf_transformation,[],[f58]) ).
fof(f160,plain,
! [X2,X0,X1] :
( doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f109]) ).
fof(f161,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X2) = X1
| sdtsldt0(X1,X0) != X2
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f162,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X2)
| sdtsldt0(X1,X0) != X2
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f163,plain,
! [X2,X0,X1] :
( sdtsldt0(X1,X0) = X2
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f168,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f36]) ).
fof(f169,plain,
aNaturalNumber0(xl),
inference(cnf_transformation,[],[f36]) ).
fof(f170,plain,
doDivides0(xl,xm),
inference(cnf_transformation,[],[f37]) ).
fof(f171,plain,
sz00 != xl,
inference(cnf_transformation,[],[f37]) ).
fof(f172,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f38]) ).
fof(f174,plain,
sdtsldt0(sdtasdt0(xn,xm),xl) != sdtasdt0(xn,sdtsldt0(xm,xl)),
inference(cnf_transformation,[],[f44]) ).
fof(f181,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f160]) ).
fof(f182,plain,
! [X2,X0] :
( ~ doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| sz00 = X0
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f163]) ).
fof(f183,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(equality_resolution,[],[f162]) ).
fof(f184,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(equality_resolution,[],[f161]) ).
fof(f185,definition,
sF2 = sdtasdt0(xn,xm),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f186,plain,
sdtasdt0(xn,xm) = sF2,
inference(reorient_equations,[],[f185]) ).
fof(f187,definition,
sF3 = sdtsldt0(sF2,xl),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f188,plain,
sdtsldt0(sF2,xl) = sF3,
inference(reorient_equations,[],[f187]) ).
fof(f189,definition,
sF4 = sdtsldt0(xm,xl),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f190,plain,
sdtsldt0(xm,xl) = sF4,
inference(reorient_equations,[],[f189]) ).
fof(f191,definition,
sF5 = sdtasdt0(xn,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f192,plain,
sdtasdt0(xn,sF4) = sF5,
inference(reorient_equations,[],[f191]) ).
fof(f193,plain,
sF3 != sF5,
inference(definition_folding,[],[f174,f192,f190,f188,f186]) ).
fof(f244,plain,
( aNaturalNumber0(sF5)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sF4) ),
inference(superposition,[],[f116,f192]) ).
fof(f245,plain,
( ~ aNaturalNumber0(sF4)
| aNaturalNumber0(sF5) ),
inference(forward_subsumption_resolution,[],[f244,f172]) ).
fof(f269,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xl) = sdtasdt0(xl,X0) ),
inference(resolution,[],[f121,f169]) ).
fof(f512,plain,
( aNaturalNumber0(sF4)
| sz00 = xl
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[],[f183,f190]) ).
fof(f513,plain,
( aNaturalNumber0(sF4)
| ~ doDivides0(xl,xm)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f512,f171]) ).
fof(f515,plain,
( aNaturalNumber0(sF4)
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f513,f170]) ).
fof(f517,plain,
( aNaturalNumber0(sF4)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f515,f169]) ).
fof(f519,plain,
aNaturalNumber0(sF4),
inference(forward_subsumption_resolution,[],[f517,f168]) ).
fof(f520,plain,
aNaturalNumber0(sF5),
inference(resolution,[],[f519,f245]) ).
fof(f753,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,X1),xl) = sdtasdt0(X0,sdtasdt0(X1,xl)) ),
inference(resolution,[],[f122,f169]) ).
fof(f811,plain,
( sz00 = xl
| xm = sdtasdt0(xl,sdtsldt0(xm,xl))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(resolution,[],[f184,f170]) ).
fof(f828,plain,
( xm = sdtasdt0(xl,sdtsldt0(xm,xl))
| ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f811,f171]) ).
fof(f837,plain,
( xm = sdtasdt0(xl,sdtsldt0(xm,xl))
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f828,f169]) ).
fof(f842,plain,
xm = sdtasdt0(xl,sdtsldt0(xm,xl)),
inference(forward_subsumption_resolution,[],[f837,f168]) ).
fof(f846,plain,
xm = sdtasdt0(xl,sF4),
inference(forward_demodulation,[],[f842,f190]) ).
fof(f1754,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X1
| sdtsldt0(sdtasdt0(X1,X0),X1) = X0
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtasdt0(X1,X0)) ),
inference(resolution,[],[f182,f181]) ).
fof(f1781,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X1
| sdtsldt0(sdtasdt0(X1,X0),X1) = X0
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(sdtasdt0(X1,X0)) ),
inference(duplicate_literal_removal,[],[f1754]) ).
fof(f1796,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| sz00 = X1
| sdtsldt0(sdtasdt0(X1,X0),X1) = X0
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1781,f116]) ).
fof(f2311,plain,
sdtasdt0(xl,sF4) = sdtasdt0(sF4,xl),
inference(resolution,[],[f269,f519]) ).
fof(f2312,plain,
sdtasdt0(sF5,xl) = sdtasdt0(xl,sF5),
inference(resolution,[],[f269,f520]) ).
fof(f2313,plain,
xm = sdtasdt0(sF4,xl),
inference(forward_demodulation,[],[f2311,f846]) ).
fof(f4199,plain,
! [X0] :
( sz00 = xl
| sdtsldt0(sdtasdt0(xl,X0),xl) = X0
| ~ aNaturalNumber0(X0) ),
inference(resolution,[],[f1796,f169]) ).
fof(f4207,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtsldt0(sdtasdt0(xl,X0),xl) = X0 ),
inference(forward_subsumption_resolution,[],[f4199,f171]) ).
fof(f4292,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,sF4),xl) = sdtasdt0(X0,sdtasdt0(sF4,xl)) ),
inference(resolution,[],[f753,f519]) ).
fof(f4295,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xm) = sdtasdt0(sdtasdt0(X0,sF4),xl) ),
inference(forward_demodulation,[],[f4292,f2313]) ).
fof(f21193,plain,
sF5 = sdtsldt0(sdtasdt0(xl,sF5),xl),
inference(resolution,[],[f4207,f520]) ).
fof(f26074,plain,
sdtasdt0(xn,xm) = sdtasdt0(sdtasdt0(xn,sF4),xl),
inference(resolution,[],[f4295,f172]) ).
fof(f26083,plain,
sdtasdt0(xn,xm) = sdtasdt0(sF5,xl),
inference(forward_demodulation,[],[f26074,f192]) ).
fof(f26089,plain,
sdtasdt0(xn,xm) = sdtasdt0(xl,sF5),
inference(forward_demodulation,[],[f26083,f2312]) ).
fof(f26093,plain,
sF2 = sdtasdt0(xl,sF5),
inference(forward_demodulation,[],[f26089,f186]) ).
fof(f26094,plain,
sdtsldt0(sF2,xl) = sF5,
inference(superposition,[],[f21193,f26093]) ).
fof(f26155,plain,
sF3 = sF5,
inference(forward_demodulation,[],[f26094,f188]) ).
fof(f26182,plain,
$false,
inference(forward_subsumption_resolution,[],[f26155,f193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM480+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 20:05:50 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.74/1.59 % (2701195)Will run a generic schedule for satisfiability detection.
% 7.74/1.59 % (2701201)% WARNING: option uhcvi not known.
% 7.74/1.59 % (2701203)dis+10_1_sil=32000:sp=arity:random_seed=2297068909:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.74/1.59 % (2701200)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3035762627_2999 on theBenchmark for (2999ds/0Mi)
% 7.74/1.59 % (2701204)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3342074318:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.74/1.59 % (2701202)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2162350593:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.74/1.59 % (2701201)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=537268695:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.74/1.59 % (2701205)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=360993331:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.74/1.59 % (2701206)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=316187897:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.74/1.59 % TRYING [1]
% 7.74/1.59 % TRYING [2]
% 7.74/1.59 % TRYING [3]
% 7.74/1.59 % TRYING [4]
% 7.74/1.59 % TRYING [5]
% 7.74/1.59 % (2701203)Instruction limit reached!
% 7.74/1.59 % (2701203)------------------------------
% 7.74/1.59 % (2701203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.59 % (2701203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.59 % (2701203)CaDiCaL version: 2.1.3
% 7.74/1.59 % (2701203)Termination reason: Instruction limit
% 7.74/1.59 % (2701203)Termination phase: Saturation
% 7.74/1.59 % (2701203)Time elapsed: 0.033 s
% 7.74/1.59 % (2701203)Peak memory usage: 12 MB
% 7.74/1.59 % (2701203)Instructions burned: 105 (million)
% 7.74/1.59 % (2701204)Instruction limit reached!
% 7.74/1.59 % (2701204)------------------------------
% 7.74/1.59 % (2701204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.59 % (2701204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.59 % (2701204)CaDiCaL version: 2.1.3
% 7.74/1.59 % (2701204)Termination reason: Instruction limit
% 7.74/1.59 % (2701204)Termination phase: Saturation
% 7.74/1.59 % (2701204)Time elapsed: 0.036 s
% 7.74/1.59 % (2701204)Peak memory usage: 13 MB
% 7.74/1.59 % (2701204)Instructions burned: 116 (million)
% 7.74/1.59 % (2701205)Instruction limit reached!
% 7.74/1.59 % (2701205)------------------------------
% 7.74/1.59 % (2701205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.59 % (2701205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.59 % (2701205)CaDiCaL version: 2.1.3
% 7.74/1.59 % (2701205)Termination reason: Instruction limit
% 7.74/1.59 % (2701205)Termination phase: Saturation
% 7.74/1.59 % (2701205)Time elapsed: 0.042 s
% 7.74/1.59 % (2701205)Peak memory usage: 13 MB
% 7.74/1.59 % (2701205)Instructions burned: 131 (million)
% 7.74/1.59 % (2701214)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3439531637:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.74/1.59 % (2701215)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3019881355:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.74/1.59 % TRYING [1]
% 7.74/1.59 % TRYING [2]
% 7.74/1.59 % TRYING [3]
% 7.74/1.59 % (2701216)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=1732683331:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.74/1.59 % TRYING [4]
% 7.74/1.59 % (2701206)Instruction limit reached!
% 7.74/1.59 % (2701206)------------------------------
% 7.74/1.59 % (2701206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.74/1.59 % (2701206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.74/1.59 % (2701206)CaDiCaL version: 2.1.3
% 7.74/1.59 % (2701206)Termination reason: Instruction limit
% 7.74/1.59 % (2701206)Termination phase: Saturation
% 7.74/1.59 % (2701206)Time elapsed: 0.055 s
% 7.74/1.59 % (2701206)Peak memory usage: 14 MB
% 7.74/1.59 % (2701206)Instructions burned: 161 (million)
% 7.74/1.59 % TRYING [6]
% 7.74/1.59 % TRYING [5]
% 7.74/1.59 % (2701220)ott-21_1_sil=16000:fs=off:random_seed=1075310648:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.74/1.59 % (2701215)Instruction limit reached!
% 7.74/1.59 % (2701215)------------------------------
% 7.74/1.59 % (2701215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701215)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701215)Termination reason: Instruction limit
% 20.48/3.38 % (2701215)Termination phase: Saturation
% 20.48/3.38 % (2701215)Time elapsed: 0.035 s
% 20.48/3.38 % (2701215)Peak memory usage: 12 MB
% 20.48/3.38 % (2701215)Instructions burned: 133 (million)
% 20.48/3.38 % (2701222)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1662380819:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 20.48/3.38 % TRYING [6]
% 20.48/3.38 % (2701220)Instruction limit reached!
% 20.48/3.38 % (2701220)------------------------------
% 20.48/3.38 % (2701220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701220)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701220)Termination reason: Instruction limit
% 20.48/3.38 % (2701220)Termination phase: Saturation
% 20.48/3.38 % (2701220)Time elapsed: 0.051 s
% 20.48/3.38 % (2701220)Peak memory usage: 13 MB
% 20.48/3.38 % (2701220)Instructions burned: 181 (million)
% 20.48/3.38 % (2701224)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1335472652:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 20.48/3.38 % TRYING [1]
% 20.48/3.38 % TRYING [2]
% 20.48/3.38 % TRYING [3]
% 20.48/3.38 % TRYING [4]
% 20.48/3.38 % TRYING [7]
% 20.48/3.38 % TRYING [5]
% 20.48/3.38 % (2701214)Instruction limit reached!
% 20.48/3.38 % (2701214)------------------------------
% 20.48/3.38 % (2701214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701214)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701214)Termination reason: Instruction limit
% 20.48/3.38 % (2701214)Termination phase: Finite model building SAT solving
% 20.48/3.38 % (2701214)Time elapsed: 0.151 s
% 20.48/3.38 % (2701214)Peak memory usage: 33 MB
% 20.48/3.38 % (2701214)Instructions burned: 714 (million)
% 20.48/3.38 % (2701226)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1873336363:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 20.48/3.38 % (2701222)Instruction limit reached!
% 20.48/3.38 % (2701222)------------------------------
% 20.48/3.38 % (2701222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701222)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701222)Termination reason: Instruction limit
% 20.48/3.38 % (2701222)Termination phase: Saturation
% 20.48/3.38 % (2701222)Time elapsed: 0.171 s
% 20.48/3.38 % (2701222)Peak memory usage: 15 MB
% 20.48/3.38 % (2701222)Instructions burned: 478 (million)
% 20.48/3.38 % (2701216)Instruction limit reached!
% 20.48/3.38 % (2701216)------------------------------
% 20.48/3.38 % (2701216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701216)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701216)Termination reason: Instruction limit
% 20.48/3.38 % (2701216)Termination phase: Saturation
% 20.48/3.38 % (2701216)Time elapsed: 0.216 s
% 20.48/3.38 % (2701216)Peak memory usage: 19 MB
% 20.48/3.38 % (2701216)Instructions burned: 686 (million)
% 20.48/3.38 % (2701229)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=1720540595:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 20.48/3.38 % (2701228)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4115001101:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 20.48/3.38 % TRYING [6]
% 20.48/3.38 % (2701224)Instruction limit reached!
% 20.48/3.38 % (2701224)------------------------------
% 20.48/3.38 % (2701224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701224)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701224)Termination reason: Instruction limit
% 20.48/3.38 % (2701224)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701224)Time elapsed: 0.179 s
% 20.48/3.38 % (2701224)Peak memory usage: 21 MB
% 20.48/3.38 % (2701224)Instructions burned: 867 (million)
% 20.48/3.38 % (2701232)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=909566080:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 20.48/3.38 % TRYING [8]
% 20.48/3.38 % TRYING [14]
% 20.48/3.38 % (2701229)Instruction limit reached!
% 20.48/3.38 % (2701229)------------------------------
% 20.48/3.38 % (2701229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701229)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701229)Termination reason: Instruction limit
% 20.48/3.38 % (2701229)Termination phase: Saturation
% 20.48/3.38 % (2701229)Time elapsed: 0.182 s
% 20.48/3.38 % (2701229)Peak memory usage: 20 MB
% 20.48/3.38 % (2701229)Instructions burned: 694 (million)
% 20.48/3.38 % (2701228)Instruction limit reached!
% 20.48/3.38 % (2701228)------------------------------
% 20.48/3.38 % (2701228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701228)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701228)Termination reason: Instruction limit
% 20.48/3.38 % (2701228)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701228)Time elapsed: 0.189 s
% 20.48/3.38 % (2701228)Peak memory usage: 73 MB
% 20.48/3.38 % (2701228)Instructions burned: 894 (million)
% 20.48/3.38 % (2701234)fmb+10_1_sil=64000:random_seed=1021326312:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 20.48/3.38 % TRYING [1]
% 20.48/3.38 % TRYING [2]
% 20.48/3.38 % TRYING [3]
% 20.48/3.38 % (2701235)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3786977476:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 20.48/3.38 % TRYING [4]
% 20.48/3.38 % TRYING [20]
% 20.48/3.38 % TRYING [5]
% 20.48/3.38 % (2701226)Instruction limit reached!
% 20.48/3.38 % (2701226)------------------------------
% 20.48/3.38 % (2701226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701226)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701226)Termination reason: Instruction limit
% 20.48/3.38 % (2701226)Termination phase: Saturation
% 20.48/3.38 % (2701226)Time elapsed: 0.360 s
% 20.48/3.38 % (2701226)Peak memory usage: 25 MB
% 20.48/3.38 % (2701226)Instructions burned: 1181 (million)
% 20.48/3.38 % (2701238)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1365380809:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 20.48/3.38 % TRYING [8]
% 20.48/3.38 % (2701232)Instruction limit reached!
% 20.48/3.38 % (2701232)------------------------------
% 20.48/3.38 % (2701232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701232)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701232)Termination reason: Instruction limit
% 20.48/3.38 % (2701232)Termination phase: Saturation
% 20.48/3.38 % (2701232)Time elapsed: 0.270 s
% 20.48/3.38 % (2701232)Peak memory usage: 19 MB
% 20.48/3.38 % (2701232)Instructions burned: 883 (million)
% 20.48/3.38 % (2701240)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=330482481:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 20.48/3.38 % TRYING [6]
% 20.48/3.38 % (2701238)Instruction limit reached!
% 20.48/3.38 % (2701238)------------------------------
% 20.48/3.38 % (2701238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701238)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701238)Termination reason: Instruction limit
% 20.48/3.38 % (2701238)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701238)Time elapsed: 0.191 s
% 20.48/3.38 % (2701238)Peak memory usage: 66 MB
% 20.48/3.38 % (2701238)Instructions burned: 925 (million)
% 20.48/3.38 % (2701242)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1474282019:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 20.48/3.38 % TRYING [9]
% 20.48/3.38 % TRYING [7]
% 20.48/3.38 % (2701242)Instruction limit reached!
% 20.48/3.38 % (2701242)------------------------------
% 20.48/3.38 % (2701242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701242)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701242)Termination reason: Instruction limit
% 20.48/3.38 % (2701242)Termination phase: Saturation
% 20.48/3.38 % (2701242)Time elapsed: 0.421 s
% 20.48/3.38 % (2701242)Peak memory usage: 33 MB
% 20.48/3.38 % (2701242)Instructions burned: 1473 (million)
% 20.48/3.38 % (2701244)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=138331526:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 20.48/3.38 % TRYING [77]
% 20.48/3.38 % TRYING [8]
% 20.48/3.38 % TRYING [10]
% 20.48/3.38 % (2701240)Instruction limit reached!
% 20.48/3.38 % (2701240)------------------------------
% 20.48/3.38 % (2701240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701240)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701240)Termination reason: Instruction limit
% 20.48/3.38 % (2701240)Termination phase: Saturation
% 20.48/3.38 % (2701240)Time elapsed: 1.436 s
% 20.48/3.38 % (2701240)Peak memory usage: 50 MB
% 20.48/3.38 % (2701240)Instructions burned: 5133 (million)
% 20.48/3.38 % (2701246)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1097805743:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 20.48/3.38 % TRYING [16]
% 20.48/3.38 % (2701235)Instruction limit reached!
% 20.48/3.38 % (2701235)------------------------------
% 20.48/3.38 % (2701235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701235)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701235)Termination reason: Instruction limit
% 20.48/3.38 % (2701235)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701235)Time elapsed: 1.839 s
% 20.48/3.38 % (2701235)Peak memory usage: 573 MB
% 20.48/3.38 % (2701235)Instructions burned: 9515 (million)
% 20.48/3.38 % (2701248)ott-2_1_sil=16000:newcnf=on:random_seed=2160138144:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2976 on theBenchmark for (2976ds/869Mi)
% 20.48/3.38 % (2701244)Instruction limit reached!
% 20.48/3.38 % (2701244)------------------------------
% 20.48/3.38 % (2701244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701244)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701244)Termination reason: Instruction limit
% 20.48/3.38 % (2701244)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701244)Time elapsed: 1.239 s
% 20.48/3.38 % (2701244)Peak memory usage: 426 MB
% 20.48/3.38 % (2701244)Instructions burned: 6329 (million)
% 20.48/3.38 % (2701246)Instruction limit reached!
% 20.48/3.38 % (2701246)------------------------------
% 20.48/3.38 % (2701246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701246)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701246)Termination reason: Instruction limit
% 20.48/3.38 % (2701246)Termination phase: Finite model building constraint generation
% 20.48/3.38 % (2701246)Time elapsed: 0.419 s
% 20.48/3.38 % (2701246)Peak memory usage: 146 MB
% 20.48/3.38 % (2701246)Instructions burned: 2178 (million)
% 20.48/3.38 % (2701250)ott+10_1_sil=32000:tgt=ground:random_seed=1087283606:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 20.48/3.38 % (2701252)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2988322580:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 20.48/3.38 % TRYING [1]
% 20.48/3.38 % TRYING [2]
% 20.48/3.38 % TRYING [3]
% 20.48/3.38 % TRYING [4]
% 20.48/3.38 % TRYING [5]
% 20.48/3.38 % TRYING [6]
% 20.48/3.38 % (2701248)Instruction limit reached!
% 20.48/3.38 % (2701248)------------------------------
% 20.48/3.38 % (2701248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701248)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701248)Termination reason: Instruction limit
% 20.48/3.38 % (2701248)Termination phase: Saturation
% 20.48/3.38 % (2701248)Time elapsed: 0.254 s
% 20.48/3.38 % (2701248)Peak memory usage: 22 MB
% 20.48/3.38 % (2701248)Instructions burned: 869 (million)
% 20.48/3.38 % (2701254)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3735230264:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi)
% 20.48/3.38 % TRYING [7]
% 20.48/3.38 % TRYING [8]
% 20.48/3.38 % (2701250) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2701195-2701250"...
% 20.48/3.38 % (2701250)...printing done.
% 20.48/3.38 % (2701250)Refutation found. Thanks to Tanya!
% 20.48/3.38 % SZS status Theorem for theBenchmark
% 20.48/3.38 % SZS output start Proof for theBenchmark
% See solution above
% 20.48/3.38 % (2701250)------------------------------
% 20.48/3.38 % (2701250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.48/3.38 % (2701250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.48/3.38 % (2701250)CaDiCaL version: 2.1.3
% 20.48/3.38 % (2701250)Termination reason: Refutation
% 20.48/3.38 % (2701250)Time elapsed: 0.493 s
% 20.48/3.38 % (2701250)Peak memory usage: 22 MB
% 20.48/3.38 % (2701250)Instructions burned: 1640 (million)
% 20.48/3.38 % (2701195)Success in time 3.042 s
% 20.48/3.38 % Vampire exiting
%------------------------------------------------------------------------------