%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : LCL421+2 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n017.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 11:52:22 AM UTC 2026 % Result : Timeout 300.29s 43.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL421+2 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.37 % Computer : n017.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 27 15:37:05 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.41 Running first-order theorem proving % 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 12.97/2.72 % (2752484)Detected formulas, will run a generic FOF schedule. % 12.97/2.72 % (2752494)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3253790013:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 12.97/2.72 % (2752493)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=812776763:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 12.97/2.72 % (2752489)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=2136246251:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 12.97/2.72 % (2752492)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1180409988:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 12.97/2.72 % (2752491)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=2886237790:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 12.97/2.72 % (2752490)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=2807065325:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 12.97/2.72 % (2752492)Refutation not found, incomplete strategy % 12.97/2.72 % (2752492)------------------------------ % 12.97/2.72 % (2752492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.97/2.72 % (2752492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.97/2.72 % (2752492)CaDiCaL version: 2.1.3 % 12.97/2.72 % (2752492)Termination reason: Refutation not found, incomplete strategy % 12.97/2.72 % (2752492)Time elapsed: 0.001 s % 12.97/2.72 % (2752492)Peak memory usage: 87 MB % 12.97/2.72 % (2752494)Instruction limit reached! % 12.97/2.72 % (2752494)------------------------------ % 12.97/2.72 % (2752494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.97/2.72 % (2752494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.97/2.72 % (2752494)CaDiCaL version: 2.1.3 % 12.97/2.72 % (2752494)Termination reason: Instruction limit % 12.97/2.72 % (2752494)Termination phase: Saturation % 12.97/2.72 % (2752494)Time elapsed: 0.048 s % 12.97/2.72 % (2752494)Peak memory usage: 88 MB % 12.97/2.72 % (2752494)Instructions burned: 140 (million) % 12.97/2.72 % (2752495)dis-21_1_sil=8000:lcm=predicate:random_seed=1437012107: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.97/2.72 % (2752493)Instruction limit reached! % 12.97/2.72 % (2752493)------------------------------ % 12.97/2.72 % (2752493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.97/2.72 % (2752493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.97/2.72 % (2752493)CaDiCaL version: 2.1.3 % 12.97/2.72 % (2752493)Termination reason: Instruction limit % 12.97/2.72 % (2752493)Termination phase: Saturation % 12.97/2.72 % (2752493)Time elapsed: 0.080 s % 12.97/2.72 % (2752493)Peak memory usage: 88 MB % 12.97/2.72 % (2752493)Instructions burned: 119 (million) % 12.97/2.72 % (2752502)lrs+10_1_sil=8000:sp=occurrence:random_seed=166065774:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 12.97/2.72 % (2752495)Instruction limit reached! % 12.97/2.72 % (2752495)------------------------------ % 12.97/2.72 % (2752495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.97/2.72 % (2752495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.97/2.72 % (2752495)CaDiCaL version: 2.1.3 % 12.97/2.72 % (2752495)Termination reason: Instruction limit % 12.97/2.72 % (2752495)Termination phase: Saturation % 12.97/2.72 % (2752495)Time elapsed: 0.084 s % 12.97/2.72 % (2752495)Peak memory usage: 89 MB % 12.97/2.72 % (2752495)Instructions burned: 130 (million) % 12.97/2.72 % (2752502)Instruction limit reached! % 12.97/2.72 % (2752502)------------------------------ % 12.97/2.72 % (2752502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.97/2.72 % (2752502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.97/2.72 % (2752502)CaDiCaL version: 2.1.3 % 12.97/2.72 % (2752502)Termination reason: Instruction limit % 12.97/2.72 % (2752502)Termination phase: Saturation % 12.97/2.72 % (2752502)Time elapsed: 0.098 s % 12.97/2.72 % (2752502)Peak memory usage: 90 MB % 12.97/2.72 % (2752502)Instructions burned: 286 (million) % 12.97/2.72 % (2752504)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2765273530:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 18.17/3.47 % (2752506)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1321177023:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 18.17/3.47 % (2752492)------------------------------ % 18.17/3.47 % (2752492)------------------------------ % 18.17/3.47 % (2752504)Instruction limit reached! % 18.17/3.47 % (2752504)------------------------------ % 18.17/3.47 % (2752504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.47 % (2752504)CaDiCaL version: 2.1.3 % 18.17/3.47 % (2752504)Termination reason: Instruction limit % 18.17/3.47 % (2752504)Termination phase: Saturation % 18.17/3.47 % (2752504)Time elapsed: 0.088 s % 18.17/3.47 % (2752504)Peak memory usage: 88 MB % 18.17/3.47 % (2752504)Instructions burned: 158 (million) % 18.17/3.47 % (2752507)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=1595513656:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 18.17/3.47 % (2752510)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1147395376:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 18.17/3.47 % (2752510)Refutation not found, incomplete strategy % 18.17/3.47 % (2752510)------------------------------ % 18.17/3.47 % (2752510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.47 % (2752510)CaDiCaL version: 2.1.3 % 18.17/3.47 % (2752510)Termination reason: Refutation not found, incomplete strategy % 18.17/3.47 % (2752510)Time elapsed: 0.001 s % 18.17/3.47 % (2752510)Peak memory usage: 87 MB % 18.17/3.47 % (2752507)Instruction limit reached! % 18.17/3.47 % (2752507)------------------------------ % 18.17/3.47 % (2752507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.47 % (2752507)CaDiCaL version: 2.1.3 % 18.17/3.47 % (2752507)Termination reason: Instruction limit % 18.17/3.47 % (2752507)Termination phase: Saturation % 18.17/3.47 % (2752507)Time elapsed: 0.073 s % 18.17/3.47 % (2752507)Peak memory usage: 88 MB % 18.17/3.47 % (2752507)Instructions burned: 249 (million) % 18.17/3.47 % (2752511)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=142505694:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 18.17/3.47 % (2752506)Instruction limit reached! % 18.17/3.47 % (2752506)------------------------------ % 18.17/3.47 % (2752506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.47 % (2752506)CaDiCaL version: 2.1.3 % 18.17/3.47 % (2752506)Termination reason: Instruction limit % 18.17/3.47 % (2752506)Termination phase: Saturation % 18.17/3.47 % (2752506)Time elapsed: 0.200 s % 18.17/3.47 % (2752506)Peak memory usage: 89 MB % 18.17/3.47 % (2752506)Instructions burned: 325 (million) % 18.17/3.47 % (2752514)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=200424307:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 18.17/3.47 % (2752514)Instruction limit reached! % 18.17/3.47 % (2752514)------------------------------ % 18.17/3.47 % (2752514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.17/3.47 % (2752514)CaDiCaL version: 2.1.3 % 18.17/3.47 % (2752514)Termination reason: Instruction limit % 18.17/3.47 % (2752514)Termination phase: Saturation % 18.17/3.47 % (2752514)Time elapsed: 0.034 s % 18.17/3.47 % (2752514)Peak memory usage: 88 MB % 18.17/3.47 % (2752514)Instructions burned: 114 (million) % 18.17/3.47 % (2752516)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1098800881:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 18.17/3.47 % (2752518)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1983853066:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 18.17/3.47 % (2752516)Instruction limit reached! % 18.17/3.47 % (2752516)------------------------------ % 18.17/3.47 % (2752516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.17/3.47 % (2752516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752516)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752516)Termination reason: Instruction limit % 44.18/7.09 % (2752516)Termination phase: Saturation % 44.18/7.09 % (2752516)Time elapsed: 0.071 s % 44.18/7.09 % (2752516)Peak memory usage: 87 MB % 44.18/7.09 % (2752516)Instructions burned: 128 (million) % 44.18/7.09 % (2752510)------------------------------ % 44.18/7.09 % (2752510)------------------------------ % 44.18/7.09 % (2752518)Instruction limit reached! % 44.18/7.09 % (2752518)------------------------------ % 44.18/7.09 % (2752518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.18/7.09 % (2752518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752518)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752518)Termination reason: Instruction limit % 44.18/7.09 % (2752518)Termination phase: Saturation % 44.18/7.09 % (2752518)Time elapsed: 0.034 s % 44.18/7.09 % (2752518)Peak memory usage: 88 MB % 44.18/7.09 % (2752518)Instructions burned: 116 (million) % 44.18/7.09 % (2752523)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4099785035:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 44.18/7.09 % (2752521)lrs+10_1_sil=8000:sp=occurrence:random_seed=2322587725:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi) % 44.18/7.09 % (2752522)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3510007974:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 44.18/7.09 % (2752522)Refutation not found, incomplete strategy % 44.18/7.09 % (2752522)------------------------------ % 44.18/7.09 % (2752522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.18/7.09 % (2752522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752522)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752522)Termination reason: Refutation not found, incomplete strategy % 44.18/7.09 % (2752522)Time elapsed: 0.001 s % 44.18/7.09 % (2752522)Peak memory usage: 88 MB % 44.18/7.09 % (2752522)------------------------------ % 44.18/7.09 % (2752522)------------------------------ % 44.18/7.09 % (2752527)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=417801558:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 44.18/7.09 % (2752527)Instruction limit reached! % 44.18/7.09 % (2752527)------------------------------ % 44.18/7.09 % (2752527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.18/7.09 % (2752527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752527)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752527)Termination reason: Instruction limit % 44.18/7.09 % (2752527)Termination phase: Saturation % 44.18/7.09 % (2752527)Time elapsed: 0.074 s % 44.18/7.09 % (2752527)Peak memory usage: 88 MB % 44.18/7.09 % (2752527)Instructions burned: 135 (million) % 44.18/7.09 % (2752521)Instruction limit reached! % 44.18/7.09 % (2752521)------------------------------ % 44.18/7.09 % (2752521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.18/7.09 % (2752521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752521)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752521)Termination reason: Instruction limit % 44.18/7.09 % (2752521)Termination phase: Saturation % 44.18/7.09 % (2752521)Time elapsed: 0.548 s % 44.18/7.09 % (2752521)Peak memory usage: 94 MB % 44.18/7.09 % (2752521)Instructions burned: 908 (million) % 44.18/7.09 % (2752529)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=715851244:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 44.18/7.09 % (2752529)Refutation not found, incomplete strategy % 44.18/7.09 % (2752529)------------------------------ % 44.18/7.09 % (2752529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.18/7.09 % (2752529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.18/7.09 % (2752529)CaDiCaL version: 2.1.3 % 44.18/7.09 % (2752529)Termination reason: Refutation not found, incomplete strategy % 44.18/7.09 % (2752529)Time elapsed: 0.001 s % 44.18/7.09 % (2752529)Peak memory usage: 88 MB % 44.18/7.09 % (2752530)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=602443420:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 44.18/7.09 % (2752529)------------------------------ % 44.18/7.09 % (2752529)------------------------------ % 44.18/7.09 % (2752533)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=935292833:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi) % 65.50/10.11 % (2752533)Instruction limit reached! % 65.50/10.11 % (2752533)------------------------------ % 65.50/10.11 % (2752533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752533)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752533)Termination reason: Instruction limit % 65.50/10.11 % (2752533)Termination phase: Saturation % 65.50/10.11 % (2752533)Time elapsed: 0.069 s % 65.50/10.11 % (2752533)Peak memory usage: 88 MB % 65.50/10.11 % (2752533)Instructions burned: 126 (million) % 65.50/10.11 % (2752511)Instruction limit reached! % 65.50/10.11 % (2752511)------------------------------ % 65.50/10.11 % (2752511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752511)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752511)Termination reason: Instruction limit % 65.50/10.11 % (2752511)Termination phase: Saturation % 65.50/10.11 % (2752511)Time elapsed: 1.393 s % 65.50/10.11 % (2752511)Peak memory usage: 143 MB % 65.50/10.11 % (2752511)Instructions burned: 2351 (million) % 65.50/10.11 % (2752535)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=858811820:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi) % 65.50/10.11 % (2752536)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4064538346:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 65.50/10.11 % (2752536)Refutation not found, incomplete strategy % 65.50/10.11 % (2752536)------------------------------ % 65.50/10.11 % (2752536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752536)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752536)Termination reason: Refutation not found, incomplete strategy % 65.50/10.11 % (2752536)Time elapsed: 0.001 s % 65.50/10.11 % (2752536)Peak memory usage: 88 MB % 65.50/10.11 % (2752535)Instruction limit reached! % 65.50/10.11 % (2752535)------------------------------ % 65.50/10.11 % (2752535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752535)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752535)Termination reason: Instruction limit % 65.50/10.11 % (2752535)Termination phase: Saturation % 65.50/10.11 % (2752535)Time elapsed: 0.067 s % 65.50/10.11 % (2752535)Peak memory usage: 90 MB % 65.50/10.11 % (2752535)Instructions burned: 134 (million) % 65.50/10.11 % (2752539)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2494824572:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 65.50/10.11 % (2752536)------------------------------ % 65.50/10.11 % (2752536)------------------------------ % 65.50/10.11 % (2752541)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=894894639:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi) % 65.50/10.11 % (2752539)Instruction limit reached! % 65.50/10.11 % (2752539)------------------------------ % 65.50/10.11 % (2752539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752539)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752539)Termination reason: Instruction limit % 65.50/10.11 % (2752539)Termination phase: Saturation % 65.50/10.11 % (2752539)Time elapsed: 0.243 s % 65.50/10.11 % (2752539)Peak memory usage: 90 MB % 65.50/10.11 % (2752539)Instructions burned: 432 (million) % 65.50/10.11 % (2752523)Instruction limit reached! % 65.50/10.11 % (2752523)------------------------------ % 65.50/10.11 % (2752523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.50/10.11 % (2752523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.50/10.11 % (2752523)CaDiCaL version: 2.1.3 % 65.50/10.11 % (2752523)Termination reason: Instruction limit % 65.50/10.11 % (2752523)Termination phase: Saturation % 65.50/10.11 % (2752523)Time elapsed: 1.711 s % 65.50/10.11 % (2752523)Peak memory usage: 167 MB % 65.50/10.11 % (2752523)Instructions burned: 5205 (million) % 65.50/10.11 % (2752543)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=210834761:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi) % 88.69/13.34 % (2752544)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3364073101:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi) % 88.69/13.34 % (2752543)Instruction limit reached! % 88.69/13.34 % (2752543)------------------------------ % 88.69/13.34 % (2752543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.69/13.34 % (2752543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.69/13.34 % (2752543)CaDiCaL version: 2.1.3 % 88.69/13.34 % (2752543)Termination reason: Instruction limit % 88.69/13.34 % (2752543)Termination phase: Saturation % 88.69/13.34 % (2752543)Time elapsed: 0.089 s % 88.69/13.34 % (2752543)Peak memory usage: 89 MB % 88.69/13.34 % (2752543)Instructions burned: 151 (million) % 88.69/13.34 % (2752547)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2946113099:i=667:av=off:fsr=off_2972 on theBenchmark for (2972ds/667Mi) % 88.69/13.34 % (2752547)Refutation not found, incomplete strategy % 88.69/13.34 % (2752547)------------------------------ % 88.69/13.34 % (2752547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.69/13.34 % (2752547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.69/13.34 % (2752547)CaDiCaL version: 2.1.3 % 88.69/13.34 % (2752547)Termination reason: Refutation not found, incomplete strategy % 88.69/13.34 % (2752547)Time elapsed: 0.001 s % 88.69/13.34 % (2752547)Peak memory usage: 87 MB % 88.69/13.34 % (2752547)------------------------------ % 88.69/13.34 % (2752547)------------------------------ % 88.69/13.34 % (2752549)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=2651495834:s2a=on:i=185:s2at=1.8:fdi=4_2969 on theBenchmark for (2969ds/185Mi) % 88.69/13.34 % (2752549)Instruction limit reached! % 88.69/13.34 % (2752549)------------------------------ % 88.69/13.34 % (2752549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.69/13.34 % (2752549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.69/13.34 % (2752549)CaDiCaL version: 2.1.3 % 88.69/13.34 % (2752549)Termination reason: Instruction limit % 88.69/13.34 % (2752549)Termination phase: Saturation % 88.69/13.34 % (2752549)Time elapsed: 0.099 s % 88.69/13.34 % (2752549)Peak memory usage: 89 MB % 88.69/13.34 % (2752549)Instructions burned: 185 (million) % 88.69/13.34 % (2752551)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2079076142:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi) % 88.69/13.34 % (2752551)Instruction limit reached! % 88.69/13.34 % (2752551)------------------------------ % 88.69/13.34 % (2752551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.69/13.34 % (2752551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.69/13.34 % (2752551)CaDiCaL version: 2.1.3 % 88.69/13.34 % (2752551)Termination reason: Instruction limit % 88.69/13.34 % (2752551)Termination phase: Saturation % 88.69/13.34 % (2752551)Time elapsed: 0.119 s % 88.69/13.34 % (2752551)Peak memory usage: 92 MB % 88.69/13.34 % (2752551)Instructions burned: 194 (million) % 88.69/13.34 % (2752553)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2005034196:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2964 on theBenchmark for (2964ds/4850Mi) % 88.69/13.34 % (2752541)Instruction limit reached! % 88.69/13.34 % (2752541)------------------------------ % 88.69/13.34 % (2752541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.69/13.34 % (2752541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.69/13.34 % (2752541)CaDiCaL version: 2.1.3 % 88.69/13.34 % (2752541)Termination reason: Instruction limit % 88.69/13.34 % (2752541)Termination phase: Saturation % 88.69/13.34 % (2752541)Time elapsed: 2.027 s % 88.69/13.34 % (2752541)Peak memory usage: 160 MB % 88.69/13.34 % (2752541)Instructions burned: 6060 (million) % 88.69/13.34 % (2752555)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1063268997:i=12111:sd=1:ss=included_2955 on theBenchmark for (2955ds/12111Mi) % 88.69/13.34 % (2752553)Instruction limit reached! % 88.69/13.34 % (2752553)------------------------------ % 126.36/18.61 % (2752553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752553)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752553)Termination reason: Instruction limit % 126.36/18.61 % (2752553)Termination phase: Saturation % 126.36/18.61 % (2752553)Time elapsed: 2.556 s % 126.36/18.61 % (2752553)Peak memory usage: 128 MB % 126.36/18.61 % (2752553)Instructions burned: 4851 (million) % 126.36/18.61 % (2752557)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3748889325:i=319:kws=precedence:fsr=off_2937 on theBenchmark for (2937ds/319Mi) % 126.36/18.61 % (2752557)Instruction limit reached! % 126.36/18.61 % (2752557)------------------------------ % 126.36/18.61 % (2752557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752557)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752557)Termination reason: Instruction limit % 126.36/18.61 % (2752557)Termination phase: Saturation % 126.36/18.61 % (2752557)Time elapsed: 0.183 s % 126.36/18.61 % (2752557)Peak memory usage: 92 MB % 126.36/18.61 % (2752557)Instructions burned: 320 (million) % 126.36/18.61 % (2752559)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3588814941:i=2064:ep=RST_2934 on theBenchmark for (2934ds/2064Mi) % 126.36/18.61 % (2752559)Refutation not found, incomplete strategy % 126.36/18.61 % (2752559)------------------------------ % 126.36/18.61 % (2752559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752559)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752559)Termination reason: Refutation not found, incomplete strategy % 126.36/18.61 % (2752559)Time elapsed: 0.001 s % 126.36/18.61 % (2752559)Peak memory usage: 88 MB % 126.36/18.61 % (2752559)------------------------------ % 126.36/18.61 % (2752559)------------------------------ % 126.36/18.61 % (2752561)dis-1011_128_sil=32000:random_seed=2476230511:i=3706:ep=RST:av=off_2930 on theBenchmark for (2930ds/3706Mi) % 126.36/18.61 % (2752555)Instruction limit reached! % 126.36/18.61 % (2752555)------------------------------ % 126.36/18.61 % (2752555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752555)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752555)Termination reason: Instruction limit % 126.36/18.61 % (2752555)Termination phase: Saturation % 126.36/18.61 % (2752555)Time elapsed: 3.650 s % 126.36/18.61 % (2752555)Peak memory usage: 236 MB % 126.36/18.61 % (2752555)Instructions burned: 12114 (million) % 126.36/18.61 % (2752563)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2414106367:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2917 on theBenchmark for (2917ds/757Mi) % 126.36/18.61 % (2752563)Refutation not found, incomplete strategy % 126.36/18.61 % (2752563)------------------------------ % 126.36/18.61 % (2752563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752563)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752563)Termination reason: Refutation not found, incomplete strategy % 126.36/18.61 % (2752563)Time elapsed: 0.0000 s % 126.36/18.61 % (2752563)Peak memory usage: 88 MB % 126.36/18.61 % (2752563)------------------------------ % 126.36/18.61 % (2752563)------------------------------ % 126.36/18.61 % (2752565)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2223333775:i=13913:ss=axioms:sgt=8_2915 on theBenchmark for (2915ds/13913Mi) % 126.36/18.61 % (2752561)Instruction limit reached! % 126.36/18.61 % (2752561)------------------------------ % 126.36/18.61 % (2752561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.36/18.61 % (2752561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.36/18.61 % (2752561)CaDiCaL version: 2.1.3 % 126.36/18.61 % (2752561)Termination reason: Instruction limit % 126.36/18.61 % (2752561)Termination phase: Saturation % 126.36/18.61 % (2752561)Time elapsed: 1.851 s % 126.36/18.61 % (2752561)Peak memory usage: 93 MB % 126.36/18.61 % (2752561)Instructions burned: 3707 (million) % 126.36/18.61 % (2752567)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2922705770:i=9925:aac=none_2910 on theBenchmark for (2910ds/9925Mi) % 126.36/18.61 % (2752530)Instruction limit reached! % 139.06/20.46 % (2752530)------------------------------ % 139.06/20.46 % (2752530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752530)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752530)Termination reason: Instruction limit % 139.06/20.46 % (2752530)Termination phase: Saturation % 139.06/20.46 % (2752530)Time elapsed: 7.669 s % 139.06/20.46 % (2752530)Peak memory usage: 242 MB % 139.06/20.46 % (2752530)Instructions burned: 13193 (million) % 139.06/20.46 % (2752569)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3073468712:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/2479Mi) % 139.06/20.46 % (2752569)Refutation not found, incomplete strategy % 139.06/20.46 % (2752569)------------------------------ % 139.06/20.46 % (2752569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752569)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752569)Termination reason: Refutation not found, incomplete strategy % 139.06/20.46 % (2752569)Time elapsed: 0.001 s % 139.06/20.46 % (2752569)Peak memory usage: 88 MB % 139.06/20.46 % (2752569)------------------------------ % 139.06/20.46 % (2752569)------------------------------ % 139.06/20.46 % (2752571)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=682766738:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2903 on theBenchmark for (2903ds/440Mi) % 139.06/20.46 % (2752571)Instruction limit reached! % 139.06/20.46 % (2752571)------------------------------ % 139.06/20.46 % (2752571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752571)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752571)Termination reason: Instruction limit % 139.06/20.46 % (2752571)Termination phase: Saturation % 139.06/20.46 % (2752571)Time elapsed: 0.246 s % 139.06/20.46 % (2752571)Peak memory usage: 90 MB % 139.06/20.46 % (2752571)Instructions burned: 440 (million) % 139.06/20.46 % (2752573)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3358705120:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/11145Mi) % 139.06/20.46 % (2752544)Instruction limit reached! % 139.06/20.46 % (2752544)------------------------------ % 139.06/20.46 % (2752544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752544)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752544)Termination reason: Instruction limit % 139.06/20.46 % (2752544)Termination phase: Saturation % 139.06/20.46 % (2752544)Time elapsed: 7.532 s % 139.06/20.46 % (2752544)Peak memory usage: 257 MB % 139.06/20.46 % (2752544)Instructions burned: 14156 (million) % 139.06/20.46 % (2752575)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=260543242:cts=off:i=3034:av=off:er=known:fsd=on_2897 on theBenchmark for (2897ds/3034Mi) % 139.06/20.46 % (2752575)Instruction limit reached! % 139.06/20.46 % (2752575)------------------------------ % 139.06/20.46 % (2752575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752575)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752575)Termination reason: Instruction limit % 139.06/20.46 % (2752575)Termination phase: Saturation % 139.06/20.46 % (2752575)Time elapsed: 1.725 s % 139.06/20.46 % (2752575)Peak memory usage: 144 MB % 139.06/20.46 % (2752575)Instructions burned: 3034 (million) % 139.06/20.46 % (2752577)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3340196889:st=2:s2a=on:i=524:s2at=2:ss=axioms_2879 on theBenchmark for (2879ds/524Mi) % 139.06/20.46 % (2752577)Instruction limit reached! % 139.06/20.46 % (2752577)------------------------------ % 139.06/20.46 % (2752577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.06/20.46 % (2752577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.06/20.46 % (2752577)CaDiCaL version: 2.1.3 % 139.06/20.46 % (2752577)Termination reason: Instruction limit % 139.06/20.46 % (2752577)Termination phase: Saturation % 139.06/20.46 % (2752577)Time elapsed: 0.283 s % 139.06/20.46 % (2752577)Peak memory usage: 90 MB % 139.06/20.46 % (2752577)Instructions burned: 524 (million) % 164.93/24.12 % (2752579)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3434835717:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2875 on theBenchmark for (2875ds/1016Mi) % 164.93/24.12 % (2752565)Instruction limit reached! % 164.93/24.12 % (2752565)------------------------------ % 164.93/24.12 % (2752565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2752565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2752565)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2752565)Termination reason: Instruction limit % 164.93/24.12 % (2752565)Termination phase: Saturation % 164.93/24.12 % (2752565)Time elapsed: 4.428 s % 164.93/24.12 % (2752565)Peak memory usage: 249 MB % 164.93/24.12 % (2752565)Instructions burned: 13913 (million) % 164.93/24.12 % (2752715)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3642740019:i=14123:bd=preordered:ins=4_2870 on theBenchmark for (2870ds/14123Mi) % 164.93/24.12 % (2752579)Instruction limit reached! % 164.93/24.12 % (2752579)------------------------------ % 164.93/24.12 % (2752579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2752579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2752579)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2752579)Termination reason: Instruction limit % 164.93/24.12 % (2752579)Termination phase: Saturation % 164.93/24.12 % (2752579)Time elapsed: 0.546 s % 164.93/24.12 % (2752579)Peak memory usage: 91 MB % 164.93/24.12 % (2752579)Instructions burned: 1016 (million) % 164.93/24.12 % (2752717)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1921990081:i=5781:kws=precedence:bd=all:rawr=on_2868 on theBenchmark for (2868ds/5781Mi) % 164.93/24.12 % (2752567)Instruction limit reached! % 164.93/24.12 % (2752567)------------------------------ % 164.93/24.12 % (2752567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2752567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2752567)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2752567)Termination reason: Instruction limit % 164.93/24.12 % (2752567)Termination phase: Saturation % 164.93/24.12 % (2752567)Time elapsed: 7.593 s % 164.93/24.12 % (2752567)Peak memory usage: 187 MB % 164.93/24.12 % (2752567)Instructions burned: 9925 (million) % 164.93/24.12 % (2753022)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=834290393:i=2448:gtgl=5:bd=preordered:gtg=all_2833 on theBenchmark for (2833ds/2448Mi) % 164.93/24.12 % (2752717)Instruction limit reached! % 164.93/24.12 % (2752717)------------------------------ % 164.93/24.12 % (2752717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2752717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2752717)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2752717)Termination reason: Instruction limit % 164.93/24.12 % (2752717)Termination phase: Saturation % 164.93/24.12 % (2752717)Time elapsed: 3.736 s % 164.93/24.12 % (2752717)Peak memory usage: 146 MB % 164.93/24.12 % (2752717)Instructions burned: 5781 (million) % 164.93/24.12 % (2752573)Instruction limit reached! % 164.93/24.12 % (2752573)------------------------------ % 164.93/24.12 % (2752573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2752573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2752573)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2752573)Termination reason: Instruction limit % 164.93/24.12 % (2752573)Termination phase: Saturation % 164.93/24.12 % (2752573)Time elapsed: 6.909 s % 164.93/24.12 % (2752573)Peak memory usage: 215 MB % 164.93/24.12 % (2752573)Instructions burned: 11146 (million) % 164.93/24.12 % (2753024)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2461497905:i=3223:kws=precedence:fgj=on:av=off_2829 on theBenchmark for (2829ds/3223Mi) % 164.93/24.12 % (2753025)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3904533261:st=5.6:i=2033:sd=3:ss=axioms_2829 on theBenchmark for (2829ds/2033Mi) % 164.93/24.12 % (2753025)Refutation not found, incomplete strategy % 164.93/24.12 % (2753025)------------------------------ % 164.93/24.12 % (2753025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.93/24.12 % (2753025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.93/24.12 % (2753025)CaDiCaL version: 2.1.3 % 164.93/24.12 % (2753025)Termination reason: Refutation not found, incomplete strategy % 240.73/34.79 % (2753025)Time elapsed: 0.565 s % 240.73/34.79 % (2753025)Peak memory usage: 127 MB % 240.73/34.79 % (2753025)Instructions burned: 855 (million) % 240.73/34.79 % (2753025)------------------------------ % 240.73/34.79 % (2753025)------------------------------ % 240.73/34.79 % (2753028)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=545163830:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2819 on theBenchmark for (2819ds/2055Mi) % 240.73/34.79 % (2753022)Instruction limit reached! % 240.73/34.79 % (2753022)------------------------------ % 240.73/34.79 % (2753022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.73/34.79 % (2753022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.73/34.79 % (2753022)CaDiCaL version: 2.1.3 % 240.73/34.79 % (2753022)Termination reason: Instruction limit % 240.73/34.79 % (2753022)Termination phase: Saturation % 240.73/34.79 % (2753022)Time elapsed: 1.464 s % 240.73/34.79 % (2753022)Peak memory usage: 141 MB % 240.73/34.79 % (2753022)Instructions burned: 2448 (million) % 240.73/34.79 % (2752715)Instruction limit reached! % 240.73/34.79 % (2752715)------------------------------ % 240.73/34.79 % (2752715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.73/34.79 % (2752715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.73/34.79 % (2752715)CaDiCaL version: 2.1.3 % 240.73/34.79 % (2752715)Termination reason: Instruction limit % 240.73/34.79 % (2752715)Termination phase: Saturation % 240.73/34.79 % (2752715)Time elapsed: 5.210 s % 240.73/34.79 % (2752715)Peak memory usage: 244 MB % 240.73/34.79 % (2752715)Instructions burned: 14124 (million) % 240.73/34.79 % (2753030)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=3604871311:i=21611:sd=3:ss=axioms_2817 on theBenchmark for (2817ds/21611Mi) % 240.73/34.79 % (2753031)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2854159284:i=4835:sd=13:ss=axioms:sgt=23_2816 on theBenchmark for (2816ds/4835Mi) % 240.73/34.79 % (2753024)Instruction limit reached! % 240.73/34.79 % (2753024)------------------------------ % 240.73/34.79 % (2753024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.73/34.79 % (2753024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.73/34.79 % (2753024)CaDiCaL version: 2.1.3 % 240.73/34.79 % (2753024)Termination reason: Instruction limit % 240.73/34.79 % (2753024)Termination phase: Saturation % 240.73/34.79 % (2753024)Time elapsed: 1.755 s % 240.73/34.79 % (2753024)Peak memory usage: 148 MB % 240.73/34.79 % (2753024)Instructions burned: 3226 (million) % 240.73/34.79 % (2753034)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=1919762146:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2810 on theBenchmark for (2810ds/797Mi) % 240.73/34.79 % (2753028)Instruction limit reached! % 240.73/34.79 % (2753028)------------------------------ % 240.73/34.79 % (2753028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.73/34.79 % (2753028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.73/34.79 % (2753028)CaDiCaL version: 2.1.3 % 240.73/34.79 % (2753028)Termination reason: Instruction limit % 240.73/34.79 % (2753028)Termination phase: Saturation % 240.73/34.79 % (2753028)Time elapsed: 1.317 s % 240.73/34.79 % (2753028)Peak memory usage: 139 MB % 240.73/34.79 % (2753028)Instructions burned: 2056 (million) % 240.73/34.79 % (2753034)Instruction limit reached! % 240.73/34.79 % (2753034)------------------------------ % 240.73/34.79 % (2753034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.73/34.79 % (2753034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.73/34.79 % (2753034)CaDiCaL version: 2.1.3 % 240.73/34.79 % (2753034)Termination reason: Instruction limit % 240.73/34.79 % (2753034)Termination phase: Saturation % 240.73/34.79 % (2753034)Time elapsed: 0.505 s % 240.73/34.79 % (2753034)Peak memory usage: 92 MB % 240.73/34.79 % (2753034)Instructions burned: 797 (million) % 240.73/34.79 % (2753036)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2210730082:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2805 on theBenchmark for (2805ds/2326Mi) % 240.73/34.79 % (2753036)Refutation not found, incomplete strategy % 240.73/34.79 % (2753036)------------------------------ % 240.73/34.79 % (2753036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07Terminated %------------------------------------------------------------------------------