%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW943+1 : 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 : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:38:04 PM UTC 2026 % Result : Timeout 293.64s 42.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW943+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 14:46:34 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.12 Running first-order theorem proving % 0.09/0.12 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 % 8.22/1.66 % (3428964)Detected formulas, will run a generic FOF schedule. % 8.22/1.66 % (3428970)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=1085689098:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 8.22/1.66 % (3428972)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=842192806:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 8.22/1.66 % (3428974)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3752380776:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 8.22/1.66 % (3428971)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=3358079909:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 8.22/1.66 % (3428969)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=3063449446:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 8.22/1.66 % (3428973)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2833884369:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 8.22/1.66 % (3428975)dis-21_1_sil=8000:lcm=predicate:random_seed=4033931371: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) % 8.22/1.66 % (3428973)Refutation not found, incomplete strategy % 8.22/1.66 % (3428973)------------------------------ % 8.22/1.66 % (3428973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.22/1.66 % (3428972)Refutation not found, incomplete strategy % 8.22/1.66 % (3428972)------------------------------ % 8.22/1.66 % (3428972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.22/1.66 % (3428973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.22/1.66 % (3428972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.22/1.66 % (3428973)CaDiCaL version: 2.1.3 % 8.22/1.66 % (3428973)Termination reason: Refutation not found, incomplete strategy % 8.22/1.66 % (3428973)Time elapsed: 0.001 s % 8.22/1.66 % (3428972)CaDiCaL version: 2.1.3 % 8.22/1.66 % (3428972)Termination reason: Refutation not found, incomplete strategy % 8.22/1.66 % (3428972)Time elapsed: 0.0000 s % 8.22/1.66 % (3428973)Peak memory usage: 87 MB % 8.22/1.66 % (3428972)Peak memory usage: 87 MB % 8.22/1.66 % (3428975)Refutation not found, incomplete strategy % 8.22/1.66 % (3428975)------------------------------ % 8.22/1.66 % (3428975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.22/1.66 % (3428975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.22/1.66 % (3428975)CaDiCaL version: 2.1.3 % 8.22/1.66 % (3428975)Termination reason: Refutation not found, incomplete strategy % 8.22/1.66 % (3428975)Time elapsed: 0.002 s % 8.22/1.66 % (3428975)Peak memory usage: 88 MB % 8.22/1.66 % (3428975)Instructions burned: 4 (million) % 8.22/1.66 % (3428974)Instruction limit reached! % 8.22/1.66 % (3428974)------------------------------ % 8.22/1.66 % (3428974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.22/1.66 % (3428974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.22/1.66 % (3428974)CaDiCaL version: 2.1.3 % 8.22/1.66 % (3428974)Termination reason: Instruction limit % 8.22/1.66 % (3428974)Termination phase: Saturation % 8.22/1.66 % (3428974)Time elapsed: 0.038 s % 8.22/1.66 % (3428974)Peak memory usage: 88 MB % 8.22/1.66 % (3428974)Instructions burned: 140 (million) % 8.22/1.66 % (3428975)------------------------------ % 8.22/1.66 % (3428975)------------------------------ % 8.22/1.66 % (3428972)------------------------------ % 8.22/1.66 % (3428972)------------------------------ % 8.22/1.66 % (3428973)------------------------------ % 8.22/1.66 % (3428973)------------------------------ % 8.22/1.66 % (3428983)lrs+10_1_sil=8000:sp=occurrence:random_seed=2990989508:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 8.22/1.66 % (3428983)Instruction limit reached! % 8.22/1.66 % (3428983)------------------------------ % 8.22/1.66 % (3428983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.22/1.66 % (3428983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.22/1.66 % (3428983)CaDiCaL version: 2.1.3 % 8.22/1.66 % (3428983)Termination reason: Instruction limit % 13.72/2.33 % (3428983)Termination phase: Saturation % 13.72/2.33 % (3428983)Time elapsed: 0.082 s % 13.72/2.33 % (3428983)Peak memory usage: 90 MB % 13.72/2.33 % (3428983)Instructions burned: 289 (million) % 13.72/2.33 % (3428985)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2903481919:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 13.72/2.33 % (3428984)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1045715269:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 13.72/2.33 % (3428986)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=1140874341:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 13.72/2.33 % (3428984)Instruction limit reached! % 13.72/2.33 % (3428984)------------------------------ % 13.72/2.33 % (3428984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.72/2.33 % (3428984)CaDiCaL version: 2.1.3 % 13.72/2.33 % (3428984)Termination reason: Instruction limit % 13.72/2.33 % (3428984)Termination phase: Saturation % 13.72/2.33 % (3428984)Time elapsed: 0.047 s % 13.72/2.33 % (3428984)Peak memory usage: 88 MB % 13.72/2.33 % (3428984)Instructions burned: 160 (million) % 13.72/2.33 % (3428986)Instruction limit reached! % 13.72/2.33 % (3428986)------------------------------ % 13.72/2.33 % (3428986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.72/2.33 % (3428986)CaDiCaL version: 2.1.3 % 13.72/2.33 % (3428986)Termination reason: Instruction limit % 13.72/2.33 % (3428986)Termination phase: Saturation % 13.72/2.33 % (3428986)Time elapsed: 0.074 s % 13.72/2.33 % (3428986)Peak memory usage: 89 MB % 13.72/2.33 % (3428986)Instructions burned: 252 (million) % 13.72/2.33 % (3428985)Instruction limit reached! % 13.72/2.33 % (3428985)------------------------------ % 13.72/2.33 % (3428985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.72/2.33 % (3428985)CaDiCaL version: 2.1.3 % 13.72/2.33 % (3428985)Termination reason: Instruction limit % 13.72/2.33 % (3428985)Termination phase: Saturation % 13.72/2.33 % (3428985)Time elapsed: 0.083 s % 13.72/2.33 % (3428985)Peak memory usage: 88 MB % 13.72/2.33 % (3428985)Instructions burned: 328 (million) % 13.72/2.33 % (3428988)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=147637311:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 13.72/2.33 % (3428988)Refutation not found, incomplete strategy % 13.72/2.33 % (3428988)------------------------------ % 13.72/2.33 % (3428988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.72/2.33 % (3428988)CaDiCaL version: 2.1.3 % 13.72/2.33 % (3428988)Termination reason: Refutation not found, incomplete strategy % 13.72/2.33 % (3428988)Time elapsed: 0.002 s % 13.72/2.33 % (3428988)Peak memory usage: 88 MB % 13.72/2.33 % (3428988)Instructions burned: 3 (million) % 13.72/2.33 % (3428992)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2944717379:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 13.72/2.33 % (3428993)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=658755389:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 13.72/2.33 % (3428994)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=599061604:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 13.72/2.33 % (3428994)Refutation not found, incomplete strategy % 13.72/2.33 % (3428994)------------------------------ % 13.72/2.33 % (3428994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.72/2.33 % (3428994)CaDiCaL version: 2.1.3 % 13.72/2.33 % (3428994)Termination reason: Refutation not found, incomplete strategy % 13.72/2.33 % (3428994)Time elapsed: 0.001 s % 13.72/2.33 % (3428994)Peak memory usage: 88 MB % 13.72/2.33 % (3428994)Instructions burned: 2 (million) % 13.72/2.33 % (3428993)Instruction limit reached! % 13.72/2.33 % (3428993)------------------------------ % 13.72/2.33 % (3428993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.72/2.33 % (3428993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3428993)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3428993)Termination reason: Instruction limit % 23.14/3.69 % (3428993)Termination phase: Saturation % 23.14/3.69 % (3428993)Time elapsed: 0.031 s % 23.14/3.69 % (3428993)Peak memory usage: 89 MB % 23.14/3.69 % (3428993)Instructions burned: 116 (million) % 23.14/3.69 % (3428988)------------------------------ % 23.14/3.69 % (3428988)------------------------------ % 23.14/3.69 % (3428999)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1394716457:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 23.14/3.69 % (3428994)------------------------------ % 23.14/3.69 % (3428994)------------------------------ % 23.14/3.69 % (3428999)Instruction limit reached! % 23.14/3.69 % (3428999)------------------------------ % 23.14/3.69 % (3428999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.14/3.69 % (3428999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3428999)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3428999)Termination reason: Instruction limit % 23.14/3.69 % (3428999)Termination phase: Saturation % 23.14/3.69 % (3428999)Time elapsed: 0.031 s % 23.14/3.69 % (3428999)Peak memory usage: 88 MB % 23.14/3.69 % (3428999)Instructions burned: 115 (million) % 23.14/3.69 % (3429000)lrs+10_1_sil=8000:sp=occurrence:random_seed=1216860991:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 23.14/3.69 % (3429002)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2545779619:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 23.14/3.69 % (3429002)Refutation not found, incomplete strategy % 23.14/3.69 % (3429002)------------------------------ % 23.14/3.69 % (3429002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.14/3.69 % (3429002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3429002)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3429002)Termination reason: Refutation not found, incomplete strategy % 23.14/3.69 % (3429002)Time elapsed: 0.001 s % 23.14/3.69 % (3429002)Peak memory usage: 88 MB % 23.14/3.69 % (3429002)Instructions burned: 3 (million) % 23.14/3.69 % (3429003)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3787810307:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi) % 23.14/3.69 % (3429000)Instruction limit reached! % 23.14/3.69 % (3429000)------------------------------ % 23.14/3.69 % (3429000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.14/3.69 % (3429000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3429000)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3429000)Termination reason: Instruction limit % 23.14/3.69 % (3429000)Termination phase: Saturation % 23.14/3.69 % (3429000)Time elapsed: 0.205 s % 23.14/3.69 % (3429000)Peak memory usage: 89 MB % 23.14/3.69 % (3429000)Instructions burned: 908 (million) % 23.14/3.69 % (3429002)------------------------------ % 23.14/3.69 % (3429002)------------------------------ % 23.14/3.69 % (3429007)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3325641875:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 23.14/3.69 % (3429007)Refutation not found, incomplete strategy % 23.14/3.69 % (3429007)------------------------------ % 23.14/3.69 % (3429007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.14/3.69 % (3429007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3429007)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3429007)Termination reason: Refutation not found, incomplete strategy % 23.14/3.69 % (3429007)Time elapsed: 0.003 s % 23.14/3.69 % (3429007)Peak memory usage: 89 MB % 23.14/3.69 % (3429007)Instructions burned: 6 (million) % 23.14/3.69 % (3429008)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3017189980:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi) % 23.14/3.69 % (3429007)------------------------------ % 23.14/3.69 % (3429007)------------------------------ % 23.14/3.69 % (3429008)Instruction limit reached! % 23.14/3.69 % (3429008)------------------------------ % 23.14/3.69 % (3429008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.14/3.69 % (3429008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.14/3.69 % (3429008)CaDiCaL version: 2.1.3 % 23.14/3.69 % (3429008)Termination reason: Instruction limit % 23.14/3.69 % (3429008)Termination phase: Saturation % 23.14/3.69 % (3429008)Time elapsed: 0.133 s % 37.64/5.77 % (3429008)Peak memory usage: 89 MB % 37.64/5.77 % (3429008)Instructions burned: 593 (million) % 37.64/5.77 % (3428992)Instruction limit reached! % 37.64/5.77 % (3428992)------------------------------ % 37.64/5.77 % (3428992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.64/5.77 % (3428992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.64/5.77 % (3428992)CaDiCaL version: 2.1.3 % 37.64/5.77 % (3428992)Termination reason: Instruction limit % 37.64/5.77 % (3428992)Termination phase: Saturation % 37.64/5.77 % (3428992)Time elapsed: 0.816 s % 37.64/5.77 % (3428992)Peak memory usage: 140 MB % 37.64/5.77 % (3428992)Instructions burned: 2352 (million) % 37.64/5.77 % (3429011)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=745342073:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 37.64/5.77 % (3429012)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=1149668009:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 37.64/5.77 % (3429012)Instruction limit reached! % 37.64/5.77 % (3429012)------------------------------ % 37.64/5.77 % (3429012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.64/5.77 % (3429012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.64/5.77 % (3429012)CaDiCaL version: 2.1.3 % 37.64/5.77 % (3429012)Termination reason: Instruction limit % 37.64/5.77 % (3429012)Termination phase: Saturation % 37.64/5.77 % (3429012)Time elapsed: 0.041 s % 37.64/5.77 % (3429012)Peak memory usage: 91 MB % 37.64/5.77 % (3429012)Instructions burned: 125 (million) % 37.64/5.77 % (3429013)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4194803116:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi) % 37.64/5.77 % (3429013)Instruction limit reached! % 37.64/5.77 % (3429013)------------------------------ % 37.64/5.77 % (3429013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.64/5.77 % (3429013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.64/5.77 % (3429013)CaDiCaL version: 2.1.3 % 37.64/5.77 % (3429013)Termination reason: Instruction limit % 37.64/5.77 % (3429013)Termination phase: Saturation % 37.64/5.77 % (3429013)Time elapsed: 0.042 s % 37.64/5.77 % (3429013)Peak memory usage: 90 MB % 37.64/5.77 % (3429013)Instructions burned: 135 (million) % 37.64/5.77 % (3429016)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=743992259:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/141Mi) % 37.64/5.77 % (3429016)Refutation not found, incomplete strategy % 37.64/5.77 % (3429016)------------------------------ % 37.64/5.77 % (3429016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.64/5.77 % (3429016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.64/5.77 % (3429016)CaDiCaL version: 2.1.3 % 37.64/5.77 % (3429016)Termination reason: Refutation not found, incomplete strategy % 37.64/5.77 % (3429016)Time elapsed: 0.001 s % 37.64/5.77 % (3429016)Peak memory usage: 88 MB % 37.64/5.77 % (3429016)Instructions burned: 1 (million) % 37.64/5.77 % (3429018)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2226166162:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi) % 37.64/5.77 % (3429018)Refutation not found, incomplete strategy % 37.64/5.77 % (3429018)------------------------------ % 37.64/5.77 % (3429018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.64/5.77 % (3429018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.64/5.77 % (3429018)CaDiCaL version: 2.1.3 % 37.64/5.77 % (3429018)Termination reason: Refutation not found, incomplete strategy % 37.64/5.77 % (3429018)Time elapsed: 0.001 s % 37.64/5.77 % (3429018)Peak memory usage: 88 MB % 37.64/5.77 % (3429018)Instructions burned: 2 (million) % 37.64/5.77 % (3429016)------------------------------ % 37.64/5.77 % (3429016)------------------------------ % 37.64/5.77 % (3429018)------------------------------ % 37.64/5.77 % (3429018)------------------------------ % 37.64/5.77 % (3429021)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=3203821726:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi) % 37.64/5.77 % (3429022)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=741626795:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi) % 52.33/7.94 % (3429022)Instruction limit reached! % 52.33/7.94 % (3429022)------------------------------ % 52.33/7.94 % (3429022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.33/7.94 % (3429022)CaDiCaL version: 2.1.3 % 52.33/7.94 % (3429022)Termination reason: Instruction limit % 52.33/7.94 % (3429022)Termination phase: Saturation % 52.33/7.94 % (3429022)Time elapsed: 0.033 s % 52.33/7.94 % (3429022)Peak memory usage: 88 MB % 52.33/7.94 % (3429022)Instructions burned: 154 (million) % 52.33/7.94 % (3429025)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1031939233:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi) % 52.33/7.94 % (3429003)Instruction limit reached! % 52.33/7.94 % (3429003)------------------------------ % 52.33/7.94 % (3429003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.33/7.94 % (3429003)CaDiCaL version: 2.1.3 % 52.33/7.94 % (3429003)Termination reason: Instruction limit % 52.33/7.94 % (3429003)Termination phase: Saturation % 52.33/7.94 % (3429003)Time elapsed: 1.567 s % 52.33/7.94 % (3429003)Peak memory usage: 148 MB % 52.33/7.94 % (3429003)Instructions burned: 5205 (million) % 52.33/7.94 % (3429027)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3568062578:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi) % 52.33/7.94 % (3429027)Refutation not found, incomplete strategy % 52.33/7.94 % (3429027)------------------------------ % 52.33/7.94 % (3429027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.33/7.94 % (3429027)CaDiCaL version: 2.1.3 % 52.33/7.94 % (3429027)Termination reason: Refutation not found, incomplete strategy % 52.33/7.94 % (3429027)Time elapsed: 0.001 s % 52.33/7.94 % (3429027)Peak memory usage: 88 MB % 52.33/7.94 % (3429027)Instructions burned: 2 (million) % 52.33/7.94 % (3429027)------------------------------ % 52.33/7.94 % (3429027)------------------------------ % 52.33/7.94 % (3429029)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=3816597879:s2a=on:i=185:s2at=1.8:fdi=4_2972 on theBenchmark for (2972ds/185Mi) % 52.33/7.94 % (3429029)Instruction limit reached! % 52.33/7.94 % (3429029)------------------------------ % 52.33/7.94 % (3429029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.33/7.94 % (3429029)CaDiCaL version: 2.1.3 % 52.33/7.94 % (3429029)Termination reason: Instruction limit % 52.33/7.94 % (3429029)Termination phase: Saturation % 52.33/7.94 % (3429029)Time elapsed: 0.051 s % 52.33/7.94 % (3429029)Peak memory usage: 90 MB % 52.33/7.94 % (3429029)Instructions burned: 187 (million) % 52.33/7.94 % (3429031)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1117591484:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/193Mi) % 52.33/7.94 % (3429031)Refutation not found, incomplete strategy % 52.33/7.94 % (3429031)------------------------------ % 52.33/7.94 % (3429031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.33/7.94 % (3429031)CaDiCaL version: 2.1.3 % 52.33/7.94 % (3429031)Termination reason: Refutation not found, incomplete strategy % 52.33/7.94 % (3429031)Time elapsed: 0.001 s % 52.33/7.94 % (3429031)Peak memory usage: 88 MB % 52.33/7.94 % (3429031)------------------------------ % 52.33/7.94 % (3429031)------------------------------ % 52.33/7.94 % (3429033)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2318907522:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2967 on theBenchmark for (2967ds/4850Mi) % 52.33/7.94 % (3429033)Refutation not found, incomplete strategy % 52.33/7.94 % (3429033)------------------------------ % 52.33/7.94 % (3429033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.33/7.94 % (3429033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429033)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429033)Termination reason: Refutation not found, incomplete strategy % 67.37/9.90 % (3429033)Time elapsed: 0.001 s % 67.37/9.90 % (3429033)Peak memory usage: 88 MB % 67.37/9.90 % (3429033)Instructions burned: 1 (million) % 67.37/9.90 % (3429033)------------------------------ % 67.37/9.90 % (3429033)------------------------------ % 67.37/9.90 % (3429035)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3921668783:i=12111:sd=1:ss=included_2964 on theBenchmark for (2964ds/12111Mi) % 67.37/9.90 % (3429021)Instruction limit reached! % 67.37/9.90 % (3429021)------------------------------ % 67.37/9.90 % (3429021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.37/9.90 % (3429021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429021)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429021)Termination reason: Instruction limit % 67.37/9.90 % (3429021)Termination phase: Saturation % 67.37/9.90 % (3429021)Time elapsed: 1.924 s % 67.37/9.90 % (3429021)Peak memory usage: 154 MB % 67.37/9.90 % (3429021)Instructions burned: 6062 (million) % 67.37/9.90 % (3429037)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4061675512:i=319:kws=precedence:fsr=off_2961 on theBenchmark for (2961ds/319Mi) % 67.37/9.90 % (3429037)Instruction limit reached! % 67.37/9.90 % (3429037)------------------------------ % 67.37/9.90 % (3429037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.37/9.90 % (3429037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429037)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429037)Termination reason: Instruction limit % 67.37/9.90 % (3429037)Termination phase: Saturation % 67.37/9.90 % (3429037)Time elapsed: 0.068 s % 67.37/9.90 % (3429037)Peak memory usage: 88 MB % 67.37/9.90 % (3429037)Instructions burned: 324 (million) % 67.37/9.90 % (3429039)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=781716443:i=2064:ep=RST_2959 on theBenchmark for (2959ds/2064Mi) % 67.37/9.90 % (3429039)Instruction limit reached! % 67.37/9.90 % (3429039)------------------------------ % 67.37/9.90 % (3429039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.37/9.90 % (3429039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429039)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429039)Termination reason: Instruction limit % 67.37/9.90 % (3429039)Termination phase: Saturation % 67.37/9.90 % (3429039)Time elapsed: 0.425 s % 67.37/9.90 % (3429039)Peak memory usage: 90 MB % 67.37/9.90 % (3429039)Instructions burned: 2064 (million) % 67.37/9.90 % (3429041)dis-1011_128_sil=32000:random_seed=576627741:i=3706:ep=RST:av=off_2954 on theBenchmark for (2954ds/3706Mi) % 67.37/9.90 % (3429011)Instruction limit reached! % 67.37/9.90 % (3429011)------------------------------ % 67.37/9.90 % (3429011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.37/9.90 % (3429011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429011)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429011)Termination reason: Instruction limit % 67.37/9.90 % (3429011)Termination phase: Saturation % 67.37/9.90 % (3429011)Time elapsed: 3.298 s % 67.37/9.90 % (3429011)Peak memory usage: 143 MB % 67.37/9.90 % (3429011)Instructions burned: 13195 (million) % 67.37/9.90 % (3429043)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1199212080:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2952 on theBenchmark for (2952ds/757Mi) % 67.37/9.90 % (3429043)Refutation not found, incomplete strategy % 67.37/9.90 % (3429043)------------------------------ % 67.37/9.90 % (3429043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.37/9.90 % (3429043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.37/9.90 % (3429043)CaDiCaL version: 2.1.3 % 67.37/9.90 % (3429043)Termination reason: Refutation not found, incomplete strategy % 67.37/9.90 % (3429043)Time elapsed: 0.001 s % 67.37/9.90 % (3429043)Peak memory usage: 88 MB % 67.37/9.90 % (3429043)Instructions burned: 2 (million) % 67.37/9.90 % (3429043)------------------------------ % 67.37/9.90 % (3429043)------------------------------ % 67.37/9.90 % (3429045)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1151613911:i=13913:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/13913Mi) % 67.37/9.90 % (3429041)Instruction limit reached! % 67.37/9.90 % (3429041)------------------------------ % 67.37/9.90 % (3429041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429041)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429041)Termination reason: Instruction limit % 71.84/10.63 % (3429041)Termination phase: Saturation % 71.84/10.63 % (3429041)Time elapsed: 0.725 s % 71.84/10.63 % (3429041)Peak memory usage: 89 MB % 71.84/10.63 % (3429041)Instructions burned: 3708 (million) % 71.84/10.63 % (3429047)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=391805372:i=9925:aac=none_2945 on theBenchmark for (2945ds/9925Mi) % 71.84/10.63 % (3429025)Instruction limit reached! % 71.84/10.63 % (3429025)------------------------------ % 71.84/10.63 % (3429025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429025)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429025)Termination reason: Instruction limit % 71.84/10.63 % (3429025)Termination phase: Saturation % 71.84/10.63 % (3429025)Time elapsed: 4.260 s % 71.84/10.63 % (3429025)Peak memory usage: 171 MB % 71.84/10.63 % (3429025)Instructions burned: 14157 (million) % 71.84/10.63 % (3429049)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2744576355:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2935 on theBenchmark for (2935ds/2479Mi) % 71.84/10.63 % (3429049)Refutation not found, incomplete strategy % 71.84/10.63 % (3429049)------------------------------ % 71.84/10.63 % (3429049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429049)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429049)Termination reason: Refutation not found, incomplete strategy % 71.84/10.63 % (3429049)Time elapsed: 0.001 s % 71.84/10.63 % (3429049)Peak memory usage: 88 MB % 71.84/10.63 % (3429049)------------------------------ % 71.84/10.63 % (3429049)------------------------------ % 71.84/10.63 % (3429051)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2462020554:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2932 on theBenchmark for (2932ds/440Mi) % 71.84/10.63 % (3429035)Instruction limit reached! % 71.84/10.63 % (3429035)------------------------------ % 71.84/10.63 % (3429035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429035)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429035)Termination reason: Instruction limit % 71.84/10.63 % (3429035)Termination phase: Saturation % 71.84/10.63 % (3429035)Time elapsed: 3.325 s % 71.84/10.63 % (3429035)Peak memory usage: 184 MB % 71.84/10.63 % (3429035)Instructions burned: 12115 (million) % 71.84/10.63 % (3429051)Instruction limit reached! % 71.84/10.63 % (3429051)------------------------------ % 71.84/10.63 % (3429051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429051)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429051)Termination reason: Instruction limit % 71.84/10.63 % (3429051)Termination phase: Saturation % 71.84/10.63 % (3429051)Time elapsed: 0.137 s % 71.84/10.63 % (3429051)Peak memory usage: 93 MB % 71.84/10.63 % (3429051)Instructions burned: 440 (million) % 71.84/10.63 % (3429053)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=417365171:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2930 on theBenchmark for (2930ds/11145Mi) % 71.84/10.63 % (3429054)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=461615956:cts=off:i=3034:av=off:er=known:fsd=on_2929 on theBenchmark for (2929ds/3034Mi) % 71.84/10.63 % (3429053)Refutation not found, incomplete strategy % 71.84/10.63 % (3429053)------------------------------ % 71.84/10.63 % (3429053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.84/10.63 % (3429053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.84/10.63 % (3429053)CaDiCaL version: 2.1.3 % 71.84/10.63 % (3429053)Termination reason: Refutation not found, incomplete strategy % 71.84/10.63 % (3429053)Time elapsed: 0.367 s % 71.84/10.63 % (3429053)Peak memory usage: 129 MB % 71.84/10.63 % (3429053)Instructions burned: 1010 (million) % 71.84/10.63 % (3429053)------------------------------ % 71.84/10.63 % (3429053)------------------------------ % 75.39/11.08 % (3429057)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=44042645:st=2:s2a=on:i=524:s2at=2:ss=axioms_2923 on theBenchmark for (2923ds/524Mi) % 75.39/11.08 % (3429057)Instruction limit reached! % 75.39/11.08 % (3429057)------------------------------ % 75.39/11.08 % (3429057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429057)CaDiCaL version: 2.1.3 % 75.39/11.08 % (3429057)Termination reason: Instruction limit % 75.39/11.08 % (3429057)Termination phase: Saturation % 75.39/11.08 % (3429057)Time elapsed: 0.151 s % 75.39/11.08 % (3429057)Peak memory usage: 91 MB % 75.39/11.08 % (3429057)Instructions burned: 525 (million) % 75.39/11.08 % (3429059)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=64815634:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2920 on theBenchmark for (2920ds/1016Mi) % 75.39/11.08 % (3429059)Refutation not found, incomplete strategy % 75.39/11.08 % (3429059)------------------------------ % 75.39/11.08 % (3429059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429059)CaDiCaL version: 2.1.3 % 75.39/11.08 % (3429059)Termination reason: Refutation not found, incomplete strategy % 75.39/11.08 % (3429059)Time elapsed: 0.001 s % 75.39/11.08 % (3429059)Peak memory usage: 88 MB % 75.39/11.08 % (3429054)Instruction limit reached! % 75.39/11.08 % (3429054)------------------------------ % 75.39/11.08 % (3429054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429054)CaDiCaL version: 2.1.3 % 75.39/11.08 % (3429054)Termination reason: Instruction limit % 75.39/11.08 % (3429054)Termination phase: Saturation % 75.39/11.08 % (3429054)Time elapsed: 0.949 s % 75.39/11.08 % (3429054)Peak memory usage: 132 MB % 75.39/11.08 % (3429054)Instructions burned: 3036 (million) % 75.39/11.08 % (3429059)------------------------------ % 75.39/11.08 % (3429059)------------------------------ % 75.39/11.08 % (3429061)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1238167176:i=14123:bd=preordered:ins=4_2919 on theBenchmark for (2919ds/14123Mi) % 75.39/11.08 % (3429063)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2710970094:i=5781:kws=precedence:bd=all:rawr=on_2917 on theBenchmark for (2917ds/5781Mi) % 75.39/11.08 % (3429047)Instruction limit reached! % 75.39/11.08 % (3429047)------------------------------ % 75.39/11.08 % (3429047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429047)CaDiCaL version: 2.1.3 % 75.39/11.08 % (3429047)Termination reason: Instruction limit % 75.39/11.08 % (3429047)Termination phase: Saturation % 75.39/11.08 % (3429047)Time elapsed: 2.932 s % 75.39/11.08 % (3429047)Peak memory usage: 172 MB % 75.39/11.08 % (3429047)Instructions burned: 9928 (million) % 75.39/11.08 % (3429065)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=1123021133:i=2448:gtgl=5:bd=preordered:gtg=all_2914 on theBenchmark for (2914ds/2448Mi) % 75.39/11.08 % (3429065)Instruction limit reached! % 75.39/11.08 % (3429065)------------------------------ % 75.39/11.08 % (3429065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429065)CaDiCaL version: 2.1.3 % 75.39/11.08 % (3429065)Termination reason: Instruction limit % 75.39/11.08 % (3429065)Termination phase: Saturation % 75.39/11.08 % (3429065)Time elapsed: 0.733 s % 75.39/11.08 % (3429065)Peak memory usage: 135 MB % 75.39/11.08 % (3429065)Instructions burned: 2449 (million) % 75.39/11.08 % (3429067)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=828703108:i=3223:kws=precedence:fgj=on:av=off_2906 on theBenchmark for (2906ds/3223Mi) % 75.39/11.08 % (3429063)Instruction limit reached! % 75.39/11.08 % (3429063)------------------------------ % 75.39/11.08 % (3429063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.39/11.08 % (3429063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/11.08 % (3429063)CaDiCaL version: 2.1.3 % 85.72/12.68 % (3429063)Termination reason: Instruction limit % 85.72/12.68 % (3429063)Termination phase: Saturation % 85.72/12.68 % (3429063)Time elapsed: 1.235 s % 85.72/12.68 % (3429063)Peak memory usage: 94 MB % 85.72/12.68 % (3429063)Instructions burned: 5785 (million) % 85.72/12.68 % (3429045)Instruction limit reached! % 85.72/12.68 % (3429045)------------------------------ % 85.72/12.68 % (3429045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.72/12.68 % (3429045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.72/12.68 % (3429045)CaDiCaL version: 2.1.3 % 85.72/12.68 % (3429045)Termination reason: Instruction limit % 85.72/12.68 % (3429045)Termination phase: Saturation % 85.72/12.68 % (3429045)Time elapsed: 4.533 s % 85.72/12.68 % (3429045)Peak memory usage: 213 MB % 85.72/12.68 % (3429045)Instructions burned: 13913 (million) % 85.72/12.68 % (3429069)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2510965968:st=5.6:i=2033:sd=3:ss=axioms_2904 on theBenchmark for (2904ds/2033Mi) % 85.72/12.68 % (3429070)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4114393891:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2902 on theBenchmark for (2902ds/2055Mi) % 85.72/12.68 % (3429069)Refutation not found, incomplete strategy % 85.72/12.68 % (3429069)------------------------------ % 85.72/12.68 % (3429069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.72/12.68 % (3429069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.72/12.68 % (3429069)CaDiCaL version: 2.1.3 % 85.72/12.68 % (3429069)Termination reason: Refutation not found, incomplete strategy % 85.72/12.68 % (3429069)Time elapsed: 0.317 s % 85.72/12.68 % (3429069)Peak memory usage: 128 MB % 85.72/12.68 % (3429069)Instructions burned: 865 (million) % 85.72/12.68 [W928 14:46:44.165129875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 [W928 14:46:44.165158519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 [W928 14:46:44.165181064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 [W928 14:46:44.165187332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 [W928 14:46:44.165201035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 [W928 14:46:44.165207028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.72/12.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.72/12.68 % (3429070)Refutation not found, incomplete strategy % 85.72/12.68 % (3429070)------------------------------ % 85.72/12.68 % (3429070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.72/12.68 % (3429070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.72/12.68 % (3429070)CaDiCaL version: 2.1.3 % 85.72/12.68 % (3429070)Termination reason: Refutation not found, incomplete strategy % 85.72/12.68 % (3429070)Time elapsed: 0.314 s % 85.72/12.68 % (3429070)Peak memory usage: 128 MB % 85.72/12.68 % (3429070)Instructions burned: 854 (million) % 85.72/12.68 % (3429069)------------------------------ % 85.72/12.68 % (3429069)------------------------------ % 85.72/12.68 % (3429070)------------------------------ % 93.29/13.69 % (3429070)------------------------------ % 93.29/13.69 % (3429073)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=4077703631:i=21611:sd=3:ss=axioms_2898 on theBenchmark for (2898ds/21611Mi) % 93.29/13.69 % (3429074)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2004799629:i=4835:sd=13:ss=axioms:sgt=23_2896 on theBenchmark for (2896ds/4835Mi) % 93.29/13.69 [W928 14:46:45.663509674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 [W928 14:46:45.663530801 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 [W928 14:46:45.663566120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 [W928 14:46:45.663572143 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 [W928 14:46:45.663585726 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 [W928 14:46:45.663592446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.29/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.29/13.69 % (3429067)Instruction limit reached! % 93.29/13.69 % (3429067)------------------------------ % 93.29/13.69 % (3429067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.29/13.69 % (3429067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.29/13.69 % (3429067)CaDiCaL version: 2.1.3 % 93.29/13.69 % (3429067)Termination reason: Instruction limit % 93.29/13.69 % (3429067)Termination phase: Saturation % 93.29/13.69 % (3429067)Time elapsed: 1.103 s % 93.29/13.69 % (3429067)Peak memory usage: 145 MB % 93.29/13.69 % (3429067)Instructions burned: 3223 (million) % 93.29/13.69 % (3429073)Refutation not found, incomplete strategy % 93.29/13.69 % (3429073)------------------------------ % 93.29/13.69 % (3429073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.29/13.69 % (3429073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.29/13.69 % (3429073)CaDiCaL version: 2.1.3 % 93.29/13.69 % (3429073)Termination reason: Refutation not found, incomplete strategy % 93.29/13.69 % (3429073)Time elapsed: 0.327 s % 93.29/13.69 % (3429073)Peak memory usage: 128 MB % 93.29/13.69 % (3429073)Instructions burned: 866 (million) % 93.29/13.69 % (3429077)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=1560300306:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2893 on theBenchmark for (2893ds/797Mi) % 93.29/13.69 % (3429077)Refutation not found, incomplete strategy % 93.29/13.69 % (3429077)------------------------------ % 93.29/13.69 % (3429077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.29/13.69 % (3429077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.29/13.69 % (3429077)CaDiCaL version: 2.1.3 % 93.29/13.69 % (3429077)Termination reason: Refutation not found, incomplete strategy % 93.29/13.69 % (3429077)Time elapsed: 0.001 s % 93.29/13.69 % (3429077)Peak memory usage: 88 MB % 118.81/17.29 % (3429077)Instructions burned: 2 (million) % 118.81/17.29 % (3429073)------------------------------ % 118.81/17.29 % (3429073)------------------------------ % 118.81/17.29 % (3429077)------------------------------ % 118.81/17.29 % (3429077)------------------------------ % 118.81/17.29 % (3429079)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3451885161:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2891 on theBenchmark for (2891ds/2326Mi) % 118.81/17.29 % (3429079)Refutation not found, incomplete strategy % 118.81/17.29 % (3429079)------------------------------ % 118.81/17.29 % (3429079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.81/17.29 % (3429079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.29 % (3429079)CaDiCaL version: 2.1.3 % 118.81/17.29 % (3429079)Termination reason: Refutation not found, incomplete strategy % 118.81/17.29 % (3429079)Time elapsed: 0.002 s % 118.81/17.29 % (3429079)Peak memory usage: 88 MB % 118.81/17.29 % (3429079)Instructions burned: 3 (million) % 118.81/17.29 % (3429080)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1159446356:i=6038:nm=6_2890 on theBenchmark for (2890ds/6038Mi) % 118.81/17.29 % (3429079)------------------------------ % 118.81/17.29 % (3429079)------------------------------ % 118.81/17.29 % (3429083)lrs+10_1_sil=32000:sp=occurrence:random_seed=421245237:st=2:i=33334:sd=3:ss=included:sgt=32_2888 on theBenchmark for (2888ds/33334Mi) % 118.81/17.29 % (3429061)Instruction limit reached! % 118.81/17.29 % (3429061)------------------------------ % 118.81/17.29 % (3429061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.81/17.29 % (3429061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.29 % (3429061)CaDiCaL version: 2.1.3 % 118.81/17.29 % (3429061)Termination reason: Instruction limit % 118.81/17.29 % (3429061)Termination phase: Saturation % 118.81/17.29 % (3429061)Time elapsed: 3.488 s % 118.81/17.29 % (3429061)Peak memory usage: 148 MB % 118.81/17.29 % (3429061)Instructions burned: 14125 (million) % 118.81/17.29 % (3429074)Instruction limit reached! % 118.81/17.29 % (3429074)------------------------------ % 118.81/17.29 % (3429074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.81/17.29 % (3429074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.29 % (3429074)CaDiCaL version: 2.1.3 % 118.81/17.29 % (3429074)Termination reason: Instruction limit % 118.81/17.29 % (3429074)Termination phase: Saturation % 118.81/17.29 % (3429074)Time elapsed: 1.250 s % 118.81/17.29 % (3429074)Peak memory usage: 104 MB % 118.81/17.29 % (3429074)Instructions burned: 4837 (million) % 118.81/17.29 % (3429086)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=1593865262:i=8327:s2at=5:bd=preordered_2882 on theBenchmark for (2882ds/8327Mi) % 118.81/17.29 % (3429085)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=539241518:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2882 on theBenchmark for (2882ds/1008Mi) % 118.81/17.29 % (3429085)Refutation not found, incomplete strategy % 118.81/17.29 % (3429085)------------------------------ % 118.81/17.29 % (3429085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.81/17.29 % (3429085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.29 % (3429085)CaDiCaL version: 2.1.3 % 118.81/17.29 % (3429085)Termination reason: Refutation not found, incomplete strategy % 118.81/17.29 % (3429085)Time elapsed: 0.011 s % 118.81/17.29 % (3429085)Peak memory usage: 88 MB % 118.81/17.29 % (3429085)Instructions burned: 32 (million) % 118.81/17.29 % (3429085)------------------------------ % 118.81/17.29 % (3429085)------------------------------ % 118.81/17.29 % (3429089)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=1863165319:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2880 on theBenchmark for (2880ds/1083Mi) % 118.81/17.29 % (3429089)Instruction limit reached! % 118.81/17.29 % (3429089)------------------------------ % 118.81/17.29 % (3429089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.81/17.29 % (3429089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.81/17.29 % (3429089)CaDiCaL version: 2.1.3 % 118.81/17.29 % (3429089)Termination reason: Instruction limit % 118.81/17.29 % (3429089)Termination phase: Saturation % 151.35/22.01 % (3429089)Time elapsed: 0.230 s % 151.35/22.01 % (3429089)Peak memory usage: 94 MB % 151.35/22.01 % (3429089)Instructions burned: 1087 (million) % 151.35/22.01 % (3429091)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3961934451:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2876 on theBenchmark for (2876ds/1084Mi) % 151.35/22.01 % (3429080)Instruction limit reached! % 151.35/22.01 % (3429080)------------------------------ % 151.35/22.01 % (3429080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.35/22.01 % (3429080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.35/22.01 % (3429080)CaDiCaL version: 2.1.3 % 151.35/22.01 % (3429080)Termination reason: Instruction limit % 151.35/22.01 % (3429080)Termination phase: Saturation % 151.35/22.01 % (3429080)Time elapsed: 1.559 s % 151.35/22.01 % (3429080)Peak memory usage: 133 MB % 151.35/22.01 % (3429080)Instructions burned: 6040 (million) % 151.35/22.01 % (3429091)Instruction limit reached! % 151.35/22.01 % (3429091)------------------------------ % 151.35/22.01 % (3429091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.35/22.01 % (3429091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.35/22.01 % (3429091)CaDiCaL version: 2.1.3 % 151.35/22.01 % (3429091)Termination reason: Instruction limit % 151.35/22.01 % (3429091)Termination phase: Saturation % 151.35/22.01 % (3429091)Time elapsed: 0.240 s % 151.35/22.01 % (3429091)Peak memory usage: 89 MB % 151.35/22.01 % (3429091)Instructions burned: 1085 (million) % 151.35/22.01 % (3429093)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1503039293:i=6995:s2at=5:gtg=all_2873 on theBenchmark for (2873ds/6995Mi) % 151.35/22.01 % (3429094)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=774535713:st=2:i=6225:sd=15:ss=axioms_2872 on theBenchmark for (2872ds/6225Mi) % 151.35/22.01 % (3429094)Refutation not found, incomplete strategy % 151.35/22.01 % (3429094)------------------------------ % 151.35/22.01 % (3429094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.35/22.01 % (3429094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.35/22.01 % (3429094)CaDiCaL version: 2.1.3 % 151.35/22.01 % (3429094)Termination reason: Refutation not found, incomplete strategy % 151.35/22.01 % (3429094)Time elapsed: 0.004 s % 151.35/22.01 % (3429094)Peak memory usage: 89 MB % 151.35/22.01 % (3429094)Instructions burned: 12 (million) % 151.35/22.01 % (3429094)------------------------------ % 151.35/22.01 % (3429094)------------------------------ % 151.35/22.01 % (3429097)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=659723185:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2869 on theBenchmark for (2869ds/3372Mi) % 151.35/22.01 [W928 14:46:47.488905250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.35/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.35/22.01 [W928 14:46:47.488927106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.35/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.35/22.01 [W928 14:46:47.488946489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.35/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.35/22.01 [W928 14:46:47.488953434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.35/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.35/22.01 [W928 14:46:47.488967713 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.35/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.35/22.01 [W928 14:46:47.488974146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.18/23.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.18/23.59 % (3429097)Refutation not found, incomplete strategy % 163.18/23.59 % (3429097)------------------------------ % 163.18/23.59 % (3429097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.18/23.59 % (3429097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.18/23.59 % (3429097)CaDiCaL version: 2.1.3 % 163.18/23.59 % (3429097)Termination reason: Refutation not found, incomplete strategy % 163.18/23.59 % (3429097)Time elapsed: 0.312 s % 163.18/23.59 % (3429097)Peak memory usage: 127 MB % 163.18/23.59 % (3429097)Instructions burned: 858 (million) % 163.18/23.59 % (3429097)------------------------------ % 163.18/23.59 % (3429097)------------------------------ % 163.18/23.59 % (3429099)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2372575870:st=2.3:i=26457:sd=10:ss=included:sgt=8_2863 on theBenchmark for (2863ds/26457Mi) % 163.18/23.59 % (3429086)Instruction limit reached! % 163.18/23.59 % (3429086)------------------------------ % 163.18/23.59 % (3429086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.18/23.59 % (3429086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.18/23.59 % (3429086)CaDiCaL version: 2.1.3 % 163.18/23.59 % (3429086)Termination reason: Instruction limit % 163.18/23.59 % (3429086)Termination phase: Saturation % 163.18/23.59 % (3429086)Time elapsed: 2.277 s % 163.18/23.59 % (3429086)Peak memory usage: 155 MB % 163.18/23.59 % (3429086)Instructions burned: 8328 (million) % 163.18/23.59 % (3429101)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=3690811082:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2858 on theBenchmark for (2858ds/13494Mi) % 163.18/23.59 % (3429093)Instruction limit reached! % 163.18/23.59 % (3429093)------------------------------ % 163.18/23.59 % (3429093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.18/23.59 % (3429093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.18/23.59 % (3429093)CaDiCaL version: 2.1.3 % 163.18/23.59 % (3429093)Termination reason: Instruction limit % 163.18/23.59 % (3429093)Termination phase: Saturation % 163.18/23.59 % (3429093)Time elapsed: 2.573 s % 163.18/23.59 % (3429093)Peak memory usage: 182 MB % 163.18/23.59 % (3429093)Instructions burned: 6996 (million) % 163.18/23.59 % (3429103)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=3361427082:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2846 on theBenchmark for (2846ds/2503Mi) % 163.18/23.59 % (3429103)Instruction limit reached! % 163.18/23.59 % (3429103)------------------------------ % 163.18/23.59 % (3429103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.18/23.59 % (3429103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.18/23.59 % (3429103)CaDiCaL version: 2.1.3 % 163.18/23.59 % (3429103)Termination reason: Instruction limit % 163.18/23.59 % (3429103)Termination phase: Saturation % 163.18/23.59 % (3429103)Time elapsed: 0.722 s % 163.18/23.59 % (3429103)Peak memory usage: 132 MB % 163.18/23.59 % (3429103)Instructions burned: 2503 (million) % 163.18/23.59 % (3429105)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2049853717:i=2559:sd=1:ep=RSTC:ss=axioms_2837 on theBenchmark for (2837ds/2559Mi) % 163.18/23.59 % (3429105)Refutation not found, incomplete strategy % 163.18/23.59 % (3429105)------------------------------ % 163.18/23.59 % (3429105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.18/23.59 % (3429105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.18/23.59 % (3429105)CaDiCaL version: 2.1.3 % 163.18/23.59 % (3429105)Termination reason: Refutation not found, incomplete strategy % 163.18/23.59 % (3429105)Time elapsed: 0.333 s % 163.18/23.59 % (3429105)Peak memory usage: 128 MB % 163.18/23.59 % (3429105)Instructions burned: 898 (million) % 163.18/23.59 % (3429105)------------------------------ % 163.18/23.59 % (3429105)------------------------------ % 163.18/23.59 % (3429107)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2766495765:i=30753:av=off:ss=included_2831 on theBenchmark for (2831ds/30753Mi) % 177.59/25.67 % (3429101)Instruction limit reached! % 177.59/25.67 % (3429101)------------------------------ % 177.59/25.67 % (3429101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429101)CaDiCaL version: 2.1.3 % 177.59/25.67 % (3429101)Termination reason: Instruction limit % 177.59/25.67 % (3429101)Termination phase: Saturation % 177.59/25.67 % (3429101)Time elapsed: 3.976 s % 177.59/25.67 % (3429101)Peak memory usage: 207 MB % 177.59/25.67 % (3429101)Instructions burned: 13494 (million) % 177.59/25.67 % (3429109)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3482904976:i=26473:ep=RSTC_2817 on theBenchmark for (2817ds/26473Mi) % 177.59/25.67 % (3429083)Instruction limit reached! % 177.59/25.67 % (3429083)------------------------------ % 177.59/25.67 % (3429083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429083)CaDiCaL version: 2.1.3 % 177.59/25.67 % (3429083)Termination reason: Instruction limit % 177.59/25.67 % (3429083)Termination phase: Saturation % 177.59/25.67 % (3429083)Time elapsed: 7.138 s % 177.59/25.67 % (3429083)Peak memory usage: 98 MB % 177.59/25.67 % (3429083)Instructions burned: 33337 (million) % 177.59/25.67 % (3429111)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=1802089094:cts=off:i=2759:kws=inv_arity:fgj=on_2816 on theBenchmark for (2816ds/2759Mi) % 177.59/25.67 % (3429111)Refutation not found, incomplete strategy % 177.59/25.67 % (3429111)------------------------------ % 177.59/25.67 % (3429111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429111)CaDiCaL version: 2.1.3 % 177.59/25.67 % (3429111)Termination reason: Refutation not found, incomplete strategy % 177.59/25.67 % (3429111)Time elapsed: 0.316 s % 177.59/25.67 % (3429111)Peak memory usage: 128 MB % 177.59/25.67 % (3429111)Instructions burned: 868 (million) % 177.59/25.67 % (3429111)------------------------------ % 177.59/25.67 % (3429111)------------------------------ % 177.59/25.67 % (3429113)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=181317220:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2810 on theBenchmark for (2810ds/5665Mi) % 177.59/25.67 % (3429099)Instruction limit reached! % 177.59/25.67 % (3429099)------------------------------ % 177.59/25.67 % (3429099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429099)CaDiCaL version: 2.1.3 % 177.59/25.67 % (3429099)Termination reason: Instruction limit % 177.59/25.67 % (3429099)Termination phase: Saturation % 177.59/25.67 % (3429099)Time elapsed: 7.458 s % 177.59/25.67 % (3429099)Peak memory usage: 227 MB % 177.59/25.67 % (3429099)Instructions burned: 26459 (million) % 177.59/25.67 % (3429113)Instruction limit reached! % 177.59/25.67 % (3429113)------------------------------ % 177.59/25.67 % (3429113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429113)CaDiCaL version: 2.1.3 % 177.59/25.67 % (3429113)Termination reason: Instruction limit % 177.59/25.67 % (3429113)Termination phase: Saturation % 177.59/25.67 % (3429113)Time elapsed: 2.148 s % 177.59/25.67 % (3429113)Peak memory usage: 153 MB % 177.59/25.67 % (3429113)Instructions burned: 5668 (million) % 177.59/25.67 % (3429116)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=4061155366:i=1532:ep=RS:ss=axioms_2787 on theBenchmark for (2787ds/1532Mi) % 177.59/25.67 % (3429117)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2378267141:i=1565:sd=2:ss=axioms:sgt=32_2787 on theBenchmark for (2787ds/1565Mi) % 177.59/25.67 % (3429116)Refutation not found, incomplete strategy % 177.59/25.67 % (3429116)------------------------------ % 177.59/25.67 % (3429116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.67 % (3429116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.67 % (3429116)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429116)Termination reason: Refutation not found, incomplete strategy % 189.19/27.22 % (3429116)Time elapsed: 0.325 s % 189.19/27.22 % (3429116)Peak memory usage: 128 MB % 189.19/27.22 % (3429116)Instructions burned: 890 (million) % 189.19/27.22 % (3429116)------------------------------ % 189.19/27.22 % (3429116)------------------------------ % 189.19/27.22 % (3429117)Instruction limit reached! % 189.19/27.22 % (3429117)------------------------------ % 189.19/27.22 % (3429117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.19/27.22 % (3429117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.19/27.22 % (3429117)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429117)Termination reason: Instruction limit % 189.19/27.22 % (3429117)Termination phase: Saturation % 189.19/27.22 % (3429117)Time elapsed: 0.485 s % 189.19/27.22 % (3429117)Peak memory usage: 130 MB % 189.19/27.22 % (3429117)Instructions burned: 1571 (million) % 189.19/27.22 % (3429120)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=2823645370:i=1572:fgj=on:gsp=on_2781 on theBenchmark for (2781ds/1572Mi) % 189.19/27.22 % (3429121)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1889381574:i=6052:sd=4:ss=axioms:sgt=24_2781 on theBenchmark for (2781ds/6052Mi) % 189.19/27.22 % (3429121)Refutation not found, incomplete strategy % 189.19/27.22 % (3429121)------------------------------ % 189.19/27.22 % (3429121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.19/27.22 % (3429121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.19/27.22 % (3429121)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429121)Termination reason: Refutation not found, incomplete strategy % 189.19/27.22 % (3429121)Time elapsed: 0.315 s % 189.19/27.22 % (3429121)Peak memory usage: 128 MB % 189.19/27.22 % (3429121)Instructions burned: 865 (million) % 189.19/27.22 % (3429121)------------------------------ % 189.19/27.22 % (3429121)------------------------------ % 189.19/27.22 % (3429120)Instruction limit reached! % 189.19/27.22 % (3429120)------------------------------ % 189.19/27.22 % (3429120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.19/27.22 % (3429120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.19/27.22 % (3429120)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429120)Termination reason: Instruction limit % 189.19/27.22 % (3429120)Termination phase: Saturation % 189.19/27.22 % (3429120)Time elapsed: 0.558 s % 189.19/27.22 % (3429120)Peak memory usage: 133 MB % 189.19/27.22 % (3429120)Instructions burned: 1574 (million) % 189.19/27.22 % (3429124)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2580629192:i=3500:sd=1:bd=preordered:sup=off:ss=included_2775 on theBenchmark for (2775ds/3500Mi) % 189.19/27.22 % (3429125)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=47128051:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2774 on theBenchmark for (2774ds/1842Mi) % 189.19/27.22 % (3429124)Refutation not found, incomplete strategy % 189.19/27.22 % (3429124)------------------------------ % 189.19/27.22 % (3429124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.19/27.22 % (3429124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.19/27.22 % (3429124)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429124)Termination reason: Refutation not found, incomplete strategy % 189.19/27.22 % (3429124)Time elapsed: 0.318 s % 189.19/27.22 % (3429124)Peak memory usage: 128 MB % 189.19/27.22 % (3429124)Instructions burned: 865 (million) % 189.19/27.22 % (3429124)------------------------------ % 189.19/27.22 % (3429124)------------------------------ % 189.19/27.22 % (3429128)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2536211140:i=66096:add=on_2769 on theBenchmark for (2769ds/66096Mi) % 189.19/27.22 % (3429125)Instruction limit reached! % 189.19/27.22 % (3429125)------------------------------ % 189.19/27.22 % (3429125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.19/27.22 % (3429125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.19/27.22 % (3429125)CaDiCaL version: 2.1.3 % 189.19/27.22 % (3429125)Termination reason: Instruction limit % 189.19/27.22 % (3429125)Termination phase: Saturation % 213.27/30.70 % (3429125)Time elapsed: 0.609 s % 213.27/30.70 % (3429125)Peak memory usage: 135 MB % 213.27/30.70 % (3429125)Instructions burned: 1843 (million) % 213.27/30.70 % (3429130)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1168245783:i=1884:sd=1:nm=60:ss=axioms_2767 on theBenchmark for (2767ds/1884Mi) % 213.27/30.70 [W928 14:46:58.726006367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 [W928 14:46:58.726047101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 [W928 14:46:58.726067937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 [W928 14:46:58.726075201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 [W928 14:46:58.726088902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 [W928 14:46:58.726095193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.27/30.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.27/30.70 % (3429130)Refutation not found, incomplete strategy % 213.27/30.70 % (3429130)------------------------------ % 213.27/30.70 % (3429130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.27/30.70 % (3429130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.70 % (3429130)CaDiCaL version: 2.1.3 % 213.27/30.70 % (3429130)Termination reason: Refutation not found, incomplete strategy % 213.27/30.70 % (3429130)Time elapsed: 0.311 s % 213.27/30.70 % (3429130)Peak memory usage: 127 MB % 213.27/30.70 % (3429130)Instructions burned: 857 (million) % 213.27/30.70 % (3429130)------------------------------ % 213.27/30.70 % (3429130)------------------------------ % 213.27/30.70 % (3429132)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3942706123:cts=off:i=5469:bs=on:fsr=off_2761 on theBenchmark for (2761ds/5469Mi) % 213.27/30.70 % (3429107)Instruction limit reached! % 213.27/30.70 % (3429107)------------------------------ % 213.27/30.70 % (3429107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.27/30.70 % (3429107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.70 % (3429107)CaDiCaL version: 2.1.3 % 213.27/30.70 % (3429107)Termination reason: Instruction limit % 213.27/30.70 % (3429107)Termination phase: Saturation % 213.27/30.70 % (3429107)Time elapsed: 7.816 s % 213.27/30.70 % (3429107)Peak memory usage: 213 MB % 213.27/30.70 % (3429107)Instructions burned: 30754 (million) % 213.27/30.70 % (3429134)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=2917683555:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2752 on theBenchmark for (2752ds/2037Mi) % 213.27/30.70 % (3429132)Instruction limit reached! % 213.27/30.70 % (3429132)------------------------------ % 213.27/30.70 % (3429132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.27/30.70 % (3429132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.27/30.70 % (3429132)CaDiCaL version: 2.1.3 % 213.27/30.70 % (3429132)Termination reason: Instruction limit % 213.27/30.70 % (3429132)Termination phase: Saturation % 213.27/30.70 % (3429132)Time elapsed: 1.360 s % 221.10/31.91 % (3429132)Peak memory usage: 92 MB % 221.10/31.91 % (3429132)Instructions burned: 5472 (million) % 221.10/31.91 % (3429136)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3760159969:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2746 on theBenchmark for (2746ds/2110Mi) % 221.10/31.91 % (3429109)Instruction limit reached! % 221.10/31.91 % (3429109)------------------------------ % 221.10/31.91 % (3429109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.10/31.91 % (3429109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.10/31.91 % (3429109)CaDiCaL version: 2.1.3 % 221.10/31.91 % (3429109)Termination reason: Instruction limit % 221.10/31.91 % (3429109)Termination phase: Saturation % 221.10/31.91 % (3429109)Time elapsed: 7.199 s % 221.10/31.91 % (3429109)Peak memory usage: 427 MB % 221.10/31.91 % (3429109)Instructions burned: 26477 (million) % 221.10/31.91 % (3429134)Instruction limit reached! % 221.10/31.91 % (3429134)------------------------------ % 221.10/31.91 % (3429134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.10/31.91 % (3429134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.10/31.91 % (3429134)CaDiCaL version: 2.1.3 % 221.10/31.91 % (3429134)Termination reason: Instruction limit % 221.10/31.91 % (3429134)Termination phase: Saturation % 221.10/31.91 % (3429134)Time elapsed: 0.722 s % 221.10/31.91 % (3429134)Peak memory usage: 138 MB % 221.10/31.91 % (3429134)Instructions burned: 2040 (million) % 221.10/31.91 % (3429138)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=105056970:i=2430:add=off:aac=none:nm=16_2743 on theBenchmark for (2743ds/2430Mi) % 221.10/31.91 % (3429139)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=916007883:cond=fast:i=4891_2743 on theBenchmark for (2743ds/4891Mi) % 221.10/31.91 % (3429136)Instruction limit reached! % 221.10/31.91 % (3429136)------------------------------ % 221.10/31.91 % (3429136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.10/31.91 % (3429136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.10/31.91 % (3429136)CaDiCaL version: 2.1.3 % 221.10/31.91 % (3429136)Termination reason: Instruction limit % 221.10/31.91 % (3429136)Termination phase: Saturation % 221.10/31.91 % (3429136)Time elapsed: 0.646 s % 221.10/31.91 % (3429136)Peak memory usage: 133 MB % 221.10/31.91 % (3429136)Instructions burned: 2112 (million) % 221.10/31.91 % (3429142)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=1963831294:st=2:i=14845:sd=2:ss=included:fsd=on_2738 on theBenchmark for (2738ds/14845Mi) % 221.10/31.91 % (3429138)Instruction limit reached! % 221.10/31.91 % (3429138)------------------------------ % 221.10/31.91 % (3429138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.10/31.91 % (3429138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.10/31.91 % (3429138)CaDiCaL version: 2.1.3 % 221.10/31.91 % (3429138)Termination reason: Instruction limit % 221.10/31.91 % (3429138)Termination phase: Saturation % 221.10/31.91 % (3429138)Time elapsed: 0.746 s % 221.10/31.91 % (3429138)Peak memory usage: 134 MB % 221.10/31.91 % (3429138)Instructions burned: 2432 (million) % 221.10/31.91 % (3429142)Refutation not found, incomplete strategy % 221.10/31.91 % (3429142)------------------------------ % 221.10/31.91 % (3429142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.10/31.91 % (3429142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.10/31.91 % (3429142)CaDiCaL version: 2.1.3 % 221.10/31.91 % (3429142)Termination reason: Refutation not found, incomplete strategy % 221.10/31.91 % (3429142)Time elapsed: 0.325 s % 221.10/31.91 % (3429142)Peak memory usage: 128 MB % 221.10/31.91 % (3429142)Instructions burned: 894 (million) % 221.10/31.91 % (3429144)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2334841633:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2735 on theBenchmark for (2735ds/7534Mi) % 221.10/31.91 % (3429142)------------------------------ % 221.10/31.91 % (3429142)------------------------------ % 221.10/31.91 % (3429146)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=2329877368:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2732 on theBenchmark for (2732ds/10353Mi) % 255.50/36.62 % (3429139)Instruction limit reached! % 255.50/36.62 % (3429139)------------------------------ % 255.50/36.62 % (3429139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.50/36.62 % (3429139)CaDiCaL version: 2.1.3 % 255.50/36.62 % (3429139)Termination reason: Instruction limit % 255.50/36.62 % (3429139)Termination phase: Saturation % 255.50/36.62 % (3429139)Time elapsed: 1.322 s % 255.50/36.62 % (3429139)Peak memory usage: 135 MB % 255.50/36.62 % (3429139)Instructions burned: 4894 (million) % 255.50/36.62 % (3429148)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=241464321:i=7860_2728 on theBenchmark for (2728ds/7860Mi) % 255.50/36.62 % (3429148)Refutation not found, incomplete strategy % 255.50/36.62 % (3429148)------------------------------ % 255.50/36.62 % (3429148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.50/36.62 % (3429148)CaDiCaL version: 2.1.3 % 255.50/36.62 % (3429148)Termination reason: Refutation not found, incomplete strategy % 255.50/36.62 % (3429148)Time elapsed: 0.001 s % 255.50/36.62 % (3429148)Peak memory usage: 88 MB % 255.50/36.62 % (3429148)Instructions burned: 3 (million) % 255.50/36.62 % (3429148)------------------------------ % 255.50/36.62 % (3429148)------------------------------ % 255.50/36.62 % (3429150)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=1585031945:i=7896:sd=2:bs=on:ss=included:sgt=20_2725 on theBenchmark for (2725ds/7896Mi) % 255.50/36.62 % (3429144)Instruction limit reached! % 255.50/36.62 % (3429144)------------------------------ % 255.50/36.62 % (3429144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.50/36.62 % (3429144)CaDiCaL version: 2.1.3 % 255.50/36.62 % (3429144)Termination reason: Instruction limit % 255.50/36.62 % (3429144)Termination phase: Saturation % 255.50/36.62 % (3429144)Time elapsed: 1.979 s % 255.50/36.62 % (3429144)Peak memory usage: 142 MB % 255.50/36.62 % (3429144)Instructions burned: 7538 (million) % 255.50/36.62 % (3429152)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3325946171:i=5812:gtgl=2:gtg=all_2713 on theBenchmark for (2713ds/5812Mi) % 255.50/36.62 % (3429150)Instruction limit reached! % 255.50/36.62 % (3429150)------------------------------ % 255.50/36.62 % (3429150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.50/36.62 % (3429150)CaDiCaL version: 2.1.3 % 255.50/36.62 % (3429150)Termination reason: Instruction limit % 255.50/36.62 % (3429150)Termination phase: Saturation % 255.50/36.62 % (3429150)Time elapsed: 2.413 s % 255.50/36.62 % (3429150)Peak memory usage: 144 MB % 255.50/36.62 % (3429150)Instructions burned: 7899 (million) % 255.50/36.62 % (3429146)Instruction limit reached! % 255.50/36.62 % (3429146)------------------------------ % 255.50/36.62 % (3429146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.50/36.62 % (3429146)CaDiCaL version: 2.1.3 % 255.50/36.62 % (3429146)Termination reason: Instruction limit % 255.50/36.62 % (3429146)Termination phase: Saturation % 255.50/36.62 % (3429146)Time elapsed: 3.170 s % 255.50/36.62 % (3429146)Peak memory usage: 157 MB % 255.50/36.62 % (3429146)Instructions burned: 10355 (million) % 255.50/36.62 % (3429154)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=398524705:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2700 on theBenchmark for (2700ds/2965Mi) % 255.50/36.62 % (3429156)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3676139784:i=2967:kws=precedence:bd=preordered:av=off_2699 on theBenchmark for (2699ds/2967Mi) % 255.50/36.62 % (3429154)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 255.50/36.62 % (3429154)------------------------------ % 255.50/36.62 % (3429154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.50/36.62 % (3429154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3429154)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3429154)Termination reason: Unknown % 280.88/40.28 % (3429154)Termination phase: Saturation % 280.88/40.28 % (3429154)Time elapsed: 0.313 s % 280.88/40.28 % (3429154)Peak memory usage: 128 MB % 280.88/40.28 % (3429154)Instructions burned: 849 (million) % 280.88/40.28 % (3429158)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=1816233252:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2696 on theBenchmark for (2696ds/3022Mi) % 280.88/40.28 % (3429152)Instruction limit reached! % 280.88/40.28 % (3429152)------------------------------ % 280.88/40.28 % (3429152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.88/40.28 % (3429152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3429152)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3429152)Termination reason: Instruction limit % 280.88/40.28 % (3429152)Termination phase: Saturation % 280.88/40.28 % (3429152)Time elapsed: 1.924 s % 280.88/40.28 % (3429152)Peak memory usage: 174 MB % 280.88/40.28 % (3429152)Instructions burned: 5813 (million) % 280.88/40.28 % (3429160)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=3572909954:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2693 on theBenchmark for (2693ds/3207Mi) % 280.88/40.28 % (3429156)Instruction limit reached! % 280.88/40.28 % (3429156)------------------------------ % 280.88/40.28 % (3429156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.88/40.28 % (3429156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3429156)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3429156)Termination reason: Instruction limit % 280.88/40.28 % (3429156)Termination phase: Saturation % 280.88/40.28 % (3429156)Time elapsed: 0.896 s % 280.88/40.28 % (3429156)Peak memory usage: 135 MB % 280.88/40.28 % (3429156)Instructions burned: 2968 (million) % 280.88/40.28 % (3429160)Refutation not found, incomplete strategy % 280.88/40.28 % (3429160)------------------------------ % 280.88/40.28 % (3429160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.88/40.28 % (3429160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3429160)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3429160)Termination reason: Refutation not found, incomplete strategy % 280.88/40.28 % (3429160)Time elapsed: 0.325 s % 280.88/40.28 % (3429160)Peak memory usage: 128 MB % 280.88/40.28 % (3429160)Instructions burned: 896 (million) % 280.88/40.28 % (3428970)Instruction limit reached! % 280.88/40.28 % (3428970)------------------------------ % 280.88/40.28 % (3428970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.88/40.28 % (3428970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3428970)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3428970)Termination reason: Instruction limit % 280.88/40.28 % (3428970)Termination phase: Saturation % 280.88/40.28 % (3428970)Time elapsed: 30.992 s % 280.88/40.28 % (3428970)Peak memory usage: 188 MB % 280.88/40.28 % (3428970)Instructions burned: 134682 (million) % 280.88/40.28 % (3429162)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2741326557:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2688 on theBenchmark for (2688ds/3289Mi) % 280.88/40.28 % (3429160)------------------------------ % 280.88/40.28 % (3429160)------------------------------ % 280.88/40.28 % (3429163)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1391348990:i=38569:sd=3:ss=axioms:sgt=32_2688 on theBenchmark for (2688ds/38569Mi) % 280.88/40.28 % (3429166)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=367839152:cts=off:i=3394_2687 on theBenchmark for (2687ds/3394Mi) % 280.88/40.28 % (3429158)Instruction limit reached! % 280.88/40.28 % (3429158)------------------------------ % 280.88/40.28 % (3429158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.88/40.28 % (3429158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.88/40.28 % (3429158)CaDiCaL version: 2.1.3 % 280.88/40.28 % (3429158)Termination reason: Instruction limit % 280.88/40.28 % (3429158)Termination phase: Saturation % 280.88/40.28 % (3429158)Time elapsed: 0.923 s % 280.88/40.28 % (3429158)Peak memory usage: 133 MB % 280.88/40.28 % (3429158)Instructions burned: 3025 (million) % 280.88/40.28 % (3429168)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=579371320:i=33824:bd=preordered_2685 on theBenchmark for (2685ds/33824Mi) % 293.64/42.11 % (3429162)Instruction limit reached! % 293.64/42.11 % (3429162)------------------------------ % 293.64/42.11 % (3429162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.64/42.11 % (3429162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/42.11 % (3429162)CaDiCaL version: 2.1.3 % 293.64/42.11 % (3429162)Termination reason: Instruction limit % 293.64/42.11 % (3429162)Termination phase: Saturation % 293.64/42.11 % (3429162)Time elapsed: 0.972 s % 293.64/42.11 % (3429162)Peak memory usage: 140 MB % 293.64/42.11 % (3429162)Instructions burned: 3293 (million) % 293.64/42.11 % (3429170)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=494564369:i=20684:bd=all:gtg=exists_sym_2677 on theBenchmark for (2677ds/20684Mi) % 293.64/42.11 % (3429166)Instruction limit reached! % 293.64/42.11 % (3429166)------------------------------ % 293.64/42.11 % (3429166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.64/42.11 % (3429166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/42.11 % (3429166)CaDiCaL version: 2.1.3 % 293.64/42.11 % (3429166)Termination reason: Instruction limit % 293.64/42.11 % (3429166)Termination phase: Saturation % 293.64/42.11 % (3429166)Time elapsed: 1.024 s % 293.64/42.11 % (3429166)Peak memory usage: 133 MB % 293.64/42.11 % (3429166)Instructions burned: 3395 (million) % 293.64/42.11 % (3429172)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=2360946781:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2675 on theBenchmark for (2675ds/7222Mi) % 293.64/42.11 % (3429172)Refutation not found, incomplete strategy % 293.64/42.11 % (3429172)------------------------------ % 293.64/42.11 % (3429172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.64/42.11 % (3429172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/42.11 % (3429172)CaDiCaL version: 2.1.3 % 293.64/42.11 % (3429172)Termination reason: Refutation not found, incomplete strategy % 293.64/42.11 % (3429172)Time elapsed: 0.319 s % 293.64/42.11 % (3429172)Peak memory usage: 128 MB % 293.64/42.11 % (3429172)Instructions burned: 863 (million) % 293.64/42.11 % (3429172)------------------------------ % 293.64/42.11 % (3429172)------------------------------ % 293.64/42.11 % (3429174)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3705833662:st=4:i=7295:sd=4:ep=R:ss=axioms_2669 on theBenchmark for (2669ds/7295Mi) % 293.64/42.11 % (3429174)Refutation not found, incomplete strategy % 293.64/42.11 % (3429174)------------------------------ % 293.64/42.11 % (3429174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.64/42.11 % (3429174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/42.11 % (3429174)CaDiCaL version: 2.1.3 % 293.64/42.11 % (3429174)Termination reason: Refutation not found, incomplete strategy % 293.64/42.11 % (3429174)Time elapsed: 0.323 s % 293.64/42.11 % (3429174)Peak memory usage: 128 MB % 293.64/42.11 % (3429174)Instructions burned: 879 (million) % 293.64/42.11 % (3429174)------------------------------ % 293.64/42.11 % (3429174)------------------------------ % 293.64/42.11 % (3429176)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=1279580047:i=4036:ins=10_2663 on theBenchmark for (2663ds/4036Mi) % 293.64/42.11 % (3429176)Instruction limit reached! % 293.64/42.11 % (3429176)------------------------------ % 293.64/42.11 % (3429176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.64/42.11 % (3429176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/42.11 % (3429176)CaDiCaL version: 2.1.3 % 293.64/42.11 % (3429176)Termination reason: Instruction limit % 293.64/42.11 % (3429176)Termination phase: Saturation % 293.64/42.11 % (3429176)Time elapsed: 1.031 s % 293.64/42.11 % (3429176)Peak memory usage: 133 MB % 293.64/42.11 % (3429176)Instructions burned: 4040 (million) % 293.64/42.11 % (3429178)lrs+10_1_sil=128000:lcm=predicate:random_seed=967041692:st=3:i=43697:sd=5:ss=axioms_2651 on theBenchmark for (2651ds/43697Mi) % 293.64/42.11 % (3428969)Instruction limit reached! % 300.67/43.05 % (3428969)------------------------------ % 300.67/43.05 % (3428969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3428969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3428969)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3428969)Termination reason: Instruction limit % 300.67/43.05 % (3428969)Termination phase: Saturation % 300.67/43.05 % (3428969)Time elapsed: 36.164 s % 300.67/43.05 % (3428969)Peak memory usage: 455 MB % 300.67/43.05 % (3428969)Instructions burned: 141196 (million) % 300.67/43.05 % (3429180)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=394733449:i=17599:gtg=all:ss=axioms:fsd=on_2636 on theBenchmark for (2636ds/17599Mi) % 300.67/43.05 % (3429128)Instruction limit reached! % 300.67/43.05 % (3429128)------------------------------ % 300.67/43.05 % (3429128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3429128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3429128)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3429128)Termination reason: Instruction limit % 300.67/43.05 % (3429128)Termination phase: Saturation % 300.67/43.05 % (3429128)Time elapsed: 13.931 s % 300.67/43.05 % (3429128)Peak memory usage: 149 MB % 300.67/43.05 % (3429128)Instructions burned: 66100 (million) % 300.67/43.05 % (3429182)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=4164385072:i=4547:bd=preordered_2628 on theBenchmark for (2628ds/4547Mi) % 300.67/43.05 % (3429182)Instruction limit reached! % 300.67/43.05 % (3429182)------------------------------ % 300.67/43.05 % (3429182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3429182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3429182)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3429182)Termination reason: Instruction limit % 300.67/43.05 % (3429182)Termination phase: Saturation % 300.67/43.05 % (3429182)Time elapsed: 1.232 s % 300.67/43.05 % (3429182)Peak memory usage: 140 MB % 300.67/43.05 % (3429182)Instructions burned: 4548 (million) % 300.67/43.05 % (3429170)Instruction limit reached! % 300.67/43.05 % (3429170)------------------------------ % 300.67/43.05 % (3429170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3429170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3429170)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3429170)Termination reason: Instruction limit % 300.67/43.05 % (3429170)Termination phase: Saturation % 300.67/43.05 % (3429170)Time elapsed: 6.200 s % 300.67/43.05 % (3429170)Peak memory usage: 212 MB % 300.67/43.05 % (3429170)Instructions burned: 20687 (million) % 300.67/43.05 % (3429184)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=1627325810:i=9294:av=off_2614 on theBenchmark for (2614ds/9294Mi) % 300.67/43.05 % (3429185)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=976549270:i=32849:add=on_2614 on theBenchmark for (2614ds/32849Mi) % 300.67/43.05 % (3429163)Instruction limit reached! % 300.67/43.05 % (3429163)------------------------------ % 300.67/43.05 % (3429163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3429163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3429163)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3429163)Termination reason: Instruction limit % 300.67/43.05 % (3429163)Termination phase: Saturation % 300.67/43.05 % (3429163)Time elapsed: 8.171 s % 300.67/43.05 % (3429163)Peak memory usage: 145 MB % 300.67/43.05 % (3429163)Instructions burned: 38572 (million) % 300.67/43.05 % (3429188)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2936092538:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2605 on theBenchmark for (2605ds/4793Mi) % 300.67/43.05 % (3429188)Refutation not found, incomplete strategy % 300.67/43.05 % (3429188)------------------------------ % 300.67/43.05 % (3429188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.05 % (3429188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.05 % (3429188)CaDiCaL version: 2.1.3 % 300.67/43.05 % (3429188)Termination reason: Refutation not found, incomplete strategy % 300.67/43.05 % (3429188)Time elapsed: 0.370 s % 300.67/43.05 % (3429188)Peak memory us % 300.67/43.06 Terminated %------------------------------------------------------------------------------