%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM925_30 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:33 PM UTC 2026 % Result : Timeout 300.46s 43.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM925_30 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.40 % Computer : n006.cluster.edu % 0.12/0.40 % Model : x86_64 x86_64 % 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.40 % Memory : 8046.5625MB % 0.12/0.40 % OS : Linux 6.8.0-71-generic % 0.12/0.40 % CPULimit : 300 % 0.12/0.40 % WCLimit : 300 % 0.12/0.40 % DateTime : Sun Sep 27 21:43:22 UTC 2026 % 0.12/0.40 % CPUTime : % 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.43 Running first-order theorem proving % 0.12/0.43 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 % 9.73/2.37 % (3345978)Detected formulas, will run a generic FOF schedule. % 9.73/2.37 % (3345986)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2092629505:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.73/2.37 % (3345986)Refutation not found, incomplete strategy % 9.73/2.37 % (3345986)------------------------------ % 9.73/2.37 % (3345986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.73/2.37 % (3345986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.73/2.37 % (3345986)CaDiCaL version: 2.1.3 % 9.73/2.37 % (3345986)Termination reason: Refutation not found, incomplete strategy % 9.73/2.37 % (3345986)Time elapsed: 0.002 s % 9.73/2.37 % (3345986)Peak memory usage: 87 MB % 9.73/2.37 % (3345986)Instructions burned: 4 (million) % 9.73/2.37 % (3345989)dis-21_1_sil=8000:lcm=predicate:random_seed=2710237278: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) % 9.73/2.37 % (3345985)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=2652656960:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.73/2.37 % (3345984)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=2867078399:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.73/2.37 % (3345988)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=594069538:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.73/2.37 % (3345983)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=1006467337:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.73/2.37 % (3345987)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2537659421:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.73/2.37 % (3345987)Refutation not found, incomplete strategy % 9.73/2.37 % (3345987)------------------------------ % 9.73/2.37 % (3345987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.73/2.37 % (3345987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.73/2.37 % (3345987)CaDiCaL version: 2.1.3 % 9.73/2.37 % (3345987)Termination reason: Refutation not found, incomplete strategy % 9.73/2.37 % (3345987)Time elapsed: 0.004 s % 9.73/2.37 % (3345987)Peak memory usage: 87 MB % 9.73/2.37 % (3345987)Instructions burned: 4 (million) % 9.73/2.37 % (3345989)Instruction limit reached! % 9.73/2.37 % (3345989)------------------------------ % 9.73/2.37 % (3345989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.73/2.37 % (3345989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.73/2.37 % (3345989)CaDiCaL version: 2.1.3 % 9.73/2.37 % (3345989)Termination reason: Instruction limit % 9.73/2.37 % (3345989)Termination phase: Saturation % 9.73/2.37 % (3345989)Time elapsed: 0.059 s % 9.73/2.37 % (3345989)Peak memory usage: 90 MB % 9.73/2.37 % (3345989)Instructions burned: 130 (million) % 9.73/2.37 % (3345988)Instruction limit reached! % 9.73/2.37 % (3345988)------------------------------ % 9.73/2.37 % (3345988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.73/2.37 % (3345988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.73/2.37 % (3345988)CaDiCaL version: 2.1.3 % 9.73/2.37 % (3345988)Termination reason: Instruction limit % 9.73/2.37 % (3345988)Termination phase: Saturation % 9.73/2.37 % (3345988)Time elapsed: 0.068 s % 9.73/2.37 % (3345988)Peak memory usage: 90 MB % 9.73/2.37 % (3345988)Instructions burned: 139 (million) % 9.73/2.37 % (3345986)------------------------------ % 9.73/2.37 % (3345986)------------------------------ % 9.73/2.37 % (3345997)lrs+10_1_sil=8000:sp=occurrence:random_seed=4200320358:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 9.73/2.37 % (3345997)Refutation not found, incomplete strategy % 9.73/2.37 % (3345997)------------------------------ % 9.73/2.37 % (3345997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.73/2.37 % (3345997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.73/2.37 % (3345997)CaDiCaL version: 2.1.3 % 9.73/2.37 % (3345997)Termination reason: Refutation not found, incomplete strategy % 9.73/2.37 % (3345997)Time elapsed: 0.004 s % 9.73/2.37 % (3345997)Peak memory usage: 87 MB % 10.73/2.60 % (3345997)Instructions burned: 4 (million) % 10.73/2.60 % (3345998)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1737617609:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 10.73/2.60 % (3345998)Refutation not found, incomplete strategy % 10.73/2.60 % (3345998)------------------------------ % 10.73/2.60 % (3345998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.73/2.60 % (3345998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.73/2.60 % (3345998)CaDiCaL version: 2.1.3 % 10.73/2.60 % (3345998)Termination reason: Refutation not found, incomplete strategy % 10.73/2.60 % (3345998)Time elapsed: 0.011 s % 10.73/2.60 % (3345998)Peak memory usage: 88 MB % 10.73/2.60 % (3345998)Instructions burned: 22 (million) % 10.73/2.60 % (3345999)lrs+1011_1_sil=32000:sp=occurrence:random_seed=963936768:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 10.73/2.60 % (3345999)Refutation not found, incomplete strategy % 10.73/2.60 % (3345999)------------------------------ % 10.73/2.60 % (3345999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.73/2.60 % (3345999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.73/2.60 % (3345999)CaDiCaL version: 2.1.3 % 10.73/2.60 % (3345999)Termination reason: Refutation not found, incomplete strategy % 10.73/2.60 % (3345999)Time elapsed: 0.002 s % 10.73/2.60 % (3345999)Peak memory usage: 87 MB % 10.73/2.60 % (3345999)Instructions burned: 4 (million) % 10.73/2.60 % (3345987)------------------------------ % 10.73/2.60 % (3345987)------------------------------ % 10.73/2.60 % (3345999)------------------------------ % 10.73/2.60 % (3345999)------------------------------ % 10.73/2.60 % (3346003)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=1879259841:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.73/2.60 % (3345997)------------------------------ % 10.73/2.60 % (3345997)------------------------------ % 10.73/2.60 % (3345998)------------------------------ % 10.73/2.60 % (3345998)------------------------------ % 10.73/2.60 % (3346004)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2184690586:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 10.73/2.60 % (3346003)Instruction limit reached! % 10.73/2.60 % (3346003)------------------------------ % 10.73/2.60 % (3346003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.73/2.60 % (3346003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.73/2.60 % (3346003)CaDiCaL version: 2.1.3 % 10.73/2.60 % (3346003)Termination reason: Instruction limit % 10.73/2.60 % (3346003)Termination phase: Saturation % 10.73/2.60 % (3346003)Time elapsed: 0.133 s % 10.73/2.60 % (3346003)Peak memory usage: 93 MB % 10.73/2.60 % (3346003)Instructions burned: 248 (million) % 10.73/2.60 % (3346004)Refutation not found, incomplete strategy % 10.73/2.60 % (3346004)------------------------------ % 10.73/2.60 % (3346004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.73/2.60 % (3346004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.73/2.60 % (3346004)CaDiCaL version: 2.1.3 % 10.73/2.60 % (3346004)Termination reason: Refutation not found, incomplete strategy % 10.73/2.60 % (3346004)Time elapsed: 0.005 s % 10.73/2.60 % (3346004)Peak memory usage: 87 MB % 10.73/2.60 % (3346004)Instructions burned: 7 (million) % 10.73/2.60 % (3346006)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=26207974:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 10.73/2.60 % (3346007)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2533155566:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 10.73/2.60 % (3346007)Instruction limit reached! % 10.73/2.60 % (3346007)------------------------------ % 10.73/2.60 % (3346007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.73/2.60 % (3346007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.73/2.60 % (3346007)CaDiCaL version: 2.1.3 % 10.73/2.60 % (3346007)Termination reason: Instruction limit % 10.73/2.60 % (3346007)Termination phase: Saturation % 10.73/2.60 % (3346007)Time elapsed: 0.056 s % 10.73/2.60 % (3346007)Peak memory usage: 90 MB % 10.73/2.60 % (3346007)Instructions burned: 113 (million) % 10.73/2.60 % (3346009)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=601803774:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 11.92/2.88 % (3345985)Refutation not found, incomplete strategy % 11.92/2.88 % (3345985)------------------------------ % 11.92/2.88 % (3345985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3345985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3345985)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3345985)Termination reason: Refutation not found, incomplete strategy % 11.92/2.88 % (3345985)Time elapsed: 0.777 s % 11.92/2.88 % (3345985)Peak memory usage: 145 MB % 11.92/2.88 % (3345985)Instructions burned: 1186 (million) % 11.92/2.88 % (3346009)Instruction limit reached! % 11.92/2.88 % (3346009)------------------------------ % 11.92/2.88 % (3346009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3346009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3346009)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3346009)Termination reason: Instruction limit % 11.92/2.88 % (3346009)Termination phase: Saturation % 11.92/2.88 % (3346009)Time elapsed: 0.057 s % 11.92/2.88 % (3346009)Peak memory usage: 90 MB % 11.92/2.88 % (3346009)Instructions burned: 127 (million) % 11.92/2.88 % (3346004)------------------------------ % 11.92/2.88 % (3346004)------------------------------ % 11.92/2.88 % (3346012)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=395584674:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 11.92/2.88 % (3346012)Instruction limit reached! % 11.92/2.88 % (3346012)------------------------------ % 11.92/2.88 % (3346012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3346012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3346012)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3346012)Termination reason: Instruction limit % 11.92/2.88 % (3346012)Termination phase: Saturation % 11.92/2.88 % (3346012)Time elapsed: 0.057 s % 11.92/2.88 % (3346012)Peak memory usage: 90 MB % 11.92/2.88 % (3346012)Instructions burned: 116 (million) % 11.92/2.88 % (3346014)lrs+10_1_sil=8000:sp=occurrence:random_seed=2581736777:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 11.92/2.88 % (3346014)Refutation not found, incomplete strategy % 11.92/2.88 % (3346014)------------------------------ % 11.92/2.88 % (3346014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3346014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3346014)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3346014)Termination reason: Refutation not found, incomplete strategy % 11.92/2.88 % (3346014)Time elapsed: 0.005 s % 11.92/2.88 % (3346014)Peak memory usage: 87 MB % 11.92/2.88 % (3346014)Instructions burned: 7 (million) % 11.92/2.88 % (3346015)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1049256422:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 11.92/2.88 % (3345985)------------------------------ % 11.92/2.88 % (3345985)------------------------------ % 11.92/2.88 % (3346015)Refutation not found, incomplete strategy % 11.92/2.88 % (3346015)------------------------------ % 11.92/2.88 % (3346015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3346015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3346015)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3346015)Termination reason: Refutation not found, incomplete strategy % 11.92/2.88 % (3346015)Time elapsed: 0.070 s % 11.92/2.88 % (3346015)Peak memory usage: 91 MB % 11.92/2.88 % (3346015)Instructions burned: 137 (million) % 11.92/2.88 % (3346017)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3992999791:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 11.92/2.88 % (3346020)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2265104653:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 11.92/2.88 % (3346014)------------------------------ % 11.92/2.88 % (3346014)------------------------------ % 11.92/2.88 % (3346020)Instruction limit reached! % 11.92/2.88 % (3346020)------------------------------ % 11.92/2.88 % (3346020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.92/2.88 % (3346020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.92/2.88 % (3346020)CaDiCaL version: 2.1.3 % 11.92/2.88 % (3346020)Termination reason: Instruction limit % 11.92/2.88 % (3346020)Termination phase: Saturation % 11.92/2.88 % (3346020)Time elapsed: 0.071 s % 12.53/2.92 % (3346020)Peak memory usage: 91 MB % 12.53/2.92 % (3346020)Instructions burned: 134 (million) % 12.53/2.92 % (3346015)------------------------------ % 12.53/2.92 % (3346015)------------------------------ % 12.53/2.92 % (3346006)Instruction limit reached! % 12.53/2.92 % (3346006)------------------------------ % 12.53/2.92 % (3346006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.53/2.92 % (3346006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.53/2.92 % (3346006)CaDiCaL version: 2.1.3 % 12.53/2.92 % (3346006)Termination reason: Instruction limit % 12.53/2.92 % (3346006)Termination phase: Saturation % 12.53/2.92 % (3346006)Time elapsed: 0.777 s % 12.53/2.92 % (3346006)Peak memory usage: 148 MB % 12.53/2.92 % (3346006)Instructions burned: 2354 (million) % 12.53/2.92 % (3346023)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3948939410:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 12.53/2.92 % (3346023)Refutation not found, incomplete strategy % 12.53/2.92 % (3346023)------------------------------ % 12.53/2.92 % (3346023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.53/2.92 % (3346023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.53/2.92 % (3346023)CaDiCaL version: 2.1.3 % 12.53/2.92 % (3346023)Termination reason: Refutation not found, incomplete strategy % 12.53/2.92 % (3346023)Time elapsed: 0.005 s % 12.53/2.92 % (3346023)Peak memory usage: 87 MB % 12.53/2.92 % (3346023)Instructions burned: 7 (million) % 12.53/2.92 % (3346024)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2022644427:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 12.53/2.92 % (3346025)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=3148693949:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 12.53/2.92 % (3346027)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=246805896:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 12.53/2.92 % (3346025)Refutation not found, incomplete strategy % 12.53/2.92 % (3346025)------------------------------ % 12.53/2.92 % (3346025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.53/2.92 % (3346025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.53/2.92 % (3346025)CaDiCaL version: 2.1.3 % 12.53/2.92 % (3346025)Termination reason: Refutation not found, incomplete strategy % 12.53/2.92 % (3346025)Time elapsed: 0.014 s % 12.53/2.92 % (3346025)Peak memory usage: 88 MB % 12.53/2.92 % (3346025)Instructions burned: 27 (million) % 12.53/2.92 [W927 21:43:25.510219914 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. % 12.53/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.53/2.92 [W927 21:43:25.510249440 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. % 12.53/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.53/2.92 [W927 21:43:25.510290654 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. % 12.53/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.53/2.92 [W927 21:43:25.510303907 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. % 12.53/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.53/2.92 [W927 21:43:25.510332087 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. % 12.53/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.53/2.92 [W927 21:43:25.510344207 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510372120 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510383307 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510469107 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510487257 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510513574 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 [W927 21:43:25.510523837 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. % 17.84/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.84/3.50 % (3346027)Instruction limit reached! % 17.84/3.50 % (3346027)------------------------------ % 17.84/3.50 % (3346027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.84/3.50 % (3346027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.84/3.50 % (3346027)CaDiCaL version: 2.1.3 % 17.84/3.50 % (3346027)Termination reason: Instruction limit % 17.84/3.50 % (3346027)Termination phase: Saturation % 17.84/3.50 % (3346027)Time elapsed: 0.032 s % 17.84/3.50 % (3346027)Peak memory usage: 90 MB % 17.84/3.50 % (3346027)Instructions burned: 136 (million) % 17.84/3.50 % (3346023)------------------------------ % 17.84/3.50 % (3346023)------------------------------ % 17.84/3.50 % (3346031)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3034305694:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi) % 17.84/3.50 % (3346031)Refutation not found, incomplete strategy % 17.84/3.50 % (3346031)------------------------------ % 17.84/3.50 % (3346031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.84/3.50 % (3346031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.84/3.50 % (3346031)CaDiCaL version: 2.1.3 % 17.84/3.50 % (3346031)Termination reason: Refutation not found, incomplete strategy % 17.84/3.50 % (3346031)Time elapsed: 0.002 s % 17.84/3.50 % (3346031)Peak memory usage: 87 MB % 17.84/3.50 % (3346031)Instructions burned: 4 (million) % 17.84/3.50 % (3346017)Refutation not found, incomplete strategy % 17.84/3.50 % (3346017)------------------------------ % 17.84/3.50 % (3346017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.84/3.50 % (3346017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.84/3.50 % (3346017)CaDiCaL version: 2.1.3 % 17.84/3.50 % (3346017)Termination reason: Refutation not found, incomplete strategy % 17.84/3.50 % (3346017)Time elapsed: 0.567 s % 17.84/3.50 % (3346017)Peak memory usage: 126 MB % 17.84/3.50 % (3346017)Instructions burned: 837 (million) % 17.84/3.50 % (3346025)------------------------------ % 17.84/3.50 % (3346025)------------------------------ % 17.84/3.50 % (3346032)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=366349948:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi) % 30.29/5.19 % (3346032)Refutation not found, incomplete strategy % 30.29/5.19 % (3346032)------------------------------ % 30.29/5.19 % (3346032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.29/5.19 % (3346032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.29/5.19 % (3346032)CaDiCaL version: 2.1.3 % 30.29/5.19 % (3346032)Termination reason: Refutation not found, incomplete strategy % 30.29/5.19 % (3346032)Time elapsed: 0.004 s % 30.29/5.19 % (3346032)Peak memory usage: 87 MB % 30.29/5.19 % (3346032)Instructions burned: 4 (million) % 30.29/5.19 % (3346031)------------------------------ % 30.29/5.19 % (3346031)------------------------------ % 30.29/5.19 [W927 21:43:25.832517761 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832550761 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832590727 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832604074 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832634501 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832646451 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832672867 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832684614 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832710324 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832722254 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.29/5.19 [W927 21:43:25.832747961 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. % 30.29/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.35/5.34 [W927 21:43:25.832759904 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. % 31.35/5.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.35/5.34 % (3346034)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=299297461:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi) % 31.35/5.34 % (3346017)------------------------------ % 31.35/5.34 % (3346017)------------------------------ % 31.35/5.34 % (3346036)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=3035239996:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi) % 31.35/5.34 % (3346036)Instruction limit reached! % 31.35/5.34 % (3346036)------------------------------ % 31.35/5.34 % (3346036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.34 % (3346036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.34 % (3346036)CaDiCaL version: 2.1.3 % 31.35/5.34 % (3346036)Termination reason: Instruction limit % 31.35/5.34 % (3346036)Termination phase: Saturation % 31.35/5.34 % (3346036)Time elapsed: 0.042 s % 31.35/5.34 % (3346036)Peak memory usage: 91 MB % 31.35/5.34 % (3346036)Instructions burned: 154 (million) % 31.35/5.34 % (3346024)Refutation not found, incomplete strategy % 31.35/5.34 % (3346024)------------------------------ % 31.35/5.34 % (3346024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.34 % (3346024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.34 % (3346024)CaDiCaL version: 2.1.3 % 31.35/5.34 % (3346024)Termination reason: Refutation not found, incomplete strategy % 31.35/5.34 % (3346024)Time elapsed: 0.574 s % 31.35/5.34 % (3346024)Peak memory usage: 126 MB % 31.35/5.34 % (3346024)Instructions burned: 834 (million) % 31.35/5.34 % (3346032)------------------------------ % 31.35/5.34 % (3346032)------------------------------ % 31.35/5.34 % (3346038)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3747864164:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi) % 31.35/5.34 % (3346040)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1779176163:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi) % 31.35/5.34 % (3346040)Refutation not found, incomplete strategy % 31.35/5.34 % (3346040)------------------------------ % 31.35/5.34 % (3346040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.34 % (3346040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.34 % (3346040)CaDiCaL version: 2.1.3 % 31.35/5.34 % (3346040)Termination reason: Refutation not found, incomplete strategy % 31.35/5.34 % (3346040)Time elapsed: 0.040 s % 31.35/5.34 % (3346040)Peak memory usage: 91 MB % 31.35/5.34 % (3346040)Instructions burned: 148 (million) % 31.35/5.34 % (3346041)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=2754297416:s2a=on:i=185:s2at=1.8:fdi=4_2977 on theBenchmark for (2977ds/185Mi) % 31.35/5.34 % (3346024)------------------------------ % 31.35/5.34 % (3346024)------------------------------ % 31.35/5.34 % (3346040)------------------------------ % 31.35/5.34 % (3346040)------------------------------ % 31.35/5.34 % (3346041)Instruction limit reached! % 31.35/5.34 % (3346041)------------------------------ % 31.35/5.34 % (3346041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.35/5.34 % (3346041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.35/5.34 % (3346041)CaDiCaL version: 2.1.3 % 31.35/5.34 % (3346041)Termination reason: Instruction limit % 31.35/5.34 % (3346041)Termination phase: Saturation % 31.35/5.34 % (3346041)Time elapsed: 0.099 s % 31.35/5.34 % (3346041)Peak memory usage: 91 MB % 31.35/5.34 % (3346041)Instructions burned: 186 (million) % 31.35/5.34 % (3346046)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=556496132:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2974 on theBenchmark for (2974ds/4850Mi) % 31.35/5.34 % (3346045)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2927718112:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2975 on theBenchmark for (2975ds/193Mi) % 38.88/6.43 % (3346045)Refutation not found, incomplete strategy % 38.88/6.43 % (3346045)------------------------------ % 38.88/6.43 % (3346045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.88/6.43 % (3346045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.88/6.43 % (3346045)CaDiCaL version: 2.1.3 % 38.88/6.43 % (3346045)Termination reason: Refutation not found, incomplete strategy % 38.88/6.43 % (3346045)Time elapsed: 0.007 s % 38.88/6.43 % (3346045)Peak memory usage: 87 MB % 38.88/6.43 % (3346045)Instructions burned: 9 (million) % 38.88/6.43 % (3346046)Refutation not found, incomplete strategy % 38.88/6.43 % (3346046)------------------------------ % 38.88/6.43 % (3346046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.88/6.43 % (3346046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.88/6.43 % (3346046)CaDiCaL version: 2.1.3 % 38.88/6.43 % (3346046)Termination reason: Refutation not found, incomplete strategy % 38.88/6.43 % (3346046)Time elapsed: 0.030 s % 38.88/6.43 % (3346046)Peak memory usage: 90 MB % 38.88/6.43 % (3346046)Instructions burned: 115 (million) % 38.88/6.43 % (3346047)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=617063727:i=12111:sd=1:ss=included_2974 on theBenchmark for (2974ds/12111Mi) % 38.88/6.43 % (3346046)------------------------------ % 38.88/6.43 % (3346046)------------------------------ % 38.88/6.43 % (3346045)------------------------------ % 38.88/6.43 % (3346045)------------------------------ % 38.88/6.43 % (3346051)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=943811941:i=319:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/319Mi) % 38.88/6.43 % (3346051)Instruction limit reached! % 38.88/6.43 % (3346051)------------------------------ % 38.88/6.43 % (3346051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.88/6.43 % (3346051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.88/6.43 % (3346051)CaDiCaL version: 2.1.3 % 38.88/6.43 % (3346051)Termination reason: Instruction limit % 38.88/6.43 % (3346051)Termination phase: Saturation % 38.88/6.43 % (3346051)Time elapsed: 0.095 s % 38.88/6.43 % (3346051)Peak memory usage: 93 MB % 38.88/6.43 % (3346051)Instructions burned: 323 (million) % 38.88/6.43 % (3346052)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3967492769:i=2064:ep=RST_2971 on theBenchmark for (2971ds/2064Mi) % 38.88/6.43 % (3346052)Refutation not found, incomplete strategy % 38.88/6.43 % (3346052)------------------------------ % 38.88/6.43 % (3346052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.88/6.43 % (3346052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.88/6.43 % (3346052)CaDiCaL version: 2.1.3 % 38.88/6.43 % (3346052)Termination reason: Refutation not found, incomplete strategy % 38.88/6.43 % (3346052)Time elapsed: 0.063 s % 38.88/6.43 % (3346052)Peak memory usage: 91 MB % 38.88/6.43 % (3346052)Instructions burned: 139 (million) % 38.88/6.43 % (3346054)dis-1011_128_sil=32000:random_seed=1108492272:i=3706:ep=RST:av=off_2969 on theBenchmark for (2969ds/3706Mi) % 38.88/6.43 % (3346052)------------------------------ % 38.88/6.43 % (3346052)------------------------------ % 38.88/6.43 % (3346057)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=95667251:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2966 on theBenchmark for (2966ds/757Mi) % 38.88/6.43 % (3346057)Refutation not found, incomplete strategy % 38.88/6.43 % (3346057)------------------------------ % 38.88/6.43 % (3346057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.88/6.43 % (3346057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.88/6.43 % (3346057)CaDiCaL version: 2.1.3 % 38.88/6.43 % (3346057)Termination reason: Refutation not found, incomplete strategy % 38.88/6.43 % (3346057)Time elapsed: 0.004 s % 38.88/6.43 % (3346057)Peak memory usage: 87 MB % 38.88/6.43 % (3346057)Instructions burned: 4 (million) % 38.88/6.43 % (3346057)------------------------------ % 38.88/6.43 % (3346057)------------------------------ % 38.88/6.43 % (3346059)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=17420414:i=13913:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/13913Mi) % 38.88/6.43 [W927 21:43:27.104614530 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104646927 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104688674 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104699590 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104725510 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104735967 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104760824 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104771404 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104796310 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104854604 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104891564 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 [W927 21:43:27.104902974 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. % 41.67/6.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.67/6.85 % (3346054)Instruction limit reached! % 41.67/6.85 % (3346054)------------------------------ % 41.67/6.85 % (3346054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.67/6.85 % (3346054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.67/6.85 % (3346054)CaDiCaL version: 2.1.3 % 41.67/6.85 % (3346054)Termination reason: Instruction limit % 41.67/6.85 % (3346054)Termination phase: Saturation % 41.67/6.85 % (3346054)Time elapsed: 1.290 s % 68.84/10.67 % (3346054)Peak memory usage: 134 MB % 68.84/10.67 % (3346054)Instructions burned: 3707 (million) % 68.84/10.67 % (3346059)Refutation not found, incomplete strategy % 68.84/10.67 % (3346059)------------------------------ % 68.84/10.67 % (3346059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.84/10.67 % (3346059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.84/10.67 % (3346059)CaDiCaL version: 2.1.3 % 68.84/10.67 % (3346059)Termination reason: Refutation not found, incomplete strategy % 68.84/10.67 % (3346059)Time elapsed: 0.553 s % 68.84/10.67 % (3346059)Peak memory usage: 126 MB % 68.84/10.67 % (3346059)Instructions burned: 836 (million) % 68.84/10.67 % (3346061)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=719296870:i=9925:aac=none_2955 on theBenchmark for (2955ds/9925Mi) % 68.84/10.67 % (3346059)------------------------------ % 68.84/10.67 % (3346059)------------------------------ % 68.84/10.67 % (3346063)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2883355308:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2953 on theBenchmark for (2953ds/2479Mi) % 68.84/10.67 % (3346063)Refutation not found, incomplete strategy % 68.84/10.67 % (3346063)------------------------------ % 68.84/10.67 % (3346063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.84/10.67 % (3346063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.84/10.67 % (3346063)CaDiCaL version: 2.1.3 % 68.84/10.67 % (3346063)Termination reason: Refutation not found, incomplete strategy % 68.84/10.67 % (3346063)Time elapsed: 0.003 s % 68.84/10.67 % (3346063)Peak memory usage: 87 MB % 68.84/10.67 % (3346063)Instructions burned: 9 (million) % 68.84/10.67 % (3346063)------------------------------ % 68.84/10.67 % (3346063)------------------------------ % 68.84/10.67 % (3346065)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=961810558:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2950 on theBenchmark for (2950ds/440Mi) % 68.84/10.67 % (3346065)Instruction limit reached! % 68.84/10.67 % (3346065)------------------------------ % 68.84/10.67 % (3346065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.84/10.67 % (3346065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.84/10.67 % (3346065)CaDiCaL version: 2.1.3 % 68.84/10.67 % (3346065)Termination reason: Instruction limit % 68.84/10.67 % (3346065)Termination phase: Saturation % 68.84/10.67 % (3346065)Time elapsed: 0.124 s % 68.84/10.67 % (3346065)Peak memory usage: 94 MB % 68.84/10.67 % (3346065)Instructions burned: 441 (million) % 68.84/10.67 % (3346067)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=916216793:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2947 on theBenchmark for (2947ds/11145Mi) % 68.84/10.67 % (3346061)Refutation not found, incomplete strategy % 68.84/10.67 % (3346061)------------------------------ % 68.84/10.67 % (3346061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.84/10.67 % (3346061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.84/10.67 % (3346061)CaDiCaL version: 2.1.3 % 68.84/10.67 % (3346061)Termination reason: Refutation not found, incomplete strategy % 68.84/10.67 % (3346061)Time elapsed: 0.746 s % 68.84/10.67 % (3346061)Peak memory usage: 145 MB % 68.84/10.67 % (3346061)Instructions burned: 1156 (million) % 68.84/10.67 [W927 21:43:28.347006605 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. % 68.84/10.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.84/10.67 [W927 21:43:28.347029548 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. % 68.84/10.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.84/10.67 [W927 21:43:28.347050567 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. % 68.84/10.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.84/10.67 [W927 21:43:28.347057915 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347071531 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347077084 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347090007 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347095365 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347107928 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347113155 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347125624 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 [W927 21:43:28.347131115 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. % 72.10/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.10/11.05 % (3346061)------------------------------ % 72.10/11.05 % (3346061)------------------------------ % 72.10/11.05 % (3346067)Refutation not found, incomplete strategy % 72.10/11.05 % (3346067)------------------------------ % 72.10/11.05 % (3346067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.10/11.05 % (3346067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.10/11.06 % (3346067)CaDiCaL version: 2.1.3 % 72.10/11.06 % (3346067)Termination reason: Refutation not found, incomplete strategy % 72.10/11.06 % (3346067)Time elapsed: 0.319 s % 72.10/11.06 % (3346067)Peak memory usage: 126 MB % 72.10/11.06 % (3346067)Instructions burned: 840 (million) % 72.10/11.06 % (3346069)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=472609756:cts=off:i=3034:av=off:er=known:fsd=on_2943 on theBenchmark for (2943ds/3034Mi) % 72.10/11.06 % (3346067)------------------------------ % 72.10/11.06 % (3346067)------------------------------ % 72.10/11.06 % (3346071)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2039607484:st=2:s2a=on:i=524:s2at=2:ss=axioms_2941 on theBenchmark for (2941ds/524Mi) % 72.10/11.06 % (3346071)Refutation not found, incomplete strategy % 72.10/11.06 % (3346071)------------------------------ % 72.10/11.06 % (3346071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.10/11.06 % (3346071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.44 % (3346071)CaDiCaL version: 2.1.3 % 74.52/11.44 % (3346071)Termination reason: Refutation not found, incomplete strategy % 74.52/11.44 % (3346071)Time elapsed: 0.005 s % 74.52/11.44 % (3346071)Peak memory usage: 88 MB % 74.52/11.44 % (3346071)Instructions burned: 14 (million) % 74.52/11.44 % (3346034)Instruction limit reached! % 74.52/11.44 % (3346034)------------------------------ % 74.52/11.44 % (3346034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.52/11.44 % (3346034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.44 % (3346034)CaDiCaL version: 2.1.3 % 74.52/11.44 % (3346034)Termination reason: Instruction limit % 74.52/11.44 % (3346034)Termination phase: Saturation % 74.52/11.44 % (3346034)Time elapsed: 3.846 s % 74.52/11.44 % (3346034)Peak memory usage: 200 MB % 74.52/11.44 % (3346034)Instructions burned: 6061 (million) % 74.52/11.44 % (3346071)------------------------------ % 74.52/11.44 % (3346071)------------------------------ % 74.52/11.44 % (3346073)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2471408493:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2939 on theBenchmark for (2939ds/1016Mi) % 74.52/11.44 % (3346073)Refutation not found, incomplete strategy % 74.52/11.45 % (3346073)------------------------------ % 74.52/11.45 % (3346073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.52/11.45 % (3346073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.45 % (3346073)CaDiCaL version: 2.1.3 % 74.52/11.45 % (3346073)Termination reason: Refutation not found, incomplete strategy % 74.52/11.45 % (3346073)Time elapsed: 0.004 s % 74.52/11.45 % (3346073)Peak memory usage: 87 MB % 74.52/11.45 % (3346073)Instructions burned: 4 (million) % 74.52/11.45 % (3346074)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3581753290:i=14123:bd=preordered:ins=4_2938 on theBenchmark for (2938ds/14123Mi) % 74.52/11.45 % (3346073)------------------------------ % 74.52/11.45 % (3346073)------------------------------ % 74.52/11.45 % (3346078)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=41371698:i=5781:kws=precedence:bd=all:rawr=on_2935 on theBenchmark for (2935ds/5781Mi) % 74.52/11.45 % (3346069)Instruction limit reached! % 74.52/11.45 % (3346069)------------------------------ % 74.52/11.45 % (3346069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.52/11.45 % (3346069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.45 % (3346069)CaDiCaL version: 2.1.3 % 74.52/11.45 % (3346069)Termination reason: Instruction limit % 74.52/11.45 % (3346069)Termination phase: Saturation % 74.52/11.45 % (3346069)Time elapsed: 1.639 s % 74.52/11.45 % (3346069)Peak memory usage: 146 MB % 74.52/11.45 % (3346069)Instructions burned: 3034 (million) % 74.52/11.45 % (3346080)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=2839816270:i=2448:gtgl=5:bd=preordered:gtg=all_2925 on theBenchmark for (2925ds/2448Mi) % 74.52/11.45 % (3346080)Instruction limit reached! % 74.52/11.45 % (3346080)------------------------------ % 74.52/11.45 % (3346080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.52/11.45 % (3346080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.45 % (3346080)CaDiCaL version: 2.1.3 % 74.52/11.45 % (3346080)Termination reason: Instruction limit % 74.52/11.45 % (3346080)Termination phase: Saturation % 74.52/11.45 % (3346080)Time elapsed: 1.435 s % 74.52/11.45 % (3346080)Peak memory usage: 147 MB % 74.52/11.45 % (3346080)Instructions burned: 2449 (million) % 74.52/11.45 % (3346082)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2255608222:i=3223:kws=precedence:fgj=on:av=off_2909 on theBenchmark for (2909ds/3223Mi) % 74.52/11.45 % (3346047)Instruction limit reached! % 74.52/11.45 % (3346047)------------------------------ % 74.52/11.45 % (3346047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.52/11.45 % (3346047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.52/11.45 % (3346047)CaDiCaL version: 2.1.3 % 74.52/11.45 % (3346047)Termination reason: Instruction limit % 74.52/11.45 % (3346047)Termination phase: Saturation % 74.52/11.45 % (3346047)Time elapsed: 6.915 s % 74.52/11.45 % (3346047)Peak memory usage: 237 MB % 74.52/11.45 % (3346047)Instructions burned: 12113 (million) % 74.52/11.45 % (3346084)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2500151651:st=5.6:i=2033:sd=3:ss=axioms_2903 on theBenchmark for (2903ds/2033Mi) % 77.32/12.02 % (3346078)Instruction limit reached! % 77.32/12.02 % (3346078)------------------------------ % 77.32/12.02 % (3346078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.32/12.02 % (3346078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.32/12.02 % (3346078)CaDiCaL version: 2.1.3 % 77.32/12.02 % (3346078)Termination reason: Instruction limit % 77.32/12.02 % (3346078)Termination phase: Saturation % 77.32/12.02 % (3346078)Time elapsed: 3.344 s % 77.32/12.02 % (3346078)Peak memory usage: 131 MB % 77.32/12.02 % (3346078)Instructions burned: 5781 (million) % 77.32/12.02 % (3346086)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4032460886:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2900 on theBenchmark for (2900ds/2055Mi) % 77.32/12.02 [W927 21:43:33.968639286 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968671743 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968708833 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968721053 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968746563 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968757776 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968783300 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968794640 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968819026 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968830283 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. % 77.32/12.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.32/12.02 [W927 21:43:33.968854010 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.968865236 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 % (3346084)Refutation not found, incomplete strategy % 79.61/12.17 % (3346084)------------------------------ % 79.61/12.17 % (3346084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.61/12.17 % (3346084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.61/12.17 % (3346084)CaDiCaL version: 2.1.3 % 79.61/12.17 % (3346084)Termination reason: Refutation not found, incomplete strategy % 79.61/12.17 % (3346084)Time elapsed: 0.556 s % 79.61/12.17 % (3346084)Peak memory usage: 126 MB % 79.61/12.17 % (3346084)Instructions burned: 838 (million) % 79.61/12.17 [W927 21:43:33.359050317 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359102620 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359143584 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359155380 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359185727 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359195877 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359221467 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359233721 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359258864 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359271194 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. % 79.61/12.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.61/12.17 [W927 21:43:33.359297724 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. % 81.97/12.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.97/12.84 [W927 21:43:33.359309621 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. % 81.97/12.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.97/12.84 % (3346084)------------------------------ % 81.97/12.84 % (3346084)------------------------------ % 81.97/12.84 % (3346086)Refutation not found, incomplete strategy % 81.97/12.84 % (3346086)------------------------------ % 81.97/12.84 % (3346086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.97/12.84 % (3346086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.97/12.84 % (3346086)CaDiCaL version: 2.1.3 % 81.97/12.84 % (3346086)Termination reason: Refutation not found, incomplete strategy % 81.97/12.84 % (3346086)Time elapsed: 0.631 s % 81.97/12.84 % (3346086)Peak memory usage: 127 MB % 81.97/12.84 % (3346086)Instructions burned: 854 (million) % 81.97/12.84 % (3346088)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=1762291074:i=21611:sd=3:ss=axioms_2894 on theBenchmark for (2894ds/21611Mi) % 81.97/12.84 % (3346038)Instruction limit reached! % 81.97/12.84 % (3346038)------------------------------ % 81.97/12.84 % (3346038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.97/12.84 % (3346038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.97/12.84 % (3346038)CaDiCaL version: 2.1.3 % 81.97/12.84 % (3346038)Termination reason: Instruction limit % 81.97/12.84 % (3346038)Termination phase: Saturation % 81.97/12.84 % (3346038)Time elapsed: 8.477 s % 81.97/12.84 % (3346038)Peak memory usage: 232 MB % 81.97/12.84 % (3346038)Instructions burned: 14155 (million) % 81.97/12.84 % (3346074)Instruction limit reached! % 81.97/12.84 % (3346074)------------------------------ % 81.97/12.84 % (3346074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.97/12.84 % (3346074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.97/12.84 % (3346074)CaDiCaL version: 2.1.3 % 81.97/12.84 % (3346074)Termination reason: Instruction limit % 81.97/12.84 % (3346074)Termination phase: Saturation % 81.97/12.84 % (3346074)Time elapsed: 4.666 s % 81.97/12.84 % (3346074)Peak memory usage: 224 MB % 81.97/12.84 % (3346074)Instructions burned: 14124 (million) % 81.97/12.84 % (3346090)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3323848258:i=4835:sd=13:ss=axioms:sgt=23_2891 on theBenchmark for (2891ds/4835Mi) % 81.97/12.84 % (3346090)Refutation not found, incomplete strategy % 81.97/12.84 % (3346090)------------------------------ % 81.97/12.84 % (3346090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.97/12.84 % (3346090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.97/12.84 % (3346090)CaDiCaL version: 2.1.3 % 81.97/12.84 % (3346090)Termination reason: Refutation not found, incomplete strategy % 81.97/12.84 % (3346090)Time elapsed: 0.004 s % 81.97/12.84 % (3346090)Peak memory usage: 87 MB % 81.97/12.84 % (3346090)Instructions burned: 4 (million) % 81.97/12.84 % (3346086)------------------------------ % 81.97/12.84 % (3346086)------------------------------ % 81.97/12.84 % (3346091)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=1675364033:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2890 on theBenchmark for (2890ds/797Mi) % 81.97/12.84 [W927 21:43:34.932368070 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. % 81.97/12.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.97/12.84 [W927 21:43:34.932466354 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. % 81.97/12.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932517427 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932529974 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932555804 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932566844 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932591877 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932602977 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932627337 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932638311 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932663714 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 [W927 21:43:34.932674717 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. % 89.91/13.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.91/13.78 % (3346082)Instruction limit reached! % 89.91/13.78 % (3346082)------------------------------ % 89.91/13.78 % (3346082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.91/13.78 % (3346082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.91/13.78 % (3346082)CaDiCaL version: 2.1.3 % 89.91/13.78 % (3346082)Termination reason: Instruction limit % 89.91/13.78 % (3346082)Termination phase: Saturation % 89.91/13.78 % (3346082)Time elapsed: 1.954 s % 89.91/13.78 % (3346082)Peak memory usage: 151 MB % 89.91/13.78 % (3346082)Instructions burned: 3224 (million) % 89.91/13.78 % (3346090)------------------------------ % 89.91/13.78 % (3346090)------------------------------ % 89.91/13.78 % (3346093)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1596124989:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2890 on theBenchmark for (2890ds/2326Mi) % 89.91/13.78 % (3346091)Instruction limit reached! % 89.91/13.78 % (3346091)------------------------------ % 89.91/13.78 % (3346091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.98/14.71 % (3346091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.98/14.71 % (3346091)CaDiCaL version: 2.1.3 % 96.98/14.71 % (3346091)Termination reason: Instruction limit % 96.98/14.71 % (3346091)Termination phase: Saturation % 96.98/14.71 % (3346091)Time elapsed: 0.230 s % 96.98/14.71 % (3346091)Peak memory usage: 94 MB % 96.98/14.71 % (3346091)Instructions burned: 798 (million) % 96.98/14.71 % (3346088)Refutation not found, incomplete strategy % 96.98/14.71 % (3346088)------------------------------ % 96.98/14.71 % (3346088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.98/14.71 % (3346088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.98/14.71 % (3346088)CaDiCaL version: 2.1.3 % 96.98/14.71 % (3346088)Termination reason: Refutation not found, incomplete strategy % 96.98/14.71 % (3346088)Time elapsed: 0.561 s % 96.98/14.71 % (3346088)Peak memory usage: 126 MB % 96.98/14.71 % (3346088)Instructions burned: 836 (million) % 96.98/14.71 % (3346095)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1013856096:i=6038:nm=6_2888 on theBenchmark for (2888ds/6038Mi) % 96.98/14.71 % (3346096)lrs+10_1_sil=32000:sp=occurrence:random_seed=4225572060:st=2:i=33334:sd=3:ss=included:sgt=32_2887 on theBenchmark for (2887ds/33334Mi) % 96.98/14.71 % (3346093)Refutation not found, incomplete strategy % 96.98/14.71 % (3346093)------------------------------ % 96.98/14.71 % (3346093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.98/14.71 % (3346093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.98/14.71 % (3346093)CaDiCaL version: 2.1.3 % 96.98/14.71 % (3346093)Termination reason: Refutation not found, incomplete strategy % 96.98/14.71 % (3346093)Time elapsed: 0.149 s % 96.98/14.71 % (3346093)Peak memory usage: 93 MB % 96.98/14.71 % (3346093)Instructions burned: 259 (million) % 96.98/14.71 % (3346098)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2130241679:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2887 on theBenchmark for (2887ds/1008Mi) % 96.98/14.71 % (3346098)Refutation not found, incomplete strategy % 96.98/14.71 % (3346098)------------------------------ % 96.98/14.71 % (3346098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.98/14.71 % (3346098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.98/14.71 % (3346098)CaDiCaL version: 2.1.3 % 96.98/14.71 % (3346098)Termination reason: Refutation not found, incomplete strategy % 96.98/14.71 % (3346098)Time elapsed: 0.005 s % 96.98/14.71 % (3346098)Peak memory usage: 87 MB % 96.98/14.71 % (3346098)Instructions burned: 14 (million) % 96.98/14.71 % (3346088)------------------------------ % 96.98/14.71 % (3346088)------------------------------ % 96.98/14.71 % (3346098)------------------------------ % 96.98/14.71 % (3346098)------------------------------ % 96.98/14.71 % (3346093)------------------------------ % 96.98/14.71 % (3346093)------------------------------ % 96.98/14.71 % (3346103)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=1470821210:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2884 on theBenchmark for (2884ds/1083Mi) % 96.98/14.71 % (3346102)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=3264901867:i=8327:s2at=5:bd=preordered_2884 on theBenchmark for (2884ds/8327Mi) % 96.98/14.71 % (3346104)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3130110911:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2883 on theBenchmark for (2883ds/1084Mi) % 96.98/14.71 % (3346104)Refutation not found, incomplete strategy % 96.98/14.71 % (3346104)------------------------------ % 96.98/14.71 % (3346104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.98/14.71 % (3346104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.98/14.71 % (3346104)CaDiCaL version: 2.1.3 % 96.98/14.71 % (3346104)Termination reason: Refutation not found, incomplete strategy % 96.98/14.71 % (3346104)Time elapsed: 0.004 s % 96.98/14.71 % (3346104)Peak memory usage: 87 MB % 96.98/14.71 % (3346104)Instructions burned: 4 (million) % 96.98/14.71 % (3346103)Instruction limit reached! % 96.98/14.71 % (3346103)------------------------------ % 96.98/14.71 % (3346103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.17/15.13 % (3346103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.17/15.13 % (3346103)CaDiCaL version: 2.1.3 % 100.17/15.13 % (3346103)Termination reason: Instruction limit % 100.17/15.13 % (3346103)Termination phase: Saturation % 100.17/15.13 % (3346103)Time elapsed: 0.268 s % 100.17/15.13 % (3346103)Peak memory usage: 101 MB % 100.17/15.13 % (3346103)Instructions burned: 1087 (million) % 100.17/15.13 % (3346104)------------------------------ % 100.17/15.13 % (3346104)------------------------------ % 100.17/15.13 % (3346095)Refutation not found, incomplete strategy % 100.17/15.13 % (3346095)------------------------------ % 100.17/15.13 % (3346095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.17/15.13 % (3346095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.17/15.13 % (3346095)CaDiCaL version: 2.1.3 % 100.17/15.13 % (3346095)Termination reason: Refutation not found, incomplete strategy % 100.17/15.13 % (3346095)Time elapsed: 0.752 s % 100.17/15.13 % (3346095)Peak memory usage: 145 MB % 100.17/15.13 % (3346095)Instructions burned: 1160 (million) % 100.17/15.13 % (3346108)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3385149421:i=6995:s2at=5:gtg=all_2880 on theBenchmark for (2880ds/6995Mi) % 100.17/15.13 % (3346109)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2776449663:st=2:i=6225:sd=15:ss=axioms_2879 on theBenchmark for (2879ds/6225Mi) % 100.17/15.13 % (3346109)Refutation not found, incomplete strategy % 100.17/15.13 % (3346109)------------------------------ % 100.17/15.13 % (3346109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.17/15.13 % (3346109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.17/15.13 % (3346109)CaDiCaL version: 2.1.3 % 100.17/15.13 % (3346109)Termination reason: Refutation not found, incomplete strategy % 100.17/15.13 % (3346109)Time elapsed: 0.005 s % 100.17/15.13 % (3346109)Peak memory usage: 87 MB % 100.17/15.13 % (3346109)Instructions burned: 7 (million) % 100.17/15.13 % (3346095)------------------------------ % 100.17/15.13 % (3346095)------------------------------ % 100.17/15.13 % (3346109)------------------------------ % 100.17/15.13 % (3346109)------------------------------ % 100.17/15.13 % (3346112)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2369479640:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2876 on theBenchmark for (2876ds/3372Mi) % 100.17/15.13 % (3346113)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=4249145419:st=2.3:i=26457:sd=10:ss=included:sgt=8_2875 on theBenchmark for (2875ds/26457Mi) % 100.17/15.13 [W927 21:43:36.698470010 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. % 100.17/15.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 100.17/15.13 [W927 21:43:36.698503240 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. % 100.17/15.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 100.17/15.13 [W927 21:43:36.698542567 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. % 100.17/15.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 100.17/15.13 [W927 21:43:36.698556240 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. % 100.17/15.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 100.17/15.13 [W927 21:43:36.698580634 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. % 100.17/15.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 100.17/15.13 [W927 21:43:36.698606054 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698633377 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698652737 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698676590 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698687220 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698711477 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:36.698722227 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 % (3346112)Refutation not found, incomplete strategy % 102.34/15.44 % (3346112)------------------------------ % 102.34/15.44 % (3346112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.34/15.44 % (3346112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/15.44 % (3346112)CaDiCaL version: 2.1.3 % 102.34/15.44 % (3346112)Termination reason: Refutation not found, incomplete strategy % 102.34/15.44 % (3346112)Time elapsed: 0.556 s % 102.34/15.44 % (3346112)Peak memory usage: 127 MB % 102.34/15.44 % (3346112)Instructions burned: 853 (million) % 102.34/15.44 % (3346112)------------------------------ % 102.34/15.44 % (3346112)------------------------------ % 102.34/15.44 % (3346113)Refutation not found, incomplete strategy % 102.34/15.44 % (3346113)------------------------------ % 102.34/15.44 % (3346113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.34/15.44 % (3346113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.34/15.44 % (3346113)CaDiCaL version: 2.1.3 % 102.34/15.44 % (3346113)Termination reason: Refutation not found, incomplete strategy % 102.34/15.44 % (3346113)Time elapsed: 0.683 s % 102.34/15.44 % (3346113)Peak memory usage: 144 MB % 102.34/15.44 % (3346113)Instructions burned: 1162 (million) % 102.34/15.44 % (3346113)------------------------------ % 102.34/15.44 % (3346113)------------------------------ % 102.34/15.44 % (3346116)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=1893126098:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2866 on theBenchmark for (2866ds/13494Mi) % 102.34/15.44 % (3346117)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=345264451:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2865 on theBenchmark for (2865ds/2503Mi) % 102.34/15.44 [W927 21:43:37.620077813 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. % 102.34/15.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.34/15.44 [W927 21:43:37.620099461 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620119976 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620134153 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620147641 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620153423 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620176076 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620181613 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620193893 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620199276 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620211785 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 [W927 21:43:37.620217394 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. % 126.34/18.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.34/18.83 % (3346117)Refutation not found, incomplete strategy % 126.34/18.83 % (3346117)------------------------------ % 126.34/18.83 % (3346117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.34/18.83 % (3346117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.34/18.83 % (3346117)CaDiCaL version: 2.1.3 % 126.34/18.83 % (3346117)Termination reason: Refutation not found, incomplete strategy % 126.34/18.83 % (3346117)Time elapsed: 0.313 s % 126.34/18.83 % (3346117)Peak memory usage: 126 MB % 126.34/18.83 % (3346117)Instructions burned: 831 (million) % 126.34/18.83 % (3346117)------------------------------ % 126.34/18.83 % (3346117)------------------------------ % 126.34/18.83 % (3346120)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=646376406:i=2559:sd=1:ep=RSTC:ss=axioms_2858 on theBenchmark for (2858ds/2559Mi) % 133.40/19.81 [W927 21:43:37.253122120 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253142588 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253164210 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253170667 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253183951 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253189317 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253202715 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253218621 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253233508 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253239058 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253254183 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 [W927 21:43:37.253259531 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. % 133.40/19.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.40/19.81 % (3346120)Refutation not found, incomplete strategy % 133.40/19.81 % (3346120)------------------------------ % 133.40/19.81 % (3346120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.40/19.81 % (3346120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.88/20.78 % (3346120)CaDiCaL version: 2.1.3 % 139.88/20.78 % (3346120)Termination reason: Refutation not found, incomplete strategy % 139.88/20.78 % (3346120)Time elapsed: 0.312 s % 139.88/20.78 % (3346120)Peak memory usage: 126 MB % 139.88/20.78 % (3346120)Instructions burned: 832 (million) % 139.88/20.78 % (3346120)------------------------------ % 139.88/20.78 % (3346120)------------------------------ % 139.88/20.78 % (3346122)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2337628523:i=30753:av=off:ss=included_2852 on theBenchmark for (2852ds/30753Mi) % 139.88/20.78 % (3346108)Instruction limit reached! % 139.88/20.78 % (3346108)------------------------------ % 139.88/20.78 % (3346108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.88/20.78 % (3346108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.88/20.78 % (3346108)CaDiCaL version: 2.1.3 % 139.88/20.78 % (3346108)Termination reason: Instruction limit % 139.88/20.78 % (3346108)Termination phase: Saturation % 139.88/20.78 % (3346108)Time elapsed: 3.172 s % 139.88/20.78 % (3346108)Peak memory usage: 183 MB % 139.88/20.78 % (3346108)Instructions burned: 6995 (million) % 139.88/20.78 % (3346124)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=186880316:i=26473:ep=RSTC_2847 on theBenchmark for (2847ds/26473Mi) % 139.88/20.78 % (3346102)Instruction limit reached! % 139.88/20.78 % (3346102)------------------------------ % 139.88/20.78 % (3346102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.88/20.78 % (3346102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.88/20.78 % (3346102)CaDiCaL version: 2.1.3 % 139.88/20.78 % (3346102)Termination reason: Instruction limit % 139.88/20.78 % (3346102)Termination phase: Saturation % 139.88/20.78 % (3346102)Time elapsed: 4.452 s % 139.88/20.78 % (3346102)Peak memory usage: 195 MB % 139.88/20.78 % (3346102)Instructions burned: 8329 (million) % 139.88/20.78 % (3346126)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=2038393842:cts=off:i=2759:kws=inv_arity:fgj=on_2837 on theBenchmark for (2837ds/2759Mi) % 139.88/20.78 % (3346126)Refutation not found, incomplete strategy % 139.88/20.78 % (3346126)------------------------------ % 139.88/20.79 % (3346126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.88/20.79 % (3346126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.88/20.79 % (3346126)CaDiCaL version: 2.1.3 % 139.88/20.79 % (3346126)Termination reason: Refutation not found, incomplete strategy % 139.88/20.79 % (3346126)Time elapsed: 0.773 s % 139.88/20.79 % (3346126)Peak memory usage: 147 MB % 139.88/20.79 % (3346126)Instructions burned: 1216 (million) % 139.88/20.79 % (3346126)------------------------------ % 139.88/20.79 % (3346126)------------------------------ % 139.88/20.79 % (3346128)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=2907898355:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2825 on theBenchmark for (2825ds/5665Mi) % 139.88/20.79 [W927 21:43:41.747365302 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. % 139.88/20.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.88/20.79 [W927 21:43:41.747397928 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. % 139.88/20.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.88/20.79 [W927 21:43:41.747437058 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. % 139.88/20.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.88/20.79 [W927 21:43:41.747449908 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. % 139.88/20.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747476475 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747486842 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747511242 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747521139 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747545075 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747555095 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747578839 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:41.747588865 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 % (3346128)Refutation not found, incomplete strategy % 144.52/21.37 % (3346128)------------------------------ % 144.52/21.37 % (3346128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.52/21.37 % (3346128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.52/21.37 % (3346128)CaDiCaL version: 2.1.3 % 144.52/21.37 % (3346128)Termination reason: Refutation not found, incomplete strategy % 144.52/21.37 % (3346128)Time elapsed: 0.550 s % 144.52/21.37 % (3346128)Peak memory usage: 126 MB % 144.52/21.37 % (3346128)Instructions burned: 833 (million) % 144.52/21.37 % (3346128)------------------------------ % 144.52/21.37 % (3346128)------------------------------ % 144.52/21.37 % (3346130)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=1279284807:i=1532:ep=RS:ss=axioms_2816 on theBenchmark for (2816ds/1532Mi) % 144.52/21.37 [W927 21:43:42.726479714 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:42.726521870 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. % 144.52/21.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.52/21.37 [W927 21:43:42.726562401 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726576477 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726610247 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726620624 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726645631 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726655867 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726680617 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726691001 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726716687 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:42.726774451 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 % (3346130)Refutation not found, incomplete strategy % 154.75/22.88 % (3346130)------------------------------ % 154.75/22.88 % (3346130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.75/22.88 % (3346130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.75/22.88 % (3346130)CaDiCaL version: 2.1.3 % 154.75/22.88 % (3346130)Termination reason: Refutation not found, incomplete strategy % 154.75/22.88 % (3346130)Time elapsed: 0.556 s % 154.75/22.88 % (3346130)Peak memory usage: 127 MB % 154.75/22.88 % (3346130)Instructions burned: 837 (million) % 154.75/22.88 % (3346130)------------------------------ % 154.75/22.88 % (3346130)------------------------------ % 154.75/22.88 % (3346132)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1713493605:i=1565:sd=2:ss=axioms:sgt=32_2806 on theBenchmark for (2806ds/1565Mi) % 154.75/22.88 [W927 21:43:43.698614889 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. % 154.75/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.75/22.88 [W927 21:43:43.698658023 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698699059 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698711363 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698741856 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698752109 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698777336 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698787453 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698811546 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698821829 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698846346 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 [W927 21:43:43.698856856 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. % 161.81/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.81/23.86 % (3346132)Refutation not found, incomplete strategy % 161.81/23.86 % (3346132)------------------------------ % 161.81/23.86 % (3346132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.81/23.86 % (3346132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.81/23.86 % (3346132)CaDiCaL version: 2.1.3 % 161.81/23.86 % (3346132)Termination reason: Refutation not found, incomplete strategy % 161.81/23.86 % (3346132)Time elapsed: 0.552 s % 161.81/23.86 % (3346132)Peak memory usage: 126 MB % 161.81/23.86 % (3346132)Instructions burned: 837 (million) % 161.81/23.86 % (3346132)------------------------------ % 161.81/23.86 % (3346132)------------------------------ % 161.81/23.86 % (3346134)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=3213786621:i=1572:fgj=on:gsp=on_2796 on theBenchmark for (2796ds/1572Mi) % 168.88/24.84 % (3346134)Instruction limit reached! % 168.88/24.84 % (3346134)------------------------------ % 168.88/24.84 % (3346134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.88/24.84 % (3346134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.88/24.84 % (3346134)CaDiCaL version: 2.1.3 % 168.88/24.84 % (3346134)Termination reason: Instruction limit % 168.88/24.84 % (3346134)Termination phase: Saturation % 168.88/24.84 % (3346134)Time elapsed: 0.945 s % 168.88/24.84 % (3346134)Peak memory usage: 146 MB % 168.88/24.84 % (3346134)Instructions burned: 1573 (million) % 168.88/24.84 % (3346136)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3635580434:i=6052:sd=4:ss=axioms:sgt=24_2785 on theBenchmark for (2785ds/6052Mi) % 168.88/24.84 % (3346116)Instruction limit reached! % 168.88/24.84 % (3346116)------------------------------ % 168.88/24.84 % (3346116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.88/24.84 % (3346116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.88/24.84 % (3346116)CaDiCaL version: 2.1.3 % 168.88/24.84 % (3346116)Termination reason: Instruction limit % 168.88/24.84 % (3346116)Termination phase: Saturation % 168.88/24.84 % (3346116)Time elapsed: 8.381 s % 168.88/24.84 % (3346116)Peak memory usage: 220 MB % 168.88/24.84 % (3346116)Instructions burned: 13495 (million) % 168.88/24.84 [W927 21:43:45.793396589 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793430342 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793468625 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793480465 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793507462 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793519772 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793547792 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793559479 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. % 168.88/24.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.88/24.84 [W927 21:43:45.793585079 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:45.793596566 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:45.793620842 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:45.793642732 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 % (3346138)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=3576396271:i=3500:sd=1:bd=preordered:sup=off:ss=included_2780 on theBenchmark for (2780ds/3500Mi) % 169.45/25.01 % (3346136)Refutation not found, incomplete strategy % 169.45/25.01 % (3346136)------------------------------ % 169.45/25.01 % (3346136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.45/25.01 % (3346136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.45/25.01 % (3346136)CaDiCaL version: 2.1.3 % 169.45/25.01 % (3346136)Termination reason: Refutation not found, incomplete strategy % 169.45/25.01 % (3346136)Time elapsed: 0.564 s % 169.45/25.01 % (3346136)Peak memory usage: 126 MB % 169.45/25.01 % (3346136)Instructions burned: 835 (million) % 169.45/25.01 % (3346136)------------------------------ % 169.45/25.01 % (3346136)------------------------------ % 169.45/25.01 % (3346140)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=1277521491:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2775 on theBenchmark for (2775ds/1842Mi) % 169.45/25.01 % (3346138)Refutation not found, incomplete strategy % 169.45/25.01 % (3346138)------------------------------ % 169.45/25.01 % (3346138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.45/25.01 % (3346138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.45/25.01 % (3346138)CaDiCaL version: 2.1.3 % 169.45/25.01 % (3346138)Termination reason: Refutation not found, incomplete strategy % 169.45/25.01 % (3346138)Time elapsed: 0.738 s % 169.45/25.01 % (3346138)Peak memory usage: 147 MB % 169.45/25.01 % (3346138)Instructions burned: 1159 (million) % 169.45/25.01 [W927 21:43:46.770840883 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:46.770875733 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:46.770915946 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:46.770927549 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. % 169.45/25.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.45/25.01 [W927 21:43:46.770954939 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.770967003 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.770992126 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.771022543 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.771055426 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.771065819 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.771091219 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 [W927 21:43:46.771101476 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. % 186.07/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.07/27.18 % (3346138)------------------------------ % 186.07/27.18 % (3346138)------------------------------ % 186.07/27.18 % (3346140)Refutation not found, incomplete strategy % 186.07/27.18 % (3346140)------------------------------ % 186.07/27.18 % (3346140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.07/27.18 % (3346140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.07/27.18 % (3346140)CaDiCaL version: 2.1.3 % 186.07/27.18 % (3346140)Termination reason: Refutation not found, incomplete strategy % 186.07/27.18 % (3346140)Time elapsed: 0.562 s % 186.07/27.18 % (3346140)Peak memory usage: 127 MB % 186.07/27.18 % (3346140)Instructions burned: 850 (million) % 186.07/27.18 % (3346142)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=341971473:i=66096:add=on_2769 on theBenchmark for (2769ds/66096Mi) % 186.07/27.18 % (3346140)------------------------------ % 186.07/27.18 % (3346140)------------------------------ % 186.07/27.18 % (3346144)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2464303482:i=1884:sd=1:nm=60:ss=axioms_2765 on theBenchmark for (2765ds/1884Mi) % 186.07/27.18 % (3346122)Instruction limit reached! % 186.07/27.18 % (3346122)------------------------------ % 186.07/27.18 % (3346122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.07/27.18 % (3346122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.07/27.18 % (3346122)CaDiCaL version: 2.1.3 % 186.07/27.18 % (3346122)Termination reason: Instruction limit % 186.07/27.18 % (3346122)Termination phase: Saturation % 186.07/27.18 % (3346122)Time elapsed: 9.052 s % 186.07/27.18 % (3346122)Peak memory usage: 351 MB % 186.07/27.18 % (3346122)Instructions burned: 30754 (million) % 186.07/27.18 [W927 21:43:47.749766484 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749812488 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749850265 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749861891 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749887645 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749909621 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749936271 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749947171 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749971091 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.749981788 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.750061338 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 [W927 21:43:47.750099601 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. % 211.24/30.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.24/30.74 % (3346146)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1979732015:cts=off:i=5469:bs=on:fsr=off_2760 on theBenchmark for (2760ds/5469Mi) % 211.24/30.74 % (3346144)Refutation not found, incomplete strategy % 211.24/30.74 % (3346144)------------------------------ % 211.24/30.74 % (3346144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.24/30.74 % (3346144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.24/30.74 % (3346144)CaDiCaL version: 2.1.3 % 211.24/30.74 % (3346144)Termination reason: Refutation not found, incomplete strategy % 214.71/31.29 % (3346144)Time elapsed: 0.558 s % 214.71/31.29 % (3346144)Peak memory usage: 126 MB % 214.71/31.29 % (3346144)Instructions burned: 835 (million) % 214.71/31.29 % (3346144)------------------------------ % 214.71/31.29 % (3346144)------------------------------ % 214.71/31.29 % (3346148)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=3794026760:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2756 on theBenchmark for (2756ds/2037Mi) % 214.71/31.29 % (3346148)Instruction limit reached! % 214.71/31.29 % (3346148)------------------------------ % 214.71/31.29 % (3346148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.71/31.29 % (3346148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.71/31.29 % (3346148)CaDiCaL version: 2.1.3 % 214.71/31.29 % (3346148)Termination reason: Instruction limit % 214.71/31.29 % (3346148)Termination phase: Saturation % 214.71/31.29 % (3346148)Time elapsed: 1.193 s % 214.71/31.29 % (3346148)Peak memory usage: 147 MB % 214.71/31.29 % (3346148)Instructions burned: 2037 (million) % 214.71/31.29 % (3346146)Instruction limit reached! % 214.71/31.29 % (3346146)------------------------------ % 214.71/31.29 % (3346146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.71/31.29 % (3346146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.71/31.29 % (3346146)CaDiCaL version: 2.1.3 % 214.71/31.29 % (3346146)Termination reason: Instruction limit % 214.71/31.29 % (3346146)Termination phase: Saturation % 214.71/31.29 % (3346146)Time elapsed: 1.794 s % 214.71/31.29 % (3346146)Peak memory usage: 106 MB % 214.71/31.29 % (3346146)Instructions burned: 5473 (million) % 214.71/31.29 % (3346150)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2578858959:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2742 on theBenchmark for (2742ds/2110Mi) % 214.71/31.29 % (3346151)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=3014151995:i=2430:add=off:aac=none:nm=16_2741 on theBenchmark for (2741ds/2430Mi) % 214.71/31.29 [W927 21:43:49.094012376 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094049609 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094090556 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094104559 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094131419 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094143296 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. % 214.71/31.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.71/31.29 [W927 21:43:49.094170282 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 [W927 21:43:49.094182062 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 [W927 21:43:49.094206452 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 [W927 21:43:49.094216909 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 [W927 21:43:49.094240842 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 [W927 21:43:49.094250979 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. % 226.17/32.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.17/32.85 % (3346150)Refutation not found, incomplete strategy % 226.17/32.85 % (3346150)------------------------------ % 226.17/32.85 % (3346150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.17/32.85 % (3346150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.17/32.85 % (3346150)CaDiCaL version: 2.1.3 % 226.17/32.85 % (3346150)Termination reason: Refutation not found, incomplete strategy % 226.17/32.85 % (3346150)Time elapsed: 0.555 s % 226.17/32.85 % (3346150)Peak memory usage: 127 MB % 226.17/32.85 % (3346150)Instructions burned: 838 (million) % 226.17/32.85 % (3346150)------------------------------ % 226.17/32.85 % (3346150)------------------------------ % 226.17/32.85 % (3346151)Instruction limit reached! % 226.17/32.85 % (3346151)------------------------------ % 226.17/32.85 % (3346151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.17/32.85 % (3346151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.17/32.85 % (3346151)CaDiCaL version: 2.1.3 % 226.17/32.85 % (3346151)Termination reason: Instruction limit % 226.17/32.85 % (3346151)Termination phase: Saturation % 226.17/32.85 % (3346151)Time elapsed: 0.775 s % 226.17/32.85 % (3346151)Peak memory usage: 148 MB % 226.17/32.85 % (3346151)Instructions burned: 2432 (million) % 226.17/32.85 % (3346154)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=2784914175:cond=fast:i=4891_2732 on theBenchmark for (2732ds/4891Mi) % 226.17/32.85 % (3346155)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=359689660:st=2:i=14845:sd=2:ss=included:fsd=on_2732 on theBenchmark for (2732ds/14845Mi) % 226.17/32.85 % (3346155)Refutation not found, incomplete strategy % 226.17/32.85 % (3346155)------------------------------ % 226.17/32.85 % (3346155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.17/32.85 % (3346155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.17/32.85 % (3346155)CaDiCaL version: 2.1.3 % 226.17/32.85 % (3346155)Termination reason: Refutation not found, incomplete strategy % 226.17/32.85 % (3346155)Time elapsed: 0.420 s % 226.17/32.85 % (3346155)Peak memory usage: 143 MB % 226.17/32.85 % (3346155)Instructions burned: 1118 (million) % 226.17/32.85 % (3346155)------------------------------ % 226.17/32.85 % (3346155)------------------------------ % 226.17/32.85 % (3346158)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2927482874:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2725 on theBenchmark for (2725ds/7534Mi) % 226.17/32.85 % (3346154)Instruction limit reached! % 230.42/33.44 % (3346154)------------------------------ % 230.42/33.44 % (3346154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.42/33.44 % (3346154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.42/33.44 % (3346154)CaDiCaL version: 2.1.3 % 230.42/33.44 % (3346154)Termination reason: Instruction limit % 230.42/33.44 % (3346154)Termination phase: Saturation % 230.42/33.44 % (3346154)Time elapsed: 2.991 s % 230.42/33.44 % (3346154)Peak memory usage: 169 MB % 230.42/33.44 % (3346154)Instructions burned: 4892 (million) % 230.42/33.44 % (3346158)Instruction limit reached! % 230.42/33.44 % (3346158)------------------------------ % 230.42/33.44 % (3346158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.42/33.44 % (3346158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.42/33.44 % (3346158)CaDiCaL version: 2.1.3 % 230.42/33.44 % (3346158)Termination reason: Instruction limit % 230.42/33.44 % (3346158)Termination phase: Saturation % 230.42/33.44 % (3346158)Time elapsed: 2.267 s % 230.42/33.44 % (3346158)Peak memory usage: 173 MB % 230.42/33.44 % (3346158)Instructions burned: 7536 (million) % 230.42/33.44 % (3346161)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1959398984:i=7860_2701 on theBenchmark for (2701ds/7860Mi) % 230.42/33.44 % (3346160)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=4228458706:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2701 on theBenchmark for (2701ds/10353Mi) % 230.42/33.44 % (3346161)Refutation not found, incomplete strategy % 230.42/33.44 % (3346161)------------------------------ % 230.42/33.44 % (3346161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.42/33.44 % (3346161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.42/33.44 % (3346161)CaDiCaL version: 2.1.3 % 230.42/33.44 % (3346161)Termination reason: Refutation not found, incomplete strategy % 230.42/33.44 % (3346161)Time elapsed: 0.040 s % 230.42/33.44 % (3346161)Peak memory usage: 92 MB % 230.42/33.44 % (3346161)Instructions burned: 148 (million) % 230.42/33.44 % (3346161)------------------------------ % 230.42/33.44 % (3346161)------------------------------ % 230.42/33.44 % (3346164)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=3150455700:i=7896:sd=2:bs=on:ss=included:sgt=20_2697 on theBenchmark for (2697ds/7896Mi) % 230.42/33.44 [W927 21:43:53.200265049 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.42/33.44 [W927 21:43:53.200297403 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.42/33.44 [W927 21:43:53.200336109 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.42/33.44 [W927 21:43:53.200349649 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.42/33.44 [W927 21:43:53.200375783 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.42/33.44 [W927 21:43:53.200385903 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. % 230.42/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200411063 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200421586 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200444626 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200454413 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200477899 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 [W927 21:43:53.200487649 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. % 235.73/34.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.73/34.17 % (3346160)Refutation not found, incomplete strategy % 235.73/34.17 % (3346160)------------------------------ % 235.73/34.17 % (3346160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.73/34.17 % (3346160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/34.17 % (3346160)CaDiCaL version: 2.1.3 % 235.73/34.17 % (3346160)Termination reason: Refutation not found, incomplete strategy % 235.73/34.17 % (3346160)Time elapsed: 0.557 s % 235.73/34.17 % (3346160)Peak memory usage: 126 MB % 235.73/34.17 % (3346160)Instructions burned: 836 (million) % 235.73/34.17 % (3346124)Instruction limit reached! % 235.73/34.17 % (3346124)------------------------------ % 235.73/34.17 % (3346124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.73/34.17 % (3346124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/34.17 % (3346124)CaDiCaL version: 2.1.3 % 235.73/34.17 % (3346124)Termination reason: Instruction limit % 235.73/34.17 % (3346124)Termination phase: Saturation % 235.73/34.17 % (3346124)Time elapsed: 15.264 s % 235.73/34.17 % (3346124)Peak memory usage: 427 MB % 235.73/34.17 % (3346124)Instructions burned: 26474 (million) % 235.73/34.17 % (3346160)------------------------------ % 235.73/34.17 % (3346160)------------------------------ % 235.73/34.17 % (3346167)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=250510439:i=5812:gtgl=2:gtg=all_2692 on theBenchmark for (2692ds/5812Mi) % 235.73/34.17 % (3346168)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=3502297471:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2691 on theBenchmark for (2691ds/2965Mi) % 235.73/34.17 % (3346168)Refutation not found, incomplete strategy % 235.73/34.17 % (3346168)------------------------------ % 235.73/34.17 % (3346168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.73/34.17 % (3346168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.73/34.17 % (3346168)CaDiCaL version: 2.1.3 % 235.73/34.17 % (3346168)Termination reason: Refutation not found, incomplete strategy % 235.73/34.17 % (3346168)Time elapsed: 0.771 s % 235.73/34.17 % (3346168)Peak memory usage: 143 MB % 235.73/34.17 % (3346168)Instructions burned: 1223 (million) % 235.73/34.17 % (3346096)Instruction limit reached! % 235.73/34.17 % (3346096)------------------------------ % 235.73/34.17 % (3346096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.38/34.78 % (3346096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.38/34.78 % (3346096)CaDiCaL version: 2.1.3 % 239.38/34.78 % (3346096)Termination reason: Instruction limit % 239.38/34.78 % (3346096)Termination phase: Saturation % 239.38/34.78 % (3346096)Time elapsed: 20.598 s % 239.38/34.78 % (3346096)Peak memory usage: 257 MB % 239.38/34.78 % (3346096)Instructions burned: 33336 (million) % 239.38/34.78 % (3346168)------------------------------ % 239.38/34.78 % (3346168)------------------------------ % 239.38/34.78 % (3346171)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=3391481517:i=2967:kws=precedence:bd=preordered:av=off_2680 on theBenchmark for (2680ds/2967Mi) % 239.38/34.78 % (3346172)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=2614278498:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2679 on theBenchmark for (2679ds/3022Mi) % 239.38/34.78 [W927 21:43:55.353247473 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353284114 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353323030 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353335457 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353361174 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353372650 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. % 239.38/34.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.78 [W927 21:43:55.353398624 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. % 239.38/34.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.79 [W927 21:43:55.353410067 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. % 239.38/34.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.79 [W927 21:43:55.353434827 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. % 239.38/34.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.38/34.79 [W927 21:43:55.353446220 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. % 239.38/34.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:55.353471994 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:55.353493257 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 % (3346172)Refutation not found, incomplete strategy % 242.06/35.06 % (3346172)------------------------------ % 242.06/35.06 % (3346172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.06/35.06 % (3346172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.06/35.06 % (3346172)CaDiCaL version: 2.1.3 % 242.06/35.06 % (3346172)Termination reason: Refutation not found, incomplete strategy % 242.06/35.06 % (3346172)Time elapsed: 0.552 s % 242.06/35.06 % (3346172)Peak memory usage: 126 MB % 242.06/35.06 % (3346172)Instructions burned: 835 (million) % 242.06/35.06 % (3346164)Instruction limit reached! % 242.06/35.06 % (3346164)------------------------------ % 242.06/35.06 % (3346164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.06/35.06 % (3346164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.06/35.06 % (3346164)CaDiCaL version: 2.1.3 % 242.06/35.06 % (3346164)Termination reason: Instruction limit % 242.06/35.06 % (3346164)Termination phase: Saturation % 242.06/35.06 % (3346164)Time elapsed: 2.634 s % 242.06/35.06 % (3346164)Peak memory usage: 197 MB % 242.06/35.06 % (3346164)Instructions burned: 7899 (million) % 242.06/35.06 % (3346172)------------------------------ % 242.06/35.06 % (3346172)------------------------------ % 242.06/35.06 % (3346175)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=2317601585:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2670 on theBenchmark for (2670ds/3207Mi) % 242.06/35.06 % (3346176)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=444386095:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2670 on theBenchmark for (2670ds/3289Mi) % 242.06/35.06 [W927 21:43:56.088461286 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:56.088499588 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:56.088521884 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:56.088528839 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:56.088542151 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 242.06/35.06 [W927 21:43:56.088548109 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. % 242.06/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088561352 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088567395 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088580629 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088592559 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088606255 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:56.088611829 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 % (3346175)Refutation not found, incomplete strategy % 258.76/37.47 % (3346175)------------------------------ % 258.76/37.47 % (3346175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.76/37.47 % (3346175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.76/37.47 % (3346175)CaDiCaL version: 2.1.3 % 258.76/37.47 % (3346175)Termination reason: Refutation not found, incomplete strategy % 258.76/37.47 % (3346175)Time elapsed: 0.313 s % 258.76/37.47 % (3346175)Peak memory usage: 126 MB % 258.76/37.47 % (3346175)Instructions burned: 833 (million) % 258.76/37.47 % (3346175)------------------------------ % 258.76/37.47 % (3346175)------------------------------ % 258.76/37.47 % (3346179)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=363586613:i=38569:sd=3:ss=axioms:sgt=32_2664 on theBenchmark for (2664ds/38569Mi) % 258.76/37.47 [W927 21:43:57.699149190 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:57.699170017 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:57.699191220 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:57.699197566 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. % 258.76/37.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.76/37.47 [W927 21:43:57.699212410 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699218816 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699232582 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699237979 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699250992 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699263452 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699277753 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 [W927 21:43:57.699283342 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. % 279.31/40.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.31/40.35 % (3346171)Instruction limit reached! % 279.31/40.35 % (3346171)------------------------------ % 279.31/40.35 % (3346171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.31/40.35 % (3346171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.31/40.35 % (3346171)CaDiCaL version: 2.1.3 % 279.31/40.35 % (3346171)Termination reason: Instruction limit % 279.31/40.35 % (3346171)Termination phase: Saturation % 279.31/40.35 % (3346171)Time elapsed: 1.764 s % 279.31/40.35 % (3346171)Peak memory usage: 150 MB % 279.31/40.35 % (3346171)Instructions burned: 2968 (million) % 279.31/40.35 % (3346176)Refutation not found, incomplete strategy % 279.31/40.35 % (3346176)------------------------------ % 279.31/40.35 % (3346176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.31/40.35 % (3346176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.31/40.35 % (3346176)CaDiCaL version: 2.1.3 % 279.31/40.35 % (3346176)Termination reason: Refutation not found, incomplete strategy % 279.31/40.35 % (3346176)Time elapsed: 0.792 s % 279.31/40.35 % (3346176)Peak memory usage: 145 MB % 279.31/40.35 % (3346176)Instructions burned: 1236 (million) % 279.31/40.35 % (3346179)Refutation not found, incomplete strategy % 279.31/40.35 % (3346179)------------------------------ % 279.31/40.35 % (3346179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.31/40.35 % (3346179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.31/40.35 % (3346179)CaDiCaL version: 2.1.3 % 279.31/40.35 % (3346179)Termination reason: Refutation not found, incomplete strategy % 279.31/40.35 % (3346179)Time elapsed: 0.318 s % 279.31/40.35 % (3346179)Peak memory usage: 126 MB % 279.31/40.35 % (3346179)Instructions burned: 833 (million) % 279.31/40.35 % (3346181)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=651726778:cts=off:i=3394_2660 on theBenchmark for (2660ds/3394Mi) % 279.31/40.35 % (3346Terminated %------------------------------------------------------------------------------