%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW478_30 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:38 PM UTC 2026 % Result : Timeout 287.20s 41.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW478_30 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n014.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 14:13:31 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.95/2.27 % (1794555)Detected formulas, will run a generic FOF schedule. % 8.95/2.27 % (1794563)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1939605349:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi) % 8.95/2.27 % (1794563)Refutation not found, incomplete strategy % 8.95/2.27 % (1794563)------------------------------ % 8.95/2.27 % (1794563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.27 % (1794563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.27 % (1794563)CaDiCaL version: 2.1.3 % 8.95/2.27 % (1794563)Termination reason: Refutation not found, incomplete strategy % 8.95/2.27 % (1794563)Time elapsed: 0.004 s % 8.95/2.27 % (1794563)Peak memory usage: 89 MB % 8.95/2.27 % (1794563)Instructions burned: 10 (million) % 8.95/2.27 % (1794561)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=3719813684:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi) % 8.95/2.27 % (1794560)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=3160609496:i=141193_2998 on theBenchmark for (2998ds/141193Mi) % 8.95/2.27 % (1794562)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=1148843437:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi) % 8.95/2.27 % (1794564)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3708092850:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi) % 8.95/2.27 % (1794566)dis-21_1_sil=8000:lcm=predicate:random_seed=2422704521:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi) % 8.95/2.27 % (1794565)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4291426149:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi) % 8.95/2.27 % (1794564)Refutation not found, incomplete strategy % 8.95/2.27 % (1794564)------------------------------ % 8.95/2.27 % (1794564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.27 % (1794564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.27 % (1794564)CaDiCaL version: 2.1.3 % 8.95/2.27 % (1794564)Termination reason: Refutation not found, incomplete strategy % 8.95/2.27 % (1794564)Time elapsed: 0.007 s % 8.95/2.27 % (1794564)Peak memory usage: 89 MB % 8.95/2.27 % (1794564)Instructions burned: 10 (million) % 8.95/2.27 % (1794566)Instruction limit reached! % 8.95/2.27 % (1794566)------------------------------ % 8.95/2.27 % (1794566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.27 % (1794566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.27 % (1794566)CaDiCaL version: 2.1.3 % 8.95/2.27 % (1794566)Termination reason: Instruction limit % 8.95/2.27 % (1794566)Termination phase: Property scanning % 8.95/2.27 % (1794566)Time elapsed: 0.063 s % 8.95/2.27 % (1794566)Peak memory usage: 90 MB % 8.95/2.27 % (1794566)Instructions burned: 130 (million) % 8.95/2.27 % (1794565)Instruction limit reached! % 8.95/2.27 % (1794565)------------------------------ % 8.95/2.27 % (1794565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.27 % (1794565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.27 % (1794565)CaDiCaL version: 2.1.3 % 8.95/2.27 % (1794565)Termination reason: Instruction limit % 8.95/2.27 % (1794565)Termination phase: Property scanning % 8.95/2.27 % (1794565)Time elapsed: 0.070 s % 8.95/2.27 % (1794565)Peak memory usage: 90 MB % 8.95/2.27 % (1794565)Instructions burned: 141 (million) % 8.95/2.27 % (1794563)------------------------------ % 8.95/2.27 % (1794563)------------------------------ % 8.95/2.27 % (1794574)lrs+10_1_sil=8000:sp=occurrence:random_seed=2734836202:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 8.95/2.27 % (1794574)Refutation not found, incomplete strategy % 8.95/2.27 % (1794574)------------------------------ % 8.95/2.27 % (1794574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.27 % (1794574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.27 % (1794574)CaDiCaL version: 2.1.3 % 8.95/2.27 % (1794574)Termination reason: Refutation not found, incomplete strategy % 8.95/2.27 % (1794574)Time elapsed: 0.007 s % 11.02/2.35 % (1794574)Peak memory usage: 89 MB % 11.02/2.35 % (1794574)Instructions burned: 8 (million) % 11.02/2.35 % (1794576)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1586873050:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 11.02/2.35 % (1794576)Refutation not found, incomplete strategy % 11.02/2.35 % (1794576)------------------------------ % 11.02/2.35 % (1794576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.02/2.35 % (1794576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.02/2.35 % (1794576)CaDiCaL version: 2.1.3 % 11.02/2.35 % (1794576)Termination reason: Refutation not found, incomplete strategy % 11.02/2.35 % (1794576)Time elapsed: 0.004 s % 11.02/2.35 % (1794576)Peak memory usage: 89 MB % 11.02/2.35 % (1794576)Instructions burned: 8 (million) % 11.02/2.35 % (1794575)lrs+10_1_sil=32000:urr=on:br=off:random_seed=808287111:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 11.02/2.35 % (1794575)Refutation not found, incomplete strategy % 11.02/2.35 % (1794575)------------------------------ % 11.02/2.35 % (1794575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.02/2.35 % (1794575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.02/2.35 % (1794575)CaDiCaL version: 2.1.3 % 11.02/2.35 % (1794575)Termination reason: Refutation not found, incomplete strategy % 11.02/2.35 % (1794575)Time elapsed: 0.020 s % 11.02/2.35 % (1794575)Peak memory usage: 90 MB % 11.02/2.35 % (1794575)Instructions burned: 39 (million) % 11.02/2.35 % (1794564)------------------------------ % 11.02/2.35 % (1794564)------------------------------ % 11.02/2.35 % (1794576)------------------------------ % 11.02/2.35 % (1794576)------------------------------ % 11.02/2.35 % (1794580)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=1883214331:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 11.02/2.35 % (1794574)------------------------------ % 11.02/2.35 % (1794574)------------------------------ % 11.02/2.35 % (1794581)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3000838940:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 11.02/2.35 % (1794581)Refutation not found, incomplete strategy % 11.02/2.35 % (1794581)------------------------------ % 11.02/2.35 % (1794581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.02/2.35 % (1794581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.02/2.35 % (1794581)CaDiCaL version: 2.1.3 % 11.02/2.35 % (1794581)Termination reason: Refutation not found, incomplete strategy % 11.02/2.35 % (1794581)Time elapsed: 0.009 s % 11.02/2.35 % (1794581)Peak memory usage: 89 MB % 11.02/2.35 % (1794581)Instructions burned: 14 (million) % 11.02/2.35 % (1794575)------------------------------ % 11.02/2.35 % (1794575)------------------------------ % 11.02/2.35 % (1794580)Instruction limit reached! % 11.02/2.35 % (1794580)------------------------------ % 11.02/2.35 % (1794580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.02/2.35 % (1794580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.02/2.35 % (1794580)CaDiCaL version: 2.1.3 % 11.02/2.35 % (1794580)Termination reason: Instruction limit % 11.02/2.35 % (1794580)Termination phase: Saturation % 11.02/2.35 % (1794580)Time elapsed: 0.135 s % 11.02/2.35 % (1794580)Peak memory usage: 94 MB % 11.02/2.35 % (1794580)Instructions burned: 248 (million) % 11.02/2.35 % (1794583)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2975540833:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 11.02/2.35 % (1794585)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3855439438:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 11.02/2.35 % (1794586)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1510515311:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 11.02/2.35 % (1794585)Instruction limit reached! % 11.02/2.35 % (1794585)------------------------------ % 11.02/2.35 % (1794585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.02/2.35 % (1794585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.02/2.35 % (1794585)CaDiCaL version: 2.1.3 % 11.02/2.35 % (1794585)Termination reason: Instruction limit % 11.02/2.35 % (1794585)Termination phase: Property scanning % 11.02/2.35 % (1794585)Time elapsed: 0.061 s % 11.02/2.35 % (1794585)Peak memory usage: 90 MB % 13.39/2.74 % (1794585)Instructions burned: 114 (million) % 13.39/2.74 % (1794581)------------------------------ % 13.39/2.74 % (1794581)------------------------------ % 13.39/2.74 % (1794586)Instruction limit reached! % 13.39/2.74 % (1794586)------------------------------ % 13.39/2.74 % (1794586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794586)CaDiCaL version: 2.1.3 % 13.39/2.74 % (1794586)Termination reason: Instruction limit % 13.39/2.74 % (1794586)Termination phase: Property scanning % 13.39/2.74 % (1794586)Time elapsed: 0.066 s % 13.39/2.74 % (1794586)Peak memory usage: 90 MB % 13.39/2.74 % (1794586)Instructions burned: 128 (million) % 13.39/2.74 % (1794590)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2039376552:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 13.39/2.74 % (1794591)lrs+10_1_sil=8000:sp=occurrence:random_seed=1168181695:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 13.39/2.74 % (1794591)Refutation not found, incomplete strategy % 13.39/2.74 % (1794591)------------------------------ % 13.39/2.74 % (1794591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794591)CaDiCaL version: 2.1.3 % 13.39/2.74 % (1794591)Termination reason: Refutation not found, incomplete strategy % 13.39/2.74 % (1794591)Time elapsed: 0.008 s % 13.39/2.74 % (1794591)Peak memory usage: 89 MB % 13.39/2.74 % (1794591)Instructions burned: 10 (million) % 13.39/2.74 % (1794590)Instruction limit reached! % 13.39/2.74 % (1794590)------------------------------ % 13.39/2.74 % (1794590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794590)CaDiCaL version: 2.1.3 % 13.39/2.74 % (1794590)Termination reason: Instruction limit % 13.39/2.74 % (1794590)Termination phase: Property scanning % 13.39/2.74 % (1794590)Time elapsed: 0.056 s % 13.39/2.74 % (1794590)Peak memory usage: 89 MB % 13.39/2.74 % (1794590)Instructions burned: 115 (million) % 13.39/2.74 % (1794592)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=983398604:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 13.39/2.74 % (1794562)Refutation not found, incomplete strategy % 13.39/2.74 % (1794562)------------------------------ % 13.39/2.74 % (1794562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794562)CaDiCaL version: 2.1.3 % 13.39/2.74 % (1794562)Termination reason: Refutation not found, incomplete strategy % 13.39/2.74 % (1794562)Time elapsed: 1.009 s % 13.39/2.74 % (1794562)Peak memory usage: 183 MB % 13.39/2.74 % (1794562)Instructions burned: 1670 (million) % 13.39/2.74 % (1794595)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1298672289:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 13.39/2.74 % (1794592)Refutation not found, incomplete strategy % 13.39/2.74 % (1794592)------------------------------ % 13.39/2.74 % (1794592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794592)CaDiCaL version: 2.1.3 % 13.39/2.74 % (1794592)Termination reason: Refutation not found, incomplete strategy % 13.39/2.74 % (1794592)Time elapsed: 0.141 s % 13.39/2.74 % (1794592)Peak memory usage: 96 MB % 13.39/2.74 % (1794592)Instructions burned: 266 (million) % 13.39/2.74 % (1794591)------------------------------ % 13.39/2.74 % (1794591)------------------------------ % 13.39/2.74 % (1794562)------------------------------ % 13.39/2.74 % (1794562)------------------------------ % 13.39/2.74 % (1794598)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=638348642:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 13.39/2.74 % (1794592)------------------------------ % 13.39/2.74 % (1794592)------------------------------ % 13.39/2.74 % (1794598)Instruction limit reached! % 13.39/2.74 % (1794598)------------------------------ % 13.39/2.74 % (1794598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.39/2.74 % (1794598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.39/2.74 % (1794598)CaDiCaL version: 2.1.3 % 14.26/2.92 % (1794598)Termination reason: Instruction limit % 14.26/2.92 % (1794598)Termination phase: Property scanning % 14.26/2.92 % (1794598)Time elapsed: 0.070 s % 14.26/2.92 % (1794598)Peak memory usage: 90 MB % 14.26/2.92 % (1794598)Instructions burned: 135 (million) % 14.26/2.92 % (1794600)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3245787026:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi) % 14.26/2.92 % (1794600)Refutation not found, incomplete strategy % 14.26/2.92 % (1794600)------------------------------ % 14.26/2.92 % (1794600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/2.92 % (1794600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/2.92 % (1794600)CaDiCaL version: 2.1.3 % 14.26/2.92 % (1794600)Termination reason: Refutation not found, incomplete strategy % 14.26/2.92 % (1794600)Time elapsed: 0.009 s % 14.26/2.92 % (1794600)Peak memory usage: 89 MB % 14.26/2.92 % (1794600)Instructions burned: 13 (million) % 14.26/2.92 % (1794601)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=488722652:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 14.26/2.92 [W928 14:13:33.247659538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247693985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247732351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247745591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247771648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247783615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247809545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247821452 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247846105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.26/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.26/2.92 [W928 14:13:33.247857698 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:33.247882915 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:33.247980389 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 % (1794602)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=2576338158:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 17.49/3.39 % (1794602)Refutation not found, incomplete strategy % 17.49/3.39 % (1794602)------------------------------ % 17.49/3.39 % (1794602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.49/3.39 % (1794602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.49/3.39 % (1794602)CaDiCaL version: 2.1.3 % 17.49/3.39 % (1794602)Termination reason: Refutation not found, incomplete strategy % 17.49/3.39 % (1794602)Time elapsed: 0.023 s % 17.49/3.39 % (1794602)Peak memory usage: 90 MB % 17.49/3.39 % (1794602)Instructions burned: 48 (million) % 17.49/3.39 % (1794595)Refutation not found, incomplete strategy % 17.49/3.39 % (1794595)------------------------------ % 17.49/3.39 % (1794595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.49/3.39 % (1794595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.49/3.39 % (1794595)CaDiCaL version: 2.1.3 % 17.49/3.39 % (1794595)Termination reason: Refutation not found, incomplete strategy % 17.49/3.39 % (1794595)Time elapsed: 0.589 s % 17.49/3.39 % (1794595)Peak memory usage: 132 MB % 17.49/3.39 % (1794595)Instructions burned: 875 (million) % 17.49/3.39 % (1794600)------------------------------ % 17.49/3.39 % (1794600)------------------------------ % 17.49/3.39 % (1794602)------------------------------ % 17.49/3.39 % (1794602)------------------------------ % 17.49/3.39 % (1794606)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3376218379:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi) % 17.49/3.39 [W928 14:13:34.629626927 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:34.629672350 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:34.629710340 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:34.629728007 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:34.629754731 register_special_ops.cpp:225] Warning: Creating a tensor from 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.49/3.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.49/3.39 [W928 14:13:34.629766704 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629792154 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629802941 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629826921 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629837624 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629862324 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 [W928 14:13:34.629934881 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/5.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.67/5.28 % (1794606)Instruction limit reached! % 31.67/5.28 % (1794606)------------------------------ % 31.67/5.28 % (1794606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.67/5.28 % (1794606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.67/5.28 % (1794606)CaDiCaL version: 2.1.3 % 31.67/5.28 % (1794606)Termination reason: Instruction limit % 31.67/5.28 % (1794606)Termination phase: Property scanning % 31.67/5.28 % (1794606)Time elapsed: 0.066 s % 31.67/5.28 % (1794606)Peak memory usage: 90 MB % 31.67/5.28 % (1794606)Instructions burned: 136 (million) % 31.67/5.28 % (1794607)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=95415480:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 31.67/5.28 % (1794607)Refutation not found, incomplete strategy % 31.67/5.28 % (1794607)------------------------------ % 31.67/5.28 % (1794607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.67/5.28 % (1794607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.67/5.28 % (1794607)CaDiCaL version: 2.1.3 % 31.67/5.28 % (1794607)Termination reason: Refutation not found, incomplete strategy % 31.67/5.28 % (1794607)Time elapsed: 0.007 s % 31.67/5.28 % (1794607)Peak memory usage: 89 MB % 31.67/5.28 % (1794607)Instructions burned: 10 (million) % 31.67/5.28 % (1794595)------------------------------ % 31.67/5.28 % (1794595)------------------------------ % 31.67/5.28 % (1794583)Instruction limit reached! % 31.67/5.28 % (1794583)------------------------------ % 31.67/5.28 % (1794583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.67/5.28 % (1794583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.67/5.28 % (1794583)CaDiCaL version: 2.1.3 % 31.67/5.28 % (1794583)Termination reason: Instruction limit % 31.67/5.28 % (1794583)Termination phase: Saturation % 31.67/5.28 % (1794583)Time elapsed: 1.307 s % 31.67/5.28 % (1794583)Peak memory usage: 151 MB % 31.67/5.28 % (1794583)Instructions burned: 2351 (million) % 31.67/5.28 % (1794609)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1218391006:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 31.67/5.28 % (1794609)Refutation not found, incomplete strategy % 31.67/5.28 % (1794609)------------------------------ % 31.67/5.28 % (1794609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.08/5.46 % (1794609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.08/5.46 % (1794609)CaDiCaL version: 2.1.3 % 33.08/5.46 % (1794609)Termination reason: Refutation not found, incomplete strategy % 33.08/5.46 % (1794609)Time elapsed: 0.007 s % 33.08/5.46 % (1794609)Peak memory usage: 89 MB % 33.08/5.46 % (1794609)Instructions burned: 8 (million) % 33.08/5.46 % (1794601)Refutation not found, incomplete strategy % 33.08/5.46 % (1794601)------------------------------ % 33.08/5.46 % (1794601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.08/5.46 % (1794601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.08/5.46 % (1794601)CaDiCaL version: 2.1.3 % 33.08/5.46 % (1794601)Termination reason: Refutation not found, incomplete strategy % 33.08/5.46 % (1794601)Time elapsed: 0.592 s % 33.08/5.46 % (1794601)Peak memory usage: 133 MB % 33.08/5.46 % (1794601)Instructions burned: 880 (million) % 33.08/5.46 % (1794612)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=1535279331:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi) % 33.08/5.46 % (1794611)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=3324312203:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi) % 33.08/5.46 % (1794612)Instruction limit reached! % 33.08/5.46 % (1794612)------------------------------ % 33.08/5.46 % (1794612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.08/5.46 % (1794612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.08/5.46 % (1794612)CaDiCaL version: 2.1.3 % 33.08/5.46 % (1794612)Termination reason: Instruction limit % 33.08/5.46 % (1794612)Termination phase: Property scanning % 33.08/5.46 % (1794612)Time elapsed: 0.076 s % 33.08/5.46 % (1794612)Peak memory usage: 91 MB % 33.08/5.46 % (1794612)Instructions burned: 152 (million) % 33.08/5.46 % (1794607)------------------------------ % 33.08/5.46 % (1794607)------------------------------ % 33.08/5.46 % (1794616)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2843737118:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 33.08/5.46 % (1794609)------------------------------ % 33.08/5.46 % (1794609)------------------------------ % 33.08/5.46 % (1794617)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3064923974:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi) % 33.08/5.46 % (1794601)------------------------------ % 33.08/5.46 % (1794601)------------------------------ % 33.08/5.46 % (1794619)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=3251880029:s2a=on:i=185:s2at=1.8:fdi=4_2975 on theBenchmark for (2975ds/185Mi) % 33.08/5.46 % (1794621)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=82072534:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi) % 33.08/5.46 % (1794617)Refutation not found, incomplete strategy % 33.08/5.46 % (1794617)------------------------------ % 33.08/5.46 % (1794617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.08/5.46 % (1794617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.08/5.46 % (1794617)CaDiCaL version: 2.1.3 % 33.08/5.46 % (1794617)Termination reason: Refutation not found, incomplete strategy % 33.08/5.46 % (1794617)Time elapsed: 0.158 s % 33.08/5.46 % (1794617)Peak memory usage: 96 MB % 33.08/5.46 % (1794617)Instructions burned: 299 (million) % 33.08/5.46 % (1794621)Refutation not found, incomplete strategy % 33.08/5.46 % (1794621)------------------------------ % 33.08/5.46 % (1794621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.08/5.46 % (1794621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.08/5.46 % (1794621)CaDiCaL version: 2.1.3 % 33.08/5.46 % (1794621)Termination reason: Refutation not found, incomplete strategy % 33.08/5.46 % (1794621)Time elapsed: 0.012 s % 33.08/5.46 % (1794621)Peak memory usage: 89 MB % 33.08/5.46 % (1794621)Instructions burned: 18 (million) % 33.08/5.46 % (1794619)Instruction limit reached! % 33.08/5.46 % (1794619)------------------------------ % 33.08/5.46 % (1794619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.90 % (1794619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.90 % (1794619)CaDiCaL version: 2.1.3 % 42.99/6.90 % (1794619)Termination reason: Instruction limit % 42.99/6.90 % (1794619)Termination phase: Saturation % 42.99/6.90 % (1794619)Time elapsed: 0.092 s % 42.99/6.90 % (1794619)Peak memory usage: 93 MB % 42.99/6.90 % (1794619)Instructions burned: 187 (million) % 42.99/6.90 % (1794624)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2493543410:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2972 on theBenchmark for (2972ds/4850Mi) % 42.99/6.90 % (1794617)------------------------------ % 42.99/6.90 % (1794617)------------------------------ % 42.99/6.90 % (1794621)------------------------------ % 42.99/6.90 % (1794621)------------------------------ % 42.99/6.90 % (1794624)Refutation not found, incomplete strategy % 42.99/6.90 % (1794624)------------------------------ % 42.99/6.90 % (1794624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.90 % (1794624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.90 % (1794624)CaDiCaL version: 2.1.3 % 42.99/6.90 % (1794624)Termination reason: Refutation not found, incomplete strategy % 42.99/6.90 % (1794624)Time elapsed: 0.106 s % 42.99/6.90 % (1794624)Peak memory usage: 94 MB % 42.99/6.90 % (1794624)Instructions burned: 210 (million) % 42.99/6.90 % (1794626)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3498688123:i=12111:sd=1:ss=included_2971 on theBenchmark for (2971ds/12111Mi) % 42.99/6.90 % (1794627)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1506415373:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi) % 42.99/6.90 % (1794624)------------------------------ % 42.99/6.90 % (1794624)------------------------------ % 42.99/6.90 % (1794627)Instruction limit reached! % 42.99/6.90 % (1794627)------------------------------ % 42.99/6.90 % (1794627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.90 % (1794627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.90 % (1794627)CaDiCaL version: 2.1.3 % 42.99/6.90 % (1794627)Termination reason: Instruction limit % 42.99/6.90 % (1794627)Termination phase: Saturation % 42.99/6.90 % (1794627)Time elapsed: 0.167 s % 42.99/6.90 % (1794627)Peak memory usage: 96 MB % 42.99/6.90 % (1794627)Instructions burned: 320 (million) % 42.99/6.90 % (1794631)dis-1011_128_sil=32000:random_seed=2565357404:i=3706:ep=RST:av=off_2967 on theBenchmark for (2967ds/3706Mi) % 42.99/6.90 % (1794630)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1573238065:i=2064:ep=RST_2967 on theBenchmark for (2967ds/2064Mi) % 42.99/6.90 % (1794630)Refutation not found, incomplete strategy % 42.99/6.90 % (1794630)------------------------------ % 42.99/6.90 % (1794630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.90 % (1794630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.90 % (1794630)CaDiCaL version: 2.1.3 % 42.99/6.90 % (1794630)Termination reason: Refutation not found, incomplete strategy % 42.99/6.90 % (1794630)Time elapsed: 0.117 s % 42.99/6.90 % (1794630)Peak memory usage: 95 MB % 42.99/6.90 % (1794630)Instructions burned: 257 (million) % 42.99/6.90 % (1794630)------------------------------ % 42.99/6.90 % (1794630)------------------------------ % 42.99/6.90 % (1794634)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4030061375:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2962 on theBenchmark for (2962ds/757Mi) % 42.99/6.90 % (1794634)Refutation not found, incomplete strategy % 42.99/6.90 % (1794634)------------------------------ % 42.99/6.90 % (1794634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.99/6.90 % (1794634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.99/6.90 % (1794634)CaDiCaL version: 2.1.3 % 42.99/6.90 % (1794634)Termination reason: Refutation not found, incomplete strategy % 42.99/6.90 % (1794634)Time elapsed: 0.007 s % 42.99/6.90 % (1794634)Peak memory usage: 89 MB % 42.99/6.90 % (1794634)Instructions burned: 8 (million) % 42.99/6.90 % (1794634)------------------------------ % 42.99/6.90 % (1794634)------------------------------ % 42.99/6.90 % (1794636)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2354137226:i=13913:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/13913Mi) % 42.99/6.90 [W928 14:13:36.171372190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171407864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171445547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171456440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171482011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171492797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171518011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171528787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171552657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171563411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171587224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 [W928 14:13:36.171597857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.35/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.35/7.09 % (1794636)Refutation not found, incomplete strategy % 43.35/7.09 % (1794636)------------------------------ % 43.35/7.09 % (1794636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.35/7.09 % (1794636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.35/7.09 % (1794636)CaDiCaL version: 2.1.3 % 43.35/7.09 % (1794636)Termination reason: Refutation not found, incomplete strategy % 60.64/9.33 % (1794636)Time elapsed: 0.571 s % 60.64/9.33 % (1794636)Peak memory usage: 132 MB % 60.64/9.33 % (1794636)Instructions burned: 873 (million) % 60.64/9.33 % (1794636)------------------------------ % 60.64/9.33 % (1794636)------------------------------ % 60.64/9.33 % (1794638)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=665887957:i=9925:aac=none_2949 on theBenchmark for (2949ds/9925Mi) % 60.64/9.33 % (1794631)Instruction limit reached! % 60.64/9.33 % (1794631)------------------------------ % 60.64/9.33 % (1794631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.64/9.33 % (1794631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.64/9.33 % (1794631)CaDiCaL version: 2.1.3 % 60.64/9.33 % (1794631)Termination reason: Instruction limit % 60.64/9.33 % (1794631)Termination phase: Saturation % 60.64/9.33 % (1794631)Time elapsed: 1.951 s % 60.64/9.33 % (1794631)Peak memory usage: 115 MB % 60.64/9.33 % (1794631)Instructions burned: 3706 (million) % 60.64/9.33 % (1794640)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3340819208:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2946 on theBenchmark for (2946ds/2479Mi) % 60.64/9.33 % (1794640)Refutation not found, incomplete strategy % 60.64/9.33 % (1794640)------------------------------ % 60.64/9.33 % (1794640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.64/9.33 % (1794640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.64/9.33 % (1794640)CaDiCaL version: 2.1.3 % 60.64/9.33 % (1794640)Termination reason: Refutation not found, incomplete strategy % 60.64/9.33 % (1794640)Time elapsed: 0.012 s % 60.64/9.33 % (1794640)Peak memory usage: 89 MB % 60.64/9.33 % (1794640)Instructions burned: 18 (million) % 60.64/9.33 % (1794611)Instruction limit reached! % 60.64/9.33 % (1794611)------------------------------ % 60.64/9.33 % (1794611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.64/9.33 % (1794611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.64/9.33 % (1794611)CaDiCaL version: 2.1.3 % 60.64/9.33 % (1794611)Termination reason: Instruction limit % 60.64/9.33 % (1794611)Termination phase: Saturation % 60.64/9.33 % (1794611)Time elapsed: 3.343 s % 60.64/9.33 % (1794611)Peak memory usage: 174 MB % 60.64/9.33 % (1794611)Instructions burned: 6060 (million) % 60.64/9.33 % (1794640)------------------------------ % 60.64/9.33 % (1794640)------------------------------ % 60.64/9.33 % (1794642)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1227633739:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2943 on theBenchmark for (2943ds/440Mi) % 60.64/9.33 % (1794643)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3952083317:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2943 on theBenchmark for (2943ds/11145Mi) % 60.64/9.33 % (1794642)Instruction limit reached! % 60.64/9.33 % (1794642)------------------------------ % 60.64/9.33 % (1794642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.64/9.33 % (1794642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.64/9.33 % (1794642)CaDiCaL version: 2.1.3 % 60.64/9.33 % (1794642)Termination reason: Instruction limit % 60.64/9.33 % (1794642)Termination phase: Saturation % 60.64/9.33 % (1794642)Time elapsed: 0.220 s % 60.64/9.33 % (1794642)Peak memory usage: 98 MB % 60.64/9.33 % (1794642)Instructions burned: 442 (million) % 60.64/9.33 % (1794638)Refutation not found, incomplete strategy % 60.64/9.33 % (1794638)------------------------------ % 60.64/9.33 % (1794638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.64/9.33 % (1794638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.64/9.33 % (1794638)CaDiCaL version: 2.1.3 % 60.64/9.33 % (1794638)Termination reason: Refutation not found, incomplete strategy % 60.64/9.33 % (1794638)Time elapsed: 0.946 s % 60.64/9.33 % (1794638)Peak memory usage: 151 MB % 60.64/9.33 % (1794638)Instructions burned: 1574 (million) % 60.64/9.33 % (1794646)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=2658472326:cts=off:i=3034:av=off:er=known:fsd=on_2940 on theBenchmark for (2940ds/3034Mi) % 60.64/9.33 [W928 14:13:38.797272610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797305637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797355950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797367580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797393857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797404360 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797429747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797440107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797464337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797475141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797499254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 [W928 14:13:38.797509857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 64.31/9.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 64.31/9.91 % (1794638)------------------------------ % 64.31/9.91 % (1794638)------------------------------ % 64.31/9.91 % (1794643)Refutation not found, incomplete strategy % 64.31/9.91 % (1794643)------------------------------ % 64.31/9.91 % (1794643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.31/9.91 % (1794643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.31/9.91 % (1794643)CaDiCaL version: 2.1.3 % 64.31/9.91 % (1794643)Termination reason: Refutation not found, incomplete strategy % 64.31/9.91 % (1794643)Time elapsed: 0.583 s % 64.31/9.91 % (1794643)Peak memory usage: 133 MB % 68.45/10.55 % (1794643)Instructions burned: 884 (million) % 68.45/10.55 % (1794648)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3078274390:st=2:s2a=on:i=524:s2at=2:ss=axioms_2936 on theBenchmark for (2936ds/524Mi) % 68.45/10.55 % (1794648)Refutation not found, incomplete strategy % 68.45/10.55 % (1794648)------------------------------ % 68.45/10.55 % (1794648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.45/10.55 % (1794648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.45/10.55 % (1794648)CaDiCaL version: 2.1.3 % 68.45/10.55 % (1794648)Termination reason: Refutation not found, incomplete strategy % 68.45/10.55 % (1794648)Time elapsed: 0.016 s % 68.45/10.55 % (1794648)Peak memory usage: 89 MB % 68.45/10.55 % (1794648)Instructions burned: 27 (million) % 68.45/10.55 % (1794643)------------------------------ % 68.45/10.55 % (1794643)------------------------------ % 68.45/10.55 % (1794648)------------------------------ % 68.45/10.55 % (1794648)------------------------------ % 68.45/10.55 % (1794650)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=870693128:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2933 on theBenchmark for (2933ds/1016Mi) % 68.45/10.55 % (1794650)Refutation not found, incomplete strategy % 68.45/10.55 % (1794650)------------------------------ % 68.45/10.55 % (1794650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.45/10.55 % (1794650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.45/10.55 % (1794650)CaDiCaL version: 2.1.3 % 68.45/10.55 % (1794650)Termination reason: Refutation not found, incomplete strategy % 68.45/10.55 % (1794650)Time elapsed: 0.007 s % 68.45/10.55 % (1794650)Peak memory usage: 89 MB % 68.45/10.55 % (1794650)Instructions burned: 10 (million) % 68.45/10.55 % (1794651)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1465319987:i=14123:bd=preordered:ins=4_2932 on theBenchmark for (2932ds/14123Mi) % 68.45/10.55 % (1794650)------------------------------ % 68.45/10.55 % (1794650)------------------------------ % 68.45/10.55 % (1794654)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1360382114:i=5781:kws=precedence:bd=all:rawr=on_2929 on theBenchmark for (2929ds/5781Mi) % 68.45/10.55 % (1794646)Instruction limit reached! % 68.45/10.55 % (1794646)------------------------------ % 68.45/10.55 % (1794646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.45/10.55 % (1794646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.45/10.55 % (1794646)CaDiCaL version: 2.1.3 % 68.45/10.55 % (1794646)Termination reason: Instruction limit % 68.45/10.55 % (1794646)Termination phase: Saturation % 68.45/10.55 % (1794646)Time elapsed: 1.694 s % 68.45/10.55 % (1794646)Peak memory usage: 174 MB % 68.45/10.55 % (1794646)Instructions burned: 3035 (million) % 68.45/10.55 % (1794656)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=3706294585:i=2448:gtgl=5:bd=preordered:gtg=all_2921 on theBenchmark for (2921ds/2448Mi) % 68.45/10.55 % (1794626)Instruction limit reached! % 68.45/10.55 % (1794626)------------------------------ % 68.45/10.55 % (1794626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.45/10.55 % (1794626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.45/10.55 % (1794626)CaDiCaL version: 2.1.3 % 68.45/10.55 % (1794626)Termination reason: Instruction limit % 68.45/10.55 % (1794626)Termination phase: Saturation % 68.45/10.55 % (1794626)Time elapsed: 4.954 s % 68.45/10.55 % (1794626)Peak memory usage: 173 MB % 68.45/10.55 % (1794626)Instructions burned: 12113 (million) % 68.45/10.55 % (1794658)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2555323003:i=3223:kws=precedence:fgj=on:av=off_2920 on theBenchmark for (2920ds/3223Mi) % 68.45/10.55 % (1794616)Instruction limit reached! % 68.45/10.55 % (1794616)------------------------------ % 68.45/10.55 % (1794616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.45/10.55 % (1794616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.45/10.55 % (1794616)CaDiCaL version: 2.1.3 % 68.45/10.55 % (1794616)Termination reason: Instruction limit % 68.45/10.55 % (1794616)Termination phase: Saturation % 68.45/10.55 % (1794616)Time elapsed: 6.025 s % 68.45/10.55 % (1794616)Peak memory usage: 176 MB % 68.45/10.55 % (1794616)Instructions burned: 14157 (million) % 68.45/10.55 % (1794660)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=29503082:st=5.6:i=2033:sd=3:ss=axioms_2914 on theBenchmark for (2914ds/2033Mi) % 68.96/10.66 [W928 14:13:41.613694877 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613733410 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613770984 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613782601 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613807317 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613819147 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613844514 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613855677 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613880821 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613892087 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613917141 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 [W928 14:13:41.613928201 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/10.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.96/10.66 % (1794660)Refutation not found, incomplete strategy % 68.96/10.66 % (1794660)------------------------------ % 68.96/10.66 % (1794660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.96/10.66 % (1794660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.02/11.12 % (1794660)CaDiCaL version: 2.1.3 % 73.02/11.12 % (1794660)Termination reason: Refutation not found, incomplete strategy % 73.02/11.12 % (1794660)Time elapsed: 0.582 s % 73.02/11.12 % (1794660)Peak memory usage: 133 MB % 73.02/11.12 % (1794660)Instructions burned: 877 (million) % 73.02/11.12 % (1794656)Instruction limit reached! % 73.02/11.12 % (1794656)------------------------------ % 73.02/11.12 % (1794656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.02/11.12 % (1794656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.02/11.12 % (1794656)CaDiCaL version: 2.1.3 % 73.02/11.12 % (1794656)Termination reason: Instruction limit % 73.02/11.12 % (1794656)Termination phase: Saturation % 73.02/11.12 % (1794656)Time elapsed: 1.381 s % 73.02/11.12 % (1794656)Peak memory usage: 176 MB % 73.02/11.12 % (1794656)Instructions burned: 2448 (million) % 73.02/11.12 % (1794660)------------------------------ % 73.02/11.12 % (1794660)------------------------------ % 73.02/11.12 % (1794662)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1277069584:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2906 on theBenchmark for (2906ds/2055Mi) % 73.02/11.12 % (1794664)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=1042671145:i=21611:sd=3:ss=axioms_2905 on theBenchmark for (2905ds/21611Mi) % 73.02/11.12 [W928 14:13:41.446054250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446086934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446126670 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446139357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446166214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446177731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446203787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446215184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.02/11.12 [W928 14:13:41.446240271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.02/11.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:41.446251564 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:41.446282154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:41.446303747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 % (1794658)Instruction limit reached! % 82.66/12.48 % (1794658)------------------------------ % 82.66/12.48 % (1794658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.66/12.48 % (1794658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.66/12.48 % (1794658)CaDiCaL version: 2.1.3 % 82.66/12.48 % (1794658)Termination reason: Instruction limit % 82.66/12.48 % (1794658)Termination phase: Saturation % 82.66/12.48 % (1794658)Time elapsed: 1.821 s % 82.66/12.48 % (1794658)Peak memory usage: 156 MB % 82.66/12.48 % (1794658)Instructions burned: 3224 (million) % 82.66/12.48 [W928 14:13:42.554303705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554342448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554380591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554393291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554419525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554441065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554467665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554477828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.66/12.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.66/12.48 [W928 14:13:42.554501858 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.40/13.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.40/13.63 [W928 14:13:42.554511935 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.40/13.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.40/13.63 [W928 14:13:42.554536412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.40/13.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.40/13.63 [W928 14:13:42.554546572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.40/13.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.40/13.63 % (1794662)Refutation not found, incomplete strategy % 90.40/13.63 % (1794662)------------------------------ % 90.40/13.63 % (1794662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.40/13.63 % (1794662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.40/13.63 % (1794662)CaDiCaL version: 2.1.3 % 90.40/13.63 % (1794662)Termination reason: Refutation not found, incomplete strategy % 90.40/13.63 % (1794662)Time elapsed: 0.580 s % 90.40/13.63 % (1794662)Peak memory usage: 130 MB % 90.40/13.63 % (1794662)Instructions burned: 905 (million) % 90.40/13.63 % (1794666)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2086042004:i=4835:sd=13:ss=axioms:sgt=23_2900 on theBenchmark for (2900ds/4835Mi) % 90.40/13.63 % (1794666)Refutation not found, incomplete strategy % 90.40/13.63 % (1794666)------------------------------ % 90.40/13.63 % (1794666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.40/13.63 % (1794666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.40/13.63 % (1794666)CaDiCaL version: 2.1.3 % 90.40/13.63 % (1794666)Termination reason: Refutation not found, incomplete strategy % 90.40/13.63 % (1794666)Time elapsed: 0.007 s % 90.40/13.63 % (1794666)Peak memory usage: 89 MB % 90.40/13.63 % (1794666)Instructions burned: 8 (million) % 90.40/13.63 % (1794654)Instruction limit reached! % 90.40/13.63 % (1794654)------------------------------ % 90.40/13.63 % (1794654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.40/13.63 % (1794654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.40/13.63 % (1794654)CaDiCaL version: 2.1.3 % 90.40/13.63 % (1794654)Termination reason: Instruction limit % 90.40/13.63 % (1794654)Termination phase: Saturation % 90.40/13.63 % (1794654)Time elapsed: 2.925 s % 90.40/13.63 % (1794654)Peak memory usage: 115 MB % 90.40/13.63 % (1794654)Instructions burned: 5782 (million) % 90.40/13.63 % (1794664)Refutation not found, incomplete strategy % 90.40/13.63 % (1794664)------------------------------ % 90.40/13.63 % (1794664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.40/13.63 % (1794664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.40/13.63 % (1794664)CaDiCaL version: 2.1.3 % 90.40/13.63 % (1794664)Termination reason: Refutation not found, incomplete strategy % 90.40/13.63 % (1794664)Time elapsed: 0.569 s % 90.40/13.63 % (1794664)Peak memory usage: 129 MB % 90.40/13.63 % (1794664)Instructions burned: 875 (million) % 90.40/13.63 % (1794668)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=2285642259:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2898 on theBenchmark for (2898ds/797Mi) % 90.40/13.63 % (1794662)------------------------------ % 90.40/13.63 % (1794662)------------------------------ % 90.40/13.63 % (1794666)------------------------------ % 90.40/13.63 % (1794666)------------------------------ % 90.40/13.63 % (1794664)------------------------------ % 90.40/13.63 % (1794664)------------------------------ % 90.40/13.63 % (1794670)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=211146214:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2896 on theBenchmark for (2896ds/2326Mi) % 101.39/15.11 % (1794671)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3162609975:i=6038:nm=6_2896 on theBenchmark for (2896ds/6038Mi) % 101.39/15.11 % (1794672)lrs+10_1_sil=32000:sp=occurrence:random_seed=430229843:st=2:i=33334:sd=3:ss=included:sgt=32_2895 on theBenchmark for (2895ds/33334Mi) % 101.39/15.11 % (1794668)Instruction limit reached! % 101.39/15.11 % (1794668)------------------------------ % 101.39/15.11 % (1794668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.39/15.11 % (1794668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.39/15.11 % (1794668)CaDiCaL version: 2.1.3 % 101.39/15.11 % (1794668)Termination reason: Instruction limit % 101.39/15.11 % (1794668)Termination phase: Saturation % 101.39/15.11 % (1794668)Time elapsed: 0.383 s % 101.39/15.11 % (1794668)Peak memory usage: 94 MB % 101.39/15.11 % (1794668)Instructions burned: 798 (million) % 101.39/15.11 % (1794676)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3339540697:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2893 on theBenchmark for (2893ds/1008Mi) % 101.39/15.11 % (1794676)Refutation not found, incomplete strategy % 101.39/15.11 % (1794676)------------------------------ % 101.39/15.11 % (1794676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.39/15.11 % (1794676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.39/15.11 % (1794676)CaDiCaL version: 2.1.3 % 101.39/15.11 % (1794676)Termination reason: Refutation not found, incomplete strategy % 101.39/15.11 % (1794676)Time elapsed: 0.015 s % 101.39/15.11 % (1794676)Peak memory usage: 89 MB % 101.39/15.11 % (1794676)Instructions burned: 25 (million) % 101.39/15.11 % (1794670)Refutation not found, incomplete strategy % 101.39/15.11 % (1794670)------------------------------ % 101.39/15.11 % (1794670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.39/15.11 % (1794670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.39/15.11 % (1794670)CaDiCaL version: 2.1.3 % 101.39/15.11 % (1794670)Termination reason: Refutation not found, incomplete strategy % 101.39/15.11 % (1794670)Time elapsed: 0.353 s % 101.39/15.11 % (1794670)Peak memory usage: 97 MB % 101.39/15.11 % (1794670)Instructions burned: 667 (million) % 101.39/15.11 % (1794676)------------------------------ % 101.39/15.11 % (1794676)------------------------------ % 101.39/15.11 % (1794670)------------------------------ % 101.39/15.11 % (1794670)------------------------------ % 101.39/15.11 % (1794678)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=3723493805:i=8327:s2at=5:bd=preordered_2889 on theBenchmark for (2889ds/8327Mi) % 101.39/15.11 % (1794679)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=1893811148:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2889 on theBenchmark for (2889ds/1083Mi) % 101.39/15.11 % (1794671)Refutation not found, incomplete strategy % 101.39/15.11 % (1794671)------------------------------ % 101.39/15.11 % (1794671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.39/15.11 % (1794671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.39/15.11 % (1794671)CaDiCaL version: 2.1.3 % 101.39/15.11 % (1794671)Termination reason: Refutation not found, incomplete strategy % 101.39/15.11 % (1794671)Time elapsed: 0.960 s % 101.39/15.11 % (1794671)Peak memory usage: 147 MB % 101.39/15.11 % (1794671)Instructions burned: 1577 (million) % 101.39/15.11 % (1794671)------------------------------ % 101.39/15.11 % (1794671)------------------------------ % 101.39/15.11 % (1794679)Instruction limit reached! % 101.39/15.11 % (1794679)------------------------------ % 101.39/15.11 % (1794679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.39/15.11 % (1794679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.39/15.11 % (1794679)CaDiCaL version: 2.1.3 % 101.39/15.11 % (1794679)Termination reason: Instruction limit % 101.39/15.11 % (1794679)Termination phase: Saturation % 101.39/15.11 % (1794679)Time elapsed: 0.509 s % 101.39/15.11 % (1794679)Peak memory usage: 106 MB % 101.39/15.11 % (1794679)Instructions burned: 1083 (million) % 101.39/15.11 % (1794682)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2066778711:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2883 on theBenchmark for (2883ds/1084Mi) % 101.39/15.11 % (1794682)Refutation not found, incomplete strategy % 105.35/15.67 % (1794682)------------------------------ % 105.35/15.67 % (1794682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.35/15.67 % (1794682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.35/15.67 % (1794682)CaDiCaL version: 2.1.3 % 105.35/15.67 % (1794682)Termination reason: Refutation not found, incomplete strategy % 105.35/15.67 % (1794682)Time elapsed: 0.007 s % 105.35/15.67 % (1794682)Peak memory usage: 88 MB % 105.35/15.67 % (1794682)Instructions burned: 10 (million) % 105.35/15.67 % (1794683)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1552307578:i=6995:s2at=5:gtg=all_2882 on theBenchmark for (2882ds/6995Mi) % 105.35/15.67 % (1794682)------------------------------ % 105.35/15.67 % (1794682)------------------------------ % 105.35/15.67 % (1794686)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1030394122:st=2:i=6225:sd=15:ss=axioms_2879 on theBenchmark for (2879ds/6225Mi) % 105.35/15.67 % (1794686)Refutation not found, incomplete strategy % 105.35/15.67 % (1794686)------------------------------ % 105.35/15.67 % (1794686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.35/15.67 % (1794686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.35/15.67 % (1794686)CaDiCaL version: 2.1.3 % 105.35/15.67 % (1794686)Termination reason: Refutation not found, incomplete strategy % 105.35/15.67 % (1794686)Time elapsed: 0.008 s % 105.35/15.67 % (1794686)Peak memory usage: 89 MB % 105.35/15.67 % (1794686)Instructions burned: 13 (million) % 105.35/15.67 % (1794686)------------------------------ % 105.35/15.67 % (1794686)------------------------------ % 105.35/15.67 % (1794688)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3112801367:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2875 on theBenchmark for (2875ds/3372Mi) % 105.35/15.67 % (1794651)Instruction limit reached! % 105.35/15.67 % (1794651)------------------------------ % 105.35/15.67 % (1794651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.35/15.67 % (1794651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.35/15.67 % (1794651)CaDiCaL version: 2.1.3 % 105.35/15.67 % (1794651)Termination reason: Instruction limit % 105.35/15.67 % (1794651)Termination phase: Saturation % 105.35/15.67 % (1794651)Time elapsed: 5.693 s % 105.35/15.67 % (1794651)Peak memory usage: 173 MB % 105.35/15.67 % (1794651)Instructions burned: 14124 (million) % 105.35/15.67 % (1794690)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1468876608:st=2.3:i=26457:sd=10:ss=included:sgt=8_2874 on theBenchmark for (2874ds/26457Mi) % 105.35/15.67 [W928 14:13:45.521232347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.35/15.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.35/15.67 [W928 14:13:45.521265170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.35/15.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.35/15.67 [W928 14:13:45.521304011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.35/15.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.35/15.67 [W928 14:13:45.521317041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.35/15.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.35/15.67 [W928 14:13:45.521344217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.35/15.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.35/15.67 [W928 14:13:45.521355634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521381171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521391691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521415634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521483128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521534304 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 [W928 14:13:45.521565554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.05 % (1794688)Refutation not found, incomplete strategy % 108.48/16.05 % (1794688)------------------------------ % 108.48/16.05 % (1794688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.48/16.05 % (1794688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.48/16.05 % (1794688)CaDiCaL version: 2.1.3 % 108.48/16.05 % (1794688)Termination reason: Refutation not found, incomplete strategy % 108.48/16.05 % (1794688)Time elapsed: 0.580 s % 108.48/16.05 % (1794688)Peak memory usage: 130 MB % 108.48/16.05 % (1794688)Instructions burned: 903 (million) % 108.48/16.05 % (1794688)------------------------------ % 108.48/16.05 % (1794688)------------------------------ % 108.48/16.05 % (1794692)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=4125503230:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2866 on theBenchmark for (2866ds/13494Mi) % 108.48/16.05 % (1794690)Refutation not found, incomplete strategy % 108.48/16.05 % (1794690)------------------------------ % 108.48/16.05 % (1794690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.48/16.05 % (1794690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.48/16.05 % (1794690)CaDiCaL version: 2.1.3 % 108.48/16.05 % (1794690)Termination reason: Refutation not found, incomplete strategy % 108.48/16.05 % (1794690)Time elapsed: 0.940 s % 108.48/16.05 % (1794690)Peak memory usage: 151 MB % 108.48/16.05 % (1794690)Instructions burned: 1582 (million) % 108.48/16.05 % (1794690)------------------------------ % 108.48/16.05 % (1794690)------------------------------ % 108.48/16.05 % (1794694)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=3112325603:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2860 on theBenchmark for (2860ds/2503Mi) % 108.48/16.05 [W928 14:13:46.004547473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004579840 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004616506 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004631566 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004655330 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004666257 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004704650 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004715710 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004739607 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004750270 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004774173 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 [W928 14:13:46.004784697 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/18.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.88/18.71 % (1794694)Refutation not found, incomplete strategy % 126.88/18.71 % (1794694)------------------------------ % 126.88/18.71 % (1794694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.88/18.71 % (1794694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.88/18.71 % (1794694)CaDiCaL version: 2.1.3 % 126.88/18.71 % (1794694)Termination reason: Refutation not found, incomplete strategy % 126.88/18.71 % (1794694)Time elapsed: 0.578 s % 126.88/18.71 % (1794694)Peak memory usage: 133 MB % 126.88/18.71 % (1794694)Instructions burned: 876 (million) % 126.88/18.71 % (1794694)------------------------------ % 126.88/18.71 % (1794694)------------------------------ % 126.88/18.71 % (1794696)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=751489827:i=2559:sd=1:ep=RSTC:ss=axioms_2851 on theBenchmark for (2851ds/2559Mi) % 133.32/19.67 % (1794678)Instruction limit reached! % 133.32/19.67 % (1794678)------------------------------ % 133.32/19.67 % (1794678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.32/19.67 % (1794678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.32/19.67 % (1794678)CaDiCaL version: 2.1.3 % 133.32/19.67 % (1794678)Termination reason: Instruction limit % 133.32/19.67 % (1794678)Termination phase: Saturation % 133.32/19.67 % (1794678)Time elapsed: 3.911 s % 133.32/19.67 % (1794678)Peak memory usage: 164 MB % 133.32/19.67 % (1794678)Instructions burned: 8328 (million) % 133.32/19.67 % (1794698)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1603348928:i=30753:av=off:ss=included_2849 on theBenchmark for (2849ds/30753Mi) % 133.32/19.67 [W928 14:13:47.946457614 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946490047 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946527290 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946538924 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946563920 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946576797 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946602571 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946613871 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946638204 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946650091 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/19.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.32/19.67 [W928 14:13:47.946675054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.38/20.62 [W928 14:13:47.946686537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.38/20.62 % (1794696)Refutation not found, incomplete strategy % 140.38/20.62 % (1794696)------------------------------ % 140.38/20.62 % (1794696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.38/20.62 % (1794696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.38/20.62 % (1794696)CaDiCaL version: 2.1.3 % 140.38/20.62 % (1794696)Termination reason: Refutation not found, incomplete strategy % 140.38/20.62 % (1794696)Time elapsed: 0.573 s % 140.38/20.62 % (1794696)Peak memory usage: 129 MB % 140.38/20.62 % (1794696)Instructions burned: 875 (million) % 140.38/20.62 % (1794696)------------------------------ % 140.38/20.62 % (1794696)------------------------------ % 140.38/20.62 % (1794700)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2209840825:i=26473:ep=RSTC_2841 on theBenchmark for (2841ds/26473Mi) % 140.38/20.62 % (1794683)Instruction limit reached! % 140.38/20.62 % (1794683)------------------------------ % 140.38/20.62 % (1794683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.38/20.62 % (1794683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.38/20.62 % (1794683)CaDiCaL version: 2.1.3 % 140.38/20.62 % (1794683)Termination reason: Instruction limit % 140.38/20.62 % (1794683)Termination phase: Saturation % 140.38/20.62 % (1794683)Time elapsed: 4.161 s % 140.38/20.62 % (1794683)Peak memory usage: 175 MB % 140.38/20.62 % (1794683)Instructions burned: 6996 (million) % 140.38/20.62 % (1794702)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=537753305:cts=off:i=2759:kws=inv_arity:fgj=on_2840 on theBenchmark for (2840ds/2759Mi) % 140.38/20.62 % (1794702)Refutation not found, incomplete strategy % 140.38/20.62 % (1794702)------------------------------ % 140.38/20.62 % (1794702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.38/20.62 % (1794702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.38/20.62 % (1794702)CaDiCaL version: 2.1.3 % 140.38/20.62 % (1794702)Termination reason: Refutation not found, incomplete strategy % 140.38/20.62 % (1794702)Time elapsed: 1.125 s % 140.38/20.62 % (1794702)Peak memory usage: 176 MB % 140.38/20.62 % (1794702)Instructions burned: 1868 (million) % 140.38/20.62 % (1794702)------------------------------ % 140.38/20.62 % (1794702)------------------------------ % 140.38/20.62 % (1794704)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=4016206015:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2824 on theBenchmark for (2824ds/5665Mi) % 140.38/20.62 [W928 14:13:50.607244456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.38/20.62 [W928 14:13:50.607276126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.38/20.62 [W928 14:13:50.607315230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.38/20.62 [W928 14:13:50.607327496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.38/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607354040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607364340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607388800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607399007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607423027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607432890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607456993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:50.607467007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 % (1794704)Refutation not found, incomplete strategy % 143.92/21.04 % (1794704)------------------------------ % 143.92/21.04 % (1794704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.92/21.04 % (1794704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.92/21.04 % (1794704)CaDiCaL version: 2.1.3 % 143.92/21.04 % (1794704)Termination reason: Refutation not found, incomplete strategy % 143.92/21.04 % (1794704)Time elapsed: 0.579 s % 143.92/21.04 % (1794704)Peak memory usage: 133 MB % 143.92/21.04 % (1794704)Instructions burned: 878 (million) % 143.92/21.04 % (1794704)------------------------------ % 143.92/21.04 % (1794704)------------------------------ % 143.92/21.04 % (1794706)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=1337213897:i=1532:ep=RS:ss=axioms_2815 on theBenchmark for (2815ds/1532Mi) % 143.92/21.04 [W928 14:13:51.568953363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:51.568994103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.92/21.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.92/21.04 [W928 14:13:51.569041056 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569059433 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569093236 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569103236 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569128156 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569138003 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569162100 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569171933 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569196010 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 [W928 14:13:51.569265093 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 154.44/22.68 % (1794706)Refutation not found, incomplete strategy % 154.44/22.68 % (1794706)------------------------------ % 154.44/22.68 % (1794706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 154.44/22.68 % (1794706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.44/22.68 % (1794706)CaDiCaL version: 2.1.3 % 154.44/22.68 % (1794706)Termination reason: Refutation not found, incomplete strategy % 154.44/22.68 % (1794706)Time elapsed: 0.576 s % 154.44/22.68 % (1794706)Peak memory usage: 133 MB % 154.44/22.68 % (1794706)Instructions burned: 876 (million) % 154.44/22.68 % (1794706)------------------------------ % 154.44/22.68 % (1794706)------------------------------ % 154.44/22.68 % (1794708)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=919213436:i=1565:sd=2:ss=axioms:sgt=32_2805 on theBenchmark for (2805ds/1565Mi) % 154.44/22.68 [W928 14:13:52.513714757 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/22.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513747413 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513784300 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513795343 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513820707 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513830604 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513856120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513921090 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.513970747 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.514009771 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.514057317 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 [W928 14:13:52.514087821 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/23.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.65/23.66 % (1794708)Refutation not found, incomplete strategy % 161.65/23.66 % (1794708)------------------------------ % 161.65/23.66 % (1794708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.65/23.66 % (1794708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.65/23.66 % (1794708)CaDiCaL version: 2.1.3 % 161.65/23.66 % (1794708)Termination reason: Refutation not found, incomplete strategy % 161.65/23.66 % (1794708)Time elapsed: 0.576 s % 161.65/23.66 % (1794708)Peak memory usage: 132 MB % 161.65/23.66 % (1794708)Instructions burned: 874 (million) % 161.65/23.66 % (1794708)------------------------------ % 161.65/23.66 % (1794708)------------------------------ % 168.11/24.60 % (1794710)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=2282698632:i=1572:fgj=on:gsp=on_2796 on theBenchmark for (2796ds/1572Mi) % 168.11/24.60 % (1794710)Instruction limit reached! % 168.11/24.60 % (1794710)------------------------------ % 168.11/24.60 % (1794710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.11/24.60 % (1794710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.11/24.60 % (1794710)CaDiCaL version: 2.1.3 % 168.11/24.60 % (1794710)Termination reason: Instruction limit % 168.11/24.60 % (1794710)Termination phase: Saturation % 168.11/24.60 % (1794710)Time elapsed: 0.969 s % 168.11/24.60 % (1794710)Peak memory usage: 180 MB % 168.11/24.60 % (1794710)Instructions burned: 1573 (million) % 168.11/24.60 % (1794712)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=396813590:i=6052:sd=4:ss=axioms:sgt=24_2785 on theBenchmark for (2785ds/6052Mi) % 168.11/24.60 % (1794692)Instruction limit reached! % 168.11/24.60 % (1794692)------------------------------ % 168.11/24.60 % (1794692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.11/24.60 % (1794692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.11/24.60 % (1794692)CaDiCaL version: 2.1.3 % 168.11/24.60 % (1794692)Termination reason: Instruction limit % 168.11/24.60 % (1794692)Termination phase: Saturation % 168.11/24.60 % (1794692)Time elapsed: 8.232 s % 168.11/24.60 % (1794692)Peak memory usage: 199 MB % 168.11/24.60 % (1794692)Instructions burned: 13495 (million) % 168.11/24.60 % (1794714)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=1743348875:i=3500:sd=1:bd=preordered:sup=off:ss=included_2782 on theBenchmark for (2782ds/3500Mi) % 168.11/24.60 [W928 14:13:54.575811894 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575844185 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575881888 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575894628 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575920235 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575932245 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575957048 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/24.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.11/24.60 [W928 14:13:54.575969028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:54.575993875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:54.576015035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:54.576041012 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:54.576051748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 % (1794712)Refutation not found, incomplete strategy % 187.22/27.18 % (1794712)------------------------------ % 187.22/27.18 % (1794712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.22/27.18 % (1794712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.22/27.18 % (1794712)CaDiCaL version: 2.1.3 % 187.22/27.18 % (1794712)Termination reason: Refutation not found, incomplete strategy % 187.22/27.18 % (1794712)Time elapsed: 0.577 s % 187.22/27.18 % (1794712)Peak memory usage: 132 MB % 187.22/27.18 % (1794712)Instructions burned: 874 (million) % 187.22/27.18 % (1794712)------------------------------ % 187.22/27.18 % (1794712)------------------------------ % 187.22/27.18 % (1794716)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=2411549290:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2775 on theBenchmark for (2775ds/1842Mi) % 187.22/27.18 % (1794714)Refutation not found, incomplete strategy % 187.22/27.18 % (1794714)------------------------------ % 187.22/27.18 % (1794714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.22/27.18 % (1794714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.22/27.18 % (1794714)CaDiCaL version: 2.1.3 % 187.22/27.18 % (1794714)Termination reason: Refutation not found, incomplete strategy % 187.22/27.18 % (1794714)Time elapsed: 0.980 s % 187.22/27.18 % (1794714)Peak memory usage: 176 MB % 187.22/27.18 % (1794714)Instructions burned: 1585 (million) % 187.22/27.18 [W928 14:13:55.551870571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:55.551904221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:55.551942214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:55.551954574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.22/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.22/27.18 [W928 14:13:55.551980614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.551992478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552028898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552040038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552063651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552073471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552096871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:55.552106888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 % (1794714)------------------------------ % 194.32/28.13 % (1794714)------------------------------ % 194.32/28.13 % (1794716)Refutation not found, incomplete strategy % 194.32/28.13 % (1794716)------------------------------ % 194.32/28.13 % (1794716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.32/28.13 % (1794716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.32/28.13 % (1794716)CaDiCaL version: 2.1.3 % 194.32/28.13 % (1794716)Termination reason: Refutation not found, incomplete strategy % 194.32/28.13 % (1794716)Time elapsed: 0.591 s % 194.32/28.13 % (1794716)Peak memory usage: 130 MB % 194.32/28.13 % (1794716)Instructions burned: 906 (million) % 194.32/28.13 % (1794718)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=839798035:i=66096:add=on_2768 on theBenchmark for (2768ds/66096Mi) % 194.32/28.13 % (1794716)------------------------------ % 194.32/28.13 % (1794716)------------------------------ % 194.32/28.13 % (1794720)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2032176413:i=1884:sd=1:nm=60:ss=axioms_2765 on theBenchmark for (2765ds/1884Mi) % 194.32/28.13 [W928 14:13:56.494435926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 194.32/28.13 [W928 14:13:56.494479666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 194.32/28.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494517773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494529450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494554827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494565277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494590850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494601573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494626030 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494636903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494660954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 [W928 14:13:56.494671520 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.95/29.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.95/29.56 % (1794720)Refutation not found, incomplete strategy % 203.95/29.56 % (1794720)------------------------------ % 203.95/29.56 % (1794720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.95/29.56 % (1794720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.95/29.56 % (1794720)CaDiCaL version: 2.1.3 % 203.95/29.56 % (1794720)Termination reason: Refutation not found, incomplete strategy % 203.95/29.56 % (1794720)Time elapsed: 0.572 s % 203.95/29.56 % (1794720)Peak memory usage: 132 MB % 203.95/29.56 % (1794720)Instructions burned: 874 (million) % 203.95/29.56 % (1794720)------------------------------ % 203.95/29.56 % (1794720)------------------------------ % 203.95/29.56 % (1794722)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1448442062:cts=off:i=5469:bs=on:fsr=off_2756 on theBenchmark for (2756ds/5469Mi) % 203.95/29.56 % (1794560)Instruction limit reached! % 203.95/29.56 % (1794560)------------------------------ % 203.95/29.56 % (1794560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.95/29.56 % (1794560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.76/30.11 % (1794560)CaDiCaL version: 2.1.3 % 207.76/30.11 % (1794560)Termination reason: Instruction limit % 207.76/30.11 % (1794560)Termination phase: Saturation % 207.76/30.11 % (1794560)Time elapsed: 26.248 s % 207.76/30.11 % (1794560)Peak memory usage: 177 MB % 207.76/30.11 % (1794560)Instructions burned: 141198 (million) % 207.76/30.11 % (1794724)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=3497469654:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2734 on theBenchmark for (2734ds/2037Mi) % 207.76/30.11 % (1794698)Instruction limit reached! % 207.76/30.11 % (1794698)------------------------------ % 207.76/30.11 % (1794698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.76/30.11 % (1794698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.76/30.11 % (1794698)CaDiCaL version: 2.1.3 % 207.76/30.11 % (1794698)Termination reason: Instruction limit % 207.76/30.11 % (1794698)Termination phase: Saturation % 207.76/30.11 % (1794698)Time elapsed: 11.686 s % 207.76/30.11 % (1794698)Peak memory usage: 155 MB % 207.76/30.11 % (1794698)Instructions burned: 30753 (million) % 207.76/30.11 % (1794726)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=358421956:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2730 on theBenchmark for (2730ds/2110Mi) % 207.76/30.11 % (1794724)Instruction limit reached! % 207.76/30.11 % (1794724)------------------------------ % 207.76/30.11 % (1794724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.76/30.11 % (1794724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.76/30.11 % (1794724)CaDiCaL version: 2.1.3 % 207.76/30.11 % (1794724)Termination reason: Instruction limit % 207.76/30.11 % (1794724)Termination phase: Saturation % 207.76/30.11 % (1794724)Time elapsed: 0.689 s % 207.76/30.11 % (1794724)Peak memory usage: 179 MB % 207.76/30.11 % (1794724)Instructions burned: 2040 (million) % 207.76/30.11 % (1794728)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=4036343908:i=2430:add=off:aac=none:nm=16_2727 on theBenchmark for (2727ds/2430Mi) % 207.76/30.11 [W928 14:13:59.027575792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027615075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027655382 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027679692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027706059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027716505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 207.76/30.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 207.76/30.11 [W928 14:13:59.027741442 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 [W928 14:13:59.027751812 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 [W928 14:13:59.027775992 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 [W928 14:13:59.027787029 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 [W928 14:13:59.027811752 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 [W928 14:13:59.027822736 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/31.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.82/31.13 % (1794726)Refutation not found, incomplete strategy % 214.82/31.13 % (1794726)------------------------------ % 214.82/31.13 % (1794726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.82/31.13 % (1794726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.82/31.13 % (1794726)CaDiCaL version: 2.1.3 % 214.82/31.13 % (1794726)Termination reason: Refutation not found, incomplete strategy % 214.82/31.13 % (1794726)Time elapsed: 0.582 s % 214.82/31.13 % (1794726)Peak memory usage: 130 MB % 214.82/31.13 % (1794726)Instructions burned: 879 (million) % 214.82/31.13 % (1794722)Instruction limit reached! % 214.82/31.13 % (1794722)------------------------------ % 214.82/31.13 % (1794722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.82/31.13 % (1794722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.82/31.13 % (1794722)CaDiCaL version: 2.1.3 % 214.82/31.13 % (1794722)Termination reason: Instruction limit % 214.82/31.13 % (1794722)Termination phase: Saturation % 214.82/31.13 % (1794722)Time elapsed: 3.266 s % 214.82/31.13 % (1794722)Peak memory usage: 121 MB % 214.82/31.13 % (1794722)Instructions burned: 5471 (million) % 214.82/31.13 % (1794730)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=3719852710:cond=fast:i=4891_2722 on theBenchmark for (2722ds/4891Mi) % 214.82/31.13 % (1794726)------------------------------ % 214.82/31.13 % (1794726)------------------------------ % 214.82/31.13 % (1794732)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=3752331975:st=2:i=14845:sd=2:ss=included:fsd=on_2720 on theBenchmark for (2720ds/14845Mi) % 214.82/31.13 % (1794728)Instruction limit reached! % 214.82/31.13 % (1794728)------------------------------ % 214.82/31.13 % (1794728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.82/31.13 % (1794728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.82/31.13 % (1794728)CaDiCaL version: 2.1.3 % 214.82/31.13 % (1794728)Termination reason: Instruction limit % 214.82/31.13 % (1794728)Termination phase: Saturation % 214.82/31.13 % (1794728)Time elapsed: 0.756 s % 214.82/31.13 % (1794728)Peak memory usage: 175 MB % 214.82/31.13 % (1794728)Instructions burned: 2430 (million) % 214.82/31.13 % (1794735)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=331235786:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2718 on theBenchmark for (2718ds/7534Mi) % 214.82/31.13 % (1794672)Instruction limit reached! % 204.25/31.96 % (1794672)------------------------------ % 204.25/31.96 % (1794672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/31.96 % (1794672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/31.96 % (1794672)CaDiCaL version: 2.1.3 % 204.25/31.96 % (1794672)Termination reason: Instruction limit % 204.25/31.96 % (1794672)Termination phase: Saturation % 204.25/31.96 % (1794672)Time elapsed: 18.327 s % 204.25/31.96 % (1794672)Peak memory usage: 229 MB % 204.25/31.96 % (1794672)Instructions burned: 33335 (million) % 204.25/31.96 % (1794732)Refutation not found, incomplete strategy % 204.25/31.96 % (1794732)------------------------------ % 204.25/31.96 % (1794732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/31.96 % (1794732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/31.96 % (1794732)CaDiCaL version: 2.1.3 % 204.25/31.96 % (1794732)Termination reason: Refutation not found, incomplete strategy % 204.25/31.96 % (1794732)Time elapsed: 0.909 s % 204.25/31.96 % (1794732)Peak memory usage: 152 MB % 204.25/31.96 % (1794732)Instructions burned: 1506 (million) % 204.25/31.96 % (1794737)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=2286289717:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2710 on theBenchmark for (2710ds/10353Mi) % 204.25/31.96 % (1794732)------------------------------ % 204.25/31.96 % (1794732)------------------------------ % 204.25/31.96 % (1794739)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=377023467:i=7860_2708 on theBenchmark for (2708ds/7860Mi) % 204.25/31.96 [W928 14:14:01.000261692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000295272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000333806 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000346679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000373606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000385663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000411889 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000423883 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 204.25/31.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 204.25/31.96 [W928 14:14:01.000449679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.71/32.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.71/32.52 [W928 14:14:01.000461616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.71/32.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.71/32.52 [W928 14:14:01.000486899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.71/32.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.71/32.52 [W928 14:14:01.000497753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.71/32.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.71/32.52 % (1794739)Refutation not found, incomplete strategy % 224.71/32.52 % (1794739)------------------------------ % 224.71/32.52 % (1794739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.71/32.52 % (1794739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.71/32.52 % (1794739)CaDiCaL version: 2.1.3 % 224.71/32.52 % (1794739)Termination reason: Refutation not found, incomplete strategy % 224.71/32.52 % (1794739)Time elapsed: 0.136 s % 224.71/32.52 % (1794739)Peak memory usage: 96 MB % 224.71/32.52 % (1794739)Instructions burned: 271 (million) % 224.71/32.52 % (1794737)Refutation not found, incomplete strategy % 224.71/32.52 % (1794737)------------------------------ % 224.71/32.52 % (1794737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.71/32.52 % (1794737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.71/32.52 % (1794737)CaDiCaL version: 2.1.3 % 224.71/32.52 % (1794737)Termination reason: Refutation not found, incomplete strategy % 224.71/32.52 % (1794737)Time elapsed: 0.575 s % 224.71/32.52 % (1794737)Peak memory usage: 133 MB % 224.71/32.52 % (1794737)Instructions burned: 875 (million) % 224.71/32.52 % (1794739)------------------------------ % 224.71/32.52 % (1794739)------------------------------ % 224.71/32.52 % (1794741)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=1060382810:i=7896:sd=2:bs=on:ss=included:sgt=20_2703 on theBenchmark for (2703ds/7896Mi) % 224.71/32.52 % (1794737)------------------------------ % 224.71/32.52 % (1794737)------------------------------ % 224.71/32.52 % (1794743)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=217727049:i=5812:gtgl=2:gtg=all_2701 on theBenchmark for (2701ds/5812Mi) % 224.71/32.52 % (1794735)Instruction limit reached! % 224.71/32.52 % (1794735)------------------------------ % 224.71/32.52 % (1794735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.71/32.52 % (1794735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.71/32.52 % (1794735)CaDiCaL version: 2.1.3 % 224.71/32.52 % (1794735)Termination reason: Instruction limit % 224.71/32.52 % (1794735)Termination phase: Saturation % 224.71/32.52 % (1794735)Time elapsed: 1.853 s % 224.71/32.52 % (1794735)Peak memory usage: 178 MB % 224.71/32.52 % (1794735)Instructions burned: 7539 (million) % 224.71/32.52 % (1794745)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=1464942859:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2699 on theBenchmark for (2699ds/2965Mi) % 224.71/32.52 % (1794730)Instruction limit reached! % 224.71/32.52 % (1794730)------------------------------ % 224.71/32.52 % (1794730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.71/32.52 % (1794730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.71/32.52 % (1794730)CaDiCaL version: 2.1.3 % 224.71/32.52 % (1794730)Termination reason: Instruction limit % 224.71/32.52 % (1794730)Termination phase: Saturation % 224.71/32.52 % (1794730)Time elapsed: 2.432 s % 224.71/32.52 % (1794730)Peak memory usage: 174 MB % 224.71/32.52 % (1794730)Instructions burned: 4892 (million) % 224.71/32.52 % (1794747)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=3174763808:i=2967:kws=precedence:bd=preordered:av=off_2696 on theBenchmark for (2696ds/2967Mi) % 230.56/33.34 % (1794745)Refutation not found, incomplete strategy % 230.56/33.34 % (1794745)------------------------------ % 230.56/33.34 % (1794745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.56/33.34 % (1794745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.56/33.34 % (1794745)CaDiCaL version: 2.1.3 % 230.56/33.34 % (1794745)Termination reason: Refutation not found, incomplete strategy % 230.56/33.34 % (1794745)Time elapsed: 0.645 s % 230.56/33.34 % (1794745)Peak memory usage: 177 MB % 230.56/33.34 % (1794745)Instructions burned: 1866 (million) % 230.56/33.34 % (1794745)------------------------------ % 230.56/33.34 % (1794745)------------------------------ % 230.56/33.34 % (1794749)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=3037837287:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2690 on theBenchmark for (2690ds/3022Mi) % 230.56/33.34 % (1794700)Instruction limit reached! % 230.56/33.34 % (1794700)------------------------------ % 230.56/33.34 % (1794700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.56/33.34 % (1794700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.56/33.34 % (1794700)CaDiCaL version: 2.1.3 % 230.56/33.34 % (1794700)Termination reason: Instruction limit % 230.56/33.34 % (1794700)Termination phase: Saturation % 230.56/33.34 % (1794700)Time elapsed: 15.177 s % 230.56/33.34 % (1794700)Peak memory usage: 535 MB % 230.56/33.34 % (1794700)Instructions burned: 26474 (million) % 230.56/33.34 [W928 14:14:03.850788530 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850810787 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850831706 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850838794 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850853436 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850860183 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850873367 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.56/33.34 [W928 14:14:03.850879863 register_special_ops.cpp:225] Warning: Creating a tensor from 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.56/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.850892502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.850898029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.850911387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.850954760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 % (1794749)Refutation not found, incomplete strategy % 232.41/33.67 % (1794749)------------------------------ % 232.41/33.67 % (1794749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.67 % (1794749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.67 % (1794749)CaDiCaL version: 2.1.3 % 232.41/33.67 % (1794749)Termination reason: Refutation not found, incomplete strategy % 232.41/33.67 % (1794749)Time elapsed: 0.320 s % 232.41/33.67 % (1794749)Peak memory usage: 132 MB % 232.41/33.67 % (1794749)Instructions burned: 876 (million) % 232.41/33.67 % (1794751)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=489853170:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2687 on theBenchmark for (2687ds/3207Mi) % 232.41/33.67 % (1794749)------------------------------ % 232.41/33.67 % (1794749)------------------------------ % 232.41/33.67 % (1794753)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2018988780:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2684 on theBenchmark for (2684ds/3289Mi) % 232.41/33.67 [W928 14:14:03.416465324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.416507175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.416546435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.416558525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.416585768 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 232.41/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 232.41/33.67 [W928 14:14:03.416598965 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416625658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416636658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416661182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416672162 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416697362 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 [W928 14:14:03.416708185 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.03/34.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.03/34.73 % (1794751)Refutation not found, incomplete strategy % 240.03/34.73 % (1794751)------------------------------ % 240.03/34.73 % (1794751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.03/34.73 % (1794751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.03/34.73 % (1794751)CaDiCaL version: 2.1.3 % 240.03/34.73 % (1794751)Termination reason: Refutation not found, incomplete strategy % 240.03/34.73 % (1794751)Time elapsed: 0.625 s % 240.03/34.73 % (1794751)Peak memory usage: 129 MB % 240.03/34.73 % (1794751)Instructions burned: 875 (million) % 240.03/34.73 % (1794751)------------------------------ % 240.03/34.73 % (1794751)------------------------------ % 240.03/34.73 % (1794747)Instruction limit reached! % 240.03/34.73 % (1794747)------------------------------ % 240.03/34.73 % (1794747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.03/34.73 % (1794747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.03/34.73 % (1794747)CaDiCaL version: 2.1.3 % 240.03/34.73 % (1794747)Termination reason: Instruction limit % 240.03/34.73 % (1794747)Termination phase: Saturation % 240.03/34.73 % (1794747)Time elapsed: 1.834 s % 240.03/34.73 % (1794747)Peak memory usage: 178 MB % 240.03/34.73 % (1794747)Instructions burned: 2967 (million) % 240.03/34.73 % (1794755)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3342060631:i=38569:sd=3:ss=axioms:sgt=32_2677 on theBenchmark for (2677ds/38569Mi) % 240.03/34.73 % (1794756)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2132499443:cts=off:i=3394_2677 on theBenchmark for (2677ds/3394Mi) % 240.03/34.73 % (1794753)Refutation not found, incomplete strategy % 240.03/34.73 % (1794753)------------------------------ % 240.03/34.73 % (1794753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.03/34.73 % (1794753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.03/34.73 % (1794753)CaDiCaL version: 2.1.3 % 240.03/34.73 % (1794753)Termination reason: Refutation not found, incomplete strategy % 240.03/34.73 % (1794753)Time elapsed: 0.734 s % 240.03/34.73 % (1794753)Peak memory usage: 171 MB % 240.03/34.73 % (1794753)Instructions burned: 1896 (million) % 240.03/34.73 % (1794753)------------------------------ % 240.03/34.73 % (1794753)------------------------------ % 240.03/34.73 % (1794759)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=3152757697:i=33824:bd=preordered_2674 on theBenchmark for (2674ds/33824Mi) % 244.02/35.20 [W928 14:14:04.374045721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374077861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374116955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374129442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374155635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374167898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374195102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374206962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374232605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374244329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374270245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 [W928 14:14:04.374281999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 244.02/35.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 244.02/35.20 % (1794755)Refutation not found, incomplete strategy % 244.02/35.20 % (1794755)------------------------------ % 244.02/35.20 % (1794755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.86/35.54 % (1794755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.86/35.54 % (1794755)CaDiCaL version: 2.1.3 % 245.86/35.54 % (1794755)Termination reason: Refutation not found, incomplete strategy % 245.86/35.54 % (1794755)Time elapsed: 0.583 s % 245.86/35.54 % (1794755)Peak memory usage: 133 MB % 245.86/35.54 % (1794755)Instructions burned: 875 (million) % 245.86/35.54 % (1794755)------------------------------ % 245.86/35.54 % (1794755)------------------------------ % 245.86/35.54 % (1794761)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=258663360:i=20684:bd=all:gtg=exists_sym_2667 on theBenchmark for (2667ds/20684Mi) % 245.86/35.54 % (1794743)Instruction limit reached! % 245.86/35.54 % (1794743)------------------------------ % 245.86/35.54 % (1794743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.86/35.54 % (1794743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.86/35.54 % (1794743)CaDiCaL version: 2.1.3 % 245.86/35.54 % (1794743)Termination reason: Instruction limit % 245.86/35.54 % (1794743)Termination phase: Saturation % 245.86/35.54 % (1794743)Time elapsed: 3.505 s % 245.86/35.54 % (1794743)Peak memory usage: 179 MB % 245.86/35.54 % (1794743)Instructions burned: 5812 (million) % 245.86/35.54 % (1794763)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=2480609463:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2664 on theBenchmark for (2664ds/7222Mi) % 245.86/35.54 % (1794741)Instruction limit reached! % 245.86/35.54 % (1794741)------------------------------ % 245.86/35.54 % (1794741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.86/35.54 % (1794741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.86/35.54 % (1794741)CaDiCaL version: 2.1.3 % 245.86/35.54 % (1794741)Termination reason: Instruction limit % 245.86/35.54 % (1794741)Termination phase: Saturation % 245.86/35.54 % (1794741)Time elapsed: 4.163 s % 245.86/35.54 % (1794741)Peak memory usage: 163 MB % 245.86/35.54 % (1794741)Instructions burned: 7897 (million) % 245.86/35.54 [W928 14:14:06.619636356 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619680246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619719750 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619731506 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619756140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619766436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 245.86/35.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.86/35.54 [W928 14:14:06.619790966 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.619800947 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.619825107 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.619835123 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.619858207 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.619868120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 % (1794765)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=4138898922:st=4:i=7295:sd=4:ep=R:ss=axioms_2659 on theBenchmark for (2659ds/7295Mi) % 279.95/40.32 % (1794763)Refutation not found, incomplete strategy % 279.95/40.32 % (1794763)------------------------------ % 279.95/40.32 % (1794763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.95/40.32 % (1794763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.95/40.32 % (1794763)CaDiCaL version: 2.1.3 % 279.95/40.32 % (1794763)Termination reason: Refutation not found, incomplete strategy % 279.95/40.32 % (1794763)Time elapsed: 0.589 s % 279.95/40.32 % (1794763)Peak memory usage: 130 MB % 279.95/40.32 % (1794763)Instructions burned: 910 (million) % 279.95/40.32 % (1794756)Instruction limit reached! % 279.95/40.32 % (1794756)------------------------------ % 279.95/40.32 % (1794756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.95/40.32 % (1794756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.95/40.32 % (1794756)CaDiCaL version: 2.1.3 % 279.95/40.32 % (1794756)Termination reason: Instruction limit % 279.95/40.32 % (1794756)Termination phase: Saturation % 279.95/40.32 % (1794756)Time elapsed: 1.853 s % 279.95/40.32 % (1794756)Peak memory usage: 154 MB % 279.95/40.32 % (1794756)Instructions burned: 3394 (million) % 279.95/40.32 % (1794767)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=958637376:i=4036:ins=10_2657 on theBenchmark for (2657ds/4036Mi) % 279.95/40.32 % (1794763)------------------------------ % 279.95/40.32 % (1794763)------------------------------ % 279.95/40.32 [W928 14:14:06.099319452 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.099353502 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/40.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 279.95/40.32 [W928 14:14:06.099392225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099404952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099430519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099453092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099479479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099489665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099517579 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099527972 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099551962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 [W928 14:14:06.099562336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.20/41.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.20/41.30 % (1794769)lrs+10_1_sil=128000:lcm=predicate:random_seed=3957244879:st=3:i=43697:sd=5:ss=axioms_2655 on theBenchmark for (2655ds/43697Mi) % 287.20/41.30 % (1794769)Refutation not found, incomplete strategy % 287.20/41.30 % (1794769)------------------------------ % 287.20/41.30 % (1794769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.20/41.30 % (1794769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.20/41.30 % (1794769)CaDiCaL version: 2.1.3 % 287.20/41.30 % (1794769)Termination reason: Refutation not found, incomplete strategy % 287.20/41.30 % (1794769)Time elapsed: 0.009 s % 287.20/41.30 % (1794769)Peak memory usage: 89 MB % 287.20/41.30 % (1794769)Instructions burned: 14 (million) % 287.20/41.30 % (1794765)Refutation not found, incomplete strategy % 287.20/41.30 % (1794765)------------------------------ % 287.20/41.30 % (1794765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.20/41.30 % (1794765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.20/41.30 % (1794765)CaDiCaL version: 2.1.3 % 287.20/41.30 % (1794765)Termination reason: Refutation not found, incomplete strategy % 287.20/41.30 % (1794765)Time elapsed: 0.578 s % 287.20/41.30 % (1794765)Peak memory usage: 132 MB % 287.20/41.30 % (1794765)Instructions burned: 880 (million) % 287.20/41.30 % (1794769)------------------------------ % 289.40/41.75 % (1794769)------------------------------ % 289.40/41.75 % (1794765)------------------------------ % 289.40/41.75 % (1794765)------------------------------ % 289.40/41.75 % (1794771)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=2120025941:i=17599:gtg=all:ss=axioms:fsd=on_2651 on theBenchmark for (2651ds/17599Mi) % 289.40/41.75 % (1794772)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=3835776546:i=4547:bd=preordered_2650 on theBenchmark for (2650ds/4547Mi) % 289.40/41.75 % (1794767)Instruction limit reached! % 289.40/41.75 % (1794767)------------------------------ % 289.40/41.75 % (1794767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.40/41.75 % (1794767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.40/41.75 % (1794767)CaDiCaL version: 2.1.3 % 289.40/41.75 % (1794767)Termination reason: Instruction limit % 289.40/41.75 % (1794767)Termination phase: Saturation % 289.40/41.75 % (1794767)Time elapsed: 2.137 s % 289.40/41.75 % (1794767)Peak memory usage: 159 MB % 289.40/41.75 % (1794767)Instructions burned: 4038 (million) % 289.40/41.75 % (1794775)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=2668101344:i=9294:av=off_2634 on theBenchmark for (2634ds/9294Mi) % 289.40/41.75 % (1794772)Instruction limit reached! % 289.40/41.75 % (1794772)------------------------------ % 289.40/41.75 % (1794772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.40/41.75 % (1794772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.40/41.75 % (1794772)CaDiCaL version: 2.1.3 % 289.40/41.75 % (1794772)Termination reason: Instruction limit % 289.40/41.75 % (1794772)Termination phase: Saturation % 289.40/41.75 % (1794772)Time elapsed: 2.830 s % 289.40/41.75 % (1794772)Peak memory usage: 176 MB % 289.40/41.75 % (1794772)Instructions burned: 4549 (million) % 289.40/41.75 % (1794777)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2173188225:i=32849:add=on_2620 on theBenchmark for (2620ds/32849Mi) % 289.40/41.75 % (1794759)Instruction limit reached! % 289.40/41.75 % (1794759)------------------------------ % 289.40/41.75 % (1794759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.40/41.75 % (1794759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.40/41.75 % (1794759)CaDiCaL version: 2.1.3 % 289.40/41.75 % (1794759)Termination reason: Instruction limit % 289.40/41.75 % (1794759)Termination phase: Saturation % 289.40/41.75 % (1794759)Time elapsed: 6.678 s % 289.40/41.75 % (1794759)Peak memory usage: 176 MB % 289.40/41.75 % (1794759)Instructions burned: 33826 (million) % 289.40/41.75 % (1794779)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3302729970:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2606 on theBenchmark for (2606ds/4793Mi) % 289.40/41.75 [W928 14:14:11.215644402 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.40/41.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.40/41.75 [W928 14:14:11.215664678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.40/41.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.40/41.75 [W928 14:14:11.215686286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.40/41.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.40/41.75 [W928 14:14:11.215692685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.40/41.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.40/41.75 [W928 14:14:11.215706428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215713399 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215726561 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215732244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215744759 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215750511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215763062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 [W928 14:14:11.215768782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.31/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.31/43.17 % (1794779)Refutation not found, incomplete strategy % 300.31/43.17 % (1794779)------------------------------ % 300.31/43.17 % (1794779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.31/43.17 % (1794779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.31/43.17 % (1794779)CaDiCaL version: 2.1.3 % 300.31/43.17 % (1794779)Termination reason: Refutation not found, incomplete strategy % 300.31/43.17 % (1794779)Time elapsed: 0.318 s % 300.31/43.17 % (1794779)Peak memory usage: 132 MB % 300.31/43.17 % (1794779)Instructions burned: 884 (million) % 300.31/43.17 % (1794779)------------------------------ % 300.31/43.17 % (1794779)------------------------------ % 300.31/43.17 % (1794781)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=2403740777:i=4840:nm=4:av=off_2600 on theBenchmark for (2600ds/4840Mi) % 300.31/43.17 % (1794775)Instruction limit reached! % 300.31/43.17 % (1794775)------------------------------ % 300.31/43.17 % (1794775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.31/43.17 % (1794775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.31/43.17 % (1794775)CaDiCaL version: 2.1.3 % 300.31/43.17 % (1794775)Termination reason: Instruction limit % 300.31/43.17 % (1794775)Termination phase: Saturation % 300.31/43.17 % (1794775)Time elapsed: 3.824 s % 300.31/43.17 % (1794775)Peak memory usage: 175 MB % 300.31/43.17 % (1794775)Instructions burned: 9297 (million) % 300.31/43.17 % (1794781)Refutation not found, incomplete strategy % 300.31/43.17 % (1794781)------------------------------ % 300.31/43.17 % (1794781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.31/43.17 % (1794781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96 % 300.31/43.18 Terminated %------------------------------------------------------------------------------