%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB044+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 : n007.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:51 PM UTC 2026
% Result : Theorem 38.62s 14.37s
% Output : Refutation 38.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 61 ( 26 unt; 0 def)
% Number of atoms : 217 ( 26 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 244 ( 88 ~; 85 |; 56 &)
% ( 10 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-2 aty)
% Number of variables : 119 ( 106 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( iext(X1,X0,X2)
=> ip(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',simple_iext_property) ).
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(f52,axiom,
! [X0,X1,X2,X3] :
( ( iext(uri_rdfs_domain,X0,X1)
& iext(X0,X2,X3) )
=> icext(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',rdfs_domain_main) ).
fof(f59,axiom,
! [X0,X1,X2,X3] :
( ( iext(uri_rdfs_range,X0,X1)
& iext(X0,X2,X3) )
=> icext(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',rdfs_range_main) ).
fof(f295,axiom,
! [X0,X1,X2] :
( ( iext(uri_rdf_first,X1,X2)
& iext(uri_rdf_rest,X1,uri_rdf_nil) )
=> ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_enum_class_001) ).
fof(f345,axiom,
! [X0,X1] :
( iext(uri_owl_differentFrom,X0,X1)
<=> X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_eqdis_differentfrom) ).
fof(f392,axiom,
! [X0] :
( icext(uri_owl_AsymmetricProperty,X0)
<=> ( ip(X0)
& ! [X1,X2] :
( iext(X0,X1,X2)
=> ~ iext(X0,X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_char_asymmetric) ).
fof(f559,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conclusion_rdfbased_sem_char_asymmetric_ext) ).
fof(f560,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X0,X1,X2,X3] :
( iext(uri_owl_oneOf,X2,X3)
& iext(uri_rdfs_domain,uri_ex_p,X0)
& iext(uri_rdfs_range,uri_ex_p,X2)
& iext(uri_owl_oneOf,X0,X1)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)
& iext(uri_rdf_first,X3,uri_ex_y)
& iext(uri_rdf_rest,X3,uri_rdf_nil)
& iext(uri_rdf_first,X1,uri_ex_x)
& iext(uri_rdf_rest,X1,uri_rdf_nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',premise_rdfbased_sem_char_asymmetric_ext) ).
fof(f572,plain,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
inference(flattening,[],[f560]) ).
fof(f573,plain,
! [X0,X1,X2] :
( ip(X1)
| ~ iext(X1,X0,X2) ),
inference(ennf_transformation,[],[f1]) ).
fof(f578,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(uri_rdfs_domain,X0,X1)
| ~ iext(X0,X2,X3) ),
inference(ennf_transformation,[],[f52]) ).
fof(f579,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(uri_rdfs_domain,X0,X1)
| ~ iext(X0,X2,X3) ),
inference(flattening,[],[f578]) ).
fof(f580,plain,
! [X0,X1,X2,X3] :
( icext(X1,X3)
| ~ iext(uri_rdfs_range,X0,X1)
| ~ iext(X0,X2,X3) ),
inference(ennf_transformation,[],[f59]) ).
fof(f581,plain,
! [X0,X1,X2,X3] :
( icext(X1,X3)
| ~ iext(uri_rdfs_range,X0,X1)
| ~ iext(X0,X2,X3) ),
inference(flattening,[],[f580]) ).
fof(f697,plain,
! [X0,X1,X2] :
( ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(ennf_transformation,[],[f295]) ).
fof(f698,plain,
! [X0,X1,X2] :
( ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(flattening,[],[f697]) ).
fof(f847,plain,
! [X0] :
( icext(uri_owl_AsymmetricProperty,X0)
<=> ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) ) ),
inference(ennf_transformation,[],[f392]) ).
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(f1139,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X3] :
( ( icext(X0,X3)
| X2 != X3 )
& ( X3 = X2
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(nnf_transformation,[],[f698]) ).
fof(f1140,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X3] :
( ( icext(X0,X3)
| X2 != X3 )
& ( X3 = X2
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(flattening,[],[f1139]) ).
fof(f1141,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X4] :
( ( icext(X0,X4)
| X2 != X4 )
& ( X2 = X4
| ~ icext(X0,X4) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(rectify,[],[f1140]) ).
fof(f1142,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ( ( sK62(X0,X2) != X2
| ~ icext(X0,sK62(X0,X2)) )
& ( sK62(X0,X2) = X2
| icext(X0,sK62(X0,X2)) ) ) )
& ( ( ic(X0)
& ! [X4] :
( ( icext(X0,X4)
| X2 != X4 )
& ( X2 = X4
| ~ icext(X0,X4) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X3,sK62(X0,X2))],[f1141]) ).
fof(f1320,plain,
! [X0,X1] :
( ( iext(uri_owl_differentFrom,X0,X1)
| X0 = X1 )
& ( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ) ),
inference(nnf_transformation,[],[f345]) ).
fof(f1411,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(nnf_transformation,[],[f847]) ).
fof(f1412,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(flattening,[],[f1411]) ).
fof(f1413,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X3,X4] :
( ~ iext(X0,X4,X3)
| ~ iext(X0,X3,X4) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(rectify,[],[f1412]) ).
fof(f1414,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ( iext(X0,sK221(X0),sK220(X0))
& iext(X0,sK220(X0),sK221(X0)) ) )
& ( ( ip(X0)
& ! [X3,X4] :
( ~ iext(X0,X4,X3)
| ~ iext(X0,X3,X4) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK220,sK221]),skolemize(X1,sK220(X0)),skolemize(X2,sK221(X0))],[f1413]) ).
fof(f1460,plain,
( iext(uri_owl_oneOf,sK253,sK254)
& iext(uri_rdfs_domain,uri_ex_p,sK251)
& iext(uri_rdfs_range,uri_ex_p,sK253)
& iext(uri_owl_oneOf,sK251,sK252)
& iext(uri_ex_p,uri_ex_x,uri_ex_y)
& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)
& iext(uri_rdf_first,sK254,uri_ex_y)
& iext(uri_rdf_rest,sK254,uri_rdf_nil)
& iext(uri_rdf_first,sK252,uri_ex_x)
& iext(uri_rdf_rest,sK252,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251,sK252,sK253,sK254]),skolemize(X0,sK251),skolemize(X1,sK252),skolemize(X2,sK253),skolemize(X3,sK254)],[f561]) ).
fof(f1461,plain,
! [X2,X0,X1] :
( ~ iext(X1,X0,X2)
| ip(X1) ),
inference(cnf_transformation,[],[f573]) ).
fof(f1487,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[],[f1061]) ).
fof(f1514,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ),
inference(cnf_transformation,[],[f579]) ).
fof(f1524,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_rdfs_range,X0,X1)
| icext(X1,X3)
| ~ iext(X0,X2,X3) ),
inference(cnf_transformation,[],[f581]) ).
fof(f1917,plain,
! [X2,X0,X1,X4] :
( ~ iext(uri_owl_oneOf,X0,X1)
| ~ icext(X0,X4)
| X2 = X4
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(cnf_transformation,[],[f1142]) ).
fof(f2321,plain,
! [X0,X1] :
( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[],[f1320]) ).
fof(f2510,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0)
| iext(X0,sK220(X0),sK221(X0)) ),
inference(cnf_transformation,[],[f1414]) ).
fof(f2511,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0)
| iext(X0,sK221(X0),sK220(X0)) ),
inference(cnf_transformation,[],[f1414]) ).
fof(f2750,plain,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_AsymmetricProperty),
inference(cnf_transformation,[],[f572]) ).
fof(f2751,plain,
iext(uri_rdf_rest,sK252,uri_rdf_nil),
inference(cnf_transformation,[],[f1460]) ).
fof(f2752,plain,
iext(uri_rdf_first,sK252,uri_ex_x),
inference(cnf_transformation,[],[f1460]) ).
fof(f2753,plain,
iext(uri_rdf_rest,sK254,uri_rdf_nil),
inference(cnf_transformation,[],[f1460]) ).
fof(f2754,plain,
iext(uri_rdf_first,sK254,uri_ex_y),
inference(cnf_transformation,[],[f1460]) ).
fof(f2755,plain,
iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y),
inference(cnf_transformation,[],[f1460]) ).
fof(f2756,plain,
iext(uri_ex_p,uri_ex_x,uri_ex_y),
inference(cnf_transformation,[],[f1460]) ).
fof(f2757,plain,
iext(uri_owl_oneOf,sK251,sK252),
inference(cnf_transformation,[],[f1460]) ).
fof(f2758,plain,
iext(uri_rdfs_range,uri_ex_p,sK253),
inference(cnf_transformation,[],[f1460]) ).
fof(f2759,plain,
iext(uri_rdfs_domain,uri_ex_p,sK251),
inference(cnf_transformation,[],[f1460]) ).
fof(f2760,plain,
iext(uri_owl_oneOf,sK253,sK254),
inference(cnf_transformation,[],[f1460]) ).
fof(f2767,plain,
! [X1] : ~ iext(uri_owl_differentFrom,X1,X1),
inference(equality_resolution,[],[f2321]) ).
fof(f4364,plain,
ip(uri_ex_p),
inference(unit_resulting_resolution,[],[f1461,f2756]) ).
fof(f8864,plain,
~ icext(uri_owl_AsymmetricProperty,uri_ex_p),
inference(unit_resulting_resolution,[],[f1487,f2750]) ).
fof(f72616,plain,
iext(uri_ex_p,sK220(uri_ex_p),sK221(uri_ex_p)),
inference(unit_resulting_resolution,[],[f2510,f4364,f8864]) ).
fof(f72727,plain,
icext(sK251,sK220(uri_ex_p)),
inference(unit_resulting_resolution,[],[f1514,f2759,f72616]) ).
fof(f72939,plain,
iext(uri_ex_p,sK221(uri_ex_p),sK220(uri_ex_p)),
inference(unit_resulting_resolution,[],[f2511,f4364,f8864]) ).
fof(f73052,plain,
icext(sK253,sK220(uri_ex_p)),
inference(unit_resulting_resolution,[],[f1524,f2758,f72939]) ).
fof(f250885,plain,
uri_ex_x = sK220(uri_ex_p),
inference(unit_resulting_resolution,[],[f1917,f72727,f2757,f2752,f2751]) ).
fof(f250919,plain,
icext(sK253,uri_ex_x),
inference(superposition,[],[f73052,f250885]) ).
fof(f251035,plain,
uri_ex_x = uri_ex_y,
inference(unit_resulting_resolution,[],[f1917,f2754,f2753,f2760,f250919]) ).
fof(f251161,plain,
iext(uri_owl_differentFrom,uri_ex_x,uri_ex_x),
inference(superposition,[],[f2755,f251035]) ).
fof(f251163,plain,
$false,
inference(forward_subsumption_resolution,[],[f251161,f2767]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB044+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 % Computer : n007.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Mon Sep 28 07:07:56 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/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
% 16.57/2.85 % (2213312)Will run a generic schedule for satisfiability detection.
% 16.57/2.85 % (2213319)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4277582386:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.57/2.85 % (2213318)% WARNING: option uhcvi not known.
% 16.57/2.85 % (2213317)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2925929712_2999 on theBenchmark for (2999ds/0Mi)
% 16.57/2.85 % (2213318)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=517671227:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.57/2.85 % (2213320)dis+10_1_sil=32000:sp=arity:random_seed=366159838:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.57/2.85 % (2213321)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3655027844:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.57/2.85 % (2213322)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3670436197:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.57/2.85 % (2213323)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2809133630:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.57/2.85 % (2213320)Instruction limit reached!
% 16.57/2.85 % (2213320)------------------------------
% 16.57/2.85 % (2213320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.57/2.85 % (2213320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/2.85 % (2213320)CaDiCaL version: 2.1.3
% 16.57/2.85 % (2213320)Termination reason: Instruction limit
% 16.57/2.85 % (2213320)Termination phase: Saturation
% 16.57/2.85 % (2213320)Time elapsed: 0.055 s
% 16.57/2.85 % (2213320)Peak memory usage: 14 MB
% 16.57/2.85 % (2213320)Instructions burned: 105 (million)
% 16.57/2.85 % (2213321)Instruction limit reached!
% 16.57/2.85 % (2213321)------------------------------
% 16.57/2.85 % (2213321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.57/2.85 % (2213321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/2.85 % (2213321)CaDiCaL version: 2.1.3
% 16.57/2.85 % (2213321)Termination reason: Instruction limit
% 16.57/2.85 % (2213321)Termination phase: Saturation
% 16.57/2.85 % (2213321)Time elapsed: 0.055 s
% 16.57/2.85 % (2213321)Peak memory usage: 13 MB
% 16.57/2.85 % (2213321)Instructions burned: 116 (million)
% 16.57/2.85 % (2213322)Instruction limit reached!
% 16.57/2.85 % (2213322)------------------------------
% 16.57/2.85 % (2213322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.57/2.85 % (2213322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/2.85 % (2213322)CaDiCaL version: 2.1.3
% 16.57/2.85 % (2213322)Termination reason: Instruction limit
% 16.57/2.85 % (2213322)Termination phase: Saturation
% 16.57/2.85 % (2213322)Time elapsed: 0.066 s
% 16.57/2.85 % (2213322)Peak memory usage: 14 MB
% 16.57/2.85 % (2213322)Instructions burned: 131 (million)
% 16.57/2.85 % (2213331)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2203450293:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.57/2.85 % (2213332)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3925585101:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.57/2.85 % (2213323)Instruction limit reached!
% 16.57/2.85 % (2213323)------------------------------
% 16.57/2.85 % (2213323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.57/2.85 % (2213323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.57/2.85 % (2213323)CaDiCaL version: 2.1.3
% 16.57/2.85 % (2213323)Termination reason: Instruction limit
% 16.57/2.85 % (2213323)Termination phase: Saturation
% 16.57/2.85 % (2213323)Time elapsed: 0.081 s
% 16.57/2.85 % (2213323)Peak memory usage: 15 MB
% 16.57/2.85 % (2213323)Instructions burned: 159 (million)
% 16.57/2.85 % (2213333)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=1305461111:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.57/2.85 % (2213336)ott-21_1_sil=16000:fs=off:random_seed=850935062:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.57/2.85 % TRYING [1]
% 16.57/2.85 % TRYING [2]
% 16.57/2.85 % (2213332)Instruction limit reached!
% 16.57/2.85 % (2213332)------------------------------
% 16.57/2.85 % (2213332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.57/2.85 % (2213332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213332)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213332)Termination reason: Instruction limit
% 42.20/6.43 % (2213332)Termination phase: Saturation
% 42.20/6.43 % (2213332)Time elapsed: 0.069 s
% 42.20/6.43 % (2213332)Peak memory usage: 14 MB
% 42.20/6.43 % (2213332)Instructions burned: 132 (million)
% 42.20/6.43 % TRYING [1]
% 42.20/6.43 % TRYING [2]
% 42.20/6.43 % (2213339)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3433982575:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.20/6.43 % TRYING [3]
% 42.20/6.43 % (2213336)Instruction limit reached!
% 42.20/6.43 % (2213336)------------------------------
% 42.20/6.43 % (2213336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.20/6.43 % (2213336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213336)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213336)Termination reason: Instruction limit
% 42.20/6.43 % (2213336)Termination phase: Saturation
% 42.20/6.43 % (2213336)Time elapsed: 0.084 s
% 42.20/6.43 % (2213336)Peak memory usage: 15 MB
% 42.20/6.43 % (2213336)Instructions burned: 180 (million)
% 42.20/6.43 % TRYING [3]
% 42.20/6.43 % (2213341)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3745414554:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.20/6.43 % TRYING [1]
% 42.20/6.43 % TRYING [2]
% 42.20/6.43 % TRYING [4]
% 42.20/6.43 % (2213331)Instruction limit reached!
% 42.20/6.43 % (2213331)------------------------------
% 42.20/6.43 % (2213331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.20/6.43 % (2213331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213331)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213331)Termination reason: Instruction limit
% 42.20/6.43 % (2213331)Termination phase: Finite model building SAT solving
% 42.20/6.43 % (2213331)Time elapsed: 0.301 s
% 42.20/6.43 % (2213331)Peak memory usage: 43 MB
% 42.20/6.43 % (2213331)Instructions burned: 714 (million)
% 42.20/6.43 % (2213343)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1368724073:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.20/6.43 % (2213339)Instruction limit reached!
% 42.20/6.43 % (2213339)------------------------------
% 42.20/6.43 % (2213339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.20/6.43 % (2213339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213339)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213339)Termination reason: Instruction limit
% 42.20/6.43 % (2213339)Termination phase: Saturation
% 42.20/6.43 % (2213339)Time elapsed: 0.274 s
% 42.20/6.43 % (2213339)Peak memory usage: 18 MB
% 42.20/6.43 % (2213339)Instructions burned: 478 (million)
% 42.20/6.43 % (2213333)Instruction limit reached!
% 42.20/6.43 % (2213333)------------------------------
% 42.20/6.43 % (2213333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.20/6.43 % (2213333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213333)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213333)Termination reason: Instruction limit
% 42.20/6.43 % (2213333)Termination phase: Saturation
% 42.20/6.43 % (2213333)Time elapsed: 0.366 s
% 42.20/6.43 % (2213333)Peak memory usage: 22 MB
% 42.20/6.43 % (2213333)Instructions burned: 686 (million)
% 42.20/6.43 % (2213345)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3067967980:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 42.20/6.43 % (2213346)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=429071991: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.20/6.43 % TRYING [3]
% 42.20/6.43 % (2213341)Instruction limit reached!
% 42.20/6.43 % (2213341)------------------------------
% 42.20/6.43 % (2213341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.20/6.43 % (2213341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.20/6.43 % (2213341)CaDiCaL version: 2.1.3
% 42.20/6.43 % (2213341)Termination reason: Instruction limit
% 42.20/6.43 % (2213341)Termination phase: Finite model building constraint generation
% 42.20/6.43 % (2213341)Time elapsed: 0.372 s
% 42.20/6.43 % (2213341)Peak memory usage: 30 MB
% 42.20/6.43 % (2213341)Instructions burned: 867 (million)
% 42.20/6.43 % (2213349)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=638167386:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.20/6.43 % (2213346)Instruction limit reached!
% 42.20/6.43 % (2213346)------------------------------
% 42.20/6.43 % (2213346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213346)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213346)Termination reason: Instruction limit
% 91.85/13.41 % (2213346)Termination phase: Saturation
% 91.85/13.41 % (2213346)Time elapsed: 0.391 s
% 91.85/13.41 % (2213346)Peak memory usage: 19 MB
% 91.85/13.41 % (2213346)Instructions burned: 693 (million)
% 91.85/13.41 % (2213345)Instruction limit reached!
% 91.85/13.41 % (2213345)------------------------------
% 91.85/13.41 % (2213345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213345)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213345)Termination reason: Instruction limit
% 91.85/13.41 % (2213345)Termination phase: Finite model building constraint generation
% 91.85/13.41 % (2213345)Time elapsed: 0.421 s
% 91.85/13.41 % (2213345)Peak memory usage: 96 MB
% 91.85/13.41 % (2213345)Instructions burned: 892 (million)
% 91.85/13.41 % (2213351)fmb+10_1_sil=64000:random_seed=500005326:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 91.85/13.41 % (2213353)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=814268945:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 91.85/13.41 % TRYING [1]
% 91.85/13.41 % TRYING [2]
% 91.85/13.41 % TRYING [20]
% 91.85/13.41 % (2213343)Instruction limit reached!
% 91.85/13.41 % (2213343)------------------------------
% 91.85/13.41 % (2213343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213343)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213343)Termination reason: Instruction limit
% 91.85/13.41 % (2213343)Termination phase: Saturation
% 91.85/13.41 % (2213343)Time elapsed: 0.610 s
% 91.85/13.41 % (2213343)Peak memory usage: 32 MB
% 91.85/13.41 % (2213343)Instructions burned: 1179 (million)
% 91.85/13.41 % (2213349)Instruction limit reached!
% 91.85/13.41 % (2213349)------------------------------
% 91.85/13.41 % (2213349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213349)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213349)Termination reason: Instruction limit
% 91.85/13.41 % (2213349)Termination phase: Saturation
% 91.85/13.41 % (2213349)Time elapsed: 0.416 s
% 91.85/13.41 % (2213349)Peak memory usage: 29 MB
% 91.85/13.41 % (2213349)Instructions burned: 880 (million)
% 91.85/13.41 % (2213355)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2931860645:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 91.85/13.41 % (2213356)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3552606471:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 91.85/13.41 % TRYING [3]
% 91.85/13.41 % TRYING [5]
% 91.85/13.41 % TRYING [8]
% 91.85/13.41 % (2213355)Instruction limit reached!
% 91.85/13.41 % (2213355)------------------------------
% 91.85/13.41 % (2213355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213355)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213355)Termination reason: Instruction limit
% 91.85/13.41 % (2213355)Termination phase: Finite model building constraint generation
% 91.85/13.41 % (2213355)Time elapsed: 0.327 s
% 91.85/13.41 % (2213355)Peak memory usage: 52 MB
% 91.85/13.41 % (2213355)Instructions burned: 921 (million)
% 91.85/13.41 % (2213359)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2422048694:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 91.85/13.41 % TRYING [4]
% 91.85/13.41 % (2213359)Instruction limit reached!
% 91.85/13.41 % (2213359)------------------------------
% 91.85/13.41 % (2213359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.85/13.41 % (2213359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.85/13.41 % (2213359)CaDiCaL version: 2.1.3
% 91.85/13.41 % (2213359)Termination reason: Instruction limit
% 91.85/13.41 % (2213359)Termination phase: Saturation
% 91.85/13.41 % (2213359)Time elapsed: 0.836 s
% 91.85/13.41 % (2213359)Peak memory usage: 38 MB
% 91.85/13.41 % (2213359)Instructions burned: 1474 (million)
% 91.85/13.41 % (2213361)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3878263665:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 91.85/13.41 % (2213361)Cannot represent all propositional literals internally
% 91.85/13.41 % (2213361)Refutation not found, incomplete strategy
% 38.62/14.37 % (2213361)------------------------------
% 38.62/14.37 % (2213361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213361)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213361)Termination reason: Refutation not found, incomplete strategy
% 38.62/14.37 % (2213361)Time elapsed: 0.120 s
% 38.62/14.37 % (2213361)Peak memory usage: 16 MB
% 38.62/14.37 % (2213361)Instructions burned: 251 (million)
% 38.62/14.37 % (2213361)------------------------------
% 38.62/14.37 % (2213361)------------------------------
% 38.62/14.37 % (2213363)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4052555013:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi)
% 38.62/14.37 % (2213363)Cannot represent all propositional literals internally
% 38.62/14.37 % (2213363)Refutation not found, incomplete strategy
% 38.62/14.37 % (2213363)------------------------------
% 38.62/14.37 % (2213363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213363)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213363)Termination reason: Refutation not found, incomplete strategy
% 38.62/14.37 % (2213363)Time elapsed: 0.482 s
% 38.62/14.37 % (2213363)Peak memory usage: 25 MB
% 38.62/14.37 % (2213363)Instructions burned: 990 (million)
% 38.62/14.37 % (2213363)------------------------------
% 38.62/14.37 % (2213363)------------------------------
% 38.62/14.37 % (2213365)ott-2_1_sil=16000:newcnf=on:random_seed=960428342:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 38.62/14.37 % TRYING [5]
% 38.62/14.37 % (2213365)Instruction limit reached!
% 38.62/14.37 % (2213365)------------------------------
% 38.62/14.37 % (2213365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213365)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213365)Termination reason: Instruction limit
% 38.62/14.37 % (2213365)Termination phase: Saturation
% 38.62/14.37 % (2213365)Time elapsed: 0.449 s
% 38.62/14.37 % (2213365)Peak memory usage: 25 MB
% 38.62/14.37 % (2213365)Instructions burned: 871 (million)
% 38.62/14.37 % (2213367)ott+10_1_sil=32000:tgt=ground:random_seed=3936999472:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 38.62/14.37 % (2213356)Instruction limit reached!
% 38.62/14.37 % (2213356)------------------------------
% 38.62/14.37 % (2213356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213356)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213356)Termination reason: Instruction limit
% 38.62/14.37 % (2213356)Termination phase: Saturation
% 38.62/14.37 % (2213356)Time elapsed: 2.420 s
% 38.62/14.37 % (2213356)Peak memory usage: 32 MB
% 38.62/14.37 % (2213356)Instructions burned: 5132 (million)
% 38.62/14.37 % (2213369)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=808356602:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 38.62/14.37 % TRYING [1]
% 38.62/14.37 % TRYING [2]
% 38.62/14.37 % TRYING [3]
% 38.62/14.37 % TRYING [6]
% 38.62/14.37 % TRYING [4]
% 38.62/14.37 % (2213353)Instruction limit reached!
% 38.62/14.37 % (2213353)------------------------------
% 38.62/14.37 % (2213353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213353)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213353)Termination reason: Instruction limit
% 38.62/14.37 % (2213353)Termination phase: Finite model building constraint generation
% 38.62/14.37 % (2213353)Time elapsed: 3.187 s
% 38.62/14.37 % (2213353)Peak memory usage: 527 MB
% 38.62/14.37 % (2213353)Instructions burned: 9516 (million)
% 38.62/14.37 % (2213371)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3069033280:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 38.62/14.37 % TRYING [5]
% 38.62/14.37 % (2213371)Instruction limit reached!
% 38.62/14.37 % (2213371)------------------------------
% 38.62/14.37 % (2213371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213371)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213371)Termination reason: Instruction limit
% 38.62/14.37 % (2213371)Termination phase: Saturation
% 38.62/14.37 % (2213371)Time elapsed: 1.762 s
% 38.62/14.37 % (2213371)Peak memory usage: 33 MB
% 38.62/14.37 % (2213371)Instructions burned: 3514 (million)
% 38.62/14.37 % (2213373)dis+21_1_sil=32000:sas=cadical:random_seed=1569703707:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 38.62/14.37 % (2213367)Instruction limit reached!
% 38.62/14.37 % (2213367)------------------------------
% 38.62/14.37 % (2213367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213367)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213367)Termination reason: Instruction limit
% 38.62/14.37 % (2213367)Termination phase: Saturation
% 38.62/14.37 % (2213367)Time elapsed: 2.761 s
% 38.62/14.37 % (2213367)Peak memory usage: 64 MB
% 38.62/14.37 % (2213367)Instructions burned: 5114 (million)
% 38.62/14.37 % (2213375)ott+11_1_sil=16000:gs=on:random_seed=3192424885:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2938 on theBenchmark for (2938ds/2251Mi)
% 38.62/14.37 % TRYING [6]
% 38.62/14.37 % (2213375)Instruction limit reached!
% 38.62/14.37 % (2213375)------------------------------
% 38.62/14.37 % (2213375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213375)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213375)Termination reason: Instruction limit
% 38.62/14.37 % (2213375)Termination phase: Saturation
% 38.62/14.37 % (2213375)Time elapsed: 1.433 s
% 38.62/14.37 % (2213375)Peak memory usage: 55 MB
% 38.62/14.37 % (2213375)Instructions burned: 2251 (million)
% 38.62/14.37 % (2213377)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1743681043:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 38.62/14.37 % (2213373)Instruction limit reached!
% 38.62/14.37 % (2213373)------------------------------
% 38.62/14.37 % (2213373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213373)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213373)Termination reason: Instruction limit
% 38.62/14.37 % (2213373)Termination phase: Saturation
% 38.62/14.37 % (2213373)Time elapsed: 1.908 s
% 38.62/14.37 % (2213373)Peak memory usage: 45 MB
% 38.62/14.37 % (2213373)Instructions burned: 3773 (million)
% 38.62/14.37 % (2213379)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2731390696:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 38.62/14.37 % TRYING [7]
% 38.62/14.37 % TRYING [6]
% 38.62/14.37 % (2213351)Instruction limit reached!
% 38.62/14.37 % (2213351)------------------------------
% 38.62/14.37 % (2213351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213351)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213351)Termination reason: Instruction limit
% 38.62/14.37 % (2213351)Termination phase: Finite model building constraint generation
% 38.62/14.37 % (2213351)Time elapsed: 9.281 s
% 38.62/14.37 % (2213351)Peak memory usage: 237 MB
% 38.62/14.37 % (2213351)Instructions burned: 22061 (million)
% 38.62/14.37 % (2213381)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3260798580:i=29340_2897 on theBenchmark for (2897ds/29340Mi)
% 38.62/14.37 % (2213379)Instruction limit reached!
% 38.62/14.37 % (2213379)------------------------------
% 38.62/14.37 % (2213379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213379)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213379)Termination reason: Instruction limit
% 38.62/14.37 % (2213379)Termination phase: Saturation
% 38.62/14.37 % (2213379)Time elapsed: 2.454 s
% 38.62/14.37 % (2213379)Peak memory usage: 53 MB
% 38.62/14.37 % (2213379)Instructions burned: 4592 (million)
% 38.62/14.37 % (2213383)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1030213251:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 38.62/14.37 % (2213383)Instruction limit reached!
% 38.62/14.37 % (2213383)------------------------------
% 38.62/14.37 % (2213383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.37 % (2213383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.37 % (2213383)CaDiCaL version: 2.1.3
% 38.62/14.37 % (2213383)Termination reason: Instruction limit
% 38.62/14.37 % (2213383)Termination phase: Saturation
% 38.62/14.37 % (2213383)Time elapsed: 2.540 s
% 38.62/14.37 % (2213383)Peak memory usage: 63 MB
% 38.62/14.37 % (2213383)Instructions burned: 5213 (million)
% 38.62/14.37 % (2213385)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1743716548:i=5497:nm=2_2870 on theBenchmark for (2870ds/5497Mi)
% 38.62/14.37 % TRYING [17]
% 38.62/14.37 % (2213381) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2213312-2213381"...
% 38.62/14.37 % (2213381)...printing done.
% 38.62/14.37 % (2213381)Refutation found. Thanks to Tanya!
% 38.62/14.37 % SZS status Theorem for theBenchmark
% 38.62/14.37 % SZS output start Proof for theBenchmark
% See solution above
% 38.62/14.38 % (2213381)------------------------------
% 38.62/14.38 % (2213381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.62/14.38 % (2213381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.62/14.38 % (2213381)CaDiCaL version: 2.1.3
% 38.62/14.38 % (2213381)Termination reason: Refutation
% 38.62/14.38 % (2213381)Time elapsed: 3.528 s
% 38.62/14.38 % (2213381)Peak memory usage: 85 MB
% 38.62/14.38 % (2213381)Instructions burned: 7227 (million)
% 38.62/14.38 % (2213312)Success in time 13.947 s
% 38.62/14.38 % Vampire exiting
%------------------------------------------------------------------------------