%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM784+4 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.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 12:16:59 PM UTC 2026 % Result : Timeout 289.67s 41.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM784+4 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.37 % Computer : n002.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sun Sep 27 21:25:51 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.40 Running first-order theorem proving % 0.10/0.40 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 % 12.39/2.68 % (3897420)Detected formulas, will run a generic FOF schedule. % 12.39/2.68 % (3897429)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1329103322:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 12.39/2.68 % (3897429)Refutation not found, incomplete strategy % 12.39/2.68 % (3897429)------------------------------ % 12.39/2.68 % (3897429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.68 % (3897429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.68 % (3897429)CaDiCaL version: 2.1.3 % 12.39/2.68 % (3897429)Termination reason: Refutation not found, incomplete strategy % 12.39/2.68 % (3897429)Time elapsed: 0.003 s % 12.39/2.68 % (3897429)Peak memory usage: 89 MB % 12.39/2.68 % (3897429)Instructions burned: 7 (million) % 12.39/2.68 % (3897430)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4063658199:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 12.39/2.68 % (3897428)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2912634660:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 12.39/2.68 % (3897426)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=753835098:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 12.39/2.68 % (3897425)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=320232922:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 12.39/2.68 % (3897431)dis-21_1_sil=8000:lcm=predicate:random_seed=752400036:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 12.39/2.68 % (3897427)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=977846617:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 12.39/2.68 % (3897428)Refutation not found, incomplete strategy % 12.39/2.68 % (3897428)------------------------------ % 12.39/2.68 % (3897428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.68 % (3897428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.68 % (3897428)CaDiCaL version: 2.1.3 % 12.39/2.68 % (3897428)Termination reason: Refutation not found, incomplete strategy % 12.39/2.68 % (3897428)Time elapsed: 0.005 s % 12.39/2.68 % (3897428)Peak memory usage: 89 MB % 12.39/2.68 % (3897428)Instructions burned: 6 (million) % 12.39/2.68 % (3897431)Instruction limit reached! % 12.39/2.68 % (3897431)------------------------------ % 12.39/2.68 % (3897431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.68 % (3897431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.68 % (3897431)CaDiCaL version: 2.1.3 % 12.39/2.68 % (3897431)Termination reason: Instruction limit % 12.39/2.68 % (3897431)Termination phase: Saturation % 12.39/2.68 % (3897431)Time elapsed: 0.056 s % 12.39/2.68 % (3897431)Peak memory usage: 90 MB % 12.39/2.68 % (3897431)Instructions burned: 130 (million) % 12.39/2.68 % (3897430)Instruction limit reached! % 12.39/2.68 % (3897430)------------------------------ % 12.39/2.68 % (3897430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.68 % (3897430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.68 % (3897430)CaDiCaL version: 2.1.3 % 12.39/2.68 % (3897430)Termination reason: Instruction limit % 12.39/2.68 % (3897430)Termination phase: Saturation % 12.39/2.68 % (3897430)Time elapsed: 0.063 s % 12.39/2.68 % (3897430)Peak memory usage: 91 MB % 12.39/2.68 % (3897430)Instructions burned: 140 (million) % 12.39/2.68 % (3897429)------------------------------ % 12.39/2.68 % (3897429)------------------------------ % 12.39/2.68 % (3897439)lrs+10_1_sil=8000:sp=occurrence:random_seed=2230154563:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 12.39/2.68 % (3897439)Refutation not found, incomplete strategy % 12.39/2.68 % (3897439)------------------------------ % 12.39/2.68 % (3897439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.68 % (3897439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.68 % (3897439)CaDiCaL version: 2.1.3 % 12.39/2.68 % (3897439)Termination reason: Refutation not found, incomplete strategy % 12.39/2.68 % (3897439)Time elapsed: 0.006 s % 12.39/2.68 % (3897439)Peak memory usage: 89 MB % 19.85/3.74 % (3897439)Instructions burned: 6 (million) % 19.85/3.74 % (3897440)lrs+10_1_sil=32000:urr=on:br=off:random_seed=108285661:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 19.85/3.74 % (3897440)Refutation not found, incomplete strategy % 19.85/3.74 % (3897440)------------------------------ % 19.85/3.74 % (3897440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.85/3.74 % (3897440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.74 % (3897440)CaDiCaL version: 2.1.3 % 19.85/3.74 % (3897440)Termination reason: Refutation not found, incomplete strategy % 19.85/3.74 % (3897440)Time elapsed: 0.011 s % 19.85/3.74 % (3897440)Peak memory usage: 89 MB % 19.85/3.74 % (3897440)Instructions burned: 21 (million) % 19.85/3.74 % (3897428)------------------------------ % 19.85/3.74 % (3897428)------------------------------ % 19.85/3.74 % (3897441)lrs+1011_1_sil=32000:sp=occurrence:random_seed=608384773:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 19.85/3.74 % (3897441)Refutation not found, incomplete strategy % 19.85/3.74 % (3897441)------------------------------ % 19.85/3.74 % (3897441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.85/3.74 % (3897441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.74 % (3897441)CaDiCaL version: 2.1.3 % 19.85/3.74 % (3897441)Termination reason: Refutation not found, incomplete strategy % 19.85/3.74 % (3897441)Time elapsed: 0.005 s % 19.85/3.74 % (3897441)Peak memory usage: 90 MB % 19.85/3.74 % (3897441)Instructions burned: 12 (million) % 19.85/3.74 % (3897441)------------------------------ % 19.85/3.74 % (3897441)------------------------------ % 19.85/3.74 % (3897445)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=1525726850:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 19.85/3.74 % (3897439)------------------------------ % 19.85/3.74 % (3897439)------------------------------ % 19.85/3.74 % (3897440)------------------------------ % 19.85/3.74 % (3897440)------------------------------ % 19.85/3.74 % (3897446)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1020972777:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 19.85/3.74 % (3897446)Refutation not found, incomplete strategy % 19.85/3.74 % (3897446)------------------------------ % 19.85/3.74 % (3897446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.85/3.74 % (3897446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.74 % (3897446)CaDiCaL version: 2.1.3 % 19.85/3.74 % (3897446)Termination reason: Refutation not found, incomplete strategy % 19.85/3.74 % (3897446)Time elapsed: 0.005 s % 19.85/3.74 % (3897446)Peak memory usage: 90 MB % 19.85/3.74 % (3897446)Instructions burned: 15 (million) % 19.85/3.74 % (3897445)Instruction limit reached! % 19.85/3.74 % (3897445)------------------------------ % 19.85/3.74 % (3897445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.85/3.74 % (3897445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.74 % (3897445)CaDiCaL version: 2.1.3 % 19.85/3.74 % (3897445)Termination reason: Instruction limit % 19.85/3.74 % (3897445)Termination phase: Saturation % 19.85/3.74 % (3897445)Time elapsed: 0.133 s % 19.85/3.74 % (3897445)Peak memory usage: 93 MB % 19.85/3.74 % (3897445)Instructions burned: 248 (million) % 19.85/3.74 % (3897449)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=272553171:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 19.85/3.74 % (3897448)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1451402812:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 19.85/3.74 % (3897446)------------------------------ % 19.85/3.74 % (3897446)------------------------------ % 19.85/3.74 % (3897449)Instruction limit reached! % 19.85/3.74 % (3897449)------------------------------ % 19.85/3.74 % (3897449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.85/3.74 % (3897449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.85/3.74 % (3897449)CaDiCaL version: 2.1.3 % 19.85/3.74 % (3897449)Termination reason: Instruction limit % 19.85/3.74 % (3897449)Termination phase: Saturation % 19.85/3.74 % (3897449)Time elapsed: 0.055 s % 19.85/3.74 % (3897449)Peak memory usage: 90 MB % 19.85/3.74 % (3897449)Instructions burned: 113 (million) % 19.85/3.74 % (3897451)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=469332649:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 38.04/6.24 % (3897451)Instruction limit reached! % 38.04/6.24 % (3897451)------------------------------ % 38.04/6.24 % (3897451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897451)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897451)Termination reason: Instruction limit % 38.04/6.24 % (3897451)Termination phase: Property scanning % 38.04/6.24 % (3897451)Time elapsed: 0.059 s % 38.04/6.24 % (3897451)Peak memory usage: 89 MB % 38.04/6.24 % (3897451)Instructions burned: 129 (million) % 38.04/6.24 % (3897454)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3832002686:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 38.04/6.24 % (3897454)Instruction limit reached! % 38.04/6.24 % (3897454)------------------------------ % 38.04/6.24 % (3897454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897454)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897454)Termination reason: Instruction limit % 38.04/6.24 % (3897454)Termination phase: Saturation % 38.04/6.24 % (3897454)Time elapsed: 0.032 s % 38.04/6.24 % (3897454)Peak memory usage: 90 MB % 38.04/6.24 % (3897454)Instructions burned: 117 (million) % 38.04/6.24 % (3897455)lrs+10_1_sil=8000:sp=occurrence:random_seed=2851906176:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 38.04/6.24 % (3897457)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=527820694:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 38.04/6.24 % (3897459)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=254881637:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 38.04/6.24 % (3897457)Refutation not found, incomplete strategy % 38.04/6.24 % (3897457)------------------------------ % 38.04/6.24 % (3897457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897457)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897457)Termination reason: Refutation not found, incomplete strategy % 38.04/6.24 % (3897457)Time elapsed: 0.093 s % 38.04/6.24 % (3897457)Peak memory usage: 93 MB % 38.04/6.24 % (3897457)Instructions burned: 191 (million) % 38.04/6.24 % (3897457)------------------------------ % 38.04/6.24 % (3897457)------------------------------ % 38.04/6.24 % (3897455)Instruction limit reached! % 38.04/6.24 % (3897455)------------------------------ % 38.04/6.24 % (3897455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897455)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897455)Termination reason: Instruction limit % 38.04/6.24 % (3897455)Termination phase: Saturation % 38.04/6.24 % (3897455)Time elapsed: 0.546 s % 38.04/6.24 % (3897455)Peak memory usage: 101 MB % 38.04/6.24 % (3897455)Instructions burned: 907 (million) % 38.04/6.24 % (3897463)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3468471640:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi) % 38.04/6.24 % (3897463)Instruction limit reached! % 38.04/6.24 % (3897463)------------------------------ % 38.04/6.24 % (3897463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897463)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897463)Termination reason: Instruction limit % 38.04/6.24 % (3897463)Termination phase: Saturation % 38.04/6.24 % (3897463)Time elapsed: 0.061 s % 38.04/6.24 % (3897463)Peak memory usage: 91 MB % 38.04/6.24 % (3897463)Instructions burned: 135 (million) % 38.04/6.24 % (3897464)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3871794850:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi) % 38.04/6.24 % (3897464)Refutation not found, incomplete strategy % 38.04/6.24 % (3897464)------------------------------ % 38.04/6.24 % (3897464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.04/6.24 % (3897464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.04/6.24 % (3897464)CaDiCaL version: 2.1.3 % 38.04/6.24 % (3897464)Termination reason: Refutation not found, incomplete strategy % 68.47/10.54 % (3897464)Time elapsed: 0.021 s % 68.47/10.54 % (3897464)Peak memory usage: 90 MB % 68.47/10.54 % (3897464)Instructions burned: 39 (million) % 68.47/10.54 % (3897466)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3504747671:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi) % 68.47/10.54 % (3897464)------------------------------ % 68.47/10.54 % (3897464)------------------------------ % 68.47/10.54 % (3897469)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=1398103435:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi) % 68.47/10.54 % (3897448)Instruction limit reached! % 68.47/10.54 % (3897448)------------------------------ % 68.47/10.54 % (3897448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.47/10.54 % (3897448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.47/10.54 % (3897448)CaDiCaL version: 2.1.3 % 68.47/10.54 % (3897448)Termination reason: Instruction limit % 68.47/10.54 % (3897448)Termination phase: Saturation % 68.47/10.54 % (3897448)Time elapsed: 1.398 s % 68.47/10.54 % (3897448)Peak memory usage: 159 MB % 68.47/10.54 % (3897448)Instructions burned: 2351 (million) % 68.47/10.54 % (3897469)Instruction limit reached! % 68.47/10.54 % (3897469)------------------------------ % 68.47/10.54 % (3897469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.47/10.54 % (3897469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.47/10.54 % (3897469)CaDiCaL version: 2.1.3 % 68.47/10.54 % (3897469)Termination reason: Instruction limit % 68.47/10.54 % (3897469)Termination phase: Saturation % 68.47/10.54 % (3897469)Time elapsed: 0.066 s % 68.47/10.54 % (3897469)Peak memory usage: 91 MB % 68.47/10.54 % (3897469)Instructions burned: 125 (million) % 68.47/10.54 % (3897471)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1535574106:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi) % 68.47/10.54 % (3897472)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2854157943:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi) % 68.47/10.54 % (3897472)Refutation not found, incomplete strategy % 68.47/10.54 % (3897472)------------------------------ % 68.47/10.54 % (3897472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.47/10.54 % (3897472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.47/10.54 % (3897472)CaDiCaL version: 2.1.3 % 68.47/10.54 % (3897472)Termination reason: Refutation not found, incomplete strategy % 68.47/10.54 % (3897472)Time elapsed: 0.005 s % 68.47/10.54 % (3897472)Peak memory usage: 89 MB % 68.47/10.54 % (3897472)Instructions burned: 6 (million) % 68.47/10.54 % (3897471)Instruction limit reached! % 68.47/10.54 % (3897471)------------------------------ % 68.47/10.54 % (3897471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.47/10.54 % (3897471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.47/10.54 % (3897471)CaDiCaL version: 2.1.3 % 68.47/10.54 % (3897471)Termination reason: Instruction limit % 68.47/10.54 % (3897471)Termination phase: Twee Goal Transformation % 68.47/10.54 % (3897471)Time elapsed: 0.063 s % 68.47/10.54 % (3897471)Peak memory usage: 91 MB % 68.47/10.54 % (3897471)Instructions burned: 135 (million) % 68.47/10.54 % (3897475)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3812923152:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi) % 68.47/10.54 % (3897475)Refutation not found, incomplete strategy % 68.47/10.54 % (3897475)------------------------------ % 68.47/10.54 % (3897475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.47/10.54 % (3897475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.47/10.54 % (3897475)CaDiCaL version: 2.1.3 % 68.47/10.54 % (3897475)Termination reason: Refutation not found, incomplete strategy % 68.47/10.54 % (3897475)Time elapsed: 0.005 s % 68.47/10.54 % (3897475)Peak memory usage: 90 MB % 68.47/10.54 % (3897475)Instructions burned: 6 (million) % 68.47/10.54 % (3897472)------------------------------ % 68.47/10.54 % (3897472)------------------------------ % 68.47/10.54 % (3897477)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=4159189750:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi) % 83.47/12.63 % (3897475)------------------------------ % 83.47/12.63 % (3897475)------------------------------ % 83.47/12.63 % (3897459)Instruction limit reached! % 83.47/12.63 % (3897459)------------------------------ % 83.47/12.63 % (3897459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.47/12.63 % (3897459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.63 % (3897459)CaDiCaL version: 2.1.3 % 83.47/12.63 % (3897459)Termination reason: Instruction limit % 83.47/12.63 % (3897459)Termination phase: Saturation % 83.47/12.63 % (3897459)Time elapsed: 1.785 s % 83.47/12.63 % (3897459)Peak memory usage: 163 MB % 83.47/12.63 % (3897459)Instructions burned: 5202 (million) % 83.47/12.63 % (3897479)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=2065381376:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi) % 83.47/12.63 % (3897480)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3313283548:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi) % 83.47/12.63 % (3897479)Instruction limit reached! % 83.47/12.63 % (3897479)------------------------------ % 83.47/12.63 % (3897479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.47/12.63 % (3897479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.63 % (3897479)CaDiCaL version: 2.1.3 % 83.47/12.63 % (3897479)Termination reason: Instruction limit % 83.47/12.63 % (3897479)Termination phase: Saturation % 83.47/12.63 % (3897479)Time elapsed: 0.069 s % 83.47/12.63 % (3897479)Peak memory usage: 91 MB % 83.47/12.63 % (3897479)Instructions burned: 151 (million) % 83.47/12.63 % (3897483)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3889115982:i=667:av=off:fsr=off_2968 on theBenchmark for (2968ds/667Mi) % 83.47/12.63 % (3897483)Instruction limit reached! % 83.47/12.63 % (3897483)------------------------------ % 83.47/12.63 % (3897483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.47/12.63 % (3897483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.63 % (3897483)CaDiCaL version: 2.1.3 % 83.47/12.63 % (3897483)Termination reason: Instruction limit % 83.47/12.63 % (3897483)Termination phase: Saturation % 83.47/12.63 % (3897483)Time elapsed: 0.317 s % 83.47/12.63 % (3897483)Peak memory usage: 100 MB % 83.47/12.63 % (3897483)Instructions burned: 667 (million) % 83.47/12.63 % (3897487)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=2557001488:s2a=on:i=185:s2at=1.8:fdi=4_2963 on theBenchmark for (2963ds/185Mi) % 83.47/12.63 % (3897487)Instruction limit reached! % 83.47/12.63 % (3897487)------------------------------ % 83.47/12.63 % (3897487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.47/12.63 % (3897487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.63 % (3897487)CaDiCaL version: 2.1.3 % 83.47/12.63 % (3897487)Termination reason: Instruction limit % 83.47/12.63 % (3897487)Termination phase: Saturation % 83.47/12.63 % (3897487)Time elapsed: 0.079 s % 83.47/12.63 % (3897487)Peak memory usage: 91 MB % 83.47/12.63 % (3897487)Instructions burned: 186 (million) % 83.47/12.63 % (3897489)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2759775338:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2961 on theBenchmark for (2961ds/193Mi) % 83.47/12.63 % (3897489)Refutation not found, incomplete strategy % 83.47/12.63 % (3897489)------------------------------ % 83.47/12.63 % (3897489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.47/12.63 % (3897489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.63 % (3897489)CaDiCaL version: 2.1.3 % 83.47/12.63 % (3897489)Termination reason: Refutation not found, incomplete strategy % 83.47/12.63 % (3897489)Time elapsed: 0.009 s % 83.47/12.63 % (3897489)Peak memory usage: 90 MB % 83.47/12.63 % (3897489)Instructions burned: 12 (million) % 83.47/12.63 % (3897489)------------------------------ % 83.47/12.63 % (3897489)------------------------------ % 83.47/12.63 % (3897491)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2862757522:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi) % 83.47/12.63 % (3897477)Instruction limit reached! % 83.47/12.63 % (3897477)------------------------------ % 83.47/12.63 % (3897477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897477)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897477)Termination reason: Instruction limit % 108.46/16.19 % (3897477)Termination phase: Saturation % 108.46/16.19 % (3897477)Time elapsed: 2.503 s % 108.46/16.19 % (3897477)Peak memory usage: 178 MB % 108.46/16.19 % (3897477)Instructions burned: 6061 (million) % 108.46/16.19 % (3897493)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2200736915:i=12111:sd=1:ss=included_2945 on theBenchmark for (2945ds/12111Mi) % 108.46/16.19 % (3897491)Instruction limit reached! % 108.46/16.19 % (3897491)------------------------------ % 108.46/16.19 % (3897491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897491)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897491)Termination reason: Instruction limit % 108.46/16.19 % (3897491)Termination phase: Saturation % 108.46/16.19 % (3897491)Time elapsed: 3.118 s % 108.46/16.19 % (3897491)Peak memory usage: 154 MB % 108.46/16.19 % (3897491)Instructions burned: 4850 (million) % 108.46/16.19 % (3897495)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=570628564:i=319:kws=precedence:fsr=off_2924 on theBenchmark for (2924ds/319Mi) % 108.46/16.19 % (3897495)Instruction limit reached! % 108.46/16.19 % (3897495)------------------------------ % 108.46/16.19 % (3897495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897495)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897495)Termination reason: Instruction limit % 108.46/16.19 % (3897495)Termination phase: Saturation % 108.46/16.19 % (3897495)Time elapsed: 0.157 s % 108.46/16.19 % (3897495)Peak memory usage: 95 MB % 108.46/16.19 % (3897495)Instructions burned: 320 (million) % 108.46/16.19 % (3897497)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=746611700:i=2064:ep=RST_2920 on theBenchmark for (2920ds/2064Mi) % 108.46/16.19 % (3897497)Refutation not found, incomplete strategy % 108.46/16.19 % (3897497)------------------------------ % 108.46/16.19 % (3897497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897497)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897497)Termination reason: Refutation not found, incomplete strategy % 108.46/16.19 % (3897497)Time elapsed: 0.072 s % 108.46/16.19 % (3897497)Peak memory usage: 92 MB % 108.46/16.19 % (3897497)Instructions burned: 164 (million) % 108.46/16.19 % (3897497)------------------------------ % 108.46/16.19 % (3897497)------------------------------ % 108.46/16.19 % (3897499)dis-1011_128_sil=32000:random_seed=1370701818:i=3706:ep=RST:av=off_2916 on theBenchmark for (2916ds/3706Mi) % 108.46/16.19 % (3897493)Instruction limit reached! % 108.46/16.19 % (3897493)------------------------------ % 108.46/16.19 % (3897493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897493)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897493)Termination reason: Instruction limit % 108.46/16.19 % (3897493)Termination phase: Saturation % 108.46/16.19 % (3897493)Time elapsed: 3.736 s % 108.46/16.19 % (3897493)Peak memory usage: 271 MB % 108.46/16.19 % (3897493)Instructions burned: 12115 (million) % 108.46/16.19 % (3897501)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=889049003:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2907 on theBenchmark for (2907ds/757Mi) % 108.46/16.19 % (3897501)Refutation not found, incomplete strategy % 108.46/16.19 % (3897501)------------------------------ % 108.46/16.19 % (3897501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.46/16.19 % (3897501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.46/16.19 % (3897501)CaDiCaL version: 2.1.3 % 108.46/16.19 % (3897501)Termination reason: Refutation not found, incomplete strategy % 108.46/16.19 % (3897501)Time elapsed: 0.006 s % 108.46/16.19 % (3897501)Peak memory usage: 90 MB % 108.46/16.19 % (3897501)Instructions burned: 19 (million) % 108.46/16.19 % (3897501)------------------------------ % 108.46/16.19 % (3897501)------------------------------ % 108.46/16.19 % (3897503)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1138113341:i=13913:ss=axioms:sgt=8_2904 on theBenchmark for (2904ds/13913Mi) % 123.17/18.23 % (3897466)Instruction limit reached! % 123.17/18.23 % (3897466)------------------------------ % 123.17/18.23 % (3897466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897466)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897466)Termination reason: Instruction limit % 123.17/18.23 % (3897466)Termination phase: Saturation % 123.17/18.23 % (3897466)Time elapsed: 7.803 s % 123.17/18.23 % (3897466)Peak memory usage: 232 MB % 123.17/18.23 % (3897466)Instructions burned: 13193 (million) % 123.17/18.23 % (3897505)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1642609814:i=9925:aac=none_2902 on theBenchmark for (2902ds/9925Mi) % 123.17/18.23 % (3897499)Instruction limit reached! % 123.17/18.23 % (3897499)------------------------------ % 123.17/18.23 % (3897499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897499)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897499)Termination reason: Instruction limit % 123.17/18.23 % (3897499)Termination phase: Saturation % 123.17/18.23 % (3897499)Time elapsed: 2.114 s % 123.17/18.23 % (3897499)Peak memory usage: 109 MB % 123.17/18.23 % (3897499)Instructions burned: 3707 (million) % 123.17/18.23 % (3897480)Instruction limit reached! % 123.17/18.23 % (3897480)------------------------------ % 123.17/18.23 % (3897480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897480)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897480)Termination reason: Instruction limit % 123.17/18.23 % (3897480)Termination phase: Saturation % 123.17/18.23 % (3897480)Time elapsed: 7.523 s % 123.17/18.23 % (3897480)Peak memory usage: 261 MB % 123.17/18.23 % (3897480)Instructions burned: 14155 (million) % 123.17/18.23 % (3897507)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1651176926:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/2479Mi) % 123.17/18.23 % (3897507)Refutation not found, incomplete strategy % 123.17/18.23 % (3897507)------------------------------ % 123.17/18.23 % (3897507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897507)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897507)Termination reason: Refutation not found, incomplete strategy % 123.17/18.23 % (3897507)Time elapsed: 0.008 s % 123.17/18.23 % (3897507)Peak memory usage: 89 MB % 123.17/18.23 % (3897507)Instructions burned: 11 (million) % 123.17/18.23 % (3897508)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1139617058:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2892 on theBenchmark for (2892ds/440Mi) % 123.17/18.23 % (3897508)Instruction limit reached! % 123.17/18.23 % (3897508)------------------------------ % 123.17/18.23 % (3897508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897508)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897508)Termination reason: Instruction limit % 123.17/18.23 % (3897508)Termination phase: Saturation % 123.17/18.23 % (3897508)Time elapsed: 0.164 s % 123.17/18.23 % (3897508)Peak memory usage: 91 MB % 123.17/18.23 % (3897508)Instructions burned: 441 (million) % 123.17/18.23 % (3897507)------------------------------ % 123.17/18.23 % (3897507)------------------------------ % 123.17/18.23 % (3897511)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2860298346:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2889 on theBenchmark for (2889ds/11145Mi) % 123.17/18.23 % (3897512)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=3801369968:cts=off:i=3034:av=off:er=known:fsd=on_2889 on theBenchmark for (2889ds/3034Mi) % 123.17/18.23 % (3897511)Refutation not found, incomplete strategy % 123.17/18.23 % (3897511)------------------------------ % 123.17/18.23 % (3897511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.17/18.23 % (3897511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.17/18.23 % (3897511)CaDiCaL version: 2.1.3 % 123.17/18.23 % (3897511)Termination reason: Refutation not found, incomplete strategy % 148.65/21.86 % (3897511)Time elapsed: 0.611 s % 148.65/21.86 % (3897511)Peak memory usage: 132 MB % 148.65/21.86 % (3897511)Instructions burned: 932 (million) % 148.65/21.86 % (3897511)------------------------------ % 148.65/21.86 % (3897511)------------------------------ % 148.65/21.86 % (3897515)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=550552189:st=2:s2a=on:i=524:s2at=2:ss=axioms_2879 on theBenchmark for (2879ds/524Mi) % 148.65/21.86 % (3897515)Instruction limit reached! % 148.65/21.86 % (3897515)------------------------------ % 148.65/21.86 % (3897515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.65/21.86 % (3897515)CaDiCaL version: 2.1.3 % 148.65/21.86 % (3897515)Termination reason: Instruction limit % 148.65/21.86 % (3897515)Termination phase: Saturation % 148.65/21.86 % (3897515)Time elapsed: 0.276 s % 148.65/21.86 % (3897515)Peak memory usage: 93 MB % 148.65/21.86 % (3897515)Instructions burned: 525 (million) % 148.65/21.86 % (3897517)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=821423527:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2875 on theBenchmark for (2875ds/1016Mi) % 148.65/21.86 % (3897517)Refutation not found, incomplete strategy % 148.65/21.86 % (3897517)------------------------------ % 148.65/21.86 % (3897517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.65/21.86 % (3897517)CaDiCaL version: 2.1.3 % 148.65/21.86 % (3897517)Termination reason: Refutation not found, incomplete strategy % 148.65/21.86 % (3897517)Time elapsed: 0.005 s % 148.65/21.86 % (3897517)Peak memory usage: 90 MB % 148.65/21.86 % (3897517)Instructions burned: 6 (million) % 148.65/21.86 % (3897517)------------------------------ % 148.65/21.86 % (3897517)------------------------------ % 148.65/21.86 % (3897512)Instruction limit reached! % 148.65/21.86 % (3897512)------------------------------ % 148.65/21.86 % (3897512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.65/21.86 % (3897512)CaDiCaL version: 2.1.3 % 148.65/21.86 % (3897512)Termination reason: Instruction limit % 148.65/21.86 % (3897512)Termination phase: Saturation % 148.65/21.86 % (3897512)Time elapsed: 1.657 s % 148.65/21.86 % (3897512)Peak memory usage: 162 MB % 148.65/21.86 % (3897512)Instructions burned: 3036 (million) % 148.65/21.86 % (3897519)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4275014558:i=14123:bd=preordered:ins=4_2871 on theBenchmark for (2871ds/14123Mi) % 148.65/21.86 % (3897520)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2682553058:i=5781:kws=precedence:bd=all:rawr=on_2870 on theBenchmark for (2870ds/5781Mi) % 148.65/21.86 % (3897503)Instruction limit reached! % 148.65/21.86 % (3897503)------------------------------ % 148.65/21.86 % (3897503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.65/21.86 % (3897503)CaDiCaL version: 2.1.3 % 148.65/21.86 % (3897503)Termination reason: Instruction limit % 148.65/21.86 % (3897503)Termination phase: Saturation % 148.65/21.86 % (3897503)Time elapsed: 4.746 s % 148.65/21.86 % (3897503)Peak memory usage: 211 MB % 148.65/21.86 % (3897503)Instructions burned: 13915 (million) % 148.65/21.86 % (3897523)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=1444440468:i=2448:gtgl=5:bd=preordered:gtg=all_2855 on theBenchmark for (2855ds/2448Mi) % 148.65/21.86 % (3897505)Instruction limit reached! % 148.65/21.86 % (3897505)------------------------------ % 148.65/21.86 % (3897505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.65/21.86 % (3897505)CaDiCaL version: 2.1.3 % 148.65/21.86 % (3897505)Termination reason: Instruction limit % 148.65/21.86 % (3897505)Termination phase: Saturation % 148.65/21.86 % (3897505)Time elapsed: 5.307 s % 148.65/21.86 % (3897505)Peak memory usage: 226 MB % 148.65/21.86 % (3897505)Instructions burned: 9929 (million) % 148.65/21.86 % (3897523)Instruction limit reached! % 148.65/21.86 % (3897523)------------------------------ % 148.65/21.86 % (3897523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.65/21.86 % (3897523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897523)CaDiCaL version: 2.1.3 % 181.68/26.54 % (3897523)Termination reason: Instruction limit % 181.68/26.54 % (3897523)Termination phase: Saturation % 181.68/26.54 % (3897523)Time elapsed: 0.767 s % 181.68/26.54 % (3897523)Peak memory usage: 162 MB % 181.68/26.54 % (3897523)Instructions burned: 2449 (million) % 181.68/26.54 % (3897525)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3962406447:i=3223:kws=precedence:fgj=on:av=off_2847 on theBenchmark for (2847ds/3223Mi) % 181.68/26.54 % (3897526)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3290065184:st=5.6:i=2033:sd=3:ss=axioms_2846 on theBenchmark for (2846ds/2033Mi) % 181.68/26.54 % (3897526)Refutation not found, incomplete strategy % 181.68/26.54 % (3897526)------------------------------ % 181.68/26.54 % (3897526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.68/26.54 % (3897526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897526)CaDiCaL version: 2.1.3 % 181.68/26.54 % (3897526)Termination reason: Refutation not found, incomplete strategy % 181.68/26.54 % (3897526)Time elapsed: 0.396 s % 181.68/26.54 % (3897526)Peak memory usage: 134 MB % 181.68/26.54 % (3897526)Instructions burned: 985 (million) % 181.68/26.54 % (3897520)Instruction limit reached! % 181.68/26.54 % (3897520)------------------------------ % 181.68/26.54 % (3897520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.68/26.54 % (3897520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897520)CaDiCaL version: 2.1.3 % 181.68/26.54 % (3897520)Termination reason: Instruction limit % 181.68/26.54 % (3897520)Termination phase: Saturation % 181.68/26.54 % (3897520)Time elapsed: 2.907 s % 181.68/26.54 % (3897520)Peak memory usage: 117 MB % 181.68/26.54 % (3897520)Instructions burned: 5782 (million) % 181.68/26.54 % (3897526)------------------------------ % 181.68/26.54 % (3897526)------------------------------ % 181.68/26.54 % (3897529)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4011934769:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2840 on theBenchmark for (2840ds/2055Mi) % 181.68/26.54 % (3897530)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=825348258:i=21611:sd=3:ss=axioms_2839 on theBenchmark for (2839ds/21611Mi) % 181.68/26.54 % (3897530)Refutation not found, incomplete strategy % 181.68/26.54 % (3897530)------------------------------ % 181.68/26.54 % (3897530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.68/26.54 % (3897530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897530)CaDiCaL version: 2.1.3 % 181.68/26.54 % (3897530)Termination reason: Refutation not found, incomplete strategy % 181.68/26.54 % (3897530)Time elapsed: 0.390 s % 181.68/26.54 % (3897530)Peak memory usage: 132 MB % 181.68/26.54 % (3897530)Instructions burned: 928 (million) % 181.68/26.54 % (3897529)Refutation not found, incomplete strategy % 181.68/26.54 % (3897529)------------------------------ % 181.68/26.54 % (3897529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.68/26.54 % (3897529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897529)CaDiCaL version: 2.1.3 % 181.68/26.54 % (3897529)Termination reason: Refutation not found, incomplete strategy % 181.68/26.54 % (3897529)Time elapsed: 0.596 s % 181.68/26.54 % (3897529)Peak memory usage: 132 MB % 181.68/26.54 % (3897529)Instructions burned: 912 (million) % 181.68/26.54 % (3897530)------------------------------ % 181.68/26.54 % (3897530)------------------------------ % 181.68/26.54 % (3897533)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=277943432:i=4835:sd=13:ss=axioms:sgt=23_2832 on theBenchmark for (2832ds/4835Mi) % 181.68/26.54 % (3897529)------------------------------ % 181.68/26.54 % (3897529)------------------------------ % 181.68/26.54 % (3897535)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=2947108062:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2830 on theBenchmark for (2830ds/797Mi) % 181.68/26.54 % (3897525)Instruction limit reached! % 181.68/26.54 % (3897525)------------------------------ % 181.68/26.54 % (3897525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.68/26.54 % (3897525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.68/26.54 % (3897525)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897525)Termination reason: Instruction limit % 255.93/36.99 % (3897525)Termination phase: Saturation % 255.93/36.99 % (3897525)Time elapsed: 1.999 s % 255.93/36.99 % (3897525)Peak memory usage: 153 MB % 255.93/36.99 % (3897525)Instructions burned: 3224 (million) % 255.93/36.99 % (3897535)Instruction limit reached! % 255.93/36.99 % (3897535)------------------------------ % 255.93/36.99 % (3897535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.93/36.99 % (3897535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.93/36.99 % (3897535)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897535)Termination reason: Instruction limit % 255.93/36.99 % (3897535)Termination phase: Saturation % 255.93/36.99 % (3897535)Time elapsed: 0.362 s % 255.93/36.99 % (3897535)Peak memory usage: 94 MB % 255.93/36.99 % (3897535)Instructions burned: 797 (million) % 255.93/36.99 % (3897537)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3263752758:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2825 on theBenchmark for (2825ds/2326Mi) % 255.93/36.99 % (3897538)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=876479761:i=6038:nm=6_2824 on theBenchmark for (2824ds/6038Mi) % 255.93/36.99 % (3897533)Instruction limit reached! % 255.93/36.99 % (3897533)------------------------------ % 255.93/36.99 % (3897533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.93/36.99 % (3897533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.93/36.99 % (3897533)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897533)Termination reason: Instruction limit % 255.93/36.99 % (3897533)Termination phase: Saturation % 255.93/36.99 % (3897533)Time elapsed: 1.495 s % 255.93/36.99 % (3897533)Peak memory usage: 137 MB % 255.93/36.99 % (3897533)Instructions burned: 4836 (million) % 255.93/36.99 % (3897541)lrs+10_1_sil=32000:sp=occurrence:random_seed=4261991591:st=2:i=33334:sd=3:ss=included:sgt=32_2816 on theBenchmark for (2816ds/33334Mi) % 255.93/36.99 % (3897537)Instruction limit reached! % 255.93/36.99 % (3897537)------------------------------ % 255.93/36.99 % (3897537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.93/36.99 % (3897537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.93/36.99 % (3897537)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897537)Termination reason: Instruction limit % 255.93/36.99 % (3897537)Termination phase: Saturation % 255.93/36.99 % (3897537)Time elapsed: 1.469 s % 255.93/36.99 % (3897537)Peak memory usage: 109 MB % 255.93/36.99 % (3897537)Instructions burned: 2326 (million) % 255.93/36.99 % (3897543)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2195396616:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2809 on theBenchmark for (2809ds/1008Mi) % 255.93/36.99 % (3897543)Refutation not found, incomplete strategy % 255.93/36.99 % (3897543)------------------------------ % 255.93/36.99 % (3897543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.93/36.99 % (3897543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.93/36.99 % (3897543)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897543)Termination reason: Refutation not found, incomplete strategy % 255.93/36.99 % (3897543)Time elapsed: 0.087 s % 255.93/36.99 % (3897543)Peak memory usage: 91 MB % 255.93/36.99 % (3897543)Instructions burned: 148 (million) % 255.93/36.99 % (3897543)------------------------------ % 255.93/36.99 % (3897543)------------------------------ % 255.93/36.99 % (3897545)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=3807206403:i=8327:s2at=5:bd=preordered_2804 on theBenchmark for (2804ds/8327Mi) % 255.93/36.99 % (3897538)Instruction limit reached! % 255.93/36.99 % (3897538)------------------------------ % 255.93/36.99 % (3897538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.93/36.99 % (3897538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.93/36.99 % (3897538)CaDiCaL version: 2.1.3 % 255.93/36.99 % (3897538)Termination reason: Instruction limit % 255.93/36.99 % (3897538)Termination phase: Saturation % 255.93/36.99 % (3897538)Time elapsed: 3.168 s % 255.93/36.99 % (3897538)Peak memory usage: 218 MB % 255.93/36.99 % (3897538)Instructions burned: 6038 (million) % 255.93/36.99 % (3897547)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=3332446357:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2791 on theBenchmark for (2791ds/1083Mi) % 273.47/39.57 % (3897547)Instruction limit reached! % 273.47/39.57 % (3897547)------------------------------ % 273.47/39.57 % (3897547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897547)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897547)Termination reason: Instruction limit % 273.47/39.57 % (3897547)Termination phase: Saturation % 273.47/39.57 % (3897547)Time elapsed: 0.380 s % 273.47/39.57 % (3897547)Peak memory usage: 92 MB % 273.47/39.57 % (3897547)Instructions burned: 1084 (million) % 273.47/39.57 % (3897549)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3835077803:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2785 on theBenchmark for (2785ds/1084Mi) % 273.47/39.57 % (3897549)Instruction limit reached! % 273.47/39.57 % (3897549)------------------------------ % 273.47/39.57 % (3897549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897549)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897549)Termination reason: Instruction limit % 273.47/39.57 % (3897549)Termination phase: Saturation % 273.47/39.57 % (3897549)Time elapsed: 0.389 s % 273.47/39.57 % (3897549)Peak memory usage: 90 MB % 273.47/39.57 % (3897549)Instructions burned: 1087 (million) % 273.47/39.57 % (3897519)Instruction limit reached! % 273.47/39.57 % (3897519)------------------------------ % 273.47/39.57 % (3897519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897519)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897519)Termination reason: Instruction limit % 273.47/39.57 % (3897519)Termination phase: Saturation % 273.47/39.57 % (3897519)Time elapsed: 8.964 s % 273.47/39.57 % (3897519)Peak memory usage: 240 MB % 273.47/39.57 % (3897519)Instructions burned: 14123 (million) % 273.47/39.57 % (3897551)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3383118841:i=6995:s2at=5:gtg=all_2780 on theBenchmark for (2780ds/6995Mi) % 273.47/39.57 % (3897552)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3721314442:st=2:i=6225:sd=15:ss=axioms_2779 on theBenchmark for (2779ds/6225Mi) % 273.47/39.57 % (3897545)Instruction limit reached! % 273.47/39.57 % (3897545)------------------------------ % 273.47/39.57 % (3897545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897545)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897545)Termination reason: Instruction limit % 273.47/39.57 % (3897545)Termination phase: Saturation % 273.47/39.57 % (3897545)Time elapsed: 5.225 s % 273.47/39.57 % (3897545)Peak memory usage: 202 MB % 273.47/39.57 % (3897545)Instructions burned: 8328 (million) % 273.47/39.57 % (3897555)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3369146500:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2750 on theBenchmark for (2750ds/3372Mi) % 273.47/39.57 % (3897552)Instruction limit reached! % 273.47/39.57 % (3897552)------------------------------ % 273.47/39.57 % (3897552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897552)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897552)Termination reason: Instruction limit % 273.47/39.57 % (3897552)Termination phase: Saturation % 273.47/39.57 % (3897552)Time elapsed: 3.009 s % 273.47/39.57 % (3897552)Peak memory usage: 158 MB % 273.47/39.57 % (3897552)Instructions burned: 6227 (million) % 273.47/39.57 % (3897557)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2680883137:st=2.3:i=26457:sd=10:ss=included:sgt=8_2747 on theBenchmark for (2747ds/26457Mi) % 273.47/39.57 % (3897555)Refutation not found, incomplete strategy % 273.47/39.57 % (3897555)------------------------------ % 273.47/39.57 % (3897555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.47/39.57 % (3897555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.47/39.57 % (3897555)CaDiCaL version: 2.1.3 % 273.47/39.57 % (3897555)Termination reason: Refutation not found, incomplete strategy % 273.47/39.57 % (3897555)Time elapsed: 0.598 s % 273.47/39.57 % (3897555)Peak memory usage: 132 MB % 273.47/39.57 % (3897555)Instructions burned: 905 (million) % 289.67/41.76 % (3897555)------------------------------ % 289.67/41.76 % (3897555)------------------------------ % 289.67/41.76 % (3897559)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=95592718:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2740 on theBenchmark for (2740ds/13494Mi) % 289.67/41.76 % (3897551)Instruction limit reached! % 289.67/41.76 % (3897551)------------------------------ % 289.67/41.76 % (3897551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.67/41.76 % (3897551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.67/41.76 % (3897551)CaDiCaL version: 2.1.3 % 289.67/41.76 % (3897551)Termination reason: Instruction limit % 289.67/41.76 % (3897551)Termination phase: Saturation % 289.67/41.76 % (3897551)Time elapsed: 4.306 s % 289.67/41.76 % (3897551)Peak memory usage: 189 MB % 289.67/41.76 % (3897551)Instructions burned: 6995 (million) % 289.67/41.76 % (3897561)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=291699684:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2735 on theBenchmark for (2735ds/2503Mi) % 289.67/41.76 % (3897561)Instruction limit reached! % 289.67/41.76 % (3897561)------------------------------ % 289.67/41.76 % (3897561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.67/41.76 % (3897561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.67/41.76 % (3897561)CaDiCaL version: 2.1.3 % 289.67/41.76 % (3897561)Termination reason: Instruction limit % 289.67/41.76 % (3897561)Termination phase: Saturation % 289.67/41.76 % (3897561)Time elapsed: 1.679 s % 289.67/41.76 % (3897561)Peak memory usage: 146 MB % 289.67/41.76 % (3897561)Instructions burned: 2503 (million) % 289.67/41.76 % (3897541)Instruction limit reached! % 289.67/41.76 % (3897541)------------------------------ % 289.67/41.76 % (3897541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.67/41.76 % (3897541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.67/41.76 % (3897541)CaDiCaL version: 2.1.3 % 289.67/41.76 % (3897541)Termination reason: Instruction limit % 289.67/41.76 % (3897541)Termination phase: Saturation % 289.67/41.76 % (3897541)Time elapsed: 9.864 s % 289.67/41.76 % (3897541)Peak memory usage: 412 MB % 289.67/41.76 % (3897541)Instructions burned: 33339 (million) % 289.67/41.76 % (3897563)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=71407313:i=2559:sd=1:ep=RSTC:ss=axioms_2716 on theBenchmark for (2716ds/2559Mi) % 289.67/41.76 % (3897564)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1101265880:i=30753:av=off:ss=included_2715 on theBenchmark for (2715ds/30753Mi) % 289.67/41.76 % (3897563)Refutation not found, incomplete strategy % 289.67/41.76 % (3897563)------------------------------ % 289.67/41.76 % (3897563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.67/41.76 % (3897563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.67/41.76 % (3897563)CaDiCaL version: 2.1.3 % 289.67/41.76 % (3897563)Termination reason: Refutation not found, incomplete strategy % 289.67/41.76 % (3897563)Time elapsed: 0.588 s % 289.67/41.76 % (3897563)Peak memory usage: 131 MB % 289.67/41.76 % (3897563)Instructions burned: 887 (million) % 289.67/41.76 % (3897563)------------------------------ % 289.67/41.76 % (3897563)------------------------------ % 289.67/41.76 % (3897568)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2355924238:i=26473:ep=RSTC_2706 on theBenchmark for (2706ds/26473Mi) % 289.67/41.76 % (3897559)Instruction limit reached! % 289.67/41.76 % (3897559)------------------------------ % 289.67/41.76 % (3897559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.67/41.76 % (3897559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.67/41.76 % (3897559)CaDiCaL version: 2.1.3 % 289.67/41.76 % (3897559)Termination reason: Instruction limit % 289.67/41.76 % (3897559)Termination phase: Saturation % 289.67/41.76 % (3897559)Time elapsed: 8.095 s % 289.67/41.76 % (3897559)Peak memory usage: 259 MB % 289.67/41.76 % (3897559)Instructions burned: 13494 (million) % 289.67/41.76 % (3897570)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=148667839:cts=off:i=2759:kws=inv_arity:fgj=on_2657 on theBenchmark for (2657ds/2759Mi) % 289.67/41.76 % (3897570)Instruction limit reached! % 289.67/41.76 % (3897570)------------------------------ % 300.15/43.17 % (3897570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/43.17 % (3897570)CaDiCaL version: 2.1.3 % 300.15/43.17 % (3897570)Termination reason: Instruction limit % 300.15/43.17 % (3897570)Termination phase: Saturation % 300.15/43.17 % (3897570)Time elapsed: 1.732 s % 300.15/43.17 % (3897570)Peak memory usage: 154 MB % 300.15/43.17 % (3897570)Instructions burned: 2761 (million) % 300.15/43.17 % (3897572)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2915830403:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2638 on theBenchmark for (2638ds/5665Mi) % 300.15/43.17 % (3897572)Refutation not found, incomplete strategy % 300.15/43.17 % (3897572)------------------------------ % 300.15/43.17 % (3897572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/43.17 % (3897572)CaDiCaL version: 2.1.3 % 300.15/43.17 % (3897572)Termination reason: Refutation not found, incomplete strategy % 300.15/43.17 % (3897572)Time elapsed: 0.592 s % 300.15/43.17 % (3897572)Peak memory usage: 132 MB % 300.15/43.17 % (3897572)Instructions burned: 891 (million) % 300.15/43.17 % (3897572)------------------------------ % 300.15/43.17 % (3897572)------------------------------ % 300.15/43.17 % (3897574)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=561415097:i=1532:ep=RS:ss=axioms_2628 on theBenchmark for (2628ds/1532Mi) % 300.15/43.17 % (3897564)Instruction limit reached! % 300.15/43.17 % (3897564)------------------------------ % 300.15/43.17 % (3897564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/43.17 % (3897564)CaDiCaL version: 2.1.3 % 300.15/43.17 % (3897564)Termination reason: Instruction limit % 300.15/43.17 % (3897564)Termination phase: Saturation % 300.15/43.17 % (3897564)Time elapsed: 9.001 s % 300.15/43.17 % (3897564)Peak memory usage: 319 MB % 300.15/43.17 % (3897564)Instructions burned: 30757 (million) % 300.15/43.17 % (3897576)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=631421735:i=1565:sd=2:ss=axioms:sgt=32_2624 on theBenchmark for (2624ds/1565Mi) % 300.15/43.17 % (3897574)Refutation not found, incomplete strategy % 300.15/43.17 % (3897574)------------------------------ % 300.15/43.17 % (3897574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/43.17 % (3897574)CaDiCaL version: 2.1.3 % 300.15/43.17 % (3897574)Termination reason: Refutation not found, incomplete strategy % 300.15/43.17 % (3897574)Time elapsed: 0.594 s % 300.15/43.17 % (3897574)Peak memory usage: 132 MB % 300.15/43.17 % (3897574)Instructions burned: 893 (million) % 300.15/43.17 % (3897574)------------------------------ % 300.15/43.17 % (3897574)------------------------------ % 300.15/43.17 % (3897576)Instruction limit reached! % 300.15/43.17 % (3897576)------------------------------ % 300.15/43.17 % (3897576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/43.17 % (3897576)CaDiCaL version: 2.1.3 % 300.15/43.17 % (3897576)Termination reason: Instruction limit % 300.15/43.17 % (3897576)Termination phase: Saturation % 300.15/43.17 % (3897576)Time elapsed: 0.534 s % 300.15/43.17 % (3897576)Peak memory usage: 136 MB % 300.15/43.17 % (3897576)Instructions burned: 1567 (million) % 300.15/43.17 % (3897579)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2198065736:i=6052:sd=4:ss=axioms:sgt=24_2617 on theBenchmark for (2617ds/6052Mi) % 300.15/43.17 % (3897578)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=4116971939:i=1572:fgj=on:gsp=on_2618 on theBenchmark for (2618ds/1572Mi) % 300.15/43.17 % (3897579)Refutation not found, incomplete strategy % 300.15/43.17 % (3897579)------------------------------ % 300.15/43.17 % (3897579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.15/43.17 % (3897579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84 % 300.15/43.18 Terminated %------------------------------------------------------------------------------