%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR077+2 : 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 : n005.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:44:59 AM UTC 2026
% Result : Theorem 83.38s 23.57s
% Output : Refutation 83.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 48 ( 11 unt; 3 def)
% Number of atoms : 143 ( 42 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 155 ( 60 ~; 64 |; 22 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 7 usr; 7 con; 0-2 aty)
% Number of variables : 28 ( 0 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4433,axiom,
! [X0,X1] :
( ( s__AbsoluteValueFn(X1) = X0
& s__instance(X1,s__RealNumber)
& s__instance(X0,s__RealNumber) )
<=> ( ( s__instance(X1,s__NonnegativeRealNumber)
& X1 = X0 )
| ( s__instance(X1,s__NegativeRealNumber)
& X0 = minus("0",X1) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4445) ).
fof(f4596,axiom,
! [X0] :
( s__instance(X0,s__RealNumber)
=> ( s__instance(X0,s__NonnegativeRealNumber)
=> ( s__SignumFn(X0) = "1"
| s__SignumFn(X0) = "0" ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4608) ).
fof(f4598,axiom,
! [X0] :
( s__instance(X0,s__RealNumber)
=> ( s__instance(X0,s__NegativeRealNumber)
=> s__SignumFn(X0) = "-1" ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4610) ).
fof(f37982,axiom,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f37983,conjecture,
~ s__instance(s__Number3_1,s__NegativeRealNumber),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f37984,negated_conjecture,
~ ~ s__instance(s__Number3_1,s__NegativeRealNumber),
inference(negated_conjecture,[status(cth)],[f37983]) ).
fof(f37997,plain,
s__instance(s__Number3_1,s__NegativeRealNumber),
inference(flattening,[],[f37984]) ).
fof(f44366,plain,
! [X0] :
( s__SignumFn(X0) = "1"
| s__SignumFn(X0) = "0"
| ~ s__instance(X0,s__NonnegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(ennf_transformation,[],[f4596]) ).
fof(f44367,plain,
! [X0] :
( s__SignumFn(X0) = "1"
| s__SignumFn(X0) = "0"
| ~ s__instance(X0,s__NonnegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(flattening,[],[f44366]) ).
fof(f44370,plain,
! [X0] :
( s__SignumFn(X0) = "-1"
| ~ s__instance(X0,s__NegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(ennf_transformation,[],[f4598]) ).
fof(f44371,plain,
! [X0] :
( s__SignumFn(X0) = "-1"
| ~ s__instance(X0,s__NegativeRealNumber)
| ~ s__instance(X0,s__RealNumber) ),
inference(flattening,[],[f44370]) ).
fof(f48381,definition,
! [X0,X1] :
( sP14(X0,X1)
<=> ( s__AbsoluteValueFn(X1) = X0
& s__instance(X1,s__RealNumber)
& s__instance(X0,s__RealNumber) ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f48382,plain,
! [X0,X1] :
( sP14(X0,X1)
<=> ( ( s__instance(X1,s__NonnegativeRealNumber)
& X1 = X0 )
| ( s__instance(X1,s__NegativeRealNumber)
& X0 = minus("0",X1) ) ) ),
inference(definition_folding,[],[f4433,f48381]) ).
fof(f48682,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| s__AbsoluteValueFn(X1) != X0
| ~ s__instance(X1,s__RealNumber)
| ~ s__instance(X0,s__RealNumber) )
& ( ( s__AbsoluteValueFn(X1) = X0
& s__instance(X1,s__RealNumber)
& s__instance(X0,s__RealNumber) )
| ~ sP14(X0,X1) ) ),
inference(nnf_transformation,[],[f48381]) ).
fof(f48683,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| s__AbsoluteValueFn(X1) != X0
| ~ s__instance(X1,s__RealNumber)
| ~ s__instance(X0,s__RealNumber) )
& ( ( s__AbsoluteValueFn(X1) = X0
& s__instance(X1,s__RealNumber)
& s__instance(X0,s__RealNumber) )
| ~ sP14(X0,X1) ) ),
inference(flattening,[],[f48682]) ).
fof(f48684,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| ( ( ~ s__instance(X1,s__NonnegativeRealNumber)
| X0 != X1 )
& ( ~ s__instance(X1,s__NegativeRealNumber)
| minus("0",X1) != X0 ) ) )
& ( ( s__instance(X1,s__NonnegativeRealNumber)
& X1 = X0 )
| ( s__instance(X1,s__NegativeRealNumber)
& X0 = minus("0",X1) )
| ~ sP14(X0,X1) ) ),
inference(nnf_transformation,[],[f48382]) ).
fof(f48685,plain,
! [X0,X1] :
( ( sP14(X0,X1)
| ( ( ~ s__instance(X1,s__NonnegativeRealNumber)
| X0 != X1 )
& ( ~ s__instance(X1,s__NegativeRealNumber)
| minus("0",X1) != X0 ) ) )
& ( ( s__instance(X1,s__NonnegativeRealNumber)
& X1 = X0 )
| ( s__instance(X1,s__NegativeRealNumber)
& X0 = minus("0",X1) )
| ~ sP14(X0,X1) ) ),
inference(flattening,[],[f48684]) ).
fof(f54496,plain,
! [X0,X1] :
( s__instance(X1,s__RealNumber)
| ~ sP14(X0,X1) ),
inference(cnf_transformation,[],[f48683]) ).
fof(f54504,plain,
! [X0,X1] :
( sP14(X0,X1)
| ~ s__instance(X1,s__NonnegativeRealNumber)
| X0 != X1 ),
inference(cnf_transformation,[],[f48685]) ).
fof(f54727,plain,
! [X0] :
( ~ s__instance(X0,s__NonnegativeRealNumber)
| "0" = s__SignumFn(X0)
| "1" = s__SignumFn(X0)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[],[f44367]) ).
fof(f54729,plain,
! [X0] :
( ~ s__instance(X0,s__NegativeRealNumber)
| "-1" = s__SignumFn(X0)
| ~ s__instance(X0,s__RealNumber) ),
inference(cnf_transformation,[],[f44371]) ).
fof(f91042,plain,
s__instance(s__Number3_1,s__NonnegativeRealNumber),
inference(cnf_transformation,[],[f37982]) ).
fof(f91043,plain,
s__instance(s__Number3_1,s__NegativeRealNumber),
inference(cnf_transformation,[],[f37997]) ).
fof(f91196,plain,
! [X1] :
( sP14(X1,X1)
| ~ s__instance(X1,s__NonnegativeRealNumber) ),
inference(equality_resolution,[],[f54504]) ).
fof(f103460,plain,
( "-1" = s__SignumFn(s__Number3_1)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[],[f54729,f91043]) ).
fof(f103464,definition,
( spl1514_150
<=> s__instance(s__Number3_1,s__RealNumber) ),
introduced(definition,[new_symbols(definition,[spl1514_150])],[avatar_definition]) ).
fof(f103465,plain,
( s__instance(s__Number3_1,s__RealNumber)
| ~ spl1514_150 ),
inference(avatar_component_clause,[],[f103464]) ).
fof(f103466,plain,
( ~ s__instance(s__Number3_1,s__RealNumber)
| spl1514_150 ),
inference(avatar_component_clause,[],[f103464]) ).
fof(f103468,definition,
( spl1514_151
<=> "-1" = s__SignumFn(s__Number3_1) ),
introduced(definition,[new_symbols(definition,[spl1514_151])],[avatar_definition]) ).
fof(f103470,plain,
( "-1" = s__SignumFn(s__Number3_1)
| ~ spl1514_151 ),
inference(avatar_component_clause,[],[f103468]) ).
fof(f103471,plain,
( ~ spl1514_150
| spl1514_151 ),
inference(avatar_split_clause,[],[f103460,f103468,f103464]) ).
fof(f103476,plain,
( ! [X0] : ~ sP14(X0,s__Number3_1)
| spl1514_150 ),
inference(resolution,[],[f103466,f54496]) ).
fof(f103481,plain,
( ~ s__instance(s__Number3_1,s__NonnegativeRealNumber)
| spl1514_150 ),
inference(resolution,[],[f103476,f91196]) ).
fof(f103485,plain,
( $false
| spl1514_150 ),
inference(forward_subsumption_resolution,[],[f103481,f91042]) ).
fof(f103486,plain,
spl1514_150,
inference(avatar_contradiction_clause,[],[f103485]) ).
fof(f550714,plain,
( "0" = s__SignumFn(s__Number3_1)
| "1" = s__SignumFn(s__Number3_1)
| ~ s__instance(s__Number3_1,s__RealNumber) ),
inference(resolution,[],[f54727,f91042]) ).
fof(f550719,plain,
( "0" = s__SignumFn(s__Number3_1)
| "1" = s__SignumFn(s__Number3_1)
| ~ spl1514_150 ),
inference(forward_subsumption_resolution,[],[f550714,f103465]) ).
fof(f550721,plain,
( "-1" = "0"
| "1" = s__SignumFn(s__Number3_1)
| ~ spl1514_150
| ~ spl1514_151 ),
inference(forward_demodulation,[],[f550719,f103470]) ).
fof(f550722,plain,
( "1" = s__SignumFn(s__Number3_1)
| ~ spl1514_150
| ~ spl1514_151 ),
inference(distinct_equality_removal,[],[f550721]) ).
fof(f550723,plain,
( "1" = "-1"
| ~ spl1514_150
| ~ spl1514_151 ),
inference(superposition,[],[f550722,f103470]) ).
fof(f550727,plain,
( $false
| ~ spl1514_150
| ~ spl1514_151 ),
inference(distinct_equality_removal,[],[f550723]) ).
fof(f550728,plain,
( ~ spl1514_150
| ~ spl1514_151 ),
inference(avatar_contradiction_clause,[],[f550727]) ).
cnf(s247,plain,
( ~ spl1514_150
| spl1514_151 ),
inference(sat_conversion,[],[f103471]) ).
cnf(s249,plain,
spl1514_150,
inference(sat_conversion,[],[f103486]) ).
cnf(s138894,plain,
( ~ spl1514_150
| ~ spl1514_151 ),
inference(sat_conversion,[],[f550728]) ).
cnf(s139044,plain,
~ spl1514_151,
inference(rat,[],[s138894,s249]) ).
cnf(s139045,plain,
$false,
inference(rat,[],[s247,s139044,s249]) ).
fof(f550729,plain,
$false,
inference(avatar_sat_refutation,[],[s139045]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR077+2 : 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.19 % Computer : n005.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 22:27:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 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
% 23.91/4.17 % (1256257)Will run a generic schedule for satisfiability detection.
% 23.91/4.17 % (1256264)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2664995823:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi)
% 23.91/4.17 % (1256263)% WARNING: option uhcvi not known.
% 23.91/4.17 % (1256262)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3010700649_2993 on theBenchmark for (2993ds/0Mi)
% 23.91/4.17 % (1256263)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3582077010:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi)
% 23.91/4.17 % (1256265)dis+10_1_sil=32000:sp=arity:random_seed=3957950601:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi)
% 23.91/4.17 % (1256266)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3100084907:i=116_2993 on theBenchmark for (2993ds/116Mi)
% 23.91/4.17 % (1256267)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1012985177:i=131_2993 on theBenchmark for (2993ds/131Mi)
% 23.91/4.17 % (1256268)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3577314256:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi)
% 23.91/4.17 % (1256265)Instruction limit reached!
% 23.91/4.17 % (1256265)------------------------------
% 23.91/4.17 % (1256265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/4.17 % (1256265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/4.17 % (1256265)CaDiCaL version: 2.1.3
% 23.91/4.17 % (1256265)Termination reason: Instruction limit
% 23.91/4.17 % (1256265)Termination phase: Preprocessing 2
% 23.91/4.17 % (1256265)Time elapsed: 0.088 s
% 23.91/4.17 % (1256265)Peak memory usage: 51 MB
% 23.91/4.17 % (1256265)Instructions burned: 103 (million)
% 23.91/4.17 % (1256267)Instruction limit reached!
% 23.91/4.17 % (1256267)------------------------------
% 23.91/4.17 % (1256267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/4.17 % (1256267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/4.17 % (1256267)CaDiCaL version: 2.1.3
% 23.91/4.17 % (1256267)Termination reason: Instruction limit
% 23.91/4.17 % (1256267)Termination phase: Naming
% 23.91/4.17 % (1256267)Time elapsed: 0.095 s
% 23.91/4.17 % (1256267)Peak memory usage: 52 MB
% 23.91/4.17 % (1256267)Instructions burned: 133 (million)
% 23.91/4.17 % (1256266)Instruction limit reached!
% 23.91/4.17 % (1256266)------------------------------
% 23.91/4.17 % (1256266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/4.17 % (1256266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/4.17 % (1256266)CaDiCaL version: 2.1.3
% 23.91/4.17 % (1256266)Termination reason: Instruction limit
% 23.91/4.17 % (1256266)Termination phase: NewCNF
% 23.91/4.17 % (1256266)Time elapsed: 0.099 s
% 23.91/4.17 % (1256266)Peak memory usage: 53 MB
% 23.91/4.17 % (1256266)Instructions burned: 116 (million)
% 23.91/4.17 % (1256276)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1048865074:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi)
% 23.91/4.17 % (1256268)Instruction limit reached!
% 23.91/4.17 % (1256268)------------------------------
% 23.91/4.17 % (1256268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/4.17 % (1256268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/4.17 % (1256268)CaDiCaL version: 2.1.3
% 23.91/4.17 % (1256268)Termination reason: Instruction limit
% 23.91/4.17 % (1256268)Termination phase: Preprocessing 3
% 23.91/4.17 % (1256268)Time elapsed: 0.112 s
% 23.91/4.17 % (1256268)Peak memory usage: 52 MB
% 23.91/4.17 % (1256268)Instructions burned: 160 (million)
% 23.91/4.17 % (1256277)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=791085844:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi)
% 23.91/4.17 % (1256278)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=2861087127:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi)
% 23.91/4.17 % (1256281)ott-21_1_sil=16000:fs=off:random_seed=420250001:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi)
% 23.91/4.17 % (1256277)Instruction limit reached!
% 23.91/4.17 % (1256277)------------------------------
% 23.91/4.17 % (1256277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/4.17 % (1256277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/4.17 % (1256277)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256277)Termination reason: Instruction limit
% 32.19/5.37 % (1256277)Termination phase: Naming
% 32.19/5.37 % (1256277)Time elapsed: 0.098 s
% 32.19/5.37 % (1256277)Peak memory usage: 51 MB
% 32.19/5.37 % (1256277)Instructions burned: 132 (million)
% 32.19/5.37 % (1256284)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=826595317:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi)
% 32.19/5.37 % (1256281)Instruction limit reached!
% 32.19/5.37 % (1256281)------------------------------
% 32.19/5.37 % (1256281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.19/5.37 % (1256281)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256281)Termination reason: Instruction limit
% 32.19/5.37 % (1256281)Termination phase: Preprocessing 3
% 32.19/5.37 % (1256281)Time elapsed: 0.117 s
% 32.19/5.37 % (1256281)Peak memory usage: 52 MB
% 32.19/5.37 % (1256281)Instructions burned: 182 (million)
% 32.19/5.37 % (1256286)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3376723670:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi)
% 32.19/5.37 % (1256278)Instruction limit reached!
% 32.19/5.37 % (1256278)------------------------------
% 32.19/5.37 % (1256278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.19/5.37 % (1256278)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256278)Termination reason: Instruction limit
% 32.19/5.37 % (1256278)Termination phase: NewCNF
% 32.19/5.37 % (1256278)Time elapsed: 0.323 s
% 32.19/5.37 % (1256278)Peak memory usage: 61 MB
% 32.19/5.37 % (1256278)Instructions burned: 688 (million)
% 32.19/5.37 % (1256288)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1111847601:i=1179_2988 on theBenchmark for (2988ds/1179Mi)
% 32.19/5.37 % (1256284)Instruction limit reached!
% 32.19/5.37 % (1256284)------------------------------
% 32.19/5.37 % (1256284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.19/5.37 % (1256284)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256284)Termination reason: Instruction limit
% 32.19/5.37 % (1256284)Termination phase: Equality resolution with deletion
% 32.19/5.37 % (1256284)Time elapsed: 0.259 s
% 32.19/5.37 % (1256284)Peak memory usage: 58 MB
% 32.19/5.37 % (1256284)Instructions burned: 478 (million)
% 32.19/5.37 % (1256276)Instruction limit reached!
% 32.19/5.37 % (1256276)------------------------------
% 32.19/5.37 % (1256276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.19/5.37 % (1256276)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256276)Termination reason: Instruction limit
% 32.19/5.37 % (1256276)Termination phase: Clausification
% 32.19/5.37 % (1256276)Time elapsed: 0.397 s
% 32.19/5.37 % (1256276)Peak memory usage: 85 MB
% 32.19/5.37 % (1256276)Instructions burned: 715 (million)
% 32.19/5.37 % (1256290)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=261478784:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi)
% 32.19/5.37 % (1256291)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=4208723967:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2988 on theBenchmark for (2988ds/692Mi)
% 32.19/5.37 % (1256286)Instruction limit reached!
% 32.19/5.37 % (1256286)------------------------------
% 32.19/5.37 % (1256286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.19/5.37 % (1256286)CaDiCaL version: 2.1.3
% 32.19/5.37 % (1256286)Termination reason: Instruction limit
% 32.19/5.37 % (1256286)Termination phase: Property scanning
% 32.19/5.37 % (1256286)Time elapsed: 0.439 s
% 32.19/5.37 % (1256286)Peak memory usage: 89 MB
% 32.19/5.37 % (1256286)Instructions burned: 868 (million)
% 32.19/5.37 % (1256294)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3925756934:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi)
% 32.19/5.37 % (1256291)Instruction limit reached!
% 32.19/5.37 % (1256291)------------------------------
% 32.19/5.37 % (1256291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.19/5.37 % (1256291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256291)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256291)Termination reason: Instruction limit
% 51.55/8.11 % (1256291)Termination phase: NewCNF
% 51.55/8.11 % (1256291)Time elapsed: 0.322 s
% 51.55/8.11 % (1256291)Peak memory usage: 61 MB
% 51.55/8.11 % (1256291)Instructions burned: 693 (million)
% 51.55/8.11 % (1256296)fmb+10_1_sil=64000:random_seed=2471097127:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 51.55/8.11 % (1256290)Instruction limit reached!
% 51.55/8.11 % (1256290)------------------------------
% 51.55/8.11 % (1256290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256290)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256290)Termination reason: Instruction limit
% 51.55/8.11 % (1256290)Termination phase: Property scanning
% 51.55/8.11 % (1256290)Time elapsed: 0.451 s
% 51.55/8.11 % (1256290)Peak memory usage: 89 MB
% 51.55/8.11 % (1256290)Instructions burned: 889 (million)
% 51.55/8.11 % (1256298)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3927973846:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 51.55/8.11 % (1256288)Instruction limit reached!
% 51.55/8.11 % (1256288)------------------------------
% 51.55/8.11 % (1256288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256288)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256288)Termination reason: Instruction limit
% 51.55/8.11 % (1256288)Termination phase: Saturation
% 51.55/8.11 % (1256288)Time elapsed: 0.598 s
% 51.55/8.11 % (1256288)Peak memory usage: 72 MB
% 51.55/8.11 % (1256288)Instructions burned: 1180 (million)
% 51.55/8.11 % (1256300)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=524469219:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 51.55/8.11 % (1256294)Instruction limit reached!
% 51.55/8.11 % (1256294)------------------------------
% 51.55/8.11 % (1256294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256294)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256294)Termination reason: Instruction limit
% 51.55/8.11 % (1256294)Termination phase: Property scanning
% 51.55/8.11 % (1256294)Time elapsed: 0.386 s
% 51.55/8.11 % (1256294)Peak memory usage: 62 MB
% 51.55/8.11 % (1256294)Instructions burned: 880 (million)
% 51.55/8.11 % (1256302)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=578234726:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 51.55/8.11 % (1256300)Instruction limit reached!
% 51.55/8.11 % (1256300)------------------------------
% 51.55/8.11 % (1256300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256300)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256300)Termination reason: Instruction limit
% 51.55/8.11 % (1256300)Termination phase: Property scanning
% 51.55/8.11 % (1256300)Time elapsed: 0.473 s
% 51.55/8.11 % (1256300)Peak memory usage: 89 MB
% 51.55/8.11 % (1256300)Instructions burned: 920 (million)
% 51.55/8.11 % (1256304)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1747383222:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 51.55/8.11 % (1256304)Instruction limit reached!
% 51.55/8.11 % (1256304)------------------------------
% 51.55/8.11 % (1256304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.55/8.11 % (1256304)CaDiCaL version: 2.1.3
% 51.55/8.11 % (1256304)Termination reason: Instruction limit
% 51.55/8.11 % (1256304)Termination phase: Saturation
% 51.55/8.11 % (1256304)Time elapsed: 0.801 s
% 51.55/8.11 % (1256304)Peak memory usage: 79 MB
% 51.55/8.11 % (1256304)Instructions burned: 1472 (million)
% 51.55/8.11 % (1256306)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=577196872:i=6324_2969 on theBenchmark for (2969ds/6324Mi)
% 51.55/8.11 % Detected minimum model sizes of [447]
% 51.55/8.11 % Detected maximum model sizes of [max]
% 51.55/8.11 % (1256262)Cannot represent all propositional literals internally
% 51.55/8.11 % (1256262)Refutation not found, incomplete strategy
% 51.55/8.11 % (1256262)------------------------------
% 51.55/8.11 % (1256262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.55/8.11 % (1256262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256262)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256262)Termination reason: Refutation not found, incomplete strategy
% 86.14/12.94 % (1256262)Time elapsed: 3.290 s
% 86.14/12.94 % (1256262)Peak memory usage: 174 MB
% 86.14/12.94 % (1256262)Instructions burned: 6861 (million)
% 86.14/12.94 % (1256262)------------------------------
% 86.14/12.94 % (1256262)------------------------------
% 86.14/12.94 % (1256308)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1906564459:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 86.14/12.94 % Detected minimum model sizes of [447]
% 86.14/12.94 % Detected maximum model sizes of [max]
% 86.14/12.94 % (1256296)Cannot represent all propositional literals internally
% 86.14/12.94 % (1256296)Refutation not found, incomplete strategy
% 86.14/12.94 % (1256296)------------------------------
% 86.14/12.94 % (1256296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.14/12.94 % (1256296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256296)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256296)Termination reason: Refutation not found, incomplete strategy
% 86.14/12.94 % (1256296)Time elapsed: 2.670 s
% 86.14/12.94 % (1256296)Peak memory usage: 153 MB
% 86.14/12.94 % (1256296)Instructions burned: 5782 (million)
% 86.14/12.94 % (1256296)------------------------------
% 86.14/12.94 % (1256296)------------------------------
% 86.14/12.94 % (1256310)ott-2_1_sil=16000:newcnf=on:random_seed=523629217:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 86.14/12.94 % Detected minimum model sizes of [447]
% 86.14/12.94 % Detected maximum model sizes of [max]
% 86.14/12.94 % (1256298)Cannot represent all propositional literals internally
% 86.14/12.94 % (1256298)Refutation not found, incomplete strategy
% 86.14/12.94 % (1256298)------------------------------
% 86.14/12.94 % (1256298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.14/12.94 % (1256298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256298)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256298)Termination reason: Refutation not found, incomplete strategy
% 86.14/12.94 % (1256298)Time elapsed: 2.805 s
% 86.14/12.94 % (1256298)Peak memory usage: 157 MB
% 86.14/12.94 % (1256298)Instructions burned: 5979 (million)
% 86.14/12.94 % (1256298)------------------------------
% 86.14/12.94 % (1256298)------------------------------
% 86.14/12.94 % (1256302)Instruction limit reached!
% 86.14/12.94 % (1256302)------------------------------
% 86.14/12.94 % (1256302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.14/12.94 % (1256302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256302)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256302)Termination reason: Instruction limit
% 86.14/12.94 % (1256302)Termination phase: Saturation
% 86.14/12.94 % (1256302)Time elapsed: 2.744 s
% 86.14/12.94 % (1256302)Peak memory usage: 107 MB
% 86.14/12.94 % (1256302)Instructions burned: 5132 (million)
% 86.14/12.94 % (1256312)ott+10_1_sil=32000:tgt=ground:random_seed=1564894708:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 86.14/12.94 % (1256314)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3384780885:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 86.14/12.94 % (1256310)Instruction limit reached!
% 86.14/12.94 % (1256310)------------------------------
% 86.14/12.94 % (1256310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.14/12.94 % (1256310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256310)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256310)Termination reason: Instruction limit
% 86.14/12.94 % (1256310)Termination phase: Property scanning
% 86.14/12.94 % (1256310)Time elapsed: 0.398 s
% 86.14/12.94 % (1256310)Peak memory usage: 62 MB
% 86.14/12.94 % (1256310)Instructions burned: 871 (million)
% 86.14/12.94 % (1256316)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2823826425:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 86.14/12.94 % (1256308)Instruction limit reached!
% 86.14/12.94 % (1256308)------------------------------
% 86.14/12.94 % (1256308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.14/12.94 % (1256308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.14/12.94 % (1256308)CaDiCaL version: 2.1.3
% 86.14/12.94 % (1256308)Termination reason: Instruction limit
% 86.14/12.94 % (1256308)Termination phase: Finite model building preprocessing
% 86.14/12.94 % (1256308)Time elapsed: 1.092 s
% 86.14/12.94 % (1256308)Peak memory usage: 116 MB
% 86.14/12.94 % (1256308)Instructions burned: 2175 (million)
% 145.09/21.23 % (1256318)dis+21_1_sil=32000:sas=cadical:random_seed=1173475350:i=3773:amm=off_2948 on theBenchmark for (2948ds/3773Mi)
% 145.09/21.23 % (1256306)Instruction limit reached!
% 145.09/21.23 % (1256306)------------------------------
% 145.09/21.23 % (1256306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256306)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256306)Termination reason: Instruction limit
% 145.09/21.23 % (1256306)Termination phase: Finite model building preprocessing
% 145.09/21.23 % (1256306)Time elapsed: 3.001 s
% 145.09/21.23 % (1256306)Peak memory usage: 167 MB
% 145.09/21.23 % (1256306)Instructions burned: 6325 (million)
% 145.09/21.23 % (1256320)ott+11_1_sil=16000:gs=on:random_seed=1267356436:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2938 on theBenchmark for (2938ds/2251Mi)
% 145.09/21.23 % (1256316)Instruction limit reached!
% 145.09/21.23 % (1256316)------------------------------
% 145.09/21.23 % (1256316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256316)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256316)Termination reason: Instruction limit
% 145.09/21.23 % (1256316)Termination phase: Saturation
% 145.09/21.23 % (1256316)Time elapsed: 2.041 s
% 145.09/21.23 % (1256316)Peak memory usage: 116 MB
% 145.09/21.23 % (1256316)Instructions burned: 3512 (million)
% 145.09/21.23 % (1256322)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1756648855:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi)
% 145.09/21.23 % (1256320)Instruction limit reached!
% 145.09/21.23 % (1256320)------------------------------
% 145.09/21.23 % (1256320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256320)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256320)Termination reason: Instruction limit
% 145.09/21.23 % (1256320)Termination phase: Saturation
% 145.09/21.23 % (1256320)Time elapsed: 0.865 s
% 145.09/21.23 % (1256320)Peak memory usage: 65 MB
% 145.09/21.23 % (1256320)Instructions burned: 2254 (million)
% 145.09/21.23 % (1256324)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=21171981:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 145.09/21.23 % (1256318)Instruction limit reached!
% 145.09/21.23 % (1256318)------------------------------
% 145.09/21.23 % (1256318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256318)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256318)Termination reason: Instruction limit
% 145.09/21.23 % (1256318)Termination phase: Saturation
% 145.09/21.23 % (1256318)Time elapsed: 1.968 s
% 145.09/21.23 % (1256318)Peak memory usage: 101 MB
% 145.09/21.23 % (1256318)Instructions burned: 3773 (million)
% 145.09/21.23 % (1256326)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1573262103:i=29340_2928 on theBenchmark for (2928ds/29340Mi)
% 145.09/21.23 % (1256312)Instruction limit reached!
% 145.09/21.23 % (1256312)------------------------------
% 145.09/21.23 % (1256312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256312)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256312)Termination reason: Instruction limit
% 145.09/21.23 % (1256312)Termination phase: Saturation
% 145.09/21.23 % (1256312)Time elapsed: 3.119 s
% 145.09/21.23 % (1256312)Peak memory usage: 95 MB
% 145.09/21.23 % (1256312)Instructions burned: 5115 (million)
% 145.09/21.23 % (1256328)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4145734207:i=5211_2922 on theBenchmark for (2922ds/5211Mi)
% 145.09/21.23 % Detected minimum model sizes of [447]
% 145.09/21.23 % Detected maximum model sizes of [max]
% 145.09/21.23 % (1256314)Cannot represent all propositional literals internally
% 145.09/21.23 % (1256314)Refutation not found, incomplete strategy
% 145.09/21.23 % (1256314)------------------------------
% 145.09/21.23 % (1256314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.09/21.23 % (1256314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.09/21.23 % (1256314)CaDiCaL version: 2.1.3
% 145.09/21.23 % (1256314)Termination reason: Refutation not found, incomplete strategy
% 145.09/21.23 % (1256314)Time elapsed: 3.276 s
% 83.38/23.53 % (1256314)Peak memory usage: 177 MB
% 83.38/23.53 % (1256314)Instructions burned: 6910 (million)
% 83.38/23.53 % (1256314)------------------------------
% 83.38/23.53 % (1256314)------------------------------
% 83.38/23.53 % (1256330)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=139202050:i=5497:nm=2_2920 on theBenchmark for (2920ds/5497Mi)
% 83.38/23.53 % (1256324)Instruction limit reached!
% 83.38/23.53 % (1256324)------------------------------
% 83.38/23.53 % (1256324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256324)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256324)Termination reason: Instruction limit
% 83.38/23.53 % (1256324)Termination phase: Saturation
% 83.38/23.53 % (1256324)Time elapsed: 2.705 s
% 83.38/23.53 % (1256324)Peak memory usage: 100 MB
% 83.38/23.53 % (1256324)Instructions burned: 4591 (million)
% 83.38/23.53 % (1256332)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1386143470:fmbsr=2:i=46332_2902 on theBenchmark for (2902ds/46332Mi)
% 83.38/23.53 % Detected minimum model sizes of [447]
% 83.38/23.53 % Detected maximum model sizes of [max]
% 83.38/23.53 % (1256322)Cannot represent all propositional literals internally
% 83.38/23.53 % (1256322)Refutation not found, incomplete strategy
% 83.38/23.53 % (1256322)------------------------------
% 83.38/23.53 % (1256322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256322)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256322)Termination reason: Refutation not found, incomplete strategy
% 83.38/23.53 % (1256322)Time elapsed: 2.955 s
% 83.38/23.53 % (1256322)Peak memory usage: 162 MB
% 83.38/23.53 % (1256322)Instructions burned: 6558 (million)
% 83.38/23.53 % (1256322)------------------------------
% 83.38/23.53 % (1256322)------------------------------
% 83.38/23.53 % (1256334)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4182176569:i=14071_2901 on theBenchmark for (2901ds/14071Mi)
% 83.38/23.53 % (1256328)Instruction limit reached!
% 83.38/23.53 % (1256328)------------------------------
% 83.38/23.53 % (1256328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256328)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256328)Termination reason: Instruction limit
% 83.38/23.53 % (1256328)Termination phase: Saturation
% 83.38/23.53 % (1256328)Time elapsed: 2.656 s
% 83.38/23.53 % (1256328)Peak memory usage: 112 MB
% 83.38/23.53 % (1256328)Instructions burned: 5212 (million)
% 83.38/23.53 % (1256336)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3292817853:i=22565:add=on:rawr=on_2896 on theBenchmark for (2896ds/22565Mi)
% 83.38/23.53 % (1256330)Instruction limit reached!
% 83.38/23.53 % (1256330)------------------------------
% 83.38/23.53 % (1256330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256330)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256330)Termination reason: Instruction limit
% 83.38/23.53 % (1256330)Termination phase: Finite model building preprocessing
% 83.38/23.53 % (1256330)Time elapsed: 2.660 s
% 83.38/23.53 % (1256330)Peak memory usage: 159 MB
% 83.38/23.53 % (1256330)Instructions burned: 5498 (million)
% 83.38/23.53 % (1256338)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1095984177:i=8173:av=off_2893 on theBenchmark for (2893ds/8173Mi)
% 83.38/23.53 % Detected minimum model sizes of [447]
% 83.38/23.53 % Detected maximum model sizes of [max]
% 83.38/23.53 % (1256334)Cannot represent all propositional literals internally
% 83.38/23.53 % (1256334)Refutation not found, incomplete strategy
% 83.38/23.53 % (1256334)------------------------------
% 83.38/23.53 % (1256334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256334)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256334)Termination reason: Refutation not found, incomplete strategy
% 83.38/23.53 % (1256334)Time elapsed: 2.826 s
% 83.38/23.53 % (1256334)Peak memory usage: 160 MB
% 83.38/23.53 % (1256334)Instructions burned: 6105 (million)
% 83.38/23.53 % Detected minimum model sizes of [447]
% 83.38/23.53 % Detected maximum model sizes of [max]
% 83.38/23.53 % (1256332)Cannot represent all propositional literals internally
% 83.38/23.53 % (1256332)Refutation not found, incomplete strategy
% 83.38/23.53 % (1256332)------------------------------
% 83.38/23.53 % (1256332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256332)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256332)Termination reason: Refutation not found, incomplete strategy
% 83.38/23.53 % (1256332)Time elapsed: 2.946 s
% 83.38/23.53 % (1256332)Peak memory usage: 162 MB
% 83.38/23.53 % (1256332)Instructions burned: 6559 (million)
% 83.38/23.53 % (1256334)------------------------------
% 83.38/23.53 % (1256334)------------------------------
% 83.38/23.53 % (1256332)------------------------------
% 83.38/23.53 % (1256332)------------------------------
% 83.38/23.53 % (1256340)dis+10_16:1_sil=16000:random_seed=259384616:i=9155:fsr=off_2872 on theBenchmark for (2872ds/9155Mi)
% 83.38/23.53 % (1256341)ott-3_8_sil=64000:random_seed=179424021:i=20139:bs=on_2872 on theBenchmark for (2872ds/20139Mi)
% 83.38/23.53 % (1256338)Instruction limit reached!
% 83.38/23.53 % (1256338)------------------------------
% 83.38/23.53 % (1256338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256338)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256338)Termination reason: Instruction limit
% 83.38/23.53 % (1256338)Termination phase: Saturation
% 83.38/23.53 % (1256338)Time elapsed: 2.253 s
% 83.38/23.53 % (1256338)Peak memory usage: 70 MB
% 83.38/23.53 % (1256338)Instructions burned: 8175 (million)
% 83.38/23.53 % (1256344)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2968674979:fmbsr=2:i=32576_2870 on theBenchmark for (2870ds/32576Mi)
% 83.38/23.53 % Detected minimum model sizes of [447]
% 83.38/23.53 % Detected maximum model sizes of [max]
% 83.38/23.53 % (1256344)Cannot represent all propositional literals internally
% 83.38/23.53 % (1256344)Refutation not found, incomplete strategy
% 83.38/23.53 % (1256344)------------------------------
% 83.38/23.53 % (1256344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256344)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256344)Termination reason: Refutation not found, incomplete strategy
% 83.38/23.53 % (1256344)Time elapsed: 3.256 s
% 83.38/23.53 % (1256344)Peak memory usage: 171 MB
% 83.38/23.53 % (1256344)Instructions burned: 6820 (million)
% 83.38/23.53 % (1256344)------------------------------
% 83.38/23.53 % (1256344)------------------------------
% 83.38/23.53 % (1256627)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=514647711:i=11404_2836 on theBenchmark for (2836ds/11404Mi)
% 83.38/23.53 % (1256340)Instruction limit reached!
% 83.38/23.53 % (1256340)------------------------------
% 83.38/23.53 % (1256340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256340)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256340)Termination reason: Instruction limit
% 83.38/23.53 % (1256340)Termination phase: Saturation
% 83.38/23.53 % (1256340)Time elapsed: 4.582 s
% 83.38/23.53 % (1256340)Peak memory usage: 115 MB
% 83.38/23.53 % (1256340)Instructions burned: 9155 (million)
% 83.38/23.53 % (1256629)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1791624081:i=14134_2825 on theBenchmark for (2825ds/14134Mi)
% 83.38/23.53 % (1256627)Instruction limit reached!
% 83.38/23.53 % (1256627)------------------------------
% 83.38/23.53 % (1256627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256627)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256627)Termination reason: Instruction limit
% 83.38/23.53 % (1256627)Termination phase: Saturation
% 83.38/23.53 % (1256627)Time elapsed: 4.016 s
% 83.38/23.53 % (1256627)Peak memory usage: 106 MB
% 83.38/23.53 % (1256627)Instructions burned: 11404 (million)
% 83.38/23.53 % (1256631)dis+33_16_sil=32000:sac=on:random_seed=2942366118:i=15851:nm=0_2796 on theBenchmark for (2796ds/15851Mi)
% 83.38/23.53 % (1256336)Instruction limit reached!
% 83.38/23.53 % (1256336)------------------------------
% 83.38/23.53 % (1256336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.53 % (1256336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.53 % (1256336)CaDiCaL version: 2.1.3
% 83.38/23.53 % (1256336)Termination reason: Instruction limit
% 83.38/23.53 % (1256336)Termination phase: Saturation
% 83.38/23.53 % (1256336)Time elapsed: 10.585 s
% 83.38/23.57 % (1256336)Peak memory usage: 560 MB
% 83.38/23.57 % (1256336)Instructions burned: 22565 (million)
% 83.38/23.57 % (1256633)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1345485805:avsq=on:i=17627:add=on:amm=off_2789 on theBenchmark for (2789ds/17627Mi)
% 83.38/23.57 % (1256629) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1256257-1256629"...
% 83.38/23.57 % (1256629)...printing done.
% 83.38/23.57 % (1256629)Refutation found. Thanks to Tanya!
% 83.38/23.57 % SZS status Theorem for theBenchmark
% 83.38/23.57 % SZS output start Proof for theBenchmark
% See solution above
% 83.38/23.57 % (1256629)------------------------------
% 83.38/23.57 % (1256629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 83.38/23.57 % (1256629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.38/23.57 % (1256629)CaDiCaL version: 2.1.3
% 83.38/23.57 % (1256629)Termination reason: Refutation
% 83.38/23.57 % (1256629)Time elapsed: 5.588 s
% 83.38/23.57 % (1256629)Peak memory usage: 213 MB
% 83.38/23.57 % (1256629)Instructions burned: 8906 (million)
% 83.38/23.57 % (1256257)Success in time 23.31 s
% 83.38/23.58 % Vampire exiting
%------------------------------------------------------------------------------