%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR079+7 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 09:45:01 AM UTC 2026
% Result : Theorem 112.36s 21.03s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 30 ( 14 unt; 1 def)
% Number of atoms : 156 ( 16 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 192 ( 66 ~; 63 |; 55 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 84 ( 72 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11718,axiom,
s__instance(s__WhalingConvention,s__Agreement),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_11834) ).
fof(f32412,axiom,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__instance(X3,X2)
& s__instance(X4,X0)
& s__instance(X5,X1) )
=> ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32603) ).
fof(f39577,axiom,
! [X0] :
( s__instance(X0,s__Agreement)
=> ? [X1,X2] :
( s__instance(X2,s__CognitiveAgent)
& s__instance(X1,s__CognitiveAgent)
& s__partyToAgreement(X1,X0)
& s__partyToAgreement(X2,X0)
& X1 != X2 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+2.ax',kb_SUMO_39907) ).
fof(f55620,conjecture,
? [X0] : s__instance(X0,s__Animal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f55621,negated_conjecture,
~ ? [X0] : s__instance(X0,s__Animal),
inference(negated_conjecture,[status(cth)],[f55620]) ).
fof(f73315,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
inference(ennf_transformation,[],[f32412]) ).
fof(f73316,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
inference(flattening,[],[f73315]) ).
fof(f75802,plain,
! [X0] :
( ? [X1,X2] :
( s__instance(X2,s__CognitiveAgent)
& s__instance(X1,s__CognitiveAgent)
& s__partyToAgreement(X1,X0)
& s__partyToAgreement(X2,X0)
& X1 != X2 )
| ~ s__instance(X0,s__Agreement) ),
inference(ennf_transformation,[],[f39577]) ).
fof(f79020,plain,
! [X0] : ~ s__instance(X0,s__Animal),
inference(ennf_transformation,[],[f55621]) ).
fof(f79182,definition,
! [X1,X2,X0] :
( sP84(X1,X2,X0)
<=> ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ) ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f79183,plain,
! [X0,X1,X2] :
( X1 = s__UnionFn(X2,X0)
<=> sP84(X1,X2,X0) ),
inference(definition_folding,[],[f73316,f79182]) ).
fof(f80409,plain,
! [X1,X2,X0] :
( ( sP84(X1,X2,X0)
| ? [X3,X4,X5] :
( ( ~ s__instance(X3,X1)
| ~ s__instance(X4,X1)
| ( ~ s__instance(X5,X2)
& ~ s__instance(X5,X0) ) )
& s__instance(X3,X2)
& s__instance(X4,X0)
& s__instance(X5,X1)
& s__instance(X2,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) ) )
& ( ! [X3,X4,X5] :
( ( s__instance(X3,X1)
& s__instance(X4,X1)
& ( s__instance(X5,X2)
| s__instance(X5,X0) ) )
| ~ s__instance(X3,X2)
| ~ s__instance(X4,X0)
| ~ s__instance(X5,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) )
| ~ sP84(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f79182]) ).
fof(f80410,plain,
! [X0,X1,X2] :
( ( sP84(X0,X1,X2)
| ? [X3,X4,X5] :
( ( ~ s__instance(X3,X0)
| ~ s__instance(X4,X0)
| ( ~ s__instance(X5,X1)
& ~ s__instance(X5,X2) ) )
& s__instance(X3,X1)
& s__instance(X4,X2)
& s__instance(X5,X0)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass)
& s__instance(X2,s__SetOrClass) ) )
& ( ! [X6,X7,X8] :
( ( s__instance(X6,X0)
& s__instance(X7,X0)
& ( s__instance(X8,X1)
| s__instance(X8,X2) ) )
| ~ s__instance(X6,X1)
| ~ s__instance(X7,X2)
| ~ s__instance(X8,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) )
| ~ sP84(X0,X1,X2) ) ),
inference(rectify,[],[f80409]) ).
fof(f80411,plain,
! [X0,X1,X2] :
( ( sP84(X0,X1,X2)
| ( ( ~ s__instance(sK1217(X0,X1,X2),X0)
| ~ s__instance(sK1218(X0,X1,X2),X0)
| ( ~ s__instance(sK1219(X0,X1,X2),X1)
& ~ s__instance(sK1219(X0,X1,X2),X2) ) )
& s__instance(sK1217(X0,X1,X2),X1)
& s__instance(sK1218(X0,X1,X2),X2)
& s__instance(sK1219(X0,X1,X2),X0)
& s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass)
& s__instance(X2,s__SetOrClass) ) )
& ( ! [X6,X7,X8] :
( ( s__instance(X6,X0)
& s__instance(X7,X0)
& ( s__instance(X8,X1)
| s__instance(X8,X2) ) )
| ~ s__instance(X6,X1)
| ~ s__instance(X7,X2)
| ~ s__instance(X8,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) )
| ~ sP84(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1217,sK1218,sK1219]),skolemize(X3,sK1217(X0,X1,X2)),skolemize(X4,sK1218(X0,X1,X2)),skolemize(X5,sK1219(X0,X1,X2))],[f80410]) ).
fof(f80412,plain,
! [X0,X1,X2] :
( ( X1 = s__UnionFn(X2,X0)
| ~ sP84(X1,X2,X0) )
& ( sP84(X1,X2,X0)
| s__UnionFn(X2,X0) != X1 ) ),
inference(nnf_transformation,[],[f79183]) ).
fof(f81202,plain,
! [X0] :
( ( s__instance(sK2048(X0),s__CognitiveAgent)
& s__instance(sK2047(X0),s__CognitiveAgent)
& s__partyToAgreement(sK2047(X0),X0)
& s__partyToAgreement(sK2048(X0),X0)
& sK2047(X0) != sK2048(X0) )
| ~ s__instance(X0,s__Agreement) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2047,sK2048]),skolemize(X1,sK2047(X0)),skolemize(X2,sK2048(X0))],[f75802]) ).
fof(f95188,plain,
s__instance(s__WhalingConvention,s__Agreement),
inference(cnf_transformation,[],[f11718]) ).
fof(f111071,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| s__instance(sK1219(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f80411]) ).
fof(f111072,plain,
! [X2,X0,X1] :
( sP84(X0,X1,X2)
| s__instance(sK1218(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f80411]) ).
fof(f111077,plain,
! [X2,X0,X1] :
( ~ sP84(X1,X2,X0)
| s__UnionFn(X2,X0) = X1 ),
inference(cnf_transformation,[],[f80412]) ).
fof(f120148,plain,
! [X0] :
( sK2047(X0) != sK2048(X0)
| ~ s__instance(X0,s__Agreement) ),
inference(cnf_transformation,[],[f81202]) ).
fof(f139318,plain,
! [X0] : ~ s__instance(X0,s__Animal),
inference(cnf_transformation,[],[f79020]) ).
fof(f253649,plain,
sK2048(s__WhalingConvention) != sK2047(s__WhalingConvention),
inference(unit_resulting_resolution,[],[f120148,f95188]) ).
fof(f439075,plain,
! [X0,X1] : sP84(s__Animal,X0,X1),
inference(unit_resulting_resolution,[],[f111071,f139318]) ).
fof(f439117,plain,
! [X0,X1] : s__Animal = s__UnionFn(X0,X1),
inference(unit_resulting_resolution,[],[f111077,f439075]) ).
fof(f439354,plain,
! [X0,X1] : sP84(X0,X1,s__Animal),
inference(unit_resulting_resolution,[],[f111072,f139318]) ).
fof(f439426,plain,
! [X0,X1] : s__UnionFn(X0,s__Animal) = X1,
inference(resolution,[],[f439354,f111077]) ).
fof(f439427,plain,
! [X1] : s__Animal = X1,
inference(forward_demodulation,[],[f439426,f439117]) ).
fof(f592619,plain,
s__Animal != sK2047(s__WhalingConvention),
inference(superposition,[],[f253649,f439427]) ).
fof(f593936,plain,
$false,
inference(forward_subsumption_resolution,[],[f592619,f439427]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR079+7 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n020.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 22:30:05 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 28.80/6.06 % (648736)Will run a generic schedule for satisfiability detection.
% 28.80/6.06 % (648742)% WARNING: option uhcvi not known.
% 28.80/6.06 % (648742)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1928716231:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi)
% 28.80/6.06 % (648741)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2475548223_2984 on theBenchmark for (2984ds/0Mi)
% 28.80/6.06 % (648743)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=568862065:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi)
% 28.80/6.06 % (648744)dis+10_1_sil=32000:sp=arity:random_seed=1974985576:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi)
% 28.80/6.06 % (648745)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3444662099:i=116_2984 on theBenchmark for (2984ds/116Mi)
% 28.80/6.06 % (648746)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1043918106:i=131_2984 on theBenchmark for (2984ds/131Mi)
% 28.80/6.06 % (648747)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4046231863:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi)
% 28.80/6.06 % (648744)Instruction limit reached!
% 28.80/6.06 % (648744)------------------------------
% 28.80/6.06 % (648744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/6.06 % (648744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/6.06 % (648744)CaDiCaL version: 2.1.3
% 28.80/6.06 % (648744)Termination reason: Instruction limit
% 28.80/6.06 % (648744)Termination phase: Preprocessing 1
% 28.80/6.06 % (648744)Time elapsed: 0.066 s
% 28.80/6.06 % (648744)Peak memory usage: 90 MB
% 28.80/6.06 % (648744)Instructions burned: 104 (million)
% 28.80/6.06 % (648745)Instruction limit reached!
% 28.80/6.06 % (648745)------------------------------
% 28.80/6.06 % (648745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/6.06 % (648745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/6.06 % (648745)CaDiCaL version: 2.1.3
% 28.80/6.06 % (648745)Termination reason: Instruction limit
% 28.80/6.06 % (648745)Termination phase: Preprocessing 1
% 28.80/6.06 % (648745)Time elapsed: 0.083 s
% 28.80/6.06 % (648745)Peak memory usage: 90 MB
% 28.80/6.06 % (648745)Instructions burned: 116 (million)
% 28.80/6.06 % (648746)Instruction limit reached!
% 28.80/6.06 % (648746)------------------------------
% 28.80/6.06 % (648746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/6.06 % (648746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/6.06 % (648746)CaDiCaL version: 2.1.3
% 28.80/6.06 % (648746)Termination reason: Instruction limit
% 28.80/6.06 % (648746)Termination phase: Preprocessing 1
% 28.80/6.06 % (648746)Time elapsed: 0.082 s
% 28.80/6.06 % (648746)Peak memory usage: 90 MB
% 28.80/6.06 % (648746)Instructions burned: 131 (million)
% 28.80/6.06 % (648755)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=527379368:i=714:nm=2_2983 on theBenchmark for (2983ds/714Mi)
% 28.80/6.06 % (648747)Instruction limit reached!
% 28.80/6.06 % (648747)------------------------------
% 28.80/6.06 % (648747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/6.06 % (648747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/6.06 % (648747)CaDiCaL version: 2.1.3
% 28.80/6.06 % (648747)Termination reason: Instruction limit
% 28.80/6.06 % (648747)Termination phase: Preprocessing 1
% 28.80/6.06 % (648747)Time elapsed: 0.104 s
% 28.80/6.06 % (648747)Peak memory usage: 90 MB
% 28.80/6.06 % (648747)Instructions burned: 160 (million)
% 28.80/6.06 % (648757)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2511689348:i=131:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/131Mi)
% 28.80/6.06 % (648758)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=1771046137:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2982 on theBenchmark for (2982ds/684Mi)
% 28.80/6.06 % (648761)ott-21_1_sil=16000:fs=off:random_seed=505913760:i=180:av=off:fsr=off_2982 on theBenchmark for (2982ds/180Mi)
% 28.80/6.06 % (648757)Instruction limit reached!
% 28.80/6.06 % (648757)------------------------------
% 28.80/6.06 % (648757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.80/6.06 % (648757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.80/6.06 % (648757)CaDiCaL version: 2.1.3
% 28.80/6.06 % (648757)Termination reason: Instruction limit
% 46.44/8.14 % (648757)Termination phase: Preprocessing 1
% 46.44/8.14 % (648757)Time elapsed: 0.086 s
% 46.44/8.14 % (648757)Peak memory usage: 90 MB
% 46.44/8.14 % (648757)Instructions burned: 131 (million)
% 46.44/8.14 % (648763)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4077086464:i=477:bd=all_2981 on theBenchmark for (2981ds/477Mi)
% 46.44/8.14 % (648761)Instruction limit reached!
% 46.44/8.14 % (648761)------------------------------
% 46.44/8.14 % (648761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648761)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648761)Termination reason: Instruction limit
% 46.44/8.14 % (648761)Termination phase: Unused predicate definition removal
% 46.44/8.14 % (648761)Time elapsed: 0.126 s
% 46.44/8.14 % (648761)Peak memory usage: 91 MB
% 46.44/8.14 % (648761)Instructions burned: 180 (million)
% 46.44/8.14 % (648765)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=922530034:fmbsr=1.3:i=865:ins=25_2981 on theBenchmark for (2981ds/865Mi)
% 46.44/8.14 % (648755)Instruction limit reached!
% 46.44/8.14 % (648755)------------------------------
% 46.44/8.14 % (648755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648755)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648755)Termination reason: Instruction limit
% 46.44/8.14 % (648755)Termination phase: Unused predicate definition removal
% 46.44/8.14 % (648755)Time elapsed: 0.420 s
% 46.44/8.14 % (648755)Peak memory usage: 127 MB
% 46.44/8.14 % (648755)Instructions burned: 714 (million)
% 46.44/8.14 % (648758)Instruction limit reached!
% 46.44/8.14 % (648758)------------------------------
% 46.44/8.14 % (648758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648758)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648758)Termination reason: Instruction limit
% 46.44/8.14 % (648758)Termination phase: NewCNF
% 46.44/8.14 % (648758)Time elapsed: 0.428 s
% 46.44/8.14 % (648758)Peak memory usage: 106 MB
% 46.44/8.14 % (648758)Instructions burned: 686 (million)
% 46.44/8.14 % (648763)Instruction limit reached!
% 46.44/8.14 % (648763)------------------------------
% 46.44/8.14 % (648763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648763)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648763)Termination reason: Instruction limit
% 46.44/8.14 % (648763)Termination phase: Preprocessing 3
% 46.44/8.14 % (648763)Time elapsed: 0.318 s
% 46.44/8.14 % (648763)Peak memory usage: 102 MB
% 46.44/8.14 % (648763)Instructions burned: 477 (million)
% 46.44/8.14 % (648767)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=904697639:i=1179_2978 on theBenchmark for (2978ds/1179Mi)
% 46.44/8.14 % (648769)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=385521314:i=889:ins=1_2978 on theBenchmark for (2978ds/889Mi)
% 46.44/8.14 % (648770)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=1813399050:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2978 on theBenchmark for (2978ds/692Mi)
% 46.44/8.14 % (648765)Instruction limit reached!
% 46.44/8.14 % (648765)------------------------------
% 46.44/8.14 % (648765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648765)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648765)Termination reason: Instruction limit
% 46.44/8.14 % (648765)Termination phase: Naming
% 46.44/8.14 % (648765)Time elapsed: 0.536 s
% 46.44/8.14 % (648765)Peak memory usage: 156 MB
% 46.44/8.14 % (648765)Instructions burned: 866 (million)
% 46.44/8.14 % (648773)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1604614731:i=879:kws=inv_precedence:fsr=off_2975 on theBenchmark for (2975ds/879Mi)
% 46.44/8.14 % (648770)Instruction limit reached!
% 46.44/8.14 % (648770)------------------------------
% 46.44/8.14 % (648770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.44/8.14 % (648770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.44/8.14 % (648770)CaDiCaL version: 2.1.3
% 46.44/8.14 % (648770)Termination reason: Instruction limit
% 82.54/13.20 % (648770)Termination phase: NewCNF
% 82.54/13.20 % (648770)Time elapsed: 0.430 s
% 82.54/13.20 % (648770)Peak memory usage: 106 MB
% 82.54/13.20 % (648770)Instructions burned: 694 (million)
% 82.54/13.20 % (648775)fmb+10_1_sil=64000:random_seed=4178509871:i=22061:nm=2:gsp=on_2973 on theBenchmark for (2973ds/22061Mi)
% 82.54/13.20 % (648769)Instruction limit reached!
% 82.54/13.20 % (648769)------------------------------
% 82.54/13.20 % (648769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648769)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648769)Termination reason: Instruction limit
% 82.54/13.20 % (648769)Termination phase: Naming
% 82.54/13.20 % (648769)Time elapsed: 0.535 s
% 82.54/13.20 % (648769)Peak memory usage: 149 MB
% 82.54/13.20 % (648769)Instructions burned: 890 (million)
% 82.54/13.20 % (648777)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4047303563:i=9515:nm=5_2972 on theBenchmark for (2972ds/9515Mi)
% 82.54/13.20 % (648767)Instruction limit reached!
% 82.54/13.20 % (648767)------------------------------
% 82.54/13.20 % (648767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648767)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648767)Termination reason: Instruction limit
% 82.54/13.20 % (648767)Termination phase: Property scanning
% 82.54/13.20 % (648767)Time elapsed: 0.702 s
% 82.54/13.20 % (648767)Peak memory usage: 111 MB
% 82.54/13.20 % (648767)Instructions burned: 1179 (million)
% 82.54/13.20 % (648779)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2473632782:fmbsr=1.7:i=920_2971 on theBenchmark for (2971ds/920Mi)
% 82.54/13.20 % (648773)Instruction limit reached!
% 82.54/13.20 % (648773)------------------------------
% 82.54/13.20 % (648773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648773)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648773)Termination reason: Instruction limit
% 82.54/13.20 % (648773)Termination phase: NewCNF
% 82.54/13.20 % (648773)Time elapsed: 0.482 s
% 82.54/13.20 % (648773)Peak memory usage: 114 MB
% 82.54/13.20 % (648773)Instructions burned: 882 (million)
% 82.54/13.20 % (648781)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=863244070:i=5131_2970 on theBenchmark for (2970ds/5131Mi)
% 82.54/13.20 % (648779)Instruction limit reached!
% 82.54/13.20 % (648779)------------------------------
% 82.54/13.20 % (648779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648779)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648779)Termination reason: Instruction limit
% 82.54/13.20 % (648779)Termination phase: Preprocessing 3
% 82.54/13.20 % (648779)Time elapsed: 0.580 s
% 82.54/13.20 % (648779)Peak memory usage: 149 MB
% 82.54/13.20 % (648779)Instructions burned: 922 (million)
% 82.54/13.20 % (648783)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4039035752:i=1472:ins=7:fdi=8:gsp=on_2965 on theBenchmark for (2965ds/1472Mi)
% 82.54/13.20 % (648783)Instruction limit reached!
% 82.54/13.20 % (648783)------------------------------
% 82.54/13.20 % (648783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648783)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648783)Termination reason: Instruction limit
% 82.54/13.20 % (648783)Termination phase: Saturation
% 82.54/13.20 % (648783)Time elapsed: 0.841 s
% 82.54/13.20 % (648783)Peak memory usage: 117 MB
% 82.54/13.20 % (648783)Instructions burned: 1473 (million)
% 82.54/13.20 % (648785)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=446909753:i=6324_2956 on theBenchmark for (2956ds/6324Mi)
% 82.54/13.20 % (648781)Instruction limit reached!
% 82.54/13.20 % (648781)------------------------------
% 82.54/13.20 % (648781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.54/13.20 % (648781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.54/13.20 % (648781)CaDiCaL version: 2.1.3
% 82.54/13.20 % (648781)Termination reason: Instruction limit
% 82.54/13.20 % (648781)Termination phase: Saturation
% 82.54/13.20 % (648781)Time elapsed: 2.810 s
% 82.54/13.20 % (648781)Peak memory usage: 163 MB
% 82.54/13.20 % (648781)Instructions burned: 5131 (million)
% 82.54/13.20 % (648787)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4261638157:fmbsr=2.30978:i=2174_2941 on theBenchmark for (2941ds/2174Mi)
% 128.91/19.81 % (648787)Instruction limit reached!
% 128.91/19.81 % (648787)------------------------------
% 128.91/19.81 % (648787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648787)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648787)Termination reason: Instruction limit
% 128.91/19.81 % (648787)Termination phase: Function definition elimination
% 128.91/19.81 % (648787)Time elapsed: 1.203 s
% 128.91/19.81 % (648787)Peak memory usage: 168 MB
% 128.91/19.81 % (648787)Instructions burned: 2174 (million)
% 128.91/19.81 % (648789)ott-2_1_sil=16000:newcnf=on:random_seed=1426226806:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2929 on theBenchmark for (2929ds/869Mi)
% 128.91/19.81 % (648777)Instruction limit reached!
% 128.91/19.81 % (648777)------------------------------
% 128.91/19.81 % (648777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648777)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648777)Termination reason: Instruction limit
% 128.91/19.81 % (648777)Termination phase: Finite model building preprocessing
% 128.91/19.81 % (648777)Time elapsed: 4.596 s
% 128.91/19.81 % (648777)Peak memory usage: 284 MB
% 128.91/19.81 % (648777)Instructions burned: 9516 (million)
% 128.91/19.81 % (648791)ott+10_1_sil=32000:tgt=ground:random_seed=3217466230:i=5114:av=off_2926 on theBenchmark for (2926ds/5114Mi)
% 128.91/19.81 % (648789)Instruction limit reached!
% 128.91/19.81 % (648789)------------------------------
% 128.91/19.81 % (648789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648789)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648789)Termination reason: Instruction limit
% 128.91/19.81 % (648789)Termination phase: NewCNF
% 128.91/19.81 % (648789)Time elapsed: 0.458 s
% 128.91/19.81 % (648789)Peak memory usage: 114 MB
% 128.91/19.81 % (648789)Instructions burned: 870 (million)
% 128.91/19.81 % (648793)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2877777821:i=54282_2924 on theBenchmark for (2924ds/54282Mi)
% 128.91/19.81 % Detected minimum model sizes of [617]
% 128.91/19.81 % Detected maximum model sizes of [max]
% 128.91/19.81 % (648775)Cannot represent all propositional literals internally
% 128.91/19.81 % (648775)Refutation not found, incomplete strategy
% 128.91/19.81 % (648775)------------------------------
% 128.91/19.81 % (648775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648775)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648775)Termination reason: Refutation not found, incomplete strategy
% 128.91/19.81 % (648775)Time elapsed: 5.069 s
% 128.91/19.81 % (648775)Peak memory usage: 286 MB
% 128.91/19.81 % (648775)Instructions burned: 10574 (million)
% 128.91/19.81 % (648785)Instruction limit reached!
% 128.91/19.81 % (648785)------------------------------
% 128.91/19.81 % (648785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648785)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648785)Termination reason: Instruction limit
% 128.91/19.81 % (648785)Termination phase: Finite model building preprocessing
% 128.91/19.81 % (648785)Time elapsed: 3.356 s
% 128.91/19.81 % (648785)Peak memory usage: 263 MB
% 128.91/19.81 % (648785)Instructions burned: 6324 (million)
% 128.91/19.81 % (648795)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2747459078:i=3512:aac=none_2922 on theBenchmark for (2922ds/3512Mi)
% 128.91/19.81 % (648775)------------------------------
% 128.91/19.81 % (648775)------------------------------
% 128.91/19.81 % (648797)dis+21_1_sil=32000:sas=cadical:random_seed=423995858:i=3773:amm=off_2921 on theBenchmark for (2921ds/3773Mi)
% 128.91/19.81 % Detected minimum model sizes of [617]
% 128.91/19.81 % Detected maximum model sizes of [max]
% 128.91/19.81 % (648741)Cannot represent all propositional literals internally
% 128.91/19.81 % (648741)Refutation not found, incomplete strategy
% 128.91/19.81 % (648741)------------------------------
% 128.91/19.81 % (648741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.91/19.81 % (648741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.91/19.81 % (648741)CaDiCaL version: 2.1.3
% 128.91/19.81 % (648741)Termination reason: Refutation not found, incomplete strategy
% 112.36/20.93 % (648741)Time elapsed: 6.322 s
% 112.36/20.93 % (648741)Peak memory usage: 332 MB
% 112.36/20.93 % (648741)Instructions burned: 12757 (million)
% 112.36/20.93 % (648741)------------------------------
% 112.36/20.93 % (648741)------------------------------
% 112.36/20.93 % (648799)ott+11_1_sil=16000:gs=on:random_seed=3260459718:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi)
% 112.36/20.93 % (648799)Instruction limit reached!
% 112.36/20.93 % (648799)------------------------------
% 112.36/20.93 % (648799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648799)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648799)Termination reason: Instruction limit
% 112.36/20.93 % (648799)Termination phase: Saturation
% 112.36/20.93 % (648799)Time elapsed: 1.305 s
% 112.36/20.93 % (648799)Peak memory usage: 130 MB
% 112.36/20.93 % (648799)Instructions burned: 2251 (million)
% 112.36/20.93 % (648801)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2249072415:fmbsr=1.6:i=67534_2905 on theBenchmark for (2905ds/67534Mi)
% 112.36/20.93 % (648795)Instruction limit reached!
% 112.36/20.93 % (648795)------------------------------
% 112.36/20.93 % (648795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648795)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648795)Termination reason: Instruction limit
% 112.36/20.93 % (648795)Termination phase: Saturation
% 112.36/20.93 % (648795)Time elapsed: 1.955 s
% 112.36/20.93 % (648795)Peak memory usage: 149 MB
% 112.36/20.93 % (648795)Instructions burned: 3513 (million)
% 112.36/20.93 % (648803)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2233939563:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2902 on theBenchmark for (2902ds/4591Mi)
% 112.36/20.93 % (648797)Instruction limit reached!
% 112.36/20.93 % (648797)------------------------------
% 112.36/20.93 % (648797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648797)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648797)Termination reason: Instruction limit
% 112.36/20.93 % (648797)Termination phase: Saturation
% 112.36/20.93 % (648797)Time elapsed: 2.093 s
% 112.36/20.93 % (648797)Peak memory usage: 150 MB
% 112.36/20.93 % (648797)Instructions burned: 3774 (million)
% 112.36/20.93 % (648805)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2157600101:i=29340_2900 on theBenchmark for (2900ds/29340Mi)
% 112.36/20.93 % (648791)Instruction limit reached!
% 112.36/20.93 % (648791)------------------------------
% 112.36/20.93 % (648791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648791)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648791)Termination reason: Instruction limit
% 112.36/20.93 % (648791)Termination phase: Saturation
% 112.36/20.93 % (648791)Time elapsed: 2.924 s
% 112.36/20.93 % (648791)Peak memory usage: 156 MB
% 112.36/20.93 % (648791)Instructions burned: 5114 (million)
% 112.36/20.93 % (648807)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1401027077:i=5211_2896 on theBenchmark for (2896ds/5211Mi)
% 112.36/20.93 % (648803)Instruction limit reached!
% 112.36/20.93 % (648803)------------------------------
% 112.36/20.93 % (648803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648803)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648803)Termination reason: Instruction limit
% 112.36/20.93 % (648803)Termination phase: Saturation
% 112.36/20.93 % (648803)Time elapsed: 2.604 s
% 112.36/20.93 % (648803)Peak memory usage: 154 MB
% 112.36/20.93 % (648803)Instructions burned: 4592 (million)
% 112.36/20.93 % (648809)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3769673852:i=5497:nm=2_2875 on theBenchmark for (2875ds/5497Mi)
% 112.36/20.93 % (648807)Instruction limit reached!
% 112.36/20.93 % (648807)------------------------------
% 112.36/20.93 % (648807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648807)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648807)Termination reason: Instruction limit
% 112.36/20.93 % (648807)Termination phase: Saturation
% 112.36/20.93 % (648807)Time elapsed: 2.609 s
% 112.36/20.93 % (648807)Peak memory usage: 182 MB
% 112.36/20.93 % (648807)Instructions burned: 5211 (million)
% 112.36/20.93 % (648811)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1942681971:fmbsr=2:i=46332_2869 on theBenchmark for (2869ds/46332Mi)
% 112.36/20.93 % Detected minimum model sizes of [617]
% 112.36/20.93 % Detected maximum model sizes of [max]
% 112.36/20.93 % (648793)Cannot represent all propositional literals internally
% 112.36/20.93 % (648793)Refutation not found, incomplete strategy
% 112.36/20.93 % (648793)------------------------------
% 112.36/20.93 % (648793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648793)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648793)Termination reason: Refutation not found, incomplete strategy
% 112.36/20.93 % (648793)Time elapsed: 6.332 s
% 112.36/20.93 % (648793)Peak memory usage: 330 MB
% 112.36/20.93 % (648793)Instructions burned: 12728 (million)
% 112.36/20.93 % (648793)------------------------------
% 112.36/20.93 % (648793)------------------------------
% 112.36/20.93 % (648813)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1789501993:i=14071_2859 on theBenchmark for (2859ds/14071Mi)
% 112.36/20.93 % Detected minimum model sizes of [617]
% 112.36/20.93 % Detected maximum model sizes of [max]
% 112.36/20.93 % (648801)Cannot represent all propositional literals internally
% 112.36/20.93 % (648801)Refutation not found, incomplete strategy
% 112.36/20.93 % (648801)------------------------------
% 112.36/20.93 % (648801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648801)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648801)Termination reason: Refutation not found, incomplete strategy
% 112.36/20.93 % (648801)Time elapsed: 6.065 s
% 112.36/20.93 % (648801)Peak memory usage: 312 MB
% 112.36/20.93 % (648801)Instructions burned: 12659 (million)
% 112.36/20.93 % (648809)Instruction limit reached!
% 112.36/20.93 % (648809)------------------------------
% 112.36/20.93 % (648809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648809)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648809)Termination reason: Instruction limit
% 112.36/20.93 % (648809)Termination phase: Finite model building preprocessing
% 112.36/20.93 % (648809)Time elapsed: 3.067 s
% 112.36/20.93 % (648809)Peak memory usage: 256 MB
% 112.36/20.93 % (648809)Instructions burned: 5498 (million)
% 112.36/20.93 % (648815)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2697518934:i=22565:add=on:rawr=on_2844 on theBenchmark for (2844ds/22565Mi)
% 112.36/20.93 % (648801)------------------------------
% 112.36/20.93 % (648801)------------------------------
% 112.36/20.93 % (648817)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3304077580:i=8173:av=off_2843 on theBenchmark for (2843ds/8173Mi)
% 112.36/20.93 % Detected minimum model sizes of [617]
% 112.36/20.93 % Detected maximum model sizes of [max]
% 112.36/20.93 % (648811)Cannot represent all propositional literals internally
% 112.36/20.93 % (648811)Refutation not found, incomplete strategy
% 112.36/20.93 % (648811)------------------------------
% 112.36/20.93 % (648811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648811)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648811)Termination reason: Refutation not found, incomplete strategy
% 112.36/20.93 % (648811)Time elapsed: 5.941 s
% 112.36/20.93 % (648811)Peak memory usage: 312 MB
% 112.36/20.93 % (648811)Instructions burned: 12660 (million)
% 112.36/20.93 % (648811)------------------------------
% 112.36/20.93 % (648811)------------------------------
% 112.36/20.93 % (648819)dis+10_16:1_sil=16000:random_seed=3889831673:i=9155:fsr=off_2808 on theBenchmark for (2808ds/9155Mi)
% 112.36/20.93 % Detected minimum model sizes of [617]
% 112.36/20.93 % Detected maximum model sizes of [max]
% 112.36/20.93 % (648813)Cannot represent all propositional literals internally
% 112.36/20.93 % (648813)Refutation not found, incomplete strategy
% 112.36/20.93 % (648813)------------------------------
% 112.36/20.93 % (648813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.36/20.93 % (648813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.36/20.93 % (648813)CaDiCaL version: 2.1.3
% 112.36/20.93 % (648813)Termination reason: Refutation not found, incomplete strategy
% 112.36/21.03 % (648813)Time elapsed: 5.511 s
% 112.36/21.03 % (648813)Peak memory usage: 304 MB
% 112.36/21.03 % (648813)Instructions burned: 11512 (million)
% 112.36/21.03 % (648813)------------------------------
% 112.36/21.03 % (648813)------------------------------
% 112.36/21.03 % (648821)ott-3_8_sil=64000:random_seed=1228573525:i=20139:bs=on_2802 on theBenchmark for (2802ds/20139Mi)
% 112.36/21.03 % (648805) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-648736-648805"...
% 112.36/21.03 % (648805)...printing done.
% 112.36/21.03 % (648805)Refutation found. Thanks to Tanya!
% 112.36/21.03 % SZS status Theorem for theBenchmark
% 112.36/21.03 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/21.03 % (648805)------------------------------
% 0.18/21.03 % (648805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/21.03 % (648805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/21.03 % (648805)CaDiCaL version: 2.1.3
% 0.18/21.03 % (648805)Termination reason: Refutation
% 0.18/21.03 % (648805)Time elapsed: 10.436 s
% 0.18/21.03 % (648805)Peak memory usage: 282 MB
% 0.18/21.03 % (648805)Instructions burned: 19878 (million)
% 0.18/21.03 % (648736)Success in time 20.717 s
% 0.18/21.03 % Vampire exiting
%------------------------------------------------------------------------------