%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR049+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:19 AM UTC 2026
% Result : Theorem 202.20s 52.50s
% Output : Refutation 297.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 35
% Syntax : Number of formulae : 108 ( 93 unt; 0 def)
% Number of atoms : 135 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 77 ( 50 ~; 18 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 36 ( 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1795,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_1795) ).
fof(f2787,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_2787) ).
fof(f5992,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_5992) ).
fof(f9500,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_9500) ).
fof(f11066,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_11066) ).
fof(f27403,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_27403) ).
fof(f27872,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_27872) ).
fof(f28568,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_28568) ).
fof(f36988,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_36988) ).
fof(f38495,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_38495) ).
fof(f42611,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_42615) ).
fof(f48333,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_48340) ).
fof(f84663,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_84675) ).
fof(f88478,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_88493) ).
fof(f109015,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_109036) ).
fof(f109519,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_109540) ).
fof(f113438,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_113459) ).
fof(f115347,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_115368) ).
fof(f118428,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_118449) ).
fof(f136756,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_136780) ).
fof(f146139,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_146166) ).
fof(f150138,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_150165) ).
fof(f159333,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_159363) ).
fof(f177437,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_177467) ).
fof(f196511,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_196544) ).
fof(f211340,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_211374) ).
fof(f213678,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_213712) ).
fof(f215643,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_215677) ).
fof(f250163,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_250198) ).
fof(f254447,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_254482) ).
fof(f261454,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_261490) ).
fof(f540091,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_540136) ).
fof(f540092,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_540137) ).
fof(f540136,axiom,
! [X0,X1,X2] :
( ( genls(X0,X1)
& genls(X1,X2) )
=> genls(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_540181) ).
fof(f540250,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query249) ).
fof(f540251,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f543629,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(ennf_transformation,[],[f540251]) ).
fof(f543630,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f540092]) ).
fof(f543631,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f543630]) ).
fof(f543632,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f540091]) ).
fof(f543633,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f543632]) ).
fof(f543647,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(ennf_transformation,[],[f540136]) ).
fof(f543648,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X0,X1)
| ~ genls(X1,X2) ),
inference(flattening,[],[f543647]) ).
fof(f549970,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[],[f543629]) ).
fof(f549971,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X2,X1)
| ~ genls(X2,X0) ),
inference(cnf_transformation,[],[f543631]) ).
fof(f549972,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X0,X2)
| ~ genls(X2,X1) ),
inference(cnf_transformation,[],[f543633]) ).
fof(f549983,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[],[f28568]) ).
fof(f549987,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[],[f250163]) ).
fof(f549992,plain,
! [X2,X0,X1] :
( ~ genls(X1,X2)
| ~ genls(X0,X1)
| genls(X0,X2) ),
inference(cnf_transformation,[],[f543648]) ).
fof(f550010,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[],[f254447]) ).
fof(f550016,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[],[f109519]) ).
fof(f550057,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[],[f146139]) ).
fof(f550063,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[],[f215643]) ).
fof(f550197,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[],[f2787]) ).
fof(f550204,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[],[f213678]) ).
fof(f550643,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[],[f113438]) ).
fof(f550650,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[],[f136756]) ).
fof(f551509,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[],[f5992]) ).
fof(f551518,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[],[f27872]) ).
fof(f552650,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[],[f36988]) ).
fof(f552658,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[],[f88478]) ).
fof(f553947,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[],[f84663]) ).
fof(f553956,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[],[f159333]) ).
fof(f556131,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[],[f118428]) ).
fof(f556145,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[],[f9500]) ).
fof(f558826,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[],[f109015]) ).
fof(f558837,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[],[f211340]) ).
fof(f560065,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[],[f115347]) ).
fof(f560072,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[],[f42611]) ).
fof(f560853,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[],[f38495]) ).
fof(f560854,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f1795]) ).
fof(f561247,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[],[f177437]) ).
fof(f562011,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f150138]) ).
fof(f562509,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[],[f48333]) ).
fof(f563254,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f196511]) ).
fof(f563759,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f27403]) ).
fof(f564554,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f11066]) ).
fof(f564963,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f261454]) ).
fof(f564973,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(unit_resulting_resolution,[],[f549972,f549983,f549970]) ).
fof(f564983,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_14_92264),
inference(unit_resulting_resolution,[],[f549972,f550010,f564973]) ).
fof(f565038,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_13_92263),
inference(unit_resulting_resolution,[],[f549972,f550057,f564983]) ).
fof(f565107,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_12_92262),
inference(unit_resulting_resolution,[],[f549972,f550197,f565038]) ).
fof(f565152,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_11_92230),
inference(unit_resulting_resolution,[],[f549972,f550643,f565107]) ).
fof(f565179,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_10_92166),
inference(unit_resulting_resolution,[],[f549972,f551509,f565152]) ).
fof(f565277,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_9_92165),
inference(unit_resulting_resolution,[],[f549972,f552650,f565179]) ).
fof(f565365,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f549972,f553947,f565277]) ).
fof(f565430,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_7_92163),
inference(unit_resulting_resolution,[],[f549972,f556131,f565365]) ).
fof(f565486,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_6_92162),
inference(unit_resulting_resolution,[],[f549972,f558826,f565430]) ).
fof(f565547,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_5_90114),
inference(unit_resulting_resolution,[],[f549972,f560065,f565486]) ).
fof(f565604,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_4_90113),
inference(unit_resulting_resolution,[],[f549972,f561247,f565547]) ).
fof(f565665,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_3_81921),
inference(unit_resulting_resolution,[],[f549972,f562509,f565604]) ).
fof(f565691,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_2_65537),
inference(unit_resulting_resolution,[],[f549972,f563759,f565665]) ).
fof(f565719,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536),
inference(unit_resulting_resolution,[],[f549972,f564963,f565691]) ).
fof(f565754,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_1_1),
inference(unit_resulting_resolution,[],[f549971,f564554,f565719]) ).
fof(f565778,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_2_2),
inference(unit_resulting_resolution,[],[f549992,f563254,f565754]) ).
fof(f565820,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_3_16386),
inference(unit_resulting_resolution,[],[f549992,f562011,f565778]) ).
fof(f565872,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_4_24578),
inference(unit_resulting_resolution,[],[f549992,f560854,f565820]) ).
fof(f566005,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_5_24579),
inference(unit_resulting_resolution,[],[f549992,f560853,f565872]) ).
fof(f566270,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_6_26627),
inference(unit_resulting_resolution,[],[f549992,f560072,f566005]) ).
fof(f566580,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_7_26628),
inference(unit_resulting_resolution,[],[f549992,f558837,f566270]) ).
fof(f566873,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_8_26629),
inference(unit_resulting_resolution,[],[f549992,f556145,f566580]) ).
fof(f567084,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_9_26885),
inference(unit_resulting_resolution,[],[f549992,f553956,f566873]) ).
fof(f567171,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_10_26886),
inference(unit_resulting_resolution,[],[f549992,f552658,f567084]) ).
fof(f567319,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_11_26887),
inference(unit_resulting_resolution,[],[f549992,f551518,f567171]) ).
fof(f567368,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_12_26919),
inference(unit_resulting_resolution,[],[f549992,f550650,f567319]) ).
fof(f567446,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_13_26920),
inference(unit_resulting_resolution,[],[f549992,f550204,f567368]) ).
fof(f567513,plain,
~ genls(c_tptpcol_16_26926,c_tptpcol_14_26921),
inference(unit_resulting_resolution,[],[f549992,f550063,f567446]) ).
fof(f567707,plain,
$false,
inference(unit_resulting_resolution,[],[f549992,f550016,f549987,f567513]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n010.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:18:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.95/14.42 % (2424071)Detected formulas, will run a generic FOF schedule.
% 26.95/14.42 % (2424374)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=3958504075:i=141193_2884 on theBenchmark for (2884ds/141193Mi)
% 26.95/14.42 % (2424375)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=4105694127:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2884 on theBenchmark for (2884ds/134677Mi)
% 26.95/14.42 % (2424378)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2203769460:i=119:av=off:ss=axioms_2884 on theBenchmark for (2884ds/119Mi)
% 26.95/14.42 % (2424377)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=817411462:i=109:sd=1:ins=1:gsp=on:ss=axioms_2884 on theBenchmark for (2884ds/109Mi)
% 26.95/14.42 % (2424376)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=4095524366:i=141695:sd=1:nm=32:gsp=on:ss=included_2884 on theBenchmark for (2884ds/141695Mi)
% 26.95/14.42 % (2424379)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1528414536:s2a=on:i=139:gtg=position_2884 on theBenchmark for (2884ds/139Mi)
% 26.95/14.42 % (2424378)Instruction limit reached!
% 26.95/14.42 % (2424378)------------------------------
% 26.95/14.42 % (2424378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.95/14.42 % (2424378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.95/14.42 % (2424378)CaDiCaL version: 2.1.3
% 26.95/14.42 % (2424378)Termination reason: Instruction limit
% 26.95/14.42 % (2424378)Termination phase: SInE selection
% 26.95/14.42 % (2424378)Time elapsed: 0.057 s
% 26.95/14.42 % (2424378)Peak memory usage: 462 MB
% 26.95/14.42 % (2424378)Instructions burned: 121 (million)
% 26.95/14.42 % (2424380)dis-21_1_sil=8000:lcm=predicate:random_seed=853932663:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2884 on theBenchmark for (2884ds/129Mi)
% 26.95/14.42 % (2424377)Instruction limit reached!
% 26.95/14.42 % (2424377)------------------------------
% 26.95/14.42 % (2424377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.95/14.42 % (2424377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.95/14.42 % (2424377)CaDiCaL version: 2.1.3
% 26.95/14.42 % (2424377)Termination reason: Instruction limit
% 26.95/14.42 % (2424377)Termination phase: SInE selection
% 26.95/14.42 % (2424377)Time elapsed: 0.085 s
% 26.95/14.42 % (2424377)Peak memory usage: 462 MB
% 26.95/14.42 % (2424377)Instructions burned: 109 (million)
% 26.95/14.42 % (2424380)Instruction limit reached!
% 26.95/14.42 % (2424380)------------------------------
% 26.95/14.42 % (2424380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.95/14.42 % (2424380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.95/14.42 % (2424380)CaDiCaL version: 2.1.3
% 26.95/14.42 % (2424380)Termination reason: Instruction limit
% 26.95/14.42 % (2424380)Termination phase: SInE selection
% 26.95/14.42 % (2424380)Time elapsed: 0.106 s
% 26.95/14.42 % (2424380)Peak memory usage: 462 MB
% 26.95/14.42 % (2424380)Instructions burned: 130 (million)
% 26.95/14.42 % (2424379)Instruction limit reached!
% 26.95/14.42 % (2424379)------------------------------
% 26.95/14.42 % (2424379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.95/14.42 % (2424379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.95/14.42 % (2424379)CaDiCaL version: 2.1.3
% 26.95/14.42 % (2424379)Termination reason: Instruction limit
% 26.95/14.42 % (2424379)Termination phase: Property scanning
% 26.95/14.42 % (2424379)Time elapsed: 0.128 s
% 26.95/14.42 % (2424379)Peak memory usage: 463 MB
% 26.95/14.42 % (2424379)Instructions burned: 141 (million)
% 26.95/14.42 % (2424388)lrs+10_1_sil=8000:sp=occurrence:random_seed=475134667:i=285:sd=3:ss=axioms:sgt=8_2881 on theBenchmark for (2881ds/285Mi)
% 26.95/14.42 % (2424389)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1614019404:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2881 on theBenchmark for (2881ds/157Mi)
% 26.95/14.42 % (2424390)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2967250420:i=325:sd=1:ss=axioms:sgt=32_2880 on theBenchmark for (2880ds/325Mi)
% 26.95/14.42 % (2424391)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=2042263431:s2a=on:i=248:s2at=1.23:gtg=position_2880 on theBenchmark for (2880ds/248Mi)
% 26.95/14.42 % (2424389)Instruction limit reached!
% 34.56/15.59 % (2424389)------------------------------
% 34.56/15.59 % (2424389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424389)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424389)Termination reason: Instruction limit
% 34.56/15.59 % (2424389)Termination phase: Property scanning
% 34.56/15.59 % (2424389)Time elapsed: 0.195 s
% 34.56/15.59 % (2424389)Peak memory usage: 463 MB
% 34.56/15.59 % (2424389)Instructions burned: 157 (million)
% 34.56/15.59 % (2424388)Instruction limit reached!
% 34.56/15.59 % (2424388)------------------------------
% 34.56/15.59 % (2424388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424388)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424388)Termination reason: Instruction limit
% 34.56/15.59 % (2424388)Termination phase: SInE selection
% 34.56/15.59 % (2424388)Time elapsed: 0.242 s
% 34.56/15.59 % (2424388)Peak memory usage: 462 MB
% 34.56/15.59 % (2424388)Instructions burned: 285 (million)
% 34.56/15.59 % (2424390)Instruction limit reached!
% 34.56/15.59 % (2424390)------------------------------
% 34.56/15.59 % (2424390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424390)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424390)Termination reason: Instruction limit
% 34.56/15.59 % (2424390)Termination phase: SInE selection
% 34.56/15.59 % (2424390)Time elapsed: 0.173 s
% 34.56/15.59 % (2424390)Peak memory usage: 462 MB
% 34.56/15.59 % (2424390)Instructions burned: 326 (million)
% 34.56/15.59 % (2424391)Instruction limit reached!
% 34.56/15.59 % (2424391)------------------------------
% 34.56/15.59 % (2424391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424391)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424391)Termination reason: Instruction limit
% 34.56/15.59 % (2424391)Termination phase: Property scanning
% 34.56/15.59 % (2424391)Time elapsed: 0.239 s
% 34.56/15.59 % (2424391)Peak memory usage: 463 MB
% 34.56/15.59 % (2424391)Instructions burned: 250 (million)
% 34.56/15.59 % (2424397)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1238155707:i=2350_2877 on theBenchmark for (2877ds/2350Mi)
% 34.56/15.59 % (2424396)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=648730176:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2877 on theBenchmark for (2877ds/294Mi)
% 34.56/15.59 % (2424398)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3378779868:cts=off:i=113:fsr=off:ss=included:sgt=4_2877 on theBenchmark for (2877ds/113Mi)
% 34.56/15.59 % (2424398)Instruction limit reached!
% 34.56/15.59 % (2424398)------------------------------
% 34.56/15.59 % (2424398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424398)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424398)Termination reason: Instruction limit
% 34.56/15.59 % (2424398)Termination phase: SInE selection
% 34.56/15.59 % (2424398)Time elapsed: 0.087 s
% 34.56/15.59 % (2424398)Peak memory usage: 462 MB
% 34.56/15.59 % (2424398)Instructions burned: 114 (million)
% 34.56/15.59 % (2424400)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2221775243:i=127:av=off:fsr=off:sup=off_2876 on theBenchmark for (2876ds/127Mi)
% 34.56/15.59 % (2424396)Instruction limit reached!
% 34.56/15.59 % (2424396)------------------------------
% 34.56/15.59 % (2424396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424396)CaDiCaL version: 2.1.3
% 34.56/15.59 % (2424396)Termination reason: Instruction limit
% 34.56/15.59 % (2424396)Termination phase: SInE selection
% 34.56/15.59 % (2424396)Time elapsed: 0.250 s
% 34.56/15.59 % (2424396)Peak memory usage: 462 MB
% 34.56/15.59 % (2424396)Instructions burned: 295 (million)
% 34.56/15.59 % (2424400)Instruction limit reached!
% 34.56/15.59 % (2424400)------------------------------
% 34.56/15.59 % (2424400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.56/15.59 % (2424400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.56/15.59 % (2424400)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424400)Termination reason: Instruction limit
% 90.49/23.34 % (2424400)Termination phase: Preprocessing 1
% 90.49/23.34 % (2424400)Time elapsed: 0.109 s
% 90.49/23.34 % (2424400)Peak memory usage: 463 MB
% 90.49/23.34 % (2424400)Instructions burned: 127 (million)
% 90.49/23.34 % (2424403)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2251434737:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2874 on theBenchmark for (2874ds/114Mi)
% 90.49/23.34 % (2424405)lrs+10_1_sil=8000:sp=occurrence:random_seed=1362494365:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2873 on theBenchmark for (2873ds/907Mi)
% 90.49/23.34 % (2424406)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2368971745:i=437:sd=1:aac=none:ss=included_2873 on theBenchmark for (2873ds/437Mi)
% 90.49/23.34 % (2424403)Instruction limit reached!
% 90.49/23.34 % (2424403)------------------------------
% 90.49/23.34 % (2424403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.49/23.34 % (2424403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.49/23.34 % (2424403)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424403)Termination reason: Instruction limit
% 90.49/23.34 % (2424403)Termination phase: Property scanning
% 90.49/23.34 % (2424403)Time elapsed: 0.180 s
% 90.49/23.34 % (2424403)Peak memory usage: 463 MB
% 90.49/23.34 % (2424403)Instructions burned: 116 (million)
% 90.49/23.34 % (2424410)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2186849788:i=5202:ss=axioms:sgt=16_2870 on theBenchmark for (2870ds/5202Mi)
% 90.49/23.34 % (2424406)Instruction limit reached!
% 90.49/23.34 % (2424406)------------------------------
% 90.49/23.34 % (2424406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.49/23.34 % (2424406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.49/23.34 % (2424406)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424406)Termination reason: Instruction limit
% 90.49/23.34 % (2424406)Termination phase: SInE selection
% 90.49/23.34 % (2424406)Time elapsed: 0.348 s
% 90.49/23.34 % (2424406)Peak memory usage: 462 MB
% 90.49/23.34 % (2424406)Instructions burned: 438 (million)
% 90.49/23.34 % (2424412)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4273162234:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2867 on theBenchmark for (2867ds/134Mi)
% 90.49/23.34 % (2424412)Instruction limit reached!
% 90.49/23.34 % (2424412)------------------------------
% 90.49/23.34 % (2424412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.49/23.34 % (2424412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.49/23.34 % (2424412)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424412)Termination reason: Instruction limit
% 90.49/23.34 % (2424412)Termination phase: SInE selection
% 90.49/23.34 % (2424412)Time elapsed: 0.106 s
% 90.49/23.34 % (2424412)Peak memory usage: 463 MB
% 90.49/23.34 % (2424412)Instructions burned: 135 (million)
% 90.49/23.34 % (2424405)Instruction limit reached!
% 90.49/23.34 % (2424405)------------------------------
% 90.49/23.34 % (2424405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.49/23.34 % (2424405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.49/23.34 % (2424405)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424405)Termination reason: Instruction limit
% 90.49/23.34 % (2424405)Termination phase: SInE selection
% 90.49/23.34 % (2424405)Time elapsed: 0.737 s
% 90.49/23.34 % (2424405)Peak memory usage: 475 MB
% 90.49/23.34 % (2424405)Instructions burned: 908 (million)
% 90.49/23.34 % (2424397)Instruction limit reached!
% 90.49/23.34 % (2424397)------------------------------
% 90.49/23.34 % (2424397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.49/23.34 % (2424397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.49/23.34 % (2424397)CaDiCaL version: 2.1.3
% 90.49/23.34 % (2424397)Termination reason: Instruction limit
% 90.49/23.34 % (2424397)Termination phase: Unused predicate definition removal
% 90.49/23.34 % (2424397)Time elapsed: 1.214 s
% 90.49/23.34 % (2424397)Peak memory usage: 554 MB
% 90.49/23.34 % (2424397)Instructions burned: 2350 (million)
% 90.49/23.34 % (2424470)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1921749149:st=8:i=592:sd=3:ep=RST:ss=axioms_2864 on theBenchmark for (2864ds/592Mi)
% 90.49/23.34 % (2424503)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=511671791:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2863 on theBenchmark for (2863ds/125Mi)
% 90.49/23.34 % (2424491)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1859169897:st=3:i=13193:sd=3:ss=axioms_2864 on theBenchmark for (2864ds/13193Mi)
% 125.27/28.21 % (2424503)Instruction limit reached!
% 125.27/28.21 % (2424503)------------------------------
% 125.27/28.21 % (2424503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424503)CaDiCaL version: 2.1.3
% 125.27/28.21 % (2424503)Termination reason: Instruction limit
% 125.27/28.21 % (2424503)Termination phase: Property scanning
% 125.27/28.21 % (2424503)Time elapsed: 0.109 s
% 125.27/28.21 % (2424503)Peak memory usage: 463 MB
% 125.27/28.21 % (2424503)Instructions burned: 127 (million)
% 125.27/28.21 % (2424558)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=568390111:i=134:gtgl=5:slsql=off:gtg=exists_sym_2861 on theBenchmark for (2861ds/134Mi)
% 125.27/28.21 % (2424470)Instruction limit reached!
% 125.27/28.21 % (2424470)------------------------------
% 125.27/28.21 % (2424470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424470)CaDiCaL version: 2.1.3
% 125.27/28.21 % (2424470)Termination reason: Instruction limit
% 125.27/28.21 % (2424470)Termination phase: SInE selection
% 125.27/28.21 % (2424470)Time elapsed: 0.466 s
% 125.27/28.21 % (2424470)Peak memory usage: 469 MB
% 125.27/28.21 % (2424470)Instructions burned: 592 (million)
% 125.27/28.21 % (2424558)Instruction limit reached!
% 125.27/28.21 % (2424558)------------------------------
% 125.27/28.21 % (2424558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424558)CaDiCaL version: 2.1.3
% 125.27/28.21 % (2424558)Termination reason: Instruction limit
% 125.27/28.21 % (2424558)Termination phase: Property scanning
% 125.27/28.21 % (2424558)Time elapsed: 0.185 s
% 125.27/28.21 % (2424558)Peak memory usage: 463 MB
% 125.27/28.21 % (2424558)Instructions burned: 135 (million)
% 125.27/28.21 % (2424592)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1578252007:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2858 on theBenchmark for (2858ds/141Mi)
% 125.27/28.21 % (2424609)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1580322719:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2858 on theBenchmark for (2858ds/431Mi)
% 125.27/28.21 % (2424592)Instruction limit reached!
% 125.27/28.21 % (2424592)------------------------------
% 125.27/28.21 % (2424592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424592)CaDiCaL version: 2.1.3
% 125.27/28.21 % (2424592)Termination reason: Instruction limit
% 125.27/28.21 % (2424592)Termination phase: SInE selection
% 125.27/28.21 % (2424592)Time elapsed: 0.136 s
% 125.27/28.21 % (2424592)Peak memory usage: 462 MB
% 125.27/28.21 % (2424592)Instructions burned: 142 (million)
% 125.27/28.21 % (2424609)Instruction limit reached!
% 125.27/28.21 % (2424609)------------------------------
% 125.27/28.21 % (2424609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424609)CaDiCaL version: 2.1.3
% 125.27/28.21 % (2424609)Termination reason: Instruction limit
% 125.27/28.21 % (2424609)Termination phase: SInE selection
% 125.27/28.21 % (2424609)Time elapsed: 0.216 s
% 125.27/28.21 % (2424609)Peak memory usage: 463 MB
% 125.27/28.21 % (2424609)Instructions burned: 432 (million)
% 125.27/28.21 % (2424682)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=1112797970:i=6060:aac=none:ins=25_2855 on theBenchmark for (2855ds/6060Mi)
% 125.27/28.21 % (2424695)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=633475109:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2854 on theBenchmark for (2854ds/150Mi)
% 125.27/28.21 % (2424695)Instruction limit reached!
% 125.27/28.21 % (2424695)------------------------------
% 125.27/28.21 % (2424695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.27/28.21 % (2424695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.27/28.21 % (2424695)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424695)Termination reason: Instruction limit
% 171.30/34.71 % (2424695)Termination phase: SInE selection
% 171.30/34.71 % (2424695)Time elapsed: 0.112 s
% 171.30/34.71 % (2424695)Peak memory usage: 463 MB
% 171.30/34.71 % (2424695)Instructions burned: 150 (million)
% 171.30/34.71 % (2424699)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1138671531:i=14155:bd=all_2850 on theBenchmark for (2850ds/14155Mi)
% 171.30/34.71 % (2424410)Instruction limit reached!
% 171.30/34.71 % (2424410)------------------------------
% 171.30/34.71 % (2424410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.30/34.71 % (2424410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.30/34.71 % (2424410)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424410)Termination reason: Instruction limit
% 171.30/34.71 % (2424410)Termination phase: Saturation
% 171.30/34.71 % (2424410)Time elapsed: 4.447 s
% 171.30/34.71 % (2424410)Peak memory usage: 558 MB
% 171.30/34.71 % (2424410)Instructions burned: 5203 (million)
% 171.30/34.71 % (2424872)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2961028217:i=667:av=off:fsr=off_2824 on theBenchmark for (2824ds/667Mi)
% 171.30/34.71 % (2424872)Instruction limit reached!
% 171.30/34.71 % (2424872)------------------------------
% 171.30/34.71 % (2424872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.30/34.71 % (2424872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.30/34.71 % (2424872)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424872)Termination reason: Instruction limit
% 171.30/34.71 % (2424872)Termination phase: Preprocessing 1
% 171.30/34.71 % (2424872)Time elapsed: 0.563 s
% 171.30/34.71 % (2424872)Peak memory usage: 463 MB
% 171.30/34.71 % (2424872)Instructions burned: 668 (million)
% 171.30/34.71 % (2424874)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=38650822:s2a=on:i=185:s2at=1.8:fdi=4_2816 on theBenchmark for (2816ds/185Mi)
% 171.30/34.71 % (2424874)Instruction limit reached!
% 171.30/34.71 % (2424874)------------------------------
% 171.30/34.71 % (2424874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.30/34.71 % (2424874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.30/34.71 % (2424874)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424874)Termination reason: Instruction limit
% 171.30/34.71 % (2424874)Termination phase: SInE selection
% 171.30/34.71 % (2424874)Time elapsed: 0.157 s
% 171.30/34.71 % (2424874)Peak memory usage: 462 MB
% 171.30/34.71 % (2424874)Instructions burned: 185 (million)
% 171.30/34.71 % (2424876)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2436916701:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2812 on theBenchmark for (2812ds/193Mi)
% 171.30/34.71 % (2424876)Instruction limit reached!
% 171.30/34.71 % (2424876)------------------------------
% 171.30/34.71 % (2424876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.30/34.71 % (2424876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.30/34.71 % (2424876)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424876)Termination reason: Instruction limit
% 171.30/34.71 % (2424876)Termination phase: SInE selection
% 171.30/34.71 % (2424876)Time elapsed: 0.168 s
% 171.30/34.71 % (2424876)Peak memory usage: 462 MB
% 171.30/34.71 % (2424876)Instructions burned: 194 (million)
% 171.30/34.71 % (2424878)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=839442943:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2808 on theBenchmark for (2808ds/4850Mi)
% 171.30/34.71 % (2424682)Instruction limit reached!
% 171.30/34.71 % (2424682)------------------------------
% 171.30/34.71 % (2424682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.30/34.71 % (2424682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.30/34.71 % (2424682)CaDiCaL version: 2.1.3
% 171.30/34.71 % (2424682)Termination reason: Instruction limit
% 171.30/34.71 % (2424682)Termination phase: Property scanning
% 171.30/34.71 % (2424682)Time elapsed: 5.209 s
% 171.30/34.71 % (2424682)Peak memory usage: 701 MB
% 171.30/34.71 % (2424682)Instructions burned: 6061 (million)
% 171.30/34.71 % (2424880)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=278939207:i=12111:sd=1:ss=included_2800 on theBenchmark for (2800ds/12111Mi)
% 171.30/34.71 % (2424878)Instruction limit reached!
% 171.30/34.71 % (2424878)------------------------------
% 171.30/34.71 % (2424878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424878)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424878)Termination reason: Instruction limit
% 231.32/43.17 % (2424878)Termination phase: Saturation
% 231.32/43.17 % (2424878)Time elapsed: 3.356 s
% 231.32/43.17 % (2424878)Peak memory usage: 535 MB
% 231.32/43.17 % (2424878)Instructions burned: 4850 (million)
% 231.32/43.17 % (2424882)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4042626220:i=319:kws=precedence:fsr=off_2772 on theBenchmark for (2772ds/319Mi)
% 231.32/43.17 % (2424882)Instruction limit reached!
% 231.32/43.17 % (2424882)------------------------------
% 231.32/43.17 % (2424882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424882)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424882)Termination reason: Instruction limit
% 231.32/43.17 % (2424882)Termination phase: Preprocessing 1
% 231.32/43.17 % (2424882)Time elapsed: 0.271 s
% 231.32/43.17 % (2424882)Peak memory usage: 463 MB
% 231.32/43.17 % (2424882)Instructions burned: 320 (million)
% 231.32/43.17 % (2424884)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1008375214:i=2064:ep=RST_2768 on theBenchmark for (2768ds/2064Mi)
% 231.32/43.17 % (2424491)Instruction limit reached!
% 231.32/43.17 % (2424491)------------------------------
% 231.32/43.17 % (2424491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424491)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424491)Termination reason: Instruction limit
% 231.32/43.17 % (2424491)Termination phase: Saturation
% 231.32/43.17 % (2424491)Time elapsed: 11.023 s
% 231.32/43.17 % (2424491)Peak memory usage: 892 MB
% 231.32/43.17 % (2424491)Instructions burned: 13193 (million)
% 231.32/43.17 % (2424886)dis-1011_128_sil=32000:random_seed=53099303:i=3706:ep=RST:av=off_2751 on theBenchmark for (2751ds/3706Mi)
% 231.32/43.17 % (2424884)Instruction limit reached!
% 231.32/43.17 % (2424884)------------------------------
% 231.32/43.17 % (2424884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424884)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424884)Termination reason: Instruction limit
% 231.32/43.17 % (2424884)Termination phase: Naming
% 231.32/43.17 % (2424884)Time elapsed: 1.949 s
% 231.32/43.17 % (2424884)Peak memory usage: 567 MB
% 231.32/43.17 % (2424884)Instructions burned: 2067 (million)
% 231.32/43.17 % (2424888)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2218388587:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2746 on theBenchmark for (2746ds/757Mi)
% 231.32/43.17 % (2424888)Instruction limit reached!
% 231.32/43.17 % (2424888)------------------------------
% 231.32/43.17 % (2424888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424888)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424888)Termination reason: Instruction limit
% 231.32/43.17 % (2424888)Termination phase: SInE selection
% 231.32/43.17 % (2424888)Time elapsed: 0.633 s
% 231.32/43.17 % (2424888)Peak memory usage: 472 MB
% 231.32/43.17 % (2424888)Instructions burned: 757 (million)
% 231.32/43.17 % (2424890)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=769935947:i=13913:ss=axioms:sgt=8_2737 on theBenchmark for (2737ds/13913Mi)
% 231.32/43.17 % (2424886)Instruction limit reached!
% 231.32/43.17 % (2424886)------------------------------
% 231.32/43.17 % (2424886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.32/43.17 % (2424886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.32/43.17 % (2424886)CaDiCaL version: 2.1.3
% 231.32/43.17 % (2424886)Termination reason: Instruction limit
% 231.32/43.17 % (2424886)Termination phase: Clausification
% 231.32/43.17 % (2424886)Time elapsed: 1.785 s
% 231.32/43.17 % (2424886)Peak memory usage: 567 MB
% 231.32/43.17 % (2424886)Instructions burned: 3708 (million)
% 231.32/43.17 % (2424892)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2542873047:i=9925:aac=none_2731 on theBenchmark for (2731ds/9925Mi)
% 231.32/43.17 % (2424699)Instruction limit reached!
% 231.32/43.17 % (2424699)------------------------------
% 231.32/43.17 % (2424699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2424699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2424699)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2424699)Termination reason: Instruction limit
% 246.44/45.35 % (2424699)Termination phase: Saturation
% 246.44/45.35 % (2424699)Time elapsed: 12.316 s
% 246.44/45.35 % (2424699)Peak memory usage: 1575 MB
% 246.44/45.35 % (2424699)Instructions burned: 14155 (million)
% 246.44/45.35 % (2424894)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2908928373:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2722 on theBenchmark for (2722ds/2479Mi)
% 246.44/45.35 % (2424894)Instruction limit reached!
% 246.44/45.35 % (2424894)------------------------------
% 246.44/45.35 % (2424894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2424894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2424894)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2424894)Termination reason: Instruction limit
% 246.44/45.35 % (2424894)Termination phase: Saturation
% 246.44/45.35 % (2424894)Time elapsed: 2.172 s
% 246.44/45.35 % (2424894)Peak memory usage: 529 MB
% 246.44/45.35 % (2424894)Instructions burned: 2480 (million)
% 246.44/45.35 % (2425158)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=34595872:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2698 on theBenchmark for (2698ds/440Mi)
% 246.44/45.35 % (2425158)Instruction limit reached!
% 246.44/45.35 % (2425158)------------------------------
% 246.44/45.35 % (2425158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2425158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2425158)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2425158)Termination reason: Instruction limit
% 246.44/45.35 % (2425158)Termination phase: Property scanning
% 246.44/45.35 % (2425158)Time elapsed: 0.397 s
% 246.44/45.35 % (2425158)Peak memory usage: 463 MB
% 246.44/45.35 % (2425158)Instructions burned: 441 (million)
% 246.44/45.35 % (2425176)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1281743697:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2691 on theBenchmark for (2691ds/11145Mi)
% 246.44/45.35 % (2424892)Instruction limit reached!
% 246.44/45.35 % (2424892)------------------------------
% 246.44/45.35 % (2424892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2424892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2424892)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2424892)Termination reason: Instruction limit
% 246.44/45.35 % (2424892)Termination phase: Saturation
% 246.44/45.35 % (2424892)Time elapsed: 4.444 s
% 246.44/45.35 % (2424892)Peak memory usage: 635 MB
% 246.44/45.35 % (2424892)Instructions burned: 9925 (million)
% 246.44/45.35 % (2425217)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=940022586:cts=off:i=3034:av=off:er=known:fsd=on_2685 on theBenchmark for (2685ds/3034Mi)
% 246.44/45.35 % (2425217)Instruction limit reached!
% 246.44/45.35 % (2425217)------------------------------
% 246.44/45.35 % (2425217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2425217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2425217)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2425217)Termination reason: Instruction limit
% 246.44/45.35 % (2425217)Termination phase: Naming
% 246.44/45.35 % (2425217)Time elapsed: 1.788 s
% 246.44/45.35 % (2425217)Peak memory usage: 569 MB
% 246.44/45.35 % (2425217)Instructions burned: 3037 (million)
% 246.44/45.35 % (2425219)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2538299205:st=2:s2a=on:i=524:s2at=2:ss=axioms_2665 on theBenchmark for (2665ds/524Mi)
% 246.44/45.35 % (2425219)Instruction limit reached!
% 246.44/45.35 % (2425219)------------------------------
% 246.44/45.35 % (2425219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.44/45.35 % (2425219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.44/45.35 % (2425219)CaDiCaL version: 2.1.3
% 246.44/45.35 % (2425219)Termination reason: Instruction limit
% 246.44/45.35 % (2425219)Termination phase: SInE selection
% 246.44/45.35 % (2425219)Time elapsed: 0.260 s
% 246.44/45.35 % (2425219)Peak memory usage: 462 MB
% 246.44/45.35 % (2425219)Instructions burned: 526 (million)
% 246.44/45.35 % (2425221)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=74510663:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2661 on theBenchmark for (2661ds/1016Mi)
% 270.24/48.72 % (2425221)Instruction limit reached!
% 270.24/48.72 % (2425221)------------------------------
% 270.24/48.72 % (2425221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2425221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2425221)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2425221)Termination reason: Instruction limit
% 270.24/48.72 % (2425221)Termination phase: SInE selection
% 270.24/48.72 % (2425221)Time elapsed: 0.571 s
% 270.24/48.72 % (2425221)Peak memory usage: 476 MB
% 270.24/48.72 % (2425221)Instructions burned: 1018 (million)
% 270.24/48.72 % (2425223)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=434658565:i=14123:bd=preordered:ins=4_2653 on theBenchmark for (2653ds/14123Mi)
% 270.24/48.72 % (2424880)Instruction limit reached!
% 270.24/48.72 % (2424880)------------------------------
% 270.24/48.72 % (2424880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2424880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2424880)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2424880)Termination reason: Instruction limit
% 270.24/48.72 % (2424880)Termination phase: Saturation
% 270.24/48.72 % (2424880)Time elapsed: 15.528 s
% 270.24/48.72 % (2424880)Peak memory usage: 893 MB
% 270.24/48.72 % (2424880)Instructions burned: 12115 (million)
% 270.24/48.72 % (2425225)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2885536200:i=5781:kws=precedence:bd=all:rawr=on_2642 on theBenchmark for (2642ds/5781Mi)
% 270.24/48.72 % (2425225)Instruction limit reached!
% 270.24/48.72 % (2425225)------------------------------
% 270.24/48.72 % (2425225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2425225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2425225)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2425225)Termination reason: Instruction limit
% 270.24/48.72 % (2425225)Termination phase: Property scanning
% 270.24/48.72 % (2425225)Time elapsed: 4.254 s
% 270.24/48.72 % (2425225)Peak memory usage: 616 MB
% 270.24/48.72 % (2425225)Instructions burned: 5783 (million)
% 270.24/48.72 % (2425227)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2780766747:i=2448:gtgl=5:bd=preordered:gtg=all_2597 on theBenchmark for (2597ds/2448Mi)
% 270.24/48.72 % (2424375)Refutation not found, incomplete strategy
% 270.24/48.72 % (2424375)------------------------------
% 270.24/48.72 % (2424375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2424375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2424375)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2424375)Termination reason: Refutation not found, incomplete strategy
% 270.24/48.72 % (2424375)Time elapsed: 28.942 s
% 270.24/48.72 % (2424375)Peak memory usage: 893 MB
% 270.24/48.72 % (2424375)Instructions burned: 29623 (million)
% 270.24/48.72 % (2424375)------------------------------
% 270.24/48.72 % (2424375)------------------------------
% 270.24/48.72 % (2425229)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=877603573:i=3223:kws=precedence:fgj=on:av=off_2586 on theBenchmark for (2586ds/3223Mi)
% 270.24/48.72 % (2425227)Instruction limit reached!
% 270.24/48.72 % (2425227)------------------------------
% 270.24/48.72 % (2425227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2425227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2425227)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2425227)Termination reason: Instruction limit
% 270.24/48.72 % (2425227)Termination phase: Initialization
% 270.24/48.72 % (2425227)Time elapsed: 1.504 s
% 270.24/48.72 % (2425227)Peak memory usage: 463 MB
% 270.24/48.72 % (2425227)Instructions burned: 2448 (million)
% 270.24/48.72 % (2425231)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1666827581:st=5.6:i=2033:sd=3:ss=axioms_2580 on theBenchmark for (2580ds/2033Mi)
% 270.24/48.72 % (2425223)Instruction limit reached!
% 270.24/48.72 % (2425223)------------------------------
% 270.24/48.72 % (2425223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 270.24/48.72 % (2425223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 270.24/48.72 % (2425223)CaDiCaL version: 2.1.3
% 270.24/48.72 % (2425223)Termination reason: Instruction limit
% 202.20/52.50 % (2425223)Termination phase: Saturation
% 202.20/52.50 % (2425223)Time elapsed: 7.709 s
% 202.20/52.50 % (2425223)Peak memory usage: 1567 MB
% 202.20/52.50 % (2425223)Instructions burned: 14125 (million)
% 202.20/52.50 % (2425233)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=727872248:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2573 on theBenchmark for (2573ds/2055Mi)
% 202.20/52.50 % (2425233)Instruction limit reached!
% 202.20/52.50 % (2425233)------------------------------
% 202.20/52.50 % (2425233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425233)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425233)Termination reason: Instruction limit
% 202.20/52.50 % (2425233)Termination phase: Property scanning
% 202.20/52.50 % (2425233)Time elapsed: 0.687 s
% 202.20/52.50 % (2425233)Peak memory usage: 463 MB
% 202.20/52.50 % (2425233)Instructions burned: 2055 (million)
% 202.20/52.50 % (2425237)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=294321449:i=21611:sd=3:ss=axioms_2565 on theBenchmark for (2565ds/21611Mi)
% 202.20/52.50 % (2425231)Instruction limit reached!
% 202.20/52.50 % (2425231)------------------------------
% 202.20/52.50 % (2425231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425231)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425231)Termination reason: Instruction limit
% 202.20/52.50 % (2425231)Termination phase: SInE selection
% 202.20/52.50 % (2425231)Time elapsed: 1.645 s
% 202.20/52.50 % (2425231)Peak memory usage: 478 MB
% 202.20/52.50 % (2425231)Instructions burned: 2033 (million)
% 202.20/52.50 % (2425176)Instruction limit reached!
% 202.20/52.50 % (2425176)------------------------------
% 202.20/52.50 % (2425176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425176)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425176)Termination reason: Instruction limit
% 202.20/52.50 % (2425176)Termination phase: Saturation
% 202.20/52.50 % (2425176)Time elapsed: 12.789 s
% 202.20/52.50 % (2425176)Peak memory usage: 891 MB
% 202.20/52.50 % (2425176)Instructions burned: 11145 (million)
% 202.20/52.50 % (2425239)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2661368279:i=4835:sd=13:ss=axioms:sgt=23_2561 on theBenchmark for (2561ds/4835Mi)
% 202.20/52.50 % (2425240)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3437969525:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2561 on theBenchmark for (2561ds/797Mi)
% 202.20/52.50 % (2424890)Instruction limit reached!
% 202.20/52.50 % (2424890)------------------------------
% 202.20/52.50 % (2424890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2424890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2424890)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2424890)Termination reason: Instruction limit
% 202.20/52.50 % (2424890)Termination phase: Saturation
% 202.20/52.50 % (2424890)Time elapsed: 17.769 s
% 202.20/52.50 % (2424890)Peak memory usage: 888 MB
% 202.20/52.50 % (2424890)Instructions burned: 13914 (million)
% 202.20/52.50 % (2425229)Instruction limit reached!
% 202.20/52.50 % (2425229)------------------------------
% 202.20/52.50 % (2425229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425229)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425229)Termination reason: Instruction limit
% 202.20/52.50 % (2425229)Termination phase: Naming
% 202.20/52.50 % (2425229)Time elapsed: 2.742 s
% 202.20/52.50 % (2425229)Peak memory usage: 569 MB
% 202.20/52.50 % (2425229)Instructions burned: 3224 (million)
% 202.20/52.50 % (2425243)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1616755684:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2557 on theBenchmark for (2557ds/2326Mi)
% 202.20/52.50 % (2425244)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=401237907:i=6038:nm=6_2556 on theBenchmark for (2556ds/6038Mi)
% 202.20/52.50 % (2425240)Instruction limit reached!
% 202.20/52.50 % (2425240)------------------------------
% 202.20/52.50 % (2425240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425240)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425240)Termination reason: Instruction limit
% 202.20/52.50 % (2425240)Termination phase: SInE selection
% 202.20/52.50 % (2425240)Time elapsed: 0.604 s
% 202.20/52.50 % (2425240)Peak memory usage: 470 MB
% 202.20/52.50 % (2425240)Instructions burned: 797 (million)
% 202.20/52.50 % (2425247)lrs+10_1_sil=32000:sp=occurrence:random_seed=461608464:st=2:i=33334:sd=3:ss=included:sgt=32_2553 on theBenchmark for (2553ds/33334Mi)
% 202.20/52.50 % (2425247)Refutation not found, incomplete strategy
% 202.20/52.50 % (2425247)------------------------------
% 202.20/52.50 % (2425247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425247)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425247)Termination reason: Refutation not found, incomplete strategy
% 202.20/52.50 % (2425247)Time elapsed: 1.319 s
% 202.20/52.50 % (2425247)Peak memory usage: 536 MB
% 202.20/52.50 % (2425247)Instructions burned: 1424 (million)
% 202.20/52.50 % (2425243)Instruction limit reached!
% 202.20/52.50 % (2425243)------------------------------
% 202.20/52.50 % (2425243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425243)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425243)Termination reason: Instruction limit
% 202.20/52.50 % (2425243)Termination phase: Preprocessing 3
% 202.20/52.50 % (2425243)Time elapsed: 1.971 s
% 202.20/52.50 % (2425243)Peak memory usage: 567 MB
% 202.20/52.50 % (2425243)Instructions burned: 2328 (million)
% 202.20/52.50 % (2425249)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=640023443:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2535 on theBenchmark for (2535ds/1008Mi)
% 202.20/52.50 % (2425247)------------------------------
% 202.20/52.50 % (2425247)------------------------------
% 202.20/52.50 % (2425239)Instruction limit reached!
% 202.20/52.50 % (2425239)------------------------------
% 202.20/52.50 % (2425239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425239)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425239)Termination reason: Instruction limit
% 202.20/52.50 % (2425239)Termination phase: Saturation
% 202.20/52.50 % (2425239)Time elapsed: 2.919 s
% 202.20/52.50 % (2425239)Peak memory usage: 536 MB
% 202.20/52.50 % (2425239)Instructions burned: 4838 (million)
% 202.20/52.50 % (2425251)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=251162035:i=8327:s2at=5:bd=preordered_2532 on theBenchmark for (2532ds/8327Mi)
% 202.20/52.50 % (2425253)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2832576961:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2530 on theBenchmark for (2530ds/1083Mi)
% 202.20/52.50 % (2425249)Instruction limit reached!
% 202.20/52.50 % (2425249)------------------------------
% 202.20/52.50 % (2425249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425249)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425249)Termination reason: Instruction limit
% 202.20/52.50 % (2425249)Termination phase: SInE selection
% 202.20/52.50 % (2425249)Time elapsed: 0.788 s
% 202.20/52.50 % (2425249)Peak memory usage: 472 MB
% 202.20/52.50 % (2425249)Instructions burned: 1008 (million)
% 202.20/52.50 % (2425255)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2764063195:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2525 on theBenchmark for (2525ds/1084Mi)
% 202.20/52.50 % (2425253)Instruction limit reached!
% 202.20/52.50 % (2425253)------------------------------
% 202.20/52.50 % (2425253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425253)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425253)Termination reason: Instruction limit
% 202.20/52.50 % (2425253)Termination phase: SInE selection
% 202.20/52.50 % (2425253)Time elapsed: 0.906 s
% 202.20/52.50 % (2425253)Peak memory usage: 479 MB
% 202.20/52.50 % (2425253)Instructions burned: 1083 (million)
% 202.20/52.50 % (2425257)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2470912047:i=6995:s2at=5:gtg=all_2519 on theBenchmark for (2519ds/6995Mi)
% 202.20/52.50 % (2425255)Instruction limit reached!
% 202.20/52.50 % (2425255)------------------------------
% 202.20/52.50 % (2425255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425255)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425255)Termination reason: Instruction limit
% 202.20/52.50 % (2425255)Termination phase: SInE selection
% 202.20/52.50 % (2425255)Time elapsed: 0.918 s
% 202.20/52.50 % (2425255)Peak memory usage: 479 MB
% 202.20/52.50 % (2425255)Instructions burned: 1084 (million)
% 202.20/52.50 % (2425259)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=570379844:st=2:i=6225:sd=15:ss=axioms_2514 on theBenchmark for (2514ds/6225Mi)
% 202.20/52.50 % (2425244)Instruction limit reached!
% 202.20/52.50 % (2425244)------------------------------
% 202.20/52.50 % (2425244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425244)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425244)Termination reason: Instruction limit
% 202.20/52.50 % (2425244)Termination phase: Property scanning
% 202.20/52.50 % (2425244)Time elapsed: 4.510 s
% 202.20/52.50 % (2425244)Peak memory usage: 616 MB
% 202.20/52.50 % (2425244)Instructions burned: 6039 (million)
% 202.20/52.50 % (2425261)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=557839047:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2508 on theBenchmark for (2508ds/3372Mi)
% 202.20/52.50 % (2425259)First to succeed.
% 202.20/52.50 % (2425259)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2424071"
% 202.20/52.50 % (2425261)Instruction limit reached!
% 202.20/52.50 % (2425261)------------------------------
% 202.20/52.50 % (2425261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.20/52.50 % (2425261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.20/52.50 % (2425261)CaDiCaL version: 2.1.3
% 202.20/52.50 % (2425261)Termination reason: Instruction limit
% 202.20/52.50 % (2425261)Termination phase: SInE selection
% 202.20/52.50 % (2425261)Time elapsed: 2.155 s
% 202.20/52.50 % (2425261)Peak memory usage: 479 MB
% 202.20/52.50 % (2425261)Instructions burned: 3372 (million)
% 202.20/52.50 % (2425259)Refutation found. Thanks to Tanya!
% 202.20/52.50 % SZS status Theorem for theBenchmark
% 202.20/52.50 % SZS output start Proof for theBenchmark
% See solution above
% 297.37/53.12 % (2425259)------------------------------
% 297.37/53.12 % (2425259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 297.37/53.12 % (2425259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 297.37/53.12 % (2425259)CaDiCaL version: 2.1.3
% 297.37/53.12 % (2425259)Termination reason: Refutation
% 297.37/53.12 % (2425259)Time elapsed: 2.209 s
% 297.37/53.12 % (2425259)Peak memory usage: 536 MB
% 297.37/53.12 % (2425259)Instructions burned: 2930 (million)
% 297.37/53.12 % (2425259)------------------------------
% 297.37/53.12 % (2425259)------------------------------
% 297.37/53.12 % (2424071)Success in time 51.83 s
% 297.37/53.12 % Vampire exiting
%------------------------------------------------------------------------------