%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB014+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 01:00:36 PM UTC 2026
% Result : Theorem 53.32s 14.78s
% Output : Refutation 53.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 41 ( 16 unt; 2 def)
% Number of atoms : 200 ( 0 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 241 ( 82 ~; 82 |; 66 &)
% ( 10 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-3 aty)
% Number of variables : 86 ( 78 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [X0,X1] :
( iext(uri_rdf_type,X0,X1)
<=> icext(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',rdfs_cext_def) ).
fof(f289,axiom,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_rdf_first,X1,X2)
& iext(uri_rdf_rest,X1,X3)
& iext(uri_rdf_first,X3,X4)
& iext(uri_rdf_rest,X3,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_bool_unionof_class_002) ).
fof(f559,conjecture,
? [X0] :
( iext(uri_rdf_type,uri_ex_harry,X0)
& iext(uri_rdf_type,X0,uri_ex_Species) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_014_Harry_belongs_to_some_Species) ).
fof(f560,negated_conjecture,
~ ? [X0] :
( iext(uri_rdf_type,uri_ex_harry,X0)
& iext(uri_rdf_type,X0,uri_ex_Species) ),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X0,X1,X2] :
( iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_harry,X0)
& iext(uri_owl_unionOf,X0,X1)
& iext(uri_rdf_first,X1,uri_ex_Eagle)
& iext(uri_rdf_rest,X1,X2)
& iext(uri_rdf_first,X2,uri_ex_Falcon)
& iext(uri_rdf_rest,X2,uri_rdf_nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_014_Harry_belongs_to_some_Species) ).
fof(f686,plain,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(ennf_transformation,[],[f289]) ).
fof(f687,plain,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(flattening,[],[f686]) ).
fof(f980,plain,
! [X0] :
( ~ iext(uri_rdf_type,uri_ex_harry,X0)
| ~ iext(uri_rdf_type,X0,uri_ex_Species) ),
inference(ennf_transformation,[],[f560]) ).
fof(f987,definition,
! [X0,X2,X4] :
( sP4(X0,X2,X4)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f988,definition,
! [X4,X2,X0,X1] :
( ( iext(uri_owl_unionOf,X0,X1)
<=> sP4(X0,X2,X4) )
| ~ sP5(X4,X2,X0,X1) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f989,plain,
! [X0,X1,X2,X3,X4] :
( sP5(X4,X2,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(definition_folding,[],[f687,f988,f987]) ).
fof(f1061,plain,
! [X0,X1] :
( ( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) )
& ( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f1123,plain,
! [X4,X2,X0,X1] :
( ( ( iext(uri_owl_unionOf,X0,X1)
| ~ sP4(X0,X2,X4) )
& ( sP4(X0,X2,X4)
| ~ iext(uri_owl_unionOf,X0,X1) ) )
| ~ sP5(X4,X2,X0,X1) ),
inference(nnf_transformation,[],[f988]) ).
fof(f1124,plain,
! [X0,X1,X2,X3] :
( ( ( iext(uri_owl_unionOf,X2,X3)
| ~ sP4(X2,X1,X0) )
& ( sP4(X2,X1,X0)
| ~ iext(uri_owl_unionOf,X2,X3) ) )
| ~ sP5(X0,X1,X2,X3) ),
inference(rectify,[],[f1123]) ).
fof(f1125,plain,
! [X0,X2,X4] :
( ( sP4(X0,X2,X4)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ? [X5] :
( ( ( ~ icext(X2,X5)
& ~ icext(X4,X5) )
| ~ icext(X0,X5) )
& ( icext(X2,X5)
| icext(X4,X5)
| icext(X0,X5) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( ( icext(X0,X5)
| ( ~ icext(X2,X5)
& ~ icext(X4,X5) ) )
& ( icext(X2,X5)
| icext(X4,X5)
| ~ icext(X0,X5) ) ) )
| ~ sP4(X0,X2,X4) ) ),
inference(nnf_transformation,[],[f987]) ).
fof(f1126,plain,
! [X0,X2,X4] :
( ( sP4(X0,X2,X4)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ? [X5] :
( ( ( ~ icext(X2,X5)
& ~ icext(X4,X5) )
| ~ icext(X0,X5) )
& ( icext(X2,X5)
| icext(X4,X5)
| icext(X0,X5) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( ( icext(X0,X5)
| ( ~ icext(X2,X5)
& ~ icext(X4,X5) ) )
& ( icext(X2,X5)
| icext(X4,X5)
| ~ icext(X0,X5) ) ) )
| ~ sP4(X0,X2,X4) ) ),
inference(flattening,[],[f1125]) ).
fof(f1127,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ~ ic(X0)
| ~ ic(X1)
| ~ ic(X2)
| ? [X3] :
( ( ( ~ icext(X1,X3)
& ~ icext(X2,X3) )
| ~ icext(X0,X3) )
& ( icext(X1,X3)
| icext(X2,X3)
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ic(X1)
& ic(X2)
& ! [X4] :
( ( icext(X0,X4)
| ( ~ icext(X1,X4)
& ~ icext(X2,X4) ) )
& ( icext(X1,X4)
| icext(X2,X4)
| ~ icext(X0,X4) ) ) )
| ~ sP4(X0,X1,X2) ) ),
inference(rectify,[],[f1126]) ).
fof(f1128,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ~ ic(X0)
| ~ ic(X1)
| ~ ic(X2)
| ( ( ( ~ icext(X1,sK59(X0,X1,X2))
& ~ icext(X2,sK59(X0,X1,X2)) )
| ~ icext(X0,sK59(X0,X1,X2)) )
& ( icext(X1,sK59(X0,X1,X2))
| icext(X2,sK59(X0,X1,X2))
| icext(X0,sK59(X0,X1,X2)) ) ) )
& ( ( ic(X0)
& ic(X1)
& ic(X2)
& ! [X4] :
( ( icext(X0,X4)
| ( ~ icext(X1,X4)
& ~ icext(X2,X4) ) )
& ( icext(X1,X4)
| icext(X2,X4)
| ~ icext(X0,X4) ) ) )
| ~ sP4(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X3,sK59(X0,X1,X2))],[f1127]) ).
fof(f1460,plain,
( iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_harry,sK251)
& iext(uri_owl_unionOf,sK251,sK252)
& iext(uri_rdf_first,sK252,uri_ex_Eagle)
& iext(uri_rdf_rest,sK252,sK253)
& iext(uri_rdf_first,sK253,uri_ex_Falcon)
& iext(uri_rdf_rest,sK253,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251,sK252,sK253]),skolemize(X0,sK251),skolemize(X1,sK252),skolemize(X2,sK253)],[f561]) ).
fof(f1486,plain,
! [X0,X1] :
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ),
inference(cnf_transformation,[],[f1061]) ).
fof(f1487,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[],[f1061]) ).
fof(f1884,plain,
! [X2,X3,X0,X1] :
( ~ sP5(X0,X1,X2,X3)
| ~ iext(uri_owl_unionOf,X2,X3)
| sP4(X2,X1,X0) ),
inference(cnf_transformation,[],[f1124]) ).
fof(f1886,plain,
! [X2,X0,X1,X4] :
( ~ sP4(X0,X1,X2)
| icext(X2,X4)
| ~ icext(X0,X4)
| icext(X1,X4) ),
inference(cnf_transformation,[],[f1128]) ).
fof(f1895,plain,
! [X2,X3,X0,X1,X4] :
( sP5(X4,X2,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(cnf_transformation,[],[f989]) ).
fof(f2750,plain,
! [X0] :
( ~ iext(uri_rdf_type,uri_ex_harry,X0)
| ~ iext(uri_rdf_type,X0,uri_ex_Species) ),
inference(cnf_transformation,[],[f980]) ).
fof(f2751,plain,
iext(uri_rdf_rest,sK253,uri_rdf_nil),
inference(cnf_transformation,[],[f1460]) ).
fof(f2752,plain,
iext(uri_rdf_first,sK253,uri_ex_Falcon),
inference(cnf_transformation,[],[f1460]) ).
fof(f2753,plain,
iext(uri_rdf_rest,sK252,sK253),
inference(cnf_transformation,[],[f1460]) ).
fof(f2754,plain,
iext(uri_rdf_first,sK252,uri_ex_Eagle),
inference(cnf_transformation,[],[f1460]) ).
fof(f2755,plain,
iext(uri_owl_unionOf,sK251,sK252),
inference(cnf_transformation,[],[f1460]) ).
fof(f2756,plain,
iext(uri_rdf_type,uri_ex_harry,sK251),
inference(cnf_transformation,[],[f1460]) ).
fof(f2757,plain,
iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species),
inference(cnf_transformation,[],[f1460]) ).
fof(f2758,plain,
iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species),
inference(cnf_transformation,[],[f1460]) ).
fof(f2901,plain,
~ iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon),
inference(unit_resulting_resolution,[],[f2750,f2757]) ).
fof(f2902,plain,
~ iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle),
inference(unit_resulting_resolution,[],[f2750,f2758]) ).
fof(f8135,plain,
icext(sK251,uri_ex_harry),
inference(unit_resulting_resolution,[],[f1486,f2756]) ).
fof(f8778,plain,
~ icext(uri_ex_Falcon,uri_ex_harry),
inference(unit_resulting_resolution,[],[f1487,f2901]) ).
fof(f8779,plain,
~ icext(uri_ex_Eagle,uri_ex_harry),
inference(unit_resulting_resolution,[],[f1487,f2902]) ).
fof(f117148,plain,
~ sP4(sK251,uri_ex_Eagle,uri_ex_Falcon),
inference(unit_resulting_resolution,[],[f1886,f8779,f8135,f8778]) ).
fof(f117172,plain,
~ sP5(uri_ex_Falcon,uri_ex_Eagle,sK251,sK252),
inference(unit_resulting_resolution,[],[f1884,f2755,f117148]) ).
fof(f341050,plain,
$false,
inference(unit_resulting_resolution,[],[f1895,f117172,f2752,f2754,f2753,f2751]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB014+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 07:01:40 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.42 Running first-order model finding
% 0.15/0.42 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
% 17.34/2.94 % (3193197)Will run a generic schedule for satisfiability detection.
% 17.34/2.94 % (3193203)% WARNING: option uhcvi not known.
% 17.34/2.94 % (3193203)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1030877019:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 17.34/2.94 % (3193204)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1277817225:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 17.34/2.94 % (3193202)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=909868832_2999 on theBenchmark for (2999ds/0Mi)
% 17.34/2.94 % (3193207)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3093144369:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 17.34/2.94 % (3193205)dis+10_1_sil=32000:sp=arity:random_seed=2512089131:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 17.34/2.94 % (3193208)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3830773744:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 17.34/2.94 % (3193206)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2207010022:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 17.34/2.94 % (3193205)Instruction limit reached!
% 17.34/2.94 % (3193205)------------------------------
% 17.34/2.94 % (3193205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.34/2.94 % (3193205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/2.94 % (3193205)CaDiCaL version: 2.1.3
% 17.34/2.94 % (3193205)Termination reason: Instruction limit
% 17.34/2.94 % (3193205)Termination phase: Saturation
% 17.34/2.94 % (3193205)Time elapsed: 0.099 s
% 17.34/2.94 % (3193205)Peak memory usage: 14 MB
% 17.34/2.94 % (3193205)Instructions burned: 103 (million)
% 17.34/2.94 % (3193206)Instruction limit reached!
% 17.34/2.94 % (3193206)------------------------------
% 17.34/2.94 % (3193206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.34/2.94 % (3193206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/2.94 % (3193206)CaDiCaL version: 2.1.3
% 17.34/2.94 % (3193206)Termination reason: Instruction limit
% 17.34/2.94 % (3193206)Termination phase: Saturation
% 17.34/2.94 % (3193206)Time elapsed: 0.099 s
% 17.34/2.94 % (3193206)Peak memory usage: 13 MB
% 17.34/2.94 % (3193206)Instructions burned: 116 (million)
% 17.34/2.94 % (3193207)Instruction limit reached!
% 17.34/2.94 % (3193207)------------------------------
% 17.34/2.94 % (3193207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.34/2.94 % (3193207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/2.94 % (3193207)CaDiCaL version: 2.1.3
% 17.34/2.94 % (3193207)Termination reason: Instruction limit
% 17.34/2.94 % (3193207)Termination phase: Saturation
% 17.34/2.94 % (3193207)Time elapsed: 0.117 s
% 17.34/2.94 % (3193207)Peak memory usage: 14 MB
% 17.34/2.94 % (3193207)Instructions burned: 132 (million)
% 17.34/2.94 % (3193217)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3568186597:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 17.34/2.94 % (3193216)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=809732151:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 17.34/2.94 % (3193208)Instruction limit reached!
% 17.34/2.94 % (3193208)------------------------------
% 17.34/2.94 % (3193208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.34/2.94 % (3193208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.34/2.94 % (3193208)CaDiCaL version: 2.1.3
% 17.34/2.94 % (3193208)Termination reason: Instruction limit
% 17.34/2.94 % (3193208)Termination phase: Saturation
% 17.34/2.94 % (3193208)Time elapsed: 0.138 s
% 17.34/2.94 % (3193208)Peak memory usage: 15 MB
% 17.34/2.94 % (3193208)Instructions burned: 160 (million)
% 17.34/2.94 % (3193219)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=812998295:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 17.34/2.94 % (3193224)ott-21_1_sil=16000:fs=off:random_seed=66675412:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 17.34/2.94 % TRYING [1]
% 17.34/2.94 % TRYING [2]
% 17.34/2.94 % TRYING [1]
% 17.34/2.94 % TRYING [2]
% 17.34/2.94 % (3193217)Instruction limit reached!
% 17.34/2.94 % (3193217)------------------------------
% 17.34/2.94 % (3193217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.34/2.94 % (3193217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193217)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193217)Termination reason: Instruction limit
% 42.25/6.47 % (3193217)Termination phase: Saturation
% 42.25/6.47 % (3193217)Time elapsed: 0.095 s
% 42.25/6.47 % (3193217)Peak memory usage: 14 MB
% 42.25/6.47 % (3193217)Instructions burned: 133 (million)
% 42.25/6.47 % TRYING [3]
% 42.25/6.47 % (3193224)Instruction limit reached!
% 42.25/6.47 % (3193224)------------------------------
% 42.25/6.47 % (3193224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.25/6.47 % (3193224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193224)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193224)Termination reason: Instruction limit
% 42.25/6.47 % (3193224)Termination phase: Saturation
% 42.25/6.47 % (3193224)Time elapsed: 0.085 s
% 42.25/6.47 % (3193224)Peak memory usage: 15 MB
% 42.25/6.47 % (3193224)Instructions burned: 180 (million)
% 42.25/6.47 % (3193226)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3079079714:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.25/6.47 % TRYING [3]
% 42.25/6.47 % (3193227)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1185128433:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.25/6.47 % TRYING [1]
% 42.25/6.47 % TRYING [2]
% 42.25/6.47 % TRYING [4]
% 42.25/6.47 % (3193216)Instruction limit reached!
% 42.25/6.47 % (3193216)------------------------------
% 42.25/6.47 % (3193216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.25/6.47 % (3193216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193216)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193216)Termination reason: Instruction limit
% 42.25/6.47 % (3193216)Termination phase: Finite model building SAT solving
% 42.25/6.47 % (3193216)Time elapsed: 0.295 s
% 42.25/6.47 % (3193216)Peak memory usage: 42 MB
% 42.25/6.47 % (3193216)Instructions burned: 715 (million)
% 42.25/6.47 % (3193231)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1580342697:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.25/6.47 % (3193219)Instruction limit reached!
% 42.25/6.47 % (3193219)------------------------------
% 42.25/6.47 % (3193219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.25/6.47 % (3193219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193219)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193219)Termination reason: Instruction limit
% 42.25/6.47 % (3193219)Termination phase: Saturation
% 42.25/6.47 % (3193219)Time elapsed: 0.347 s
% 42.25/6.47 % (3193219)Peak memory usage: 24 MB
% 42.25/6.47 % (3193219)Instructions burned: 686 (million)
% 42.25/6.47 % (3193233)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3141721943:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.25/6.47 % (3193226)Instruction limit reached!
% 42.25/6.47 % (3193226)------------------------------
% 42.25/6.47 % (3193226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.25/6.47 % (3193226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193226)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193226)Termination reason: Instruction limit
% 42.25/6.47 % (3193226)Termination phase: Saturation
% 42.25/6.47 % (3193226)Time elapsed: 0.272 s
% 42.25/6.47 % (3193226)Peak memory usage: 17 MB
% 42.25/6.47 % (3193226)Instructions burned: 477 (million)
% 42.25/6.47 % (3193235)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=2100521474:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.25/6.47 % TRYING [3]
% 42.25/6.47 % (3193227)Instruction limit reached!
% 42.25/6.47 % (3193227)------------------------------
% 42.25/6.47 % (3193227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.25/6.47 % (3193227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.25/6.47 % (3193227)CaDiCaL version: 2.1.3
% 42.25/6.47 % (3193227)Termination reason: Instruction limit
% 42.25/6.47 % (3193227)Termination phase: Finite model building constraint generation
% 42.25/6.47 % (3193227)Time elapsed: 0.368 s
% 42.25/6.47 % (3193227)Peak memory usage: 30 MB
% 42.25/6.47 % (3193227)Instructions burned: 867 (million)
% 42.25/6.47 % (3193265)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=135176525:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.25/6.47 % (3193235)Instruction limit reached!
% 42.25/6.47 % (3193235)------------------------------
% 42.25/6.47 % (3193235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193235)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193235)Termination reason: Instruction limit
% 89.27/13.12 % (3193235)Termination phase: Saturation
% 89.27/13.12 % (3193235)Time elapsed: 0.392 s
% 89.27/13.12 % (3193235)Peak memory usage: 23 MB
% 89.27/13.12 % (3193235)Instructions burned: 693 (million)
% 89.27/13.12 % (3193233)Instruction limit reached!
% 89.27/13.12 % (3193233)------------------------------
% 89.27/13.12 % (3193233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193233)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193233)Termination reason: Instruction limit
% 89.27/13.12 % (3193233)Termination phase: Finite model building constraint generation
% 89.27/13.12 % (3193233)Time elapsed: 0.424 s
% 89.27/13.12 % (3193233)Peak memory usage: 101 MB
% 89.27/13.12 % (3193233)Instructions burned: 890 (million)
% 89.27/13.12 % (3193344)fmb+10_1_sil=64000:random_seed=1466838037:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 89.27/13.12 % (3193345)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3841031978:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 89.27/13.12 % TRYING [1]
% 89.27/13.12 % TRYING [2]
% 89.27/13.12 % TRYING [20]
% 89.27/13.12 % (3193231)Instruction limit reached!
% 89.27/13.12 % (3193231)------------------------------
% 89.27/13.12 % (3193231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193231)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193231)Termination reason: Instruction limit
% 89.27/13.12 % (3193231)Termination phase: Saturation
% 89.27/13.12 % (3193231)Time elapsed: 0.617 s
% 89.27/13.12 % (3193231)Peak memory usage: 32 MB
% 89.27/13.12 % (3193231)Instructions burned: 1179 (million)
% 89.27/13.12 % (3193265)Instruction limit reached!
% 89.27/13.12 % (3193265)------------------------------
% 89.27/13.12 % (3193265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193265)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193265)Termination reason: Instruction limit
% 89.27/13.12 % (3193265)Termination phase: Saturation
% 89.27/13.12 % (3193265)Time elapsed: 0.424 s
% 89.27/13.12 % (3193265)Peak memory usage: 31 MB
% 89.27/13.12 % (3193265)Instructions burned: 880 (million)
% 89.27/13.12 % (3193391)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2022981084:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 89.27/13.12 % (3193393)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=689276568:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 89.27/13.12 % TRYING [5]
% 89.27/13.12 % TRYING [3]
% 89.27/13.12 % TRYING [8]
% 89.27/13.12 % (3193391)Instruction limit reached!
% 89.27/13.12 % (3193391)------------------------------
% 89.27/13.12 % (3193391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193391)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193391)Termination reason: Instruction limit
% 89.27/13.12 % (3193391)Termination phase: Finite model building constraint generation
% 89.27/13.12 % (3193391)Time elapsed: 0.326 s
% 89.27/13.12 % (3193391)Peak memory usage: 52 MB
% 89.27/13.12 % (3193391)Instructions burned: 922 (million)
% 89.27/13.12 % (3193399)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2689411197:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 89.27/13.12 % TRYING [4]
% 89.27/13.12 % (3193399)Instruction limit reached!
% 89.27/13.12 % (3193399)------------------------------
% 89.27/13.12 % (3193399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 89.27/13.12 % (3193399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.27/13.12 % (3193399)CaDiCaL version: 2.1.3
% 89.27/13.12 % (3193399)Termination reason: Instruction limit
% 89.27/13.12 % (3193399)Termination phase: Saturation
% 89.27/13.12 % (3193399)Time elapsed: 0.867 s
% 89.27/13.12 % (3193399)Peak memory usage: 37 MB
% 89.27/13.12 % (3193399)Instructions burned: 1472 (million)
% 89.27/13.12 % (3193402)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1506859480:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 89.27/13.12 % (3193402)Cannot represent all propositional literals internally
% 89.27/13.12 % (3193402)Refutation not found, incomplete strategy
% 53.32/14.78 % (3193402)------------------------------
% 53.32/14.78 % (3193402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193402)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193402)Termination reason: Refutation not found, incomplete strategy
% 53.32/14.78 % (3193402)Time elapsed: 0.118 s
% 53.32/14.78 % (3193402)Peak memory usage: 16 MB
% 53.32/14.78 % (3193402)Instructions burned: 251 (million)
% 53.32/14.78 % (3193402)------------------------------
% 53.32/14.78 % (3193402)------------------------------
% 53.32/14.78 % (3193404)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3248990590:fmbsr=2.30978:i=2174_2974 on theBenchmark for (2974ds/2174Mi)
% 53.32/14.78 % (3193404)Cannot represent all propositional literals internally
% 53.32/14.78 % (3193404)Refutation not found, incomplete strategy
% 53.32/14.78 % (3193404)------------------------------
% 53.32/14.78 % (3193404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193404)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193404)Termination reason: Refutation not found, incomplete strategy
% 53.32/14.78 % (3193404)Time elapsed: 0.477 s
% 53.32/14.78 % (3193404)Peak memory usage: 25 MB
% 53.32/14.78 % (3193404)Instructions burned: 990 (million)
% 53.32/14.78 % (3193404)------------------------------
% 53.32/14.78 % (3193404)------------------------------
% 53.32/14.78 % (3193406)ott-2_1_sil=16000:newcnf=on:random_seed=780314991:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 53.32/14.78 % TRYING [5]
% 53.32/14.78 % (3193406)Instruction limit reached!
% 53.32/14.78 % (3193406)------------------------------
% 53.32/14.78 % (3193406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193406)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193406)Termination reason: Instruction limit
% 53.32/14.78 % (3193406)Termination phase: Saturation
% 53.32/14.78 % (3193406)Time elapsed: 0.451 s
% 53.32/14.78 % (3193406)Peak memory usage: 26 MB
% 53.32/14.78 % (3193406)Instructions burned: 871 (million)
% 53.32/14.78 % (3193408)ott+10_1_sil=32000:tgt=ground:random_seed=1502814796:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 53.32/14.78 % (3193393)Instruction limit reached!
% 53.32/14.78 % (3193393)------------------------------
% 53.32/14.78 % (3193393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193393)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193393)Termination reason: Instruction limit
% 53.32/14.78 % (3193393)Termination phase: Saturation
% 53.32/14.78 % (3193393)Time elapsed: 2.498 s
% 53.32/14.78 % (3193393)Peak memory usage: 30 MB
% 53.32/14.78 % (3193393)Instructions burned: 5131 (million)
% 53.32/14.78 % (3193410)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=238222083:i=54282_2963 on theBenchmark for (2963ds/54282Mi)
% 53.32/14.78 % TRYING [6]
% 53.32/14.78 % TRYING [1]
% 53.32/14.78 % TRYING [2]
% 53.32/14.78 % TRYING [3]
% 53.32/14.78 % TRYING [4]
% 53.32/14.78 % (3193345)Instruction limit reached!
% 53.32/14.78 % (3193345)------------------------------
% 53.32/14.78 % (3193345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193345)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193345)Termination reason: Instruction limit
% 53.32/14.78 % (3193345)Termination phase: Finite model building constraint generation
% 53.32/14.78 % (3193345)Time elapsed: 3.179 s
% 53.32/14.78 % (3193345)Peak memory usage: 527 MB
% 53.32/14.78 % (3193345)Instructions burned: 9517 (million)
% 53.32/14.78 % (3193412)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3303092421:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 53.32/14.78 % TRYING [5]
% 53.32/14.78 % (3193412)Instruction limit reached!
% 53.32/14.78 % (3193412)------------------------------
% 53.32/14.78 % (3193412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193412)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193412)Termination reason: Instruction limit
% 53.32/14.78 % (3193412)Termination phase: Saturation
% 53.32/14.78 % (3193412)Time elapsed: 1.766 s
% 53.32/14.78 % (3193412)Peak memory usage: 37 MB
% 53.32/14.78 % (3193412)Instructions burned: 3512 (million)
% 53.32/14.78 % (3193414)dis+21_1_sil=32000:sas=cadical:random_seed=3692593354:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 53.32/14.78 % (3193408)Instruction limit reached!
% 53.32/14.78 % (3193408)------------------------------
% 53.32/14.78 % (3193408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193408)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193408)Termination reason: Instruction limit
% 53.32/14.78 % (3193408)Termination phase: Saturation
% 53.32/14.78 % (3193408)Time elapsed: 2.744 s
% 53.32/14.78 % (3193408)Peak memory usage: 64 MB
% 53.32/14.78 % (3193408)Instructions burned: 5115 (million)
% 53.32/14.78 % (3193416)ott+11_1_sil=16000:gs=on:random_seed=1188841144:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 53.32/14.78 % TRYING [6]
% 53.32/14.78 % (3193416)Instruction limit reached!
% 53.32/14.78 % (3193416)------------------------------
% 53.32/14.78 % (3193416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193416)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193416)Termination reason: Instruction limit
% 53.32/14.78 % (3193416)Termination phase: Saturation
% 53.32/14.78 % (3193416)Time elapsed: 1.412 s
% 53.32/14.78 % (3193416)Peak memory usage: 56 MB
% 53.32/14.78 % (3193416)Instructions burned: 2251 (million)
% 53.32/14.78 % (3193418)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2642071463:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 53.32/14.78 % (3193414)Instruction limit reached!
% 53.32/14.78 % (3193414)------------------------------
% 53.32/14.78 % (3193414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193414)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193414)Termination reason: Instruction limit
% 53.32/14.78 % (3193414)Termination phase: Saturation
% 53.32/14.78 % (3193414)Time elapsed: 1.798 s
% 53.32/14.78 % (3193414)Peak memory usage: 42 MB
% 53.32/14.78 % (3193414)Instructions burned: 3774 (million)
% 53.32/14.78 % (3193420)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=529360688:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2921 on theBenchmark for (2921ds/4591Mi)
% 53.32/14.78 % TRYING [7]
% 53.32/14.78 % TRYING [6]
% 53.32/14.78 % (3193420)Instruction limit reached!
% 53.32/14.78 % (3193420)------------------------------
% 53.32/14.78 % (3193420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193420)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193420)Termination reason: Instruction limit
% 53.32/14.78 % (3193420)Termination phase: Saturation
% 53.32/14.78 % (3193420)Time elapsed: 1.578 s
% 53.32/14.78 % (3193420)Peak memory usage: 23 MB
% 53.32/14.78 % (3193420)Instructions burned: 4593 (million)
% 53.32/14.78 % (3193422)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=170813297:i=29340_2905 on theBenchmark for (2905ds/29340Mi)
% 53.32/14.78 % (3193344)Instruction limit reached!
% 53.32/14.78 % (3193344)------------------------------
% 53.32/14.78 % (3193344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193344)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193344)Termination reason: Instruction limit
% 53.32/14.78 % (3193344)Termination phase: Finite model building constraint generation
% 53.32/14.78 % (3193344)Time elapsed: 9.252 s
% 53.32/14.78 % (3193344)Peak memory usage: 232 MB
% 53.32/14.78 % (3193344)Instructions burned: 22063 (million)
% 53.32/14.78 % (3193424)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1270707027:i=5211_2897 on theBenchmark for (2897ds/5211Mi)
% 53.32/14.78 % (3193424)Instruction limit reached!
% 53.32/14.78 % (3193424)------------------------------
% 53.32/14.78 % (3193424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193424)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193424)Termination reason: Instruction limit
% 53.32/14.78 % (3193424)Termination phase: Saturation
% 53.32/14.78 % (3193424)Time elapsed: 2.376 s
% 53.32/14.78 % (3193424)Peak memory usage: 64 MB
% 53.32/14.78 % (3193424)Instructions burned: 5213 (million)
% 53.32/14.78 % (3193426)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2903746492:i=5497:nm=2_2873 on theBenchmark for (2873ds/5497Mi)
% 53.32/14.78 % TRYING [17]
% 53.32/14.78 % (3193422) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3193197-3193422"...
% 53.32/14.78 % (3193422)...printing done.
% 53.32/14.78 % (3193422)Refutation found. Thanks to Tanya!
% 53.32/14.78 % SZS status Theorem for theBenchmark
% 53.32/14.78 % SZS output start Proof for theBenchmark
% See solution above
% 53.32/14.78 % (3193422)------------------------------
% 53.32/14.78 % (3193422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.32/14.78 % (3193422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.32/14.78 % (3193422)CaDiCaL version: 2.1.3
% 53.32/14.78 % (3193422)Termination reason: Refutation
% 53.32/14.78 % (3193422)Time elapsed: 4.698 s
% 53.32/14.78 % (3193422)Peak memory usage: 115 MB
% 53.32/14.78 % (3193422)Instructions burned: 9513 (million)
% 53.32/14.78 % (3193197)Success in time 14.344 s
% 53.32/14.78 % Vampire exiting
%------------------------------------------------------------------------------