%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR033+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:42:06 AM UTC 2026
% Result : Theorem 49.62s 12.29s
% Output : Refutation 49.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of formulae : 64 ( 22 unt; 0 def)
% Number of atoms : 121 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 102 ( 45 ~; 40 |; 6 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 44 ( 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6757,axiom,
genlmt(c_tptpgeo_member4_mt,c_tptpgeo_spindleheadmt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_6757) ).
fof(f28207,axiom,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_28207) ).
fof(f36571,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_36571) ).
fof(f62185,axiom,
! [X0,X1] :
( geographicalsubregions(X0,X1)
=> inregion(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_62192) ).
fof(f81149,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_81161) ).
fof(f121419,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member4_mt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_121440) ).
fof(f157435,axiom,
( mtvisible(c_worldgeographymt)
=> geolevel_1(c_georegion_l1_x2_y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_157462) ).
fof(f217827,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_217861) ).
fof(f300164,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_300209) ).
fof(f301129,axiom,
( mtvisible(c_tptpgeo_member2_mt)
=> inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_301174) ).
fof(f538325,axiom,
! [X0,X1,X2] :
( ( geographicalsubregions(X0,X1)
& geographicalsubregions(X1,X2) )
=> geographicalsubregions(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_538370) ).
fof(f538805,axiom,
! [X0,X1,X2] :
( ( inregion(X0,X1)
& inregion(X1,X2) )
=> inregion(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_538850) ).
fof(f540175,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4_540220) ).
fof(f540250,conjecture,
( mtvisible(c_tptpgeo_spindlecollectormt)
=> ( inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)
& geolevel_1(c_georegion_l1_x2_y0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query233) ).
fof(f540251,negated_conjecture,
~ ( mtvisible(c_tptpgeo_spindlecollectormt)
=> ( inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)
& geolevel_1(c_georegion_l1_x2_y0) ) ),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f540459,plain,
( ( ~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)
| ~ geolevel_1(c_georegion_l1_x2_y0) )
& mtvisible(c_tptpgeo_spindlecollectormt) ),
inference(ennf_transformation,[],[f540251]) ).
fof(f540466,plain,
( geolevel_1(c_georegion_l1_x2_y0)
| ~ mtvisible(c_worldgeographymt) ),
inference(ennf_transformation,[],[f157435]) ).
fof(f540474,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(ennf_transformation,[],[f217827]) ).
fof(f540483,plain,
! [X0,X1,X2] :
( inregion(X0,X2)
| ~ inregion(X0,X1)
| ~ inregion(X1,X2) ),
inference(ennf_transformation,[],[f538805]) ).
fof(f540484,plain,
! [X0,X1,X2] :
( inregion(X0,X2)
| ~ inregion(X0,X1)
| ~ inregion(X1,X2) ),
inference(flattening,[],[f540483]) ).
fof(f540486,plain,
! [X0,X1] :
( inregion(X1,X0)
| ~ geographicalsubregions(X0,X1) ),
inference(ennf_transformation,[],[f62185]) ).
fof(f540487,plain,
( inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(ennf_transformation,[],[f301129]) ).
fof(f540512,plain,
! [X0,X1,X2] :
( geographicalsubregions(X0,X2)
| ~ geographicalsubregions(X0,X1)
| ~ geographicalsubregions(X1,X2) ),
inference(ennf_transformation,[],[f538325]) ).
fof(f540513,plain,
! [X0,X1,X2] :
( geographicalsubregions(X0,X2)
| ~ geographicalsubregions(X0,X1)
| ~ geographicalsubregions(X1,X2) ),
inference(flattening,[],[f540512]) ).
fof(f540516,plain,
( geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(ennf_transformation,[],[f300164]) ).
fof(f540532,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f540175]) ).
fof(f540533,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f540532]) ).
fof(f540534,plain,
( geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(ennf_transformation,[],[f81149]) ).
fof(f540765,plain,
mtvisible(c_tptpgeo_spindlecollectormt),
inference(cnf_transformation,[],[f540459]) ).
fof(f540766,plain,
( ~ inregion(c_geolocation_x76_y23,c_georegion_l1_x2_y0)
| ~ geolevel_1(c_georegion_l1_x2_y0) ),
inference(cnf_transformation,[],[f540459]) ).
fof(f540773,plain,
( geolevel_1(c_georegion_l1_x2_y0)
| ~ mtvisible(c_worldgeographymt) ),
inference(cnf_transformation,[],[f540466]) ).
fof(f540782,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(cnf_transformation,[],[f540474]) ).
fof(f540791,plain,
! [X2,X0,X1] :
( inregion(X0,X2)
| ~ inregion(X0,X1)
| ~ inregion(X1,X2) ),
inference(cnf_transformation,[],[f540484]) ).
fof(f540793,plain,
! [X0,X1] :
( inregion(X1,X0)
| ~ geographicalsubregions(X0,X1) ),
inference(cnf_transformation,[],[f540486]) ).
fof(f540800,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member4_mt),
inference(cnf_transformation,[],[f121419]) ).
fof(f540806,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member2_mt),
inference(cnf_transformation,[],[f36571]) ).
fof(f540808,plain,
( inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(cnf_transformation,[],[f540487]) ).
fof(f540838,plain,
! [X2,X0,X1] :
( geographicalsubregions(X0,X2)
| ~ geographicalsubregions(X0,X1)
| ~ geographicalsubregions(X1,X2) ),
inference(cnf_transformation,[],[f540513]) ).
fof(f540841,plain,
( geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(cnf_transformation,[],[f540516]) ).
fof(f540857,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(cnf_transformation,[],[f540533]) ).
fof(f540875,plain,
( geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23)
| ~ mtvisible(c_tptpgeo_member2_mt) ),
inference(cnf_transformation,[],[f540534]) ).
fof(f540932,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(cnf_transformation,[],[f28207]) ).
fof(f540934,plain,
genlmt(c_tptpgeo_member4_mt,c_tptpgeo_spindleheadmt),
inference(cnf_transformation,[],[f6757]) ).
fof(f541362,plain,
! [X0] :
( ~ genlmt(c_tptpgeo_spindlecollectormt,X0)
| mtvisible(X0) ),
inference(resolution,[],[f540765,f540857]) ).
fof(f541367,plain,
mtvisible(c_tptpgeo_member4_mt),
inference(resolution,[],[f541362,f540800]) ).
fof(f541368,plain,
mtvisible(c_tptpgeo_member2_mt),
inference(resolution,[],[f541362,f540806]) ).
fof(f541384,plain,
! [X0] :
( ~ genlmt(c_tptpgeo_member4_mt,X0)
| mtvisible(X0) ),
inference(resolution,[],[f541367,f540857]) ).
fof(f541386,plain,
geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l2_x8_y2),
inference(resolution,[],[f541368,f540782]) ).
fof(f541395,plain,
inregion(c_geolocation_x76_y23,c_georegion_l4_x76_y23),
inference(resolution,[],[f541368,f540808]) ).
fof(f541399,plain,
geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7),
inference(resolution,[],[f541368,f540841]) ).
fof(f541413,plain,
geographicalsubregions(c_georegion_l3_x25_y7,c_georegion_l4_x76_y23),
inference(resolution,[],[f541368,f540875]) ).
fof(f541539,plain,
! [X0] :
( geographicalsubregions(c_georegion_l1_x2_y0,X0)
| ~ geographicalsubregions(c_georegion_l2_x8_y2,X0) ),
inference(resolution,[],[f541386,f540838]) ).
fof(f541632,plain,
! [X0] :
( inregion(c_geolocation_x76_y23,X0)
| ~ inregion(c_georegion_l4_x76_y23,X0) ),
inference(resolution,[],[f541395,f540791]) ).
fof(f541798,plain,
! [X0] :
( ~ geographicalsubregions(X0,c_georegion_l3_x25_y7)
| geographicalsubregions(X0,c_georegion_l4_x76_y23) ),
inference(resolution,[],[f541413,f540838]) ).
fof(f542414,plain,
mtvisible(c_tptpgeo_spindleheadmt),
inference(resolution,[],[f541384,f540934]) ).
fof(f542420,plain,
! [X0] :
( ~ genlmt(c_tptpgeo_spindleheadmt,X0)
| mtvisible(X0) ),
inference(resolution,[],[f542414,f540857]) ).
fof(f544038,plain,
( ~ inregion(c_georegion_l4_x76_y23,c_georegion_l1_x2_y0)
| ~ geolevel_1(c_georegion_l1_x2_y0) ),
inference(resolution,[],[f541632,f540766]) ).
fof(f545274,plain,
( geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l4_x76_y23)
| ~ geographicalsubregions(c_georegion_l2_x8_y2,c_georegion_l3_x25_y7) ),
inference(resolution,[],[f541798,f541539]) ).
fof(f545279,plain,
geographicalsubregions(c_georegion_l1_x2_y0,c_georegion_l4_x76_y23),
inference(forward_subsumption_resolution,[],[f545274,f541399]) ).
fof(f545284,plain,
inregion(c_georegion_l4_x76_y23,c_georegion_l1_x2_y0),
inference(resolution,[],[f545279,f540793]) ).
fof(f546095,plain,
mtvisible(c_worldgeographymt),
inference(resolution,[],[f542420,f540932]) ).
fof(f546103,plain,
geolevel_1(c_georegion_l1_x2_y0),
inference(resolution,[],[f546095,f540773]) ).
fof(f547397,plain,
~ geolevel_1(c_georegion_l1_x2_y0),
inference(forward_subsumption_resolution,[],[f544038,f545284]) ).
fof(f547398,plain,
$false,
inference(forward_subsumption_resolution,[],[f547397,f546103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR033+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 22:11:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.13 Running first-order theorem proving
% 0.09/0.13 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.40/7.69 % (3845014)Detected formulas, will run a generic FOF schedule.
% 18.40/7.69 % (3845211)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=118373984:i=141193_2946 on theBenchmark for (2946ds/141193Mi)
% 18.40/7.69 % (3845212)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3153587034:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2946 on theBenchmark for (2946ds/134677Mi)
% 18.40/7.69 % (3845213)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2415160194:i=141695:sd=1:nm=32:gsp=on:ss=included_2946 on theBenchmark for (2946ds/141695Mi)
% 18.40/7.69 % (3845214)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1361115443:i=109:sd=1:ins=1:gsp=on:ss=axioms_2946 on theBenchmark for (2946ds/109Mi)
% 18.40/7.69 % (3845215)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3837054117:i=119:av=off:ss=axioms_2946 on theBenchmark for (2946ds/119Mi)
% 18.40/7.69 % (3845216)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1948514506:s2a=on:i=139:gtg=position_2946 on theBenchmark for (2946ds/139Mi)
% 18.40/7.69 % (3845217)dis-21_1_sil=8000:lcm=predicate:random_seed=2846644147:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2946 on theBenchmark for (2946ds/129Mi)
% 18.40/7.69 % (3845214)Instruction limit reached!
% 18.40/7.69 % (3845214)------------------------------
% 18.40/7.69 % (3845214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/7.69 % (3845214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/7.69 % (3845214)CaDiCaL version: 2.1.3
% 18.40/7.69 % (3845214)Termination reason: Instruction limit
% 18.40/7.69 % (3845214)Termination phase: SInE selection
% 18.40/7.69 % (3845214)Time elapsed: 0.053 s
% 18.40/7.69 % (3845214)Peak memory usage: 462 MB
% 18.40/7.69 % (3845214)Instructions burned: 109 (million)
% 18.40/7.69 % (3845215)Instruction limit reached!
% 18.40/7.69 % (3845215)------------------------------
% 18.40/7.69 % (3845215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/7.69 % (3845215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/7.69 % (3845215)CaDiCaL version: 2.1.3
% 18.40/7.69 % (3845215)Termination reason: Instruction limit
% 18.40/7.69 % (3845215)Termination phase: SInE selection
% 18.40/7.69 % (3845215)Time elapsed: 0.055 s
% 18.40/7.69 % (3845215)Peak memory usage: 462 MB
% 18.40/7.69 % (3845215)Instructions burned: 120 (million)
% 18.40/7.69 % (3845217)Instruction limit reached!
% 18.40/7.69 % (3845217)------------------------------
% 18.40/7.69 % (3845217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/7.69 % (3845217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/7.69 % (3845217)CaDiCaL version: 2.1.3
% 18.40/7.69 % (3845217)Termination reason: Instruction limit
% 18.40/7.69 % (3845217)Termination phase: SInE selection
% 18.40/7.69 % (3845217)Time elapsed: 0.066 s
% 18.40/7.69 % (3845217)Peak memory usage: 462 MB
% 18.40/7.69 % (3845217)Instructions burned: 131 (million)
% 18.40/7.69 % (3845216)Instruction limit reached!
% 18.40/7.69 % (3845216)------------------------------
% 18.40/7.69 % (3845216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.40/7.69 % (3845216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.40/7.69 % (3845216)CaDiCaL version: 2.1.3
% 18.40/7.69 % (3845216)Termination reason: Instruction limit
% 18.40/7.69 % (3845216)Termination phase: Property scanning
% 18.40/7.69 % (3845216)Time elapsed: 0.118 s
% 18.40/7.69 % (3845216)Peak memory usage: 463 MB
% 18.40/7.69 % (3845216)Instructions burned: 142 (million)
% 18.40/7.69 % (3845225)lrs+10_1_sil=8000:sp=occurrence:random_seed=2809074571:i=285:sd=3:ss=axioms:sgt=8_2944 on theBenchmark for (2944ds/285Mi)
% 18.40/7.69 % (3845226)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3799845158:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2944 on theBenchmark for (2944ds/157Mi)
% 18.40/7.69 % (3845227)lrs+1011_1_sil=32000:sp=occurrence:random_seed=120360203:i=325:sd=1:ss=axioms:sgt=32_2943 on theBenchmark for (2943ds/325Mi)
% 18.40/7.69 % (3845228)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3798002032:s2a=on:i=248:s2at=1.23:gtg=position_2943 on theBenchmark for (2943ds/248Mi)
% 18.40/7.69 % (3845226)Instruction limit reached!
% 25.18/8.66 % (3845226)------------------------------
% 25.18/8.66 % (3845226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845226)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845226)Termination reason: Instruction limit
% 25.18/8.66 % (3845226)Termination phase: Property scanning
% 25.18/8.66 % (3845226)Time elapsed: 0.121 s
% 25.18/8.66 % (3845226)Peak memory usage: 463 MB
% 25.18/8.66 % (3845226)Instructions burned: 160 (million)
% 25.18/8.66 % (3845225)Instruction limit reached!
% 25.18/8.66 % (3845225)------------------------------
% 25.18/8.66 % (3845225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845225)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845225)Termination reason: Instruction limit
% 25.18/8.66 % (3845225)Termination phase: SInE selection
% 25.18/8.66 % (3845225)Time elapsed: 0.147 s
% 25.18/8.66 % (3845225)Peak memory usage: 462 MB
% 25.18/8.66 % (3845225)Instructions burned: 286 (million)
% 25.18/8.66 % (3845227)Instruction limit reached!
% 25.18/8.66 % (3845227)------------------------------
% 25.18/8.66 % (3845227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845227)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845227)Termination reason: Instruction limit
% 25.18/8.66 % (3845227)Termination phase: SInE selection
% 25.18/8.66 % (3845227)Time elapsed: 0.167 s
% 25.18/8.66 % (3845227)Peak memory usage: 462 MB
% 25.18/8.66 % (3845227)Instructions burned: 325 (million)
% 25.18/8.66 % (3845228)Instruction limit reached!
% 25.18/8.66 % (3845228)------------------------------
% 25.18/8.66 % (3845228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845228)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845228)Termination reason: Instruction limit
% 25.18/8.66 % (3845228)Termination phase: Property scanning
% 25.18/8.66 % (3845228)Time elapsed: 0.151 s
% 25.18/8.66 % (3845228)Peak memory usage: 463 MB
% 25.18/8.66 % (3845228)Instructions burned: 249 (million)
% 25.18/8.66 % (3845233)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1211039743:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2941 on theBenchmark for (2941ds/294Mi)
% 25.18/8.66 % (3845234)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=663733631:i=2350_2941 on theBenchmark for (2941ds/2350Mi)
% 25.18/8.66 % (3845235)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1998965988:cts=off:i=113:fsr=off:ss=included:sgt=4_2940 on theBenchmark for (2940ds/113Mi)
% 25.18/8.66 % (3845235)Instruction limit reached!
% 25.18/8.66 % (3845235)------------------------------
% 25.18/8.66 % (3845235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845235)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845235)Termination reason: Instruction limit
% 25.18/8.66 % (3845235)Termination phase: SInE selection
% 25.18/8.66 % (3845235)Time elapsed: 0.052 s
% 25.18/8.66 % (3845235)Peak memory usage: 462 MB
% 25.18/8.66 % (3845235)Instructions burned: 114 (million)
% 25.18/8.66 % (3845237)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3755844302:i=127:av=off:fsr=off:sup=off_2940 on theBenchmark for (2940ds/127Mi)
% 25.18/8.66 % (3845233)Instruction limit reached!
% 25.18/8.66 % (3845233)------------------------------
% 25.18/8.66 % (3845233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845233)CaDiCaL version: 2.1.3
% 25.18/8.66 % (3845233)Termination reason: Instruction limit
% 25.18/8.66 % (3845233)Termination phase: SInE selection
% 25.18/8.66 % (3845233)Time elapsed: 0.154 s
% 25.18/8.66 % (3845233)Peak memory usage: 462 MB
% 25.18/8.66 % (3845233)Instructions burned: 295 (million)
% 25.18/8.66 % (3845237)Instruction limit reached!
% 25.18/8.66 % (3845237)------------------------------
% 25.18/8.66 % (3845237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.18/8.66 % (3845237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.18/8.66 % (3845237)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845237)Termination reason: Instruction limit
% 22.22/11.97 % (3845237)Termination phase: Preprocessing 1
% 22.22/11.97 % (3845237)Time elapsed: 0.065 s
% 22.22/11.97 % (3845237)Peak memory usage: 463 MB
% 22.22/11.97 % (3845237)Instructions burned: 129 (million)
% 22.22/11.97 % (3845241)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1665432526:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2938 on theBenchmark for (2938ds/114Mi)
% 22.22/11.97 % (3845242)lrs+10_1_sil=8000:sp=occurrence:random_seed=3847408433:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2938 on theBenchmark for (2938ds/907Mi)
% 22.22/11.97 % (3845243)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=172362513:i=437:sd=1:aac=none:ss=included_2937 on theBenchmark for (2937ds/437Mi)
% 22.22/11.97 % (3845241)Instruction limit reached!
% 22.22/11.97 % (3845241)------------------------------
% 22.22/11.97 % (3845241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845241)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845241)Termination reason: Instruction limit
% 22.22/11.97 % (3845241)Termination phase: Property scanning
% 22.22/11.97 % (3845241)Time elapsed: 0.111 s
% 22.22/11.97 % (3845241)Peak memory usage: 463 MB
% 22.22/11.97 % (3845241)Instructions burned: 118 (million)
% 22.22/11.97 % (3845247)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3606535365:i=5202:ss=axioms:sgt=16_2936 on theBenchmark for (2936ds/5202Mi)
% 22.22/11.97 % (3845243)Instruction limit reached!
% 22.22/11.97 % (3845243)------------------------------
% 22.22/11.97 % (3845243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845243)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845243)Termination reason: Instruction limit
% 22.22/11.97 % (3845243)Termination phase: SInE selection
% 22.22/11.97 % (3845243)Time elapsed: 0.220 s
% 22.22/11.97 % (3845243)Peak memory usage: 462 MB
% 22.22/11.97 % (3845243)Instructions burned: 438 (million)
% 22.22/11.97 % (3845249)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2487450496:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2934 on theBenchmark for (2934ds/134Mi)
% 22.22/11.97 % (3845242)Instruction limit reached!
% 22.22/11.97 % (3845242)------------------------------
% 22.22/11.97 % (3845242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845242)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845242)Termination reason: Instruction limit
% 22.22/11.97 % (3845242)Termination phase: SInE selection
% 22.22/11.97 % (3845242)Time elapsed: 0.466 s
% 22.22/11.97 % (3845242)Peak memory usage: 474 MB
% 22.22/11.97 % (3845242)Instructions burned: 907 (million)
% 22.22/11.97 % (3845249)Instruction limit reached!
% 22.22/11.97 % (3845249)------------------------------
% 22.22/11.97 % (3845249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845249)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845249)Termination reason: Instruction limit
% 22.22/11.97 % (3845249)Termination phase: SInE selection
% 22.22/11.97 % (3845249)Time elapsed: 0.067 s
% 22.22/11.97 % (3845249)Peak memory usage: 463 MB
% 22.22/11.97 % (3845249)Instructions burned: 134 (million)
% 22.22/11.97 % (3845251)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4101831160:st=8:i=592:sd=3:ep=RST:ss=axioms_2932 on theBenchmark for (2932ds/592Mi)
% 22.22/11.97 % (3845252)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3626376594:st=3:i=13193:sd=3:ss=axioms_2931 on theBenchmark for (2931ds/13193Mi)
% 22.22/11.97 % (3845251)Instruction limit reached!
% 22.22/11.97 % (3845251)------------------------------
% 22.22/11.97 % (3845251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845251)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845251)Termination reason: Instruction limit
% 22.22/11.97 % (3845251)Termination phase: SInE selection
% 22.22/11.97 % (3845251)Time elapsed: 0.316 s
% 22.22/11.97 % (3845251)Peak memory usage: 469 MB
% 22.22/11.97 % (3845251)Instructions burned: 594 (million)
% 22.22/11.97 % (3845234)Instruction limit reached!
% 22.22/11.97 % (3845234)------------------------------
% 22.22/11.97 % (3845234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845234)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845234)Termination reason: Instruction limit
% 22.22/11.97 % (3845234)Termination phase: Unused predicate definition removal
% 22.22/11.97 % (3845234)Time elapsed: 1.342 s
% 22.22/11.97 % (3845234)Peak memory usage: 555 MB
% 22.22/11.97 % (3845234)Instructions burned: 2350 (million)
% 22.22/11.97 % (3845255)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=272004378:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2927 on theBenchmark for (2927ds/125Mi)
% 22.22/11.97 % (3845255)Instruction limit reached!
% 22.22/11.97 % (3845255)------------------------------
% 22.22/11.97 % (3845255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845255)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845255)Termination reason: Instruction limit
% 22.22/11.97 % (3845255)Termination phase: Property scanning
% 22.22/11.97 % (3845255)Time elapsed: 0.115 s
% 22.22/11.97 % (3845255)Peak memory usage: 463 MB
% 22.22/11.97 % (3845255)Instructions burned: 126 (million)
% 22.22/11.97 % (3845256)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1569232822:i=134:gtgl=5:slsql=off:gtg=exists_sym_2926 on theBenchmark for (2926ds/134Mi)
% 22.22/11.97 % (3845256)Instruction limit reached!
% 22.22/11.97 % (3845256)------------------------------
% 22.22/11.97 % (3845256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845256)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845256)Termination reason: Instruction limit
% 22.22/11.97 % (3845256)Termination phase: Property scanning
% 22.22/11.97 % (3845256)Time elapsed: 0.118 s
% 22.22/11.97 % (3845256)Peak memory usage: 463 MB
% 22.22/11.97 % (3845256)Instructions burned: 137 (million)
% 22.22/11.97 % (3845259)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1920390545:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2924 on theBenchmark for (2924ds/141Mi)
% 22.22/11.97 % (3845259)Instruction limit reached!
% 22.22/11.97 % (3845259)------------------------------
% 22.22/11.97 % (3845259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845259)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845259)Termination reason: Instruction limit
% 22.22/11.97 % (3845259)Termination phase: SInE selection
% 22.22/11.97 % (3845259)Time elapsed: 0.069 s
% 22.22/11.97 % (3845259)Peak memory usage: 462 MB
% 22.22/11.97 % (3845259)Instructions burned: 141 (million)
% 22.22/11.97 % (3845260)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=746283304:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2923 on theBenchmark for (2923ds/431Mi)
% 22.22/11.97 % (3845262)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4056272325:i=6060:aac=none:ins=25_2922 on theBenchmark for (2922ds/6060Mi)
% 22.22/11.97 % (3845260)Instruction limit reached!
% 22.22/11.97 % (3845260)------------------------------
% 22.22/11.97 % (3845260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845260)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845260)Termination reason: Instruction limit
% 22.22/11.97 % (3845260)Termination phase: SInE selection
% 22.22/11.97 % (3845260)Time elapsed: 0.242 s
% 22.22/11.97 % (3845260)Peak memory usage: 462 MB
% 22.22/11.97 % (3845260)Instructions burned: 431 (million)
% 22.22/11.97 % (3845265)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1132538856:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2919 on theBenchmark for (2919ds/150Mi)
% 22.22/11.97 % (3845265)Instruction limit reached!
% 22.22/11.97 % (3845265)------------------------------
% 22.22/11.97 % (3845265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845265)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845265)Termination reason: Instruction limit
% 22.22/11.97 % (3845265)Termination phase: SInE selection
% 22.22/11.97 % (3845265)Time elapsed: 0.079 s
% 22.22/11.97 % (3845265)Peak memory usage: 462 MB
% 22.22/11.97 % (3845265)Instructions burned: 151 (million)
% 22.22/11.97 % (3845267)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2206283844:i=14155:bd=all_2916 on theBenchmark for (2916ds/14155Mi)
% 22.22/11.97 % (3845247)Instruction limit reached!
% 22.22/11.97 % (3845247)------------------------------
% 22.22/11.97 % (3845247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845247)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845247)Termination reason: Instruction limit
% 22.22/11.97 % (3845247)Termination phase: Saturation
% 22.22/11.97 % (3845247)Time elapsed: 2.324 s
% 22.22/11.97 % (3845247)Peak memory usage: 711 MB
% 22.22/11.97 % (3845247)Instructions burned: 5202 (million)
% 22.22/11.97 % (3845269)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1121235139:i=667:av=off:fsr=off_2911 on theBenchmark for (2911ds/667Mi)
% 22.22/11.97 % (3845269)Instruction limit reached!
% 22.22/11.97 % (3845269)------------------------------
% 22.22/11.97 % (3845269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845269)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845269)Termination reason: Instruction limit
% 22.22/11.97 % (3845269)Termination phase: Preprocessing 1
% 22.22/11.97 % (3845269)Time elapsed: 0.343 s
% 22.22/11.97 % (3845269)Peak memory usage: 463 MB
% 22.22/11.97 % (3845269)Instructions burned: 669 (million)
% 22.22/11.97 % (3845271)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2650782923:s2a=on:i=185:s2at=1.8:fdi=4_2905 on theBenchmark for (2905ds/185Mi)
% 22.22/11.97 % (3845271)Instruction limit reached!
% 22.22/11.97 % (3845271)------------------------------
% 22.22/11.97 % (3845271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845271)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845271)Termination reason: Instruction limit
% 22.22/11.97 % (3845271)Termination phase: SInE selection
% 22.22/11.97 % (3845271)Time elapsed: 0.100 s
% 22.22/11.97 % (3845271)Peak memory usage: 462 MB
% 22.22/11.97 % (3845271)Instructions burned: 186 (million)
% 22.22/11.97 % (3845273)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2040866074:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2903 on theBenchmark for (2903ds/193Mi)
% 22.22/11.97 % (3845273)Instruction limit reached!
% 22.22/11.97 % (3845273)------------------------------
% 22.22/11.97 % (3845273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845273)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845273)Termination reason: Instruction limit
% 22.22/11.97 % (3845273)Termination phase: SInE selection
% 22.22/11.97 % (3845273)Time elapsed: 0.102 s
% 22.22/11.97 % (3845273)Peak memory usage: 462 MB
% 22.22/11.97 % (3845273)Instructions burned: 194 (million)
% 22.22/11.97 % (3845275)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3000460219:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2900 on theBenchmark for (2900ds/4850Mi)
% 22.22/11.97 % (3845275)First to succeed.
% 22.22/11.97 % (3845275)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3845014"
% 22.22/11.97 % (3845262)Instruction limit reached!
% 22.22/11.97 % (3845262)------------------------------
% 22.22/11.97 % (3845262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.22/11.97 % (3845262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.22/11.97 % (3845262)CaDiCaL version: 2.1.3
% 22.22/11.97 % (3845262)Termination reason: Instruction limit
% 22.22/11.97 % (3845262)Termination phase: Property scanning
% 22.22/11.97 % (3845262)Time elapsed: 3.302 s
% 22.22/11.97 % (3845262)Peak memory usage: 701 MB
% 22.22/11.97 % (3845262)Instructions burned: 6060 (million)
% 22.22/11.97 % (3845277)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=370503175:i=12111:sd=1:ss=included_2887 on theBenchmark for (2887ds/12111Mi)
% 49.62/12.29 % (3845275)Refutation found. Thanks to Tanya!
% 49.62/12.29 % SZS status Theorem for theBenchmark
% 49.62/12.29 % SZS output start Proof for theBenchmark
% See solution above
% 49.62/12.29 % (3845275)------------------------------
% 49.62/12.29 % (3845275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/12.29 % (3845275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/12.29 % (3845275)CaDiCaL version: 2.1.3
% 49.62/12.29 % (3845275)Termination reason: Refutation
% 49.62/12.29 % (3845275)Time elapsed: 0.959 s
% 49.62/12.29 % (3845275)Peak memory usage: 536 MB
% 49.62/12.29 % (3845275)Instructions burned: 1622 (million)
% 49.62/12.29 % (3845275)------------------------------
% 49.62/12.29 % (3845275)------------------------------
% 49.62/12.29 % (3845014)Success in time 11.63 s
% 49.62/12.29 % Vampire exiting
%------------------------------------------------------------------------------