%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM926_40 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:36 PM UTC 2026 % Result : Timeout 298.89s 43.36s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM926_40 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.38 % Computer : n017.cluster.edu % 0.09/0.38 % Model : x86_64 x86_64 % 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.38 % Memory : 8046.5625MB % 0.09/0.38 % OS : Linux 6.8.0-71-generic % 0.09/0.38 % CPULimit : 300 % 0.09/0.38 % WCLimit : 300 % 0.09/0.38 % DateTime : Sun Sep 27 21:39:51 UTC 2026 % 0.09/0.38 % CPUTime : % 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.42 Running first-order theorem proving % 0.09/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 11.03/2.83 % (2964119)Detected formulas, will run a generic FOF schedule. % 11.03/2.83 % (2964126)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=3370208411:i=141695:sd=1:nm=32:gsp=on:ss=included_2996 on theBenchmark for (2996ds/141695Mi) % 11.03/2.83 % (2964129)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=572402436:s2a=on:i=139:gtg=position_2996 on theBenchmark for (2996ds/139Mi) % 11.03/2.83 % (2964128)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1754936172:i=119:av=off:ss=axioms_2996 on theBenchmark for (2996ds/119Mi) % 11.03/2.83 % (2964127)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=972568314:i=109:sd=1:ins=1:gsp=on:ss=axioms_2996 on theBenchmark for (2996ds/109Mi) % 11.03/2.83 % (2964125)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=1608061794:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2996 on theBenchmark for (2996ds/134677Mi) % 11.03/2.83 % (2964124)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=2255994049:i=141193_2996 on theBenchmark for (2996ds/141193Mi) % 11.03/2.83 % (2964130)dis-21_1_sil=8000:lcm=predicate:random_seed=2419845910:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2996 on theBenchmark for (2996ds/129Mi) % 11.03/2.83 % (2964128)Refutation not found, incomplete strategy % 11.03/2.83 % (2964128)------------------------------ % 11.03/2.83 % (2964128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.83 % (2964128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.83 % (2964128)CaDiCaL version: 2.1.3 % 11.03/2.83 % (2964128)Termination reason: Refutation not found, incomplete strategy % 11.03/2.83 % (2964128)Time elapsed: 0.023 s % 11.03/2.83 % (2964128)Peak memory usage: 91 MB % 11.03/2.83 % (2964128)Instructions burned: 35 (million) % 11.03/2.83 % (2964127)Refutation not found, incomplete strategy % 11.03/2.83 % (2964127)------------------------------ % 11.03/2.83 % (2964127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.83 % (2964127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.83 % (2964127)CaDiCaL version: 2.1.3 % 11.03/2.83 % (2964127)Termination reason: Refutation not found, incomplete strategy % 11.03/2.83 % (2964127)Time elapsed: 0.023 s % 11.03/2.83 % (2964127)Peak memory usage: 92 MB % 11.03/2.83 % (2964127)Instructions burned: 35 (million) % 11.03/2.83 % (2964129)Instruction limit reached! % 11.03/2.83 % (2964129)------------------------------ % 11.03/2.83 % (2964129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.83 % (2964129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.83 % (2964129)CaDiCaL version: 2.1.3 % 11.03/2.83 % (2964129)Termination reason: Instruction limit % 11.03/2.83 % (2964129)Termination phase: SInE selection % 11.03/2.83 % (2964129)Time elapsed: 0.059 s % 11.03/2.83 % (2964129)Peak memory usage: 90 MB % 11.03/2.83 % (2964129)Instructions burned: 140 (million) % 11.03/2.83 % (2964130)Instruction limit reached! % 11.03/2.83 % (2964130)------------------------------ % 11.03/2.83 % (2964130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.83 % (2964130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.83 % (2964130)CaDiCaL version: 2.1.3 % 11.03/2.83 % (2964130)Termination reason: Instruction limit % 11.03/2.83 % (2964130)Termination phase: Preprocessing 3 % 11.03/2.83 % (2964130)Time elapsed: 0.080 s % 11.03/2.83 % (2964130)Peak memory usage: 93 MB % 11.03/2.83 % (2964130)Instructions burned: 131 (million) % 11.03/2.83 % (2964139)lrs+10_1_sil=8000:sp=occurrence:random_seed=828896619:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi) % 11.03/2.83 % (2964139)Refutation not found, incomplete strategy % 11.03/2.83 % (2964139)------------------------------ % 11.03/2.83 % (2964139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.83 % (2964139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.83 % (2964139)CaDiCaL version: 2.1.3 % 11.03/2.83 % (2964139)Termination reason: Refutation not found, incomplete strategy % 11.03/2.83 % (2964139)Time elapsed: 0.024 s % 11.03/2.83 % (2964139)Peak memory usage: 92 MB % 11.03/2.83 % (2964139)Instructions burned: 34 (million) % 11.57/2.92 % (2964140)lrs+10_1_sil=32000:urr=on:br=off:random_seed=633470729:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi) % 11.57/2.92 % (2964128)------------------------------ % 11.57/2.92 % (2964128)------------------------------ % 11.57/2.92 % (2964127)------------------------------ % 11.57/2.92 % (2964127)------------------------------ % 11.57/2.92 % (2964140)Refutation not found, incomplete strategy % 11.57/2.92 % (2964140)------------------------------ % 11.57/2.92 % (2964140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.92 % (2964140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.92 % (2964140)CaDiCaL version: 2.1.3 % 11.57/2.92 % (2964140)Termination reason: Refutation not found, incomplete strategy % 11.57/2.92 % (2964140)Time elapsed: 0.071 s % 11.57/2.92 % (2964140)Peak memory usage: 92 MB % 11.57/2.92 % (2964140)Instructions burned: 155 (million) % 11.57/2.92 % (2964144)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=2482295637:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi) % 11.57/2.92 % (2964143)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4237300215:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi) % 11.57/2.92 % (2964143)Refutation not found, incomplete strategy % 11.57/2.92 % (2964143)------------------------------ % 11.57/2.92 % (2964143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.92 % (2964143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.92 % (2964143)CaDiCaL version: 2.1.3 % 11.57/2.92 % (2964143)Termination reason: Refutation not found, incomplete strategy % 11.57/2.92 % (2964143)Time elapsed: 0.024 s % 11.57/2.92 % (2964143)Peak memory usage: 92 MB % 11.57/2.92 % (2964143)Instructions burned: 34 (million) % 11.57/2.92 % (2964139)------------------------------ % 11.57/2.92 % (2964139)------------------------------ % 11.57/2.92 % (2964144)Instruction limit reached! % 11.57/2.92 % (2964144)------------------------------ % 11.57/2.92 % (2964144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.92 % (2964144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.92 % (2964144)CaDiCaL version: 2.1.3 % 11.57/2.92 % (2964144)Termination reason: Instruction limit % 11.57/2.92 % (2964144)Termination phase: Preprocessing 3 % 11.57/2.92 % (2964144)Time elapsed: 0.124 s % 11.57/2.92 % (2964144)Peak memory usage: 93 MB % 11.57/2.92 % (2964144)Instructions burned: 248 (million) % 11.57/2.92 % (2964140)------------------------------ % 11.57/2.92 % (2964140)------------------------------ % 11.57/2.92 % (2964147)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=482779514:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi) % 11.57/2.92 % (2964147)Refutation not found, incomplete strategy % 11.57/2.92 % (2964147)------------------------------ % 11.57/2.92 % (2964147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.92 % (2964147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.92 % (2964147)CaDiCaL version: 2.1.3 % 11.57/2.92 % (2964147)Termination reason: Refutation not found, incomplete strategy % 11.57/2.92 % (2964147)Time elapsed: 0.032 s % 11.57/2.92 % (2964147)Peak memory usage: 92 MB % 11.57/2.92 % (2964147)Instructions burned: 53 (million) % 11.57/2.92 % (2964148)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2505423420:i=2350_2989 on theBenchmark for (2989ds/2350Mi) % 11.57/2.92 % (2964143)------------------------------ % 11.57/2.92 % (2964143)------------------------------ % 11.57/2.92 % (2964149)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3050574460:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi) % 11.57/2.92 % (2964149)Instruction limit reached! % 11.57/2.92 % (2964149)------------------------------ % 11.57/2.92 % (2964149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.92 % (2964149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.92 % (2964149)CaDiCaL version: 2.1.3 % 11.57/2.92 % (2964149)Termination reason: Instruction limit % 11.57/2.92 % (2964149)Termination phase: Preprocessing 3 % 11.57/2.92 % (2964149)Time elapsed: 0.072 s % 11.57/2.92 % (2964149)Peak memory usage: 93 MB % 11.57/2.92 % (2964149)Instructions burned: 113 (million) % 11.57/2.92 % (2964153)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2013826686:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi) % 13.49/3.04 % (2964147)------------------------------ % 13.49/3.04 % (2964147)------------------------------ % 13.49/3.04 % (2964154)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3780121923:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi) % 13.49/3.04 % (2964153)Instruction limit reached! % 13.49/3.04 % (2964153)------------------------------ % 13.49/3.04 % (2964153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/3.04 % (2964153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/3.04 % (2964153)CaDiCaL version: 2.1.3 % 13.49/3.04 % (2964153)Termination reason: Instruction limit % 13.49/3.04 % (2964153)Termination phase: Property scanning % 13.49/3.04 % (2964153)Time elapsed: 0.081 s % 13.49/3.04 % (2964153)Peak memory usage: 95 MB % 13.49/3.04 % (2964153)Instructions burned: 128 (million) % 13.49/3.04 % (2964154)Instruction limit reached! % 13.49/3.04 % (2964154)------------------------------ % 13.49/3.04 % (2964154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/3.04 % (2964154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/3.04 % (2964154)CaDiCaL version: 2.1.3 % 13.49/3.04 % (2964154)Termination reason: Instruction limit % 13.49/3.04 % (2964154)Termination phase: Property scanning % 13.49/3.04 % (2964154)Time elapsed: 0.046 s % 13.49/3.04 % (2964154)Peak memory usage: 89 MB % 13.49/3.04 % (2964154)Instructions burned: 116 (million) % 13.49/3.04 % (2964156)lrs+10_1_sil=8000:sp=occurrence:random_seed=1794692066:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi) % 13.49/3.04 % (2964156)Refutation not found, incomplete strategy % 13.49/3.04 % (2964156)------------------------------ % 13.49/3.04 % (2964156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/3.04 % (2964156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/3.04 % (2964156)CaDiCaL version: 2.1.3 % 13.49/3.04 % (2964156)Termination reason: Refutation not found, incomplete strategy % 13.49/3.04 % (2964156)Time elapsed: 0.031 s % 13.49/3.04 % (2964156)Peak memory usage: 92 MB % 13.49/3.04 % (2964156)Instructions burned: 49 (million) % 13.49/3.04 % (2964158)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2076487760:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi) % 13.49/3.04 % (2964159)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4201580579:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi) % 13.49/3.04 % (2964126)Refutation not found, incomplete strategy % 13.49/3.04 % (2964126)------------------------------ % 13.49/3.04 % (2964126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/3.04 % (2964126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/3.04 % (2964126)CaDiCaL version: 2.1.3 % 13.49/3.04 % (2964126)Termination reason: Refutation not found, incomplete strategy % 13.49/3.04 % (2964126)Time elapsed: 1.170 s % 13.49/3.04 % (2964126)Peak memory usage: 224 MB % 13.49/3.04 % (2964126)Instructions burned: 3027 (million) % 13.49/3.04 % (2964158)Instruction limit reached! % 13.49/3.04 % (2964158)------------------------------ % 13.49/3.04 % (2964158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/3.04 % (2964158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/3.04 % (2964158)CaDiCaL version: 2.1.3 % 13.49/3.04 % (2964158)Termination reason: Instruction limit % 13.49/3.04 % (2964158)Termination phase: Property scanning % 13.49/3.04 % (2964158)Time elapsed: 0.210 s % 13.49/3.04 % (2964158)Peak memory usage: 95 MB % 13.49/3.04 % (2964158)Instructions burned: 439 (million) % 13.49/3.04 % (2964156)------------------------------ % 13.49/3.04 % (2964156)------------------------------ % 13.49/3.04 % (2964126)------------------------------ % 13.49/3.04 % (2964126)------------------------------ % 13.49/3.04 % (2964163)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=239729996:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi) % 13.49/3.04 % (2964165)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3604947608:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi) % 13.49/3.04 % (2964164)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1670090570:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi) % 13.49/3.04 % (2964164)Refutation not found, incomplete strategy % 15.58/3.41 % (2964164)------------------------------ % 15.58/3.41 % (2964164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.58/3.41 % (2964164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.58/3.41 % (2964164)CaDiCaL version: 2.1.3 % 15.58/3.41 % (2964164)Termination reason: Refutation not found, incomplete strategy % 15.58/3.41 % (2964164)Time elapsed: 0.032 s % 15.58/3.41 % (2964164)Peak memory usage: 92 MB % 15.58/3.41 % (2964164)Instructions burned: 52 (million) % 15.58/3.41 % (2964163)Instruction limit reached! % 15.58/3.41 % (2964163)------------------------------ % 15.58/3.41 % (2964163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.58/3.41 % (2964163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.58/3.41 % (2964163)CaDiCaL version: 2.1.3 % 15.58/3.41 % (2964163)Termination reason: Instruction limit % 15.58/3.41 % (2964163)Termination phase: NewCNF % 15.58/3.41 % (2964163)Time elapsed: 0.093 s % 15.58/3.41 % (2964163)Peak memory usage: 95 MB % 15.58/3.41 % (2964163)Instructions burned: 134 (million) % 15.58/3.41 [W927 21:39:53.998778752 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998812116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998852029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998865613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998893976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998905473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998932687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998944270 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998969807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.58/3.41 [W927 21:39:53.998981174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.58/3.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:53.999017954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:53.999029531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 % (2964169)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=2288766921:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi) % 18.05/3.99 [W927 21:39:54.122129811 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122153491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122175645 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122182388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122196217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122202924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122216550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122222857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122235466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122241786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.05/3.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.05/3.99 [W927 21:39:54.122254611 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.37/5.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.37/5.33 [W927 21:39:54.122260841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.37/5.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.37/5.33 % (2964169)Instruction limit reached! % 29.37/5.33 % (2964169)------------------------------ % 29.37/5.33 % (2964169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.37/5.33 % (2964169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.37/5.33 % (2964169)CaDiCaL version: 2.1.3 % 29.37/5.33 % (2964169)Termination reason: Instruction limit % 29.37/5.33 % (2964169)Termination phase: SInE selection % 29.37/5.33 % (2964169)Time elapsed: 0.051 s % 29.37/5.33 % (2964169)Peak memory usage: 90 MB % 29.37/5.33 % (2964169)Instructions burned: 125 (million) % 29.37/5.33 % (2964164)------------------------------ % 29.37/5.33 % (2964164)------------------------------ % 29.37/5.33 % (2964159)Refutation not found, incomplete strategy % 29.37/5.33 % (2964159)------------------------------ % 29.37/5.33 % (2964159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.37/5.33 % (2964159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.37/5.33 % (2964159)CaDiCaL version: 2.1.3 % 29.37/5.33 % (2964159)Termination reason: Refutation not found, incomplete strategy % 29.37/5.33 % (2964159)Time elapsed: 0.632 s % 29.37/5.33 % (2964159)Peak memory usage: 134 MB % 29.37/5.33 % (2964159)Instructions burned: 925 (million) % 29.37/5.33 % (2964165)Refutation not found, incomplete strategy % 29.37/5.33 % (2964165)------------------------------ % 29.37/5.33 % (2964165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.37/5.33 % (2964165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.37/5.33 % (2964165)CaDiCaL version: 2.1.3 % 29.37/5.33 % (2964165)Termination reason: Refutation not found, incomplete strategy % 29.37/5.33 % (2964165)Time elapsed: 0.354 s % 29.37/5.33 % (2964165)Peak memory usage: 135 MB % 29.37/5.33 % (2964165)Instructions burned: 943 (million) % 29.37/5.33 % (2964171)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4098766342:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi) % 29.37/5.33 % (2964172)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2154851256:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi) % 29.37/5.33 % (2964172)Refutation not found, incomplete strategy % 29.37/5.33 % (2964172)------------------------------ % 29.37/5.33 % (2964172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.37/5.33 % (2964172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.37/5.33 % (2964172)CaDiCaL version: 2.1.3 % 29.37/5.33 % (2964172)Termination reason: Refutation not found, incomplete strategy % 29.37/5.33 % (2964172)Time elapsed: 0.024 s % 29.37/5.33 % (2964172)Peak memory usage: 92 MB % 29.37/5.33 % (2964172)Instructions burned: 35 (million) % 29.37/5.33 % (2964171)Instruction limit reached! % 29.37/5.33 % (2964171)------------------------------ % 29.37/5.33 % (2964171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.37/5.33 % (2964171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.37/5.33 % (2964171)CaDiCaL version: 2.1.3 % 29.37/5.33 % (2964171)Termination reason: Instruction limit % 29.37/5.33 % (2964171)Termination phase: Initialization % 29.37/5.33 % (2964171)Time elapsed: 0.055 s % 29.37/5.33 % (2964171)Peak memory usage: 89 MB % 29.37/5.33 % (2964171)Instructions burned: 135 (million) % 29.37/5.33 % (2964165)------------------------------ % 29.37/5.33 % (2964165)------------------------------ % 29.37/5.33 % (2964159)------------------------------ % 29.37/5.33 % (2964159)------------------------------ % 29.37/5.33 % (2964175)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4175634280:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi) % 29.37/5.33 % (2964176)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=2000787884:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi) % 31.89/5.70 % (2964175)Refutation not found, incomplete strategy % 31.89/5.70 % (2964175)------------------------------ % 31.89/5.70 % (2964175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/5.70 % (2964175)CaDiCaL version: 2.1.3 % 31.89/5.70 % (2964175)Termination reason: Refutation not found, incomplete strategy % 31.89/5.70 % (2964175)Time elapsed: 0.024 s % 31.89/5.70 % (2964175)Peak memory usage: 91 MB % 31.89/5.70 % (2964175)Instructions burned: 34 (million) % 31.89/5.70 % (2964172)------------------------------ % 31.89/5.70 % (2964172)------------------------------ % 31.89/5.70 % (2964148)Instruction limit reached! % 31.89/5.70 % (2964148)------------------------------ % 31.89/5.70 % (2964148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/5.70 % (2964148)CaDiCaL version: 2.1.3 % 31.89/5.70 % (2964148)Termination reason: Instruction limit % 31.89/5.70 % (2964148)Termination phase: Saturation % 31.89/5.70 % (2964148)Time elapsed: 1.481 s % 31.89/5.70 % (2964148)Peak memory usage: 215 MB % 31.89/5.70 % (2964148)Instructions burned: 2351 (million) % 31.89/5.70 % (2964177)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=3924649052:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi) % 31.89/5.70 % (2964177)Instruction limit reached! % 31.89/5.70 % (2964177)------------------------------ % 31.89/5.70 % (2964177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/5.70 % (2964177)CaDiCaL version: 2.1.3 % 31.89/5.70 % (2964177)Termination reason: Instruction limit % 31.89/5.70 % (2964177)Termination phase: Clausification % 31.89/5.70 % (2964177)Time elapsed: 0.095 s % 31.89/5.70 % (2964177)Peak memory usage: 94 MB % 31.89/5.70 % (2964177)Instructions burned: 151 (million) % 31.89/5.70 % (2964180)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2297187150:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi) % 31.89/5.70 % (2964175)------------------------------ % 31.89/5.70 % (2964175)------------------------------ % 31.89/5.70 % (2964182)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2271964964:i=667:av=off:fsr=off_2973 on theBenchmark for (2973ds/667Mi) % 31.89/5.70 % (2964183)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=1922651709:s2a=on:i=185:s2at=1.8:fdi=4_2972 on theBenchmark for (2972ds/185Mi) % 31.89/5.70 % (2964186)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1042795902:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/193Mi) % 31.89/5.70 % (2964186)Refutation not found, incomplete strategy % 31.89/5.70 % (2964186)------------------------------ % 31.89/5.70 % (2964186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/5.70 % (2964186)CaDiCaL version: 2.1.3 % 31.89/5.70 % (2964186)Termination reason: Refutation not found, incomplete strategy % 31.89/5.70 % (2964186)Time elapsed: 0.044 s % 31.89/5.70 % (2964186)Peak memory usage: 91 MB % 31.89/5.70 % (2964186)Instructions burned: 71 (million) % 31.89/5.70 % (2964183)Instruction limit reached! % 31.89/5.70 % (2964183)------------------------------ % 31.89/5.70 % (2964183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.89/5.70 % (2964183)CaDiCaL version: 2.1.3 % 31.89/5.70 % (2964183)Termination reason: Instruction limit % 31.89/5.70 % (2964183)Termination phase: Property scanning % 31.89/5.70 % (2964183)Time elapsed: 0.110 s % 31.89/5.70 % (2964183)Peak memory usage: 95 MB % 31.89/5.70 % (2964183)Instructions burned: 187 (million) % 31.89/5.70 % (2964182)Instruction limit reached! % 31.89/5.70 % (2964182)------------------------------ % 31.89/5.70 % (2964182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.89/5.70 % (2964182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964182)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964182)Termination reason: Instruction limit % 39.20/6.76 % (2964182)Termination phase: Saturation % 39.20/6.76 % (2964182)Time elapsed: 0.324 s % 39.20/6.76 % (2964182)Peak memory usage: 101 MB % 39.20/6.76 % (2964182)Instructions burned: 667 (million) % 39.20/6.76 % (2964189)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1178375214:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2970 on theBenchmark for (2970ds/4850Mi) % 39.20/6.76 % (2964186)------------------------------ % 39.20/6.76 % (2964186)------------------------------ % 39.20/6.76 % (2964191)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=951731210:i=12111:sd=1:ss=included_2968 on theBenchmark for (2968ds/12111Mi) % 39.20/6.76 % (2964192)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2628266600:i=319:kws=precedence:fsr=off_2967 on theBenchmark for (2967ds/319Mi) % 39.20/6.76 % (2964189)Refutation not found, incomplete strategy % 39.20/6.76 % (2964189)------------------------------ % 39.20/6.76 % (2964189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.20/6.76 % (2964189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964189)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964189)Termination reason: Refutation not found, incomplete strategy % 39.20/6.76 % (2964189)Time elapsed: 0.324 s % 39.20/6.76 % (2964189)Peak memory usage: 102 MB % 39.20/6.76 % (2964189)Instructions burned: 662 (million) % 39.20/6.76 % (2964192)Instruction limit reached! % 39.20/6.76 % (2964192)------------------------------ % 39.20/6.76 % (2964192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.20/6.76 % (2964192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964192)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964192)Termination reason: Instruction limit % 39.20/6.76 % (2964192)Termination phase: Property scanning % 39.20/6.76 % (2964192)Time elapsed: 0.150 s % 39.20/6.76 % (2964192)Peak memory usage: 96 MB % 39.20/6.76 % (2964192)Instructions burned: 319 (million) % 39.20/6.76 % (2964195)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=603164817:i=2064:ep=RST_2964 on theBenchmark for (2964ds/2064Mi) % 39.20/6.76 % (2964189)------------------------------ % 39.20/6.76 % (2964189)------------------------------ % 39.20/6.76 % (2964197)dis-1011_128_sil=32000:random_seed=2866665416:i=3706:ep=RST:av=off_2962 on theBenchmark for (2962ds/3706Mi) % 39.20/6.76 % (2964195)Refutation not found, incomplete strategy % 39.20/6.76 % (2964195)------------------------------ % 39.20/6.76 % (2964195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.20/6.76 % (2964195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964195)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964195)Termination reason: Refutation not found, incomplete strategy % 39.20/6.76 % (2964195)Time elapsed: 0.380 s % 39.20/6.76 % (2964195)Peak memory usage: 104 MB % 39.20/6.76 % (2964195)Instructions burned: 807 (million) % 39.20/6.76 % (2964195)------------------------------ % 39.20/6.76 % (2964195)------------------------------ % 39.20/6.76 % (2964199)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2341147943:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2957 on theBenchmark for (2957ds/757Mi) % 39.20/6.76 % (2964199)Refutation not found, incomplete strategy % 39.20/6.76 % (2964199)------------------------------ % 39.20/6.76 % (2964199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.20/6.76 % (2964199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964199)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964199)Termination reason: Refutation not found, incomplete strategy % 39.20/6.76 % (2964199)Time elapsed: 0.024 s % 39.20/6.76 % (2964199)Peak memory usage: 92 MB % 39.20/6.76 % (2964199)Instructions burned: 34 (million) % 39.20/6.76 % (2964176)Instruction limit reached! % 39.20/6.76 % (2964176)------------------------------ % 39.20/6.76 % (2964176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.20/6.76 % (2964176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.20/6.76 % (2964176)CaDiCaL version: 2.1.3 % 39.20/6.76 % (2964176)Termination reason: Instruction limit % 39.20/6.76 % (2964176)Termination phase: Saturation % 39.20/6.76 % (2964176)Time elapsed: 1.918 s % 39.20/6.76 % (2964176)Peak memory usage: 230 MB % 39.20/6.76 % (2964176)Instructions burned: 6062 (million) % 43.46/7.33 % (2964201)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1782069781:i=13913:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/13913Mi) % 43.46/7.33 % (2964199)------------------------------ % 43.46/7.33 % (2964199)------------------------------ % 43.46/7.33 [W927 21:39:56.746864672 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746885848 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746907451 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746916854 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746930837 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746937201 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746951281 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746957613 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746970596 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746976936 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746989882 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 [W927 21:39:56.746996213 register_special_ops.cpp:225] Warning: Creating a tensor from 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.46/7.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.46/7.33 % (2964203)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2405782930:i=9925:aac=none_2952 on theBenchmark for (2952ds/9925Mi) % 73.24/11.51 % (2964201)Refutation not found, incomplete strategy % 73.24/11.51 % (2964201)------------------------------ % 73.24/11.51 % (2964201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.24/11.51 % (2964201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.24/11.51 % (2964201)CaDiCaL version: 2.1.3 % 73.24/11.51 % (2964201)Termination reason: Refutation not found, incomplete strategy % 73.24/11.51 % (2964201)Time elapsed: 0.358 s % 73.24/11.51 % (2964201)Peak memory usage: 135 MB % 73.24/11.51 % (2964201)Instructions burned: 923 (million) % 73.24/11.51 % (2964201)------------------------------ % 73.24/11.51 % (2964201)------------------------------ % 73.24/11.51 % (2964205)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2922815621:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2949 on theBenchmark for (2949ds/2479Mi) % 73.24/11.51 % (2964205)Refutation not found, incomplete strategy % 73.24/11.51 % (2964205)------------------------------ % 73.24/11.51 % (2964205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.24/11.51 % (2964205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.24/11.51 % (2964205)CaDiCaL version: 2.1.3 % 73.24/11.51 % (2964205)Termination reason: Refutation not found, incomplete strategy % 73.24/11.51 % (2964205)Time elapsed: 0.023 s % 73.24/11.51 % (2964205)Peak memory usage: 92 MB % 73.24/11.51 % (2964205)Instructions burned: 71 (million) % 73.24/11.51 % (2964205)------------------------------ % 73.24/11.51 % (2964205)------------------------------ % 73.24/11.51 % (2964207)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1664927897:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2946 on theBenchmark for (2946ds/440Mi) % 73.24/11.51 % (2964207)Instruction limit reached! % 73.24/11.51 % (2964207)------------------------------ % 73.24/11.51 % (2964207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.24/11.51 % (2964207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.24/11.51 % (2964207)CaDiCaL version: 2.1.3 % 73.24/11.51 % (2964207)Termination reason: Instruction limit % 73.24/11.51 % (2964207)Termination phase: Property scanning % 73.24/11.51 % (2964207)Time elapsed: 0.106 s % 73.24/11.51 % (2964207)Peak memory usage: 96 MB % 73.24/11.51 % (2964207)Instructions burned: 443 (million) % 73.24/11.51 % (2964209)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2489783925:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2944 on theBenchmark for (2944ds/11145Mi) % 73.24/11.51 [W927 21:39:57.839087654 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/11.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.24/11.51 [W927 21:39:57.839116398 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/11.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.24/11.51 [W927 21:39:57.839138863 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/11.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.24/11.51 [W927 21:39:57.839145166 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/11.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.24/11.51 [W927 21:39:57.839158344 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/11.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.24/11.51 [W927 21:39:57.839164106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839177114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839192067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839204630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839210250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839222905 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 [W927 21:39:57.839228842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.28/11.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.28/11.76 % (2964209)Refutation not found, incomplete strategy % 74.28/11.76 % (2964209)------------------------------ % 74.28/11.76 % (2964209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.28/11.76 % (2964209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.28/11.76 % (2964209)CaDiCaL version: 2.1.3 % 74.28/11.76 % (2964209)Termination reason: Refutation not found, incomplete strategy % 74.28/11.76 % (2964209)Time elapsed: 0.363 s % 74.28/11.76 % (2964209)Peak memory usage: 132 MB % 74.28/11.76 % (2964209)Instructions burned: 959 (million) % 74.28/11.76 % (2964197)Instruction limit reached! % 74.28/11.76 % (2964197)------------------------------ % 74.28/11.76 % (2964197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.28/11.76 % (2964197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.28/11.76 % (2964197)CaDiCaL version: 2.1.3 % 74.28/11.76 % (2964197)Termination reason: Instruction limit % 74.28/11.76 % (2964197)Termination phase: Saturation % 74.28/11.76 % (2964197)Time elapsed: 2.239 s % 74.28/11.76 % (2964197)Peak memory usage: 138 MB % 74.28/11.76 % (2964197)Instructions burned: 3706 (million) % 74.28/11.76 % (2964209)------------------------------ % 74.28/11.76 % (2964209)------------------------------ % 74.28/11.76 % (2964211)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=538592296:cts=off:i=3034:av=off:er=known:fsd=on_2939 on theBenchmark for (2939ds/3034Mi) % 74.28/11.76 % (2964212)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1072313351:st=2:s2a=on:i=524:s2at=2:ss=axioms_2938 on theBenchmark for (2938ds/524Mi) % 74.28/11.76 % (2964212)Refutation not found, incomplete strategy % 74.28/11.76 % (2964212)------------------------------ % 74.28/11.76 % (2964212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.28/11.76 % (2964212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.28/11.76 % (2964212)CaDiCaL version: 2.1.3 % 74.28/11.76 % (2964212)Termination reason: Refutation not found, incomplete strategy % 74.28/11.76 % (2964212)Time elapsed: 0.032 s % 74.28/11.76 % (2964212)Peak memory usage: 92 MB % 74.28/11.76 % (2964212)Instructions burned: 107 (million) % 74.28/11.76 % (2964212)------------------------------ % 78.03/12.14 % (2964212)------------------------------ % 78.03/12.14 % (2964203)Refutation not found, incomplete strategy % 78.03/12.14 % (2964203)------------------------------ % 78.03/12.14 % (2964203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.03/12.14 % (2964203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.03/12.14 % (2964203)CaDiCaL version: 2.1.3 % 78.03/12.14 % (2964203)Termination reason: Refutation not found, incomplete strategy % 78.03/12.14 % (2964203)Time elapsed: 1.698 s % 78.03/12.14 % (2964203)Peak memory usage: 213 MB % 78.03/12.14 % (2964203)Instructions burned: 2768 (million) % 78.03/12.14 % (2964215)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=470664571:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2935 on theBenchmark for (2935ds/1016Mi) % 78.03/12.14 % (2964215)Refutation not found, incomplete strategy % 78.03/12.14 % (2964215)------------------------------ % 78.03/12.14 % (2964215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.03/12.14 % (2964215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.03/12.14 % (2964215)CaDiCaL version: 2.1.3 % 78.03/12.14 % (2964215)Termination reason: Refutation not found, incomplete strategy % 78.03/12.14 % (2964215)Time elapsed: 0.014 s % 78.03/12.14 % (2964215)Peak memory usage: 92 MB % 78.03/12.14 % (2964215)Instructions burned: 35 (million) % 78.03/12.14 % (2964215)------------------------------ % 78.03/12.14 % (2964215)------------------------------ % 78.03/12.14 % (2964203)------------------------------ % 78.03/12.14 % (2964203)------------------------------ % 78.03/12.14 % (2964217)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2516754223:i=14123:bd=preordered:ins=4_2932 on theBenchmark for (2932ds/14123Mi) % 78.03/12.14 % (2964219)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=447842400:i=5781:kws=precedence:bd=all:rawr=on_2931 on theBenchmark for (2931ds/5781Mi) % 78.03/12.14 % (2964211)Instruction limit reached! % 78.03/12.14 % (2964211)------------------------------ % 78.03/12.14 % (2964211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.03/12.14 % (2964211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.03/12.14 % (2964211)CaDiCaL version: 2.1.3 % 78.03/12.14 % (2964211)Termination reason: Instruction limit % 78.03/12.14 % (2964211)Termination phase: Saturation % 78.03/12.14 % (2964211)Time elapsed: 1.819 s % 78.03/12.14 % (2964211)Peak memory usage: 211 MB % 78.03/12.14 % (2964211)Instructions burned: 3036 (million) % 78.03/12.14 % (2964221)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=389916983:i=2448:gtgl=5:bd=preordered:gtg=all_2919 on theBenchmark for (2919ds/2448Mi) % 78.03/12.14 % (2964221)Instruction limit reached! % 78.03/12.14 % (2964221)------------------------------ % 78.03/12.14 % (2964221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.03/12.14 % (2964221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.03/12.14 % (2964221)CaDiCaL version: 2.1.3 % 78.03/12.14 % (2964221)Termination reason: Instruction limit % 78.03/12.14 % (2964221)Termination phase: Saturation % 78.03/12.14 % (2964221)Time elapsed: 1.389 s % 78.03/12.14 % (2964221)Peak memory usage: 173 MB % 78.03/12.14 % (2964221)Instructions burned: 2449 (million) % 78.03/12.14 % (2964223)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2344128487:i=3223:kws=precedence:fgj=on:av=off_2904 on theBenchmark for (2904ds/3223Mi) % 78.03/12.14 % (2964191)Instruction limit reached! % 78.03/12.14 % (2964191)------------------------------ % 78.03/12.14 % (2964191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.03/12.14 % (2964191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.03/12.14 % (2964191)CaDiCaL version: 2.1.3 % 78.03/12.14 % (2964191)Termination reason: Instruction limit % 78.03/12.14 % (2964191)Termination phase: Saturation % 78.03/12.14 % (2964191)Time elapsed: 7.039 s % 78.03/12.14 % (2964191)Peak memory usage: 248 MB % 78.03/12.14 % (2964191)Instructions burned: 12112 (million) % 78.03/12.14 % (2964225)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=63232544:st=5.6:i=2033:sd=3:ss=axioms_2896 on theBenchmark for (2896ds/2033Mi) % 78.03/12.14 % (2964219)Instruction limit reached! % 78.03/12.14 % (2964219)------------------------------ % 78.03/12.14 % (2964219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.08/12.72 % (2964219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.08/12.72 % (2964219)CaDiCaL version: 2.1.3 % 81.08/12.72 % (2964219)Termination reason: Instruction limit % 81.08/12.72 % (2964219)Termination phase: Saturation % 81.08/12.72 % (2964219)Time elapsed: 3.679 s % 81.08/12.72 % (2964219)Peak memory usage: 134 MB % 81.08/12.72 % (2964219)Instructions burned: 5781 (million) % 81.08/12.72 % (2964227)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3673477511:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2893 on theBenchmark for (2893ds/2055Mi) % 81.08/12.72 [W927 21:40:02.846413127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846457391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846497614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846508501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846534208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846544361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846569395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846579685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846603982 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846618098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846642392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.08/12.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.08/12.72 [W927 21:40:02.846652762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 % (2964225)Refutation not found, incomplete strategy % 81.87/12.95 % (2964225)------------------------------ % 81.87/12.95 % (2964225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.87/12.95 % (2964225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.87/12.95 % (2964225)CaDiCaL version: 2.1.3 % 81.87/12.95 % (2964225)Termination reason: Refutation not found, incomplete strategy % 81.87/12.95 % (2964225)Time elapsed: 0.623 s % 81.87/12.95 % (2964225)Peak memory usage: 135 MB % 81.87/12.95 % (2964225)Instructions burned: 941 (million) % 81.87/12.95 [W927 21:40:03.226188518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226221705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226260352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226273169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226300119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226321696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226353199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226364026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226388633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226404213 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.87/12.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.87/12.95 [W927 21:40:03.226429076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.24/13.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.24/13.77 [W927 21:40:03.226439643 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.24/13.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.24/13.77 % (2964225)------------------------------ % 88.24/13.77 % (2964225)------------------------------ % 88.24/13.77 % (2964229)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=4145496410:i=21611:sd=3:ss=axioms_2886 on theBenchmark for (2886ds/21611Mi) % 88.24/13.77 % (2964227)Refutation not found, incomplete strategy % 88.24/13.77 % (2964227)------------------------------ % 88.24/13.77 % (2964227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.24/13.77 % (2964227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.24/13.77 % (2964227)CaDiCaL version: 2.1.3 % 88.24/13.77 % (2964227)Termination reason: Refutation not found, incomplete strategy % 88.24/13.77 % (2964227)Time elapsed: 0.667 s % 88.24/13.77 % (2964227)Peak memory usage: 136 MB % 88.24/13.77 % (2964227)Instructions burned: 1045 (million) % 88.24/13.77 % (2964223)Instruction limit reached! % 88.24/13.77 % (2964223)------------------------------ % 88.24/13.77 % (2964223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.24/13.77 % (2964223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.24/13.77 % (2964223)CaDiCaL version: 2.1.3 % 88.24/13.77 % (2964223)Termination reason: Instruction limit % 88.24/13.77 % (2964223)Termination phase: Saturation % 88.24/13.77 % (2964223)Time elapsed: 1.884 s % 88.24/13.77 % (2964223)Peak memory usage: 215 MB % 88.24/13.77 % (2964223)Instructions burned: 3226 (million) % 88.24/13.77 % (2964227)------------------------------ % 88.24/13.77 % (2964227)------------------------------ % 88.24/13.77 % (2964180)Instruction limit reached! % 88.24/13.77 % (2964180)------------------------------ % 88.24/13.77 % (2964180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.24/13.77 % (2964180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.24/13.77 % (2964180)CaDiCaL version: 2.1.3 % 88.24/13.77 % (2964180)Termination reason: Instruction limit % 88.24/13.77 % (2964180)Termination phase: Saturation % 88.24/13.77 % (2964180)Time elapsed: 8.948 s % 88.24/13.77 % (2964180)Peak memory usage: 220 MB % 88.24/13.77 % (2964180)Instructions burned: 14156 (million) % 88.24/13.77 % (2964217)Instruction limit reached! % 88.24/13.77 % (2964217)------------------------------ % 88.24/13.77 % (2964217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.24/13.77 % (2964217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.24/13.77 % (2964217)CaDiCaL version: 2.1.3 % 88.24/13.77 % (2964217)Termination reason: Instruction limit % 88.24/13.77 % (2964217)Termination phase: Saturation % 88.24/13.77 % (2964217)Time elapsed: 4.888 s % 88.24/13.77 % (2964217)Peak memory usage: 236 MB % 88.24/13.77 % (2964217)Instructions burned: 14123 (million) % 88.24/13.77 % (2964231)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=107840072:i=4835:sd=13:ss=axioms:sgt=23_2883 on theBenchmark for (2883ds/4835Mi) % 88.24/13.77 % (2964231)Refutation not found, incomplete strategy % 88.24/13.77 % (2964231)------------------------------ % 88.24/13.77 % (2964231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.24/13.77 % (2964231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.24/13.77 % (2964231)CaDiCaL version: 2.1.3 % 88.24/13.77 % (2964231)Termination reason: Refutation not found, incomplete strategy % 88.24/13.77 % (2964231)Time elapsed: 0.024 s % 88.24/13.77 % (2964231)Peak memory usage: 92 MB % 88.24/13.77 % (2964231)Instructions burned: 34 (million) % 88.24/13.77 % (2964233)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4085642396:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2882 on theBenchmark for (2882ds/2326Mi) % 88.24/13.77 % (2964232)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=3318926584:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2882 on theBenchmark for (2882ds/797Mi) % 88.24/13.77 % (2964234)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=169028855:i=6038:nm=6_2882 on theBenchmark for (2882ds/6038Mi) % 98.59/15.04 [W927 21:40:03.842908903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.842950703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.842997240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843021104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843049734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843061228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843087891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843099141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843125905 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843137325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843162455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 [W927 21:40:03.843173778 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.59/15.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.59/15.04 % (2964231)------------------------------ % 98.59/15.04 % (2964231)------------------------------ % 98.59/15.04 % (2964229)Refutation not found, incomplete strategy % 98.59/15.04 % (2964229)------------------------------ % 98.59/15.04 % (2964229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964229)CaDiCaL version: 2.1.3 % 107.98/16.43 % (2964229)Termination reason: Refutation not found, incomplete strategy % 107.98/16.43 % (2964229)Time elapsed: 0.618 s % 107.98/16.43 % (2964229)Peak memory usage: 134 MB % 107.98/16.43 % (2964229)Instructions burned: 925 (million) % 107.98/16.43 % (2964239)lrs+10_1_sil=32000:sp=occurrence:random_seed=1978213830:st=2:i=33334:sd=3:ss=included:sgt=32_2879 on theBenchmark for (2879ds/33334Mi) % 107.98/16.43 % (2964232)Instruction limit reached! % 107.98/16.43 % (2964232)------------------------------ % 107.98/16.43 % (2964232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964232)CaDiCaL version: 2.1.3 % 107.98/16.43 % (2964232)Termination reason: Instruction limit % 107.98/16.43 % (2964232)Termination phase: Saturation % 107.98/16.43 % (2964232)Time elapsed: 0.400 s % 107.98/16.43 % (2964232)Peak memory usage: 100 MB % 107.98/16.43 % (2964232)Instructions burned: 798 (million) % 107.98/16.43 % (2964229)------------------------------ % 107.98/16.43 % (2964229)------------------------------ % 107.98/16.43 % (2964233)Refutation not found, incomplete strategy % 107.98/16.43 % (2964233)------------------------------ % 107.98/16.43 % (2964233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964233)CaDiCaL version: 2.1.3 % 107.98/16.43 % (2964233)Termination reason: Refutation not found, incomplete strategy % 107.98/16.43 % (2964233)Time elapsed: 0.561 s % 107.98/16.43 % (2964233)Peak memory usage: 112 MB % 107.98/16.43 % (2964233)Instructions burned: 1754 (million) % 107.98/16.43 % (2964241)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1372436199:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2877 on theBenchmark for (2877ds/1008Mi) % 107.98/16.43 % (2964241)Refutation not found, incomplete strategy % 107.98/16.43 % (2964241)------------------------------ % 107.98/16.43 % (2964241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964241)CaDiCaL version: 2.1.3 % 107.98/16.43 % (2964241)Termination reason: Refutation not found, incomplete strategy % 107.98/16.43 % (2964241)Time elapsed: 0.062 s % 107.98/16.43 % (2964241)Peak memory usage: 92 MB % 107.98/16.43 % (2964241)Instructions burned: 105 (million) % 107.98/16.43 % (2964242)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=1193273611:i=8327:s2at=5:bd=preordered_2876 on theBenchmark for (2876ds/8327Mi) % 107.98/16.43 % (2964233)------------------------------ % 107.98/16.43 % (2964233)------------------------------ % 107.98/16.43 % (2964245)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=2810293009:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2874 on theBenchmark for (2874ds/1083Mi) % 107.98/16.43 % (2964241)------------------------------ % 107.98/16.43 % (2964241)------------------------------ % 107.98/16.43 % (2964247)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2602068885:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2872 on theBenchmark for (2872ds/1084Mi) % 107.98/16.43 % (2964247)Refutation not found, incomplete strategy % 107.98/16.43 % (2964247)------------------------------ % 107.98/16.43 % (2964247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964247)CaDiCaL version: 2.1.3 % 107.98/16.43 % (2964247)Termination reason: Refutation not found, incomplete strategy % 107.98/16.43 % (2964247)Time elapsed: 0.024 s % 107.98/16.43 % (2964247)Peak memory usage: 91 MB % 107.98/16.43 % (2964247)Instructions burned: 35 (million) % 107.98/16.43 % (2964245)Instruction limit reached! % 107.98/16.43 % (2964245)------------------------------ % 107.98/16.43 % (2964245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.98/16.43 % (2964245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.98/16.43 % (2964245)CaDiCaL version: 2.1.3 % 108.59/16.58 % (2964245)Termination reason: Instruction limit % 108.59/16.58 % (2964245)Termination phase: Saturation % 108.59/16.58 % (2964245)Time elapsed: 0.267 s % 108.59/16.58 % (2964245)Peak memory usage: 102 MB % 108.59/16.58 % (2964245)Instructions burned: 1085 (million) % 108.59/16.58 % (2964249)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4128479790:i=6995:s2at=5:gtg=all_2870 on theBenchmark for (2870ds/6995Mi) % 108.59/16.58 % (2964247)------------------------------ % 108.59/16.58 % (2964247)------------------------------ % 108.59/16.58 % (2964251)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=396362494:st=2:i=6225:sd=15:ss=axioms_2868 on theBenchmark for (2868ds/6225Mi) % 108.59/16.58 % (2964251)Refutation not found, incomplete strategy % 108.59/16.58 % (2964251)------------------------------ % 108.59/16.58 % (2964251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.59/16.58 % (2964251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.59/16.58 % (2964251)CaDiCaL version: 2.1.3 % 108.59/16.58 % (2964251)Termination reason: Refutation not found, incomplete strategy % 108.59/16.58 % (2964251)Time elapsed: 0.031 s % 108.59/16.58 % (2964251)Peak memory usage: 92 MB % 108.59/16.58 % (2964251)Instructions burned: 52 (million) % 108.59/16.58 % (2964251)------------------------------ % 108.59/16.58 % (2964251)------------------------------ % 108.59/16.58 % (2964234)Refutation not found, incomplete strategy % 108.59/16.58 % (2964234)------------------------------ % 108.59/16.58 % (2964234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.59/16.58 % (2964234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.59/16.58 % (2964234)CaDiCaL version: 2.1.3 % 108.59/16.58 % (2964234)Termination reason: Refutation not found, incomplete strategy % 108.59/16.58 % (2964234)Time elapsed: 1.745 s % 108.59/16.58 % (2964234)Peak memory usage: 222 MB % 108.59/16.58 % (2964234)Instructions burned: 2790 (million) % 108.59/16.58 % (2964253)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1114290818:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2864 on theBenchmark for (2864ds/3372Mi) % 108.59/16.58 % (2964234)------------------------------ % 108.59/16.58 % (2964234)------------------------------ % 108.59/16.58 % (2964255)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1436405948:st=2.3:i=26457:sd=10:ss=included:sgt=8_2860 on theBenchmark for (2860ds/26457Mi) % 108.59/16.58 [W927 21:40:06.119559099 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.59/16.58 [W927 21:40:06.119603253 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.59/16.58 [W927 21:40:06.119642870 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.59/16.58 [W927 21:40:06.119654000 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.59/16.58 [W927 21:40:06.119682093 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.59/16.58 [W927 21:40:06.119692827 register_special_ops.cpp:225] Warning: Creating a tensor from 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.59/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119719340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119730317 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119756857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119767754 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119794144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:06.119804891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 % (2964253)Refutation not found, incomplete strategy % 111.62/17.02 % (2964253)------------------------------ % 111.62/17.02 % (2964253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.62/17.02 % (2964253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.62/17.02 % (2964253)CaDiCaL version: 2.1.3 % 111.62/17.02 % (2964253)Termination reason: Refutation not found, incomplete strategy % 111.62/17.02 % (2964253)Time elapsed: 0.662 s % 111.62/17.02 % (2964253)Peak memory usage: 136 MB % 111.62/17.02 % (2964253)Instructions burned: 1044 (million) % 111.62/17.02 % (2964253)------------------------------ % 111.62/17.02 % (2964253)------------------------------ % 111.62/17.02 % (2964257)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=955528619:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2853 on theBenchmark for (2853ds/13494Mi) % 111.62/17.02 % (2964249)Instruction limit reached! % 111.62/17.02 % (2964249)------------------------------ % 111.62/17.02 % (2964249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.62/17.02 % (2964249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.62/17.02 % (2964249)CaDiCaL version: 2.1.3 % 111.62/17.02 % (2964249)Termination reason: Instruction limit % 111.62/17.02 % (2964249)Termination phase: Saturation % 111.62/17.02 % (2964249)Time elapsed: 2.235 s % 111.62/17.02 % (2964249)Peak memory usage: 208 MB % 111.62/17.02 % (2964249)Instructions burned: 6995 (million) % 111.62/17.02 % (2964259)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=523378234:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2847 on theBenchmark for (2847ds/2503Mi) % 111.62/17.02 [W927 21:40:07.510190497 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.62/17.02 [W927 21:40:07.510212846 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.62/17.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510233880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510245186 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510258179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510263662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510276708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510282062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510295216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510300779 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510313659 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 [W927 21:40:07.510319144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.33/20.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.33/20.78 % (2964259)Refutation not found, incomplete strategy % 138.33/20.78 % (2964259)------------------------------ % 138.33/20.78 % (2964259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.33/20.78 % (2964259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.33/20.78 % (2964259)CaDiCaL version: 2.1.3 % 138.33/20.78 % (2964259)Termination reason: Refutation not found, incomplete strategy % 138.33/20.78 % (2964259)Time elapsed: 0.335 s % 138.33/20.78 % (2964259)Peak memory usage: 135 MB % 138.33/20.78 % (2964259)Instructions burned: 926 (million) % 138.33/20.78 % (2964255)Refutation not found, incomplete strategy % 138.33/20.78 % (2964255)------------------------------ % 138.33/20.78 % (2964255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.33/20.78 % (2964255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.33/20.78 % (2964255)CaDiCaL version: 2.1.3 % 138.33/20.78 % (2964255)Termination reason: Refutation not found, incomplete strategy % 145.42/21.78 % (2964255)Time elapsed: 1.678 s % 145.42/21.78 % (2964255)Peak memory usage: 213 MB % 145.42/21.78 % (2964255)Instructions burned: 2801 (million) % 145.42/21.78 % (2964259)------------------------------ % 145.42/21.78 % (2964259)------------------------------ % 145.42/21.78 % (2964261)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1407894282:i=2559:sd=1:ep=RSTC:ss=axioms_2841 on theBenchmark for (2841ds/2559Mi) % 145.42/21.78 % (2964255)------------------------------ % 145.42/21.78 % (2964255)------------------------------ % 145.42/21.78 % (2964263)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1965604752:i=30753:av=off:ss=included_2839 on theBenchmark for (2839ds/30753Mi) % 145.42/21.78 [W927 21:40:07.103777282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103840721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103875573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103893076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103917446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103933698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103957338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103973121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.103996679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.104021195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.104046773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.42/21.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.42/21.78 [W927 21:40:07.104070320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.50/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.50/22.78 % (2964261)Refutation not found, incomplete strategy % 152.50/22.78 % (2964261)------------------------------ % 152.50/22.78 % (2964261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.50/22.78 % (2964261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.50/22.78 % (2964261)CaDiCaL version: 2.1.3 % 152.50/22.78 % (2964261)Termination reason: Refutation not found, incomplete strategy % 152.50/22.78 % (2964261)Time elapsed: 0.357 s % 152.50/22.78 % (2964261)Peak memory usage: 133 MB % 152.50/22.78 % (2964261)Instructions burned: 925 (million) % 152.50/22.78 % (2964261)------------------------------ % 152.50/22.78 % (2964261)------------------------------ % 152.50/22.78 % (2964265)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1173921505:i=26473:ep=RSTC_2835 on theBenchmark for (2835ds/26473Mi) % 152.50/22.78 % (2964242)Instruction limit reached! % 152.50/22.78 % (2964242)------------------------------ % 152.50/22.78 % (2964242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.50/22.78 % (2964242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.50/22.78 % (2964242)CaDiCaL version: 2.1.3 % 152.50/22.78 % (2964242)Termination reason: Instruction limit % 152.50/22.78 % (2964242)Termination phase: Saturation % 152.50/22.78 % (2964242)Time elapsed: 5.053 s % 152.50/22.78 % (2964242)Peak memory usage: 222 MB % 152.50/22.78 % (2964242)Instructions burned: 8328 (million) % 152.50/22.78 % (2964267)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=1900889127:cts=off:i=2759:kws=inv_arity:fgj=on_2824 on theBenchmark for (2824ds/2759Mi) % 152.50/22.78 % (2964267)Instruction limit reached! % 152.50/22.78 % (2964267)------------------------------ % 152.50/22.78 % (2964267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.50/22.78 % (2964267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.50/22.78 % (2964267)CaDiCaL version: 2.1.3 % 152.50/22.78 % (2964267)Termination reason: Instruction limit % 152.50/22.78 % (2964267)Termination phase: Saturation % 152.50/22.78 % (2964267)Time elapsed: 1.647 s % 152.50/22.78 % (2964267)Peak memory usage: 172 MB % 152.50/22.78 % (2964267)Instructions burned: 2760 (million) % 152.50/22.78 % (2964269)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=507836047:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2806 on theBenchmark for (2806ds/5665Mi) % 152.50/22.78 [W927 21:40:11.865349113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.50/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.50/22.78 [W927 21:40:11.865391740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.50/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.50/22.78 [W927 21:40:11.865433860 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.50/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.50/22.78 [W927 21:40:11.865445444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.50/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.50/22.78 [W927 21:40:11.865472027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865484481 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865520854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865531861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865555588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865566364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865590715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:11.865601558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 % (2964269)Refutation not found, incomplete strategy % 157.17/23.34 % (2964269)------------------------------ % 157.17/23.34 % (2964269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.17/23.34 % (2964269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.17/23.34 % (2964269)CaDiCaL version: 2.1.3 % 157.17/23.34 % (2964269)Termination reason: Refutation not found, incomplete strategy % 157.17/23.34 % (2964269)Time elapsed: 0.621 s % 157.17/23.34 % (2964269)Peak memory usage: 135 MB % 157.17/23.34 % (2964269)Instructions burned: 944 (million) % 157.17/23.34 % (2964269)------------------------------ % 157.17/23.34 % (2964269)------------------------------ % 157.17/23.34 % (2964271)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=1212730168:i=1532:ep=RS:ss=axioms_2796 on theBenchmark for (2796ds/1532Mi) % 157.17/23.34 [W927 21:40:12.859458033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:12.859500213 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:12.859538814 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.17/23.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.17/23.34 [W927 21:40:12.859550470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859575407 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859586131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859610391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859620987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859644748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859654734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859678571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:12.859689221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 % (2964271)Refutation not found, incomplete strategy % 160.28/23.92 % (2964271)------------------------------ % 160.28/23.92 % (2964271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.28/23.92 % (2964271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.28/23.92 % (2964271)CaDiCaL version: 2.1.3 % 160.28/23.92 % (2964271)Termination reason: Refutation not found, incomplete strategy % 160.28/23.92 % (2964271)Time elapsed: 0.608 s % 160.28/23.92 % (2964271)Peak memory usage: 135 MB % 160.28/23.92 % (2964271)Instructions burned: 926 (million) % 160.28/23.92 % (2964271)------------------------------ % 160.28/23.92 % (2964271)------------------------------ % 160.28/23.92 % (2964273)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3905855059:i=1565:sd=2:ss=axioms:sgt=32_2786 on theBenchmark for (2786ds/1565Mi) % 160.28/23.92 [W927 21:40:13.868132531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.28/23.92 [W927 21:40:13.868164451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.28/23.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868203368 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868214728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868239411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868249701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868274492 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868284738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868308582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868318802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868342945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 [W927 21:40:13.868353119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 167.49/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 167.49/24.96 % (2964273)Refutation not found, incomplete strategy % 167.49/24.96 % (2964273)------------------------------ % 167.49/24.96 % (2964273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.49/24.96 % (2964273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.49/24.96 % (2964273)CaDiCaL version: 2.1.3 % 167.49/24.96 % (2964273)Termination reason: Refutation not found, incomplete strategy % 167.49/24.96 % (2964273)Time elapsed: 0.616 s % 167.49/24.96 % (2964273)Peak memory usage: 135 MB % 167.49/24.96 % (2964273)Instructions burned: 926 (million) % 167.49/24.96 % (2964273)------------------------------ % 167.49/24.96 % (2964273)------------------------------ % 167.49/24.96 % (2964257)Instruction limit reached! % 167.49/24.96 % (2964257)------------------------------ % 167.49/24.96 % (2964257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.49/24.96 % (2964257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.49/24.96 % (2964257)CaDiCaL version: 2.1.3 % 177.35/26.14 % (2964257)Termination reason: Instruction limit % 177.35/26.14 % (2964257)Termination phase: Saturation % 177.35/26.14 % (2964257)Time elapsed: 7.752 s % 177.35/26.14 % (2964257)Peak memory usage: 236 MB % 177.35/26.14 % (2964257)Instructions burned: 13494 (million) % 177.35/26.14 % (2964275)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=1854985688:i=1572:fgj=on:gsp=on_2776 on theBenchmark for (2776ds/1572Mi) % 177.35/26.14 % (2964276)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=842391402:i=6052:sd=4:ss=axioms:sgt=24_2774 on theBenchmark for (2774ds/6052Mi) % 177.35/26.14 [W927 21:40:14.997956167 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.997999427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998050321 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998064224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998089707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998156388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998196102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998207578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998231462 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998241389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.35/26.14 [W927 21:40:14.998264859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.35/26.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:14.998274932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 % (2964276)Refutation not found, incomplete strategy % 179.84/26.55 % (2964276)------------------------------ % 179.84/26.55 % (2964276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 179.84/26.55 % (2964276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.84/26.55 % (2964276)CaDiCaL version: 2.1.3 % 179.84/26.55 % (2964276)Termination reason: Refutation not found, incomplete strategy % 179.84/26.55 % (2964276)Time elapsed: 0.613 s % 179.84/26.55 % (2964276)Peak memory usage: 135 MB % 179.84/26.55 % (2964276)Instructions burned: 924 (million) % 179.84/26.55 % (2964276)------------------------------ % 179.84/26.55 % (2964276)------------------------------ % 179.84/26.55 % (2964275)Instruction limit reached! % 179.84/26.55 % (2964275)------------------------------ % 179.84/26.55 % (2964275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 179.84/26.55 % (2964275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.84/26.55 % (2964275)CaDiCaL version: 2.1.3 % 179.84/26.55 % (2964275)Termination reason: Instruction limit % 179.84/26.55 % (2964275)Termination phase: Saturation % 179.84/26.55 % (2964275)Time elapsed: 0.983 s % 179.84/26.55 % (2964275)Peak memory usage: 170 MB % 179.84/26.55 % (2964275)Instructions burned: 1574 (million) % 179.84/26.55 % (2964280)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=966418923:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2764 on theBenchmark for (2764ds/1842Mi) % 179.84/26.55 % (2964279)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=1404114900:i=3500:sd=1:bd=preordered:sup=off:ss=included_2765 on theBenchmark for (2765ds/3500Mi) % 179.84/26.55 [W927 21:40:15.042402787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042446541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042485148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042502365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042528708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042540888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.84/26.55 [W927 21:40:15.042566415 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.84/26.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:15.042577902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:15.042602512 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:15.042624595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:15.042650276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:15.042660502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 % (2964280)Refutation not found, incomplete strategy % 191.97/28.27 % (2964280)------------------------------ % 191.97/28.27 % (2964280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.97/28.27 % (2964280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.97/28.27 % (2964280)CaDiCaL version: 2.1.3 % 191.97/28.27 % (2964280)Termination reason: Refutation not found, incomplete strategy % 191.97/28.27 % (2964280)Time elapsed: 0.658 s % 191.97/28.27 % (2964280)Peak memory usage: 135 MB % 191.97/28.27 % (2964280)Instructions burned: 1047 (million) % 191.97/28.27 % (2964280)------------------------------ % 191.97/28.27 % (2964280)------------------------------ % 191.97/28.27 % (2964283)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3932615582:i=66096:add=on_2754 on theBenchmark for (2754ds/66096Mi) % 191.97/28.27 % (2964265)Instruction limit reached! % 191.97/28.27 % (2964265)------------------------------ % 191.97/28.27 % (2964265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.97/28.27 % (2964265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.97/28.27 % (2964265)CaDiCaL version: 2.1.3 % 191.97/28.27 % (2964265)Termination reason: Instruction limit % 191.97/28.27 % (2964265)Termination phase: Saturation % 191.97/28.27 % (2964265)Time elapsed: 8.365 s % 191.97/28.27 % (2964265)Peak memory usage: 692 MB % 191.97/28.27 % (2964265)Instructions burned: 26474 (million) % 191.97/28.27 % (2964285)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2163778214:i=1884:sd=1:nm=60:ss=axioms_2750 on theBenchmark for (2750ds/1884Mi) % 191.97/28.27 [W927 21:40:17.221984436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:17.222029984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:17.222053283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 191.97/28.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 191.97/28.27 [W927 21:40:17.222060149 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222074266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222080443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222093885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222110749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222124031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222129451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222142257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 [W927 21:40:17.222147565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.12/31.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.12/31.65 % (2964279)Refutation not found, incomplete strategy % 216.12/31.65 % (2964279)------------------------------ % 216.12/31.65 % (2964279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.12/31.65 % (2964279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.12/31.65 % (2964279)CaDiCaL version: 2.1.3 % 216.12/31.65 % (2964279)Termination reason: Refutation not found, incomplete strategy % 216.12/31.65 % (2964279)Time elapsed: 1.679 s % 216.12/31.65 % (2964279)Peak memory usage: 173 MB % 216.12/31.65 % (2964279)Instructions burned: 2796 (million) % 216.12/31.65 % (2964285)Refutation not found, incomplete strategy % 216.12/31.65 % (2964285)------------------------------ % 216.12/31.65 % (2964285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.12/31.65 % (2964285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.12/31.65 % (2964285)CaDiCaL version: 2.1.3 % 216.12/31.65 % (2964285)Termination reason: Refutation not found, incomplete strategy % 216.12/31.65 % (2964285)Time elapsed: 0.354 s % 216.12/31.65 % (2964285)Peak memory usage: 134 MB % 216.12/31.65 % (2964285)Instructions burned: 925 (million) % 216.12/31.65 % (2964279)------------------------------ % 216.12/31.65 % (2964279)------------------------------ % 216.12/31.65 % (2964285)------------------------------ % 216.12/31.65 % (2964285)------------------------------ % 216.12/31.65 % (2964287)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2707736220:cts=off:i=5469:bs=on:fsr=off_2744 on theBenchmark for (2744ds/5469Mi) % 220.37/32.23 % (2964288)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=4130084566:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2744 on theBenchmark for (2744ds/2037Mi) % 220.37/32.23 % (2964288)Instruction limit reached! % 220.37/32.23 % (2964288)------------------------------ % 220.37/32.23 % (2964288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.37/32.23 % (2964288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.37/32.23 % (2964288)CaDiCaL version: 2.1.3 % 220.37/32.23 % (2964288)Termination reason: Instruction limit % 220.37/32.23 % (2964288)Termination phase: Saturation % 220.37/32.23 % (2964288)Time elapsed: 1.121 s % 220.37/32.23 % (2964288)Peak memory usage: 174 MB % 220.37/32.23 % (2964288)Instructions burned: 2038 (million) % 220.37/32.23 % (2964291)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4115828963:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2731 on theBenchmark for (2731ds/2110Mi) % 220.37/32.23 [W927 21:40:19.348771492 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348815329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348853456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348865076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348890706 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348900816 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348926159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348948539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348975746 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.37/32.23 [W927 21:40:19.348989573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.37/32.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.29/35.55 [W927 21:40:19.349024023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.29/35.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.29/35.55 [W927 21:40:19.349034730 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.29/35.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.29/35.55 % (2964287)Instruction limit reached! % 243.29/35.55 % (2964287)------------------------------ % 243.29/35.55 % (2964287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.29/35.55 % (2964287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.29/35.55 % (2964287)CaDiCaL version: 2.1.3 % 243.29/35.55 % (2964287)Termination reason: Instruction limit % 243.29/35.55 % (2964287)Termination phase: Saturation % 243.29/35.55 % (2964287)Time elapsed: 1.789 s % 243.29/35.55 % (2964287)Peak memory usage: 109 MB % 243.29/35.55 % (2964287)Instructions burned: 5470 (million) % 243.29/35.55 % (2964293)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=4230782507:i=2430:add=off:aac=none:nm=16_2725 on theBenchmark for (2725ds/2430Mi) % 243.29/35.55 % (2964291)Refutation not found, incomplete strategy % 243.29/35.55 % (2964291)------------------------------ % 243.29/35.55 % (2964291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.29/35.55 % (2964291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.29/35.55 % (2964291)CaDiCaL version: 2.1.3 % 243.29/35.55 % (2964291)Termination reason: Refutation not found, incomplete strategy % 243.29/35.55 % (2964291)Time elapsed: 0.616 s % 243.29/35.55 % (2964291)Peak memory usage: 133 MB % 243.29/35.55 % (2964291)Instructions burned: 943 (million) % 243.29/35.55 % (2964291)------------------------------ % 243.29/35.55 % (2964291)------------------------------ % 243.29/35.55 % (2964295)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=1978154293:cond=fast:i=4891_2721 on theBenchmark for (2721ds/4891Mi) % 243.29/35.55 % (2964293)Instruction limit reached! % 243.29/35.55 % (2964293)------------------------------ % 243.29/35.55 % (2964293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.29/35.55 % (2964293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.29/35.55 % (2964293)CaDiCaL version: 2.1.3 % 243.29/35.55 % (2964293)Termination reason: Instruction limit % 243.29/35.55 % (2964293)Termination phase: Saturation % 243.29/35.55 % (2964293)Time elapsed: 0.818 s % 243.29/35.55 % (2964293)Peak memory usage: 214 MB % 243.29/35.55 % (2964293)Instructions burned: 2431 (million) % 243.29/35.55 % (2964297)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=873217620:st=2:i=14845:sd=2:ss=included:fsd=on_2715 on theBenchmark for (2715ds/14845Mi) % 243.29/35.55 % (2964297)Refutation not found, incomplete strategy % 243.29/35.55 % (2964297)------------------------------ % 243.29/35.55 % (2964297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.29/35.55 % (2964297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.29/35.55 % (2964297)CaDiCaL version: 2.1.3 % 243.29/35.55 % (2964297)Termination reason: Refutation not found, incomplete strategy % 243.29/35.55 % (2964297)Time elapsed: 0.915 s % 243.29/35.55 % (2964297)Peak memory usage: 174 MB % 243.29/35.55 % (2964297)Instructions burned: 2574 (million) % 243.29/35.55 % (2964297)------------------------------ % 243.29/35.55 % (2964297)------------------------------ % 243.29/35.55 % (2964299)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2228889373:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2704 on theBenchmark for (2704ds/7534Mi) % 243.29/35.55 % (2964295)Instruction limit reached! % 243.29/35.55 % (2964295)------------------------------ % 243.29/35.55 % (2964295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.29/35.55 % (2964295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.36/35.96 % (2964295)CaDiCaL version: 2.1.3 % 245.36/35.96 % (2964295)Termination reason: Instruction limit % 245.36/35.96 % (2964295)Termination phase: Saturation % 245.36/35.96 % (2964295)Time elapsed: 2.804 s % 245.36/35.96 % (2964295)Peak memory usage: 218 MB % 245.36/35.96 % (2964295)Instructions burned: 4892 (million) % 245.36/35.96 % (2964301)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=4050474203:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2691 on theBenchmark for (2691ds/10353Mi) % 245.36/35.96 [W927 21:40:23.310980287 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311021873 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311060717 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311074167 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311098811 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311111224 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311136861 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311148568 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311173448 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311185165 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311210361 register_special_ops.cpp:225] Warning: Creating a tensor from 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.36/35.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 245.36/35.96 [W927 21:40:23.311222028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 250.38/36.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 250.38/36.55 % (2964301)Refutation not found, incomplete strategy % 250.38/36.55 % (2964301)------------------------------ % 250.38/36.55 % (2964301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.38/36.55 % (2964301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.38/36.55 % (2964301)CaDiCaL version: 2.1.3 % 250.38/36.55 % (2964301)Termination reason: Refutation not found, incomplete strategy % 250.38/36.55 % (2964301)Time elapsed: 0.604 s % 250.38/36.55 % (2964301)Peak memory usage: 132 MB % 250.38/36.55 % (2964301)Instructions burned: 926 (million) % 250.38/36.55 % (2964301)------------------------------ % 250.38/36.55 % (2964301)------------------------------ % 250.38/36.55 % (2964303)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1023900007:i=7860_2682 on theBenchmark for (2682ds/7860Mi) % 250.38/36.55 % (2964299)Instruction limit reached! % 250.38/36.55 % (2964299)------------------------------ % 250.38/36.55 % (2964299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.38/36.55 % (2964299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.38/36.55 % (2964299)CaDiCaL version: 2.1.3 % 250.38/36.55 % (2964299)Termination reason: Instruction limit % 250.38/36.55 % (2964299)Termination phase: Saturation % 250.38/36.55 % (2964299)Time elapsed: 2.326 s % 250.38/36.55 % (2964299)Peak memory usage: 225 MB % 250.38/36.55 % (2964299)Instructions burned: 7535 (million) % 250.38/36.55 % (2964305)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=1062008775:i=7896:sd=2:bs=on:ss=included:sgt=20_2679 on theBenchmark for (2679ds/7896Mi) % 250.38/36.55 % (2964303)Refutation not found, incomplete strategy % 250.38/36.55 % (2964303)------------------------------ % 250.38/36.55 % (2964303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.38/36.55 % (2964303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.38/36.55 % (2964303)CaDiCaL version: 2.1.3 % 250.38/36.55 % (2964303)Termination reason: Refutation not found, incomplete strategy % 250.38/36.55 % (2964303)Time elapsed: 0.472 s % 250.38/36.55 % (2964303)Peak memory usage: 108 MB % 250.38/36.55 % (2964303)Instructions burned: 900 (million) % 250.38/36.55 % (2964303)------------------------------ % 250.38/36.55 % (2964303)------------------------------ % 250.38/36.55 % (2964307)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3418332233:i=5812:gtgl=2:gtg=all_2673 on theBenchmark for (2673ds/5812Mi) % 250.38/36.55 % (2964239)Instruction limit reached! % 250.38/36.55 % (2964239)------------------------------ % 250.38/36.55 % (2964239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.38/36.55 % (2964239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.38/36.55 % (2964239)CaDiCaL version: 2.1.3 % 250.38/36.55 % (2964239)Termination reason: Instruction limit % 250.38/36.55 % (2964239)Termination phase: Saturation % 250.38/36.55 % (2964239)Time elapsed: 21.718 s % 250.38/36.55 % (2964239)Peak memory usage: 314 MB % 250.38/36.55 % (2964239)Instructions burned: 33335 (million) % 250.38/36.55 % (2964309)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=347813966:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2660 on theBenchmark for (2660ds/2965Mi) % 250.38/36.55 % (2964263)Instruction limit reached! % 250.38/36.55 % (2964263)------------------------------ % 250.38/36.55 % (2964263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.38/36.55 % (2964263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.38/36.55 % (2964263)CaDiCaL version: 2.1.3 % 250.38/36.55 % (2964263)Termination reason: Instruction limit % 250.38/36.55 % (2964263)Termination phase: Saturation % 250.38/36.55 % (2964263)Time elapsed: 18.047 s % 250.38/36.55 % (2964263)Peak memory usage: 391 MB % 250.38/36.55 % (2964263)Instructions burned: 30755 (million) % 250.38/36.55 % (2964311)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=2248646973:i=2967:kws=precedence:bd=preordered:av=off_2657 on theBenchmark for (2657ds/2967Mi) % 250.38/36.55 % (2964305)Instruction limit reached! % 250.38/36.55 % (2964305)------------------------------ % 255.17/37.16 % (2964305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.17/37.16 % (2964305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.17/37.16 % (2964305)CaDiCaL version: 2.1.3 % 255.17/37.16 % (2964305)Termination reason: Instruction limit % 255.17/37.16 % (2964305)Termination phase: Saturation % 255.17/37.16 % (2964305)Time elapsed: 2.560 s % 255.17/37.16 % (2964305)Peak memory usage: 224 MB % 255.17/37.16 % (2964305)Instructions burned: 7896 (million) % 255.17/37.16 % (2964313)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=2467429376:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2652 on theBenchmark for (2652ds/3022Mi) % 255.17/37.16 [W927 21:40:26.040213920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040236553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040258618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040264738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040278036 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040284558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040297785 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040304194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040316876 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040323227 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.17/37.16 [W927 21:40:26.040336161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.17/37.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:26.040342660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 % (2964313)Refutation not found, incomplete strategy % 256.50/37.44 % (2964313)------------------------------ % 256.50/37.44 % (2964313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.50/37.44 % (2964313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.50/37.44 % (2964313)CaDiCaL version: 2.1.3 % 256.50/37.44 % (2964313)Termination reason: Refutation not found, incomplete strategy % 256.50/37.44 % (2964313)Time elapsed: 0.412 s % 256.50/37.44 % (2964313)Peak memory usage: 135 MB % 256.50/37.44 % (2964313)Instructions burned: 926 (million) % 256.50/37.44 % (2964313)------------------------------ % 256.50/37.44 % (2964313)------------------------------ % 256.50/37.44 % (2964315)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=2685538618:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2646 on theBenchmark for (2646ds/3207Mi) % 256.50/37.44 [W927 21:40:27.637474364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637509657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637530385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637536666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637549798 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637556242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637570595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637576956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637589824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 256.50/37.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 256.50/37.44 [W927 21:40:27.637603484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 273.54/39.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 273.54/39.83 [W927 21:40:27.637617142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 273.54/39.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 273.54/39.83 [W927 21:40:27.637622752 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 273.54/39.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 273.54/39.83 % (2964315)Refutation not found, incomplete strategy % 273.54/39.83 % (2964315)------------------------------ % 273.54/39.83 % (2964315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.54/39.83 % (2964315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.83 % (2964315)CaDiCaL version: 2.1.3 % 273.54/39.83 % (2964315)Termination reason: Refutation not found, incomplete strategy % 273.54/39.83 % (2964315)Time elapsed: 0.360 s % 273.54/39.83 % (2964315)Peak memory usage: 136 MB % 273.54/39.83 % (2964315)Instructions burned: 926 (million) % 273.54/39.83 % (2964309)Instruction limit reached! % 273.54/39.83 % (2964309)------------------------------ % 273.54/39.83 % (2964309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.54/39.83 % (2964309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.83 % (2964309)CaDiCaL version: 2.1.3 % 273.54/39.83 % (2964309)Termination reason: Instruction limit % 273.54/39.83 % (2964309)Termination phase: Saturation % 273.54/39.83 % (2964309)Time elapsed: 1.791 s % 273.54/39.83 % (2964309)Peak memory usage: 213 MB % 273.54/39.83 % (2964309)Instructions burned: 2965 (million) % 273.54/39.83 % (2964315)------------------------------ % 273.54/39.83 % (2964315)------------------------------ % 273.54/39.83 % (2964317)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1617279259:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2641 on theBenchmark for (2641ds/3289Mi) % 273.54/39.83 % (2964318)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3138961905:i=38569:sd=3:ss=axioms:sgt=32_2640 on theBenchmark for (2640ds/38569Mi) % 273.54/39.83 % (2964311)Instruction limit reached! % 273.54/39.83 % (2964311)------------------------------ % 273.54/39.83 % (2964311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.54/39.83 % (2964311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.83 % (2964311)CaDiCaL version: 2.1.3 % 273.54/39.83 % (2964311)Termination reason: Instruction limit % 273.54/39.83 % (2964311)Termination phase: Saturation % 273.54/39.83 % (2964311)Time elapsed: 1.859 s % 273.54/39.83 % (2964311)Peak memory usage: 215 MB % 273.54/39.83 % (2964311)Instructions burned: 2968 (million) % 273.54/39.83 % (2964307)Instruction limit reached! % 273.54/39.83 % (2964307)------------------------------ % 273.54/39.83 % (2964307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.54/39.83 % (2964307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.83 % (2964307)CaDiCaL version: 2.1.3 % 273.54/39.83 % (2964307)Termination reason: Instruction limit % 273.54/39.83 % (2964307)Termination phase: Saturation % 273.54/39.83 % (2964307)Time elapsed: 3.456 s % 273.54/39.83 % (2964307)Peak memory usage: 220 MB % 273.54/39.83 % (2964307)Instructions burned: 5813 (million) % 273.54/39.83 [W927 21:40:28.246407537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 273.54/39.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 273.54/39.83 [W927 21:40:28.246442497 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 273.54/39.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 273.54/39.83 [W927 21:40:28.246464224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246470631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246484423 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246489710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246503352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246508989 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246521832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246527275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246540289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 [W927 21:40:28.246545769 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.89/43.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.89/43.36 % (2964321)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3771679737:cts=off:i=3394_2637 on theBenchmark for (2637ds/3394Mi) % 298.89/43.36 % (2964322)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=546415012:i=33824:bd=preordered_2637 on theBenchmark for (2637ds/33824Mi) % 298.89/43.36 % (2964318)Refutation not found, incomplete strategy % 298.89/43.36 % (2964318)------------------------------ % 298.89/43.36 % (2964318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 298.89/43.36 % (2964318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.89/43.36 % (2964318)CaDiCaL version: 2.1.3 % 298.89/43.36 % (2964318)Termination reason: Refutation not found, incomplete strategy % 298.89/43.36 % (2964318)Time elapsed: 0.351 s % 298.89/43.36 % (2964318)Peak memory usage: 132 MB % 298.89/43.36 % (2964318)Instructions burned: 925 (million) % 298.89/43.36 % (2964318)------------------------------ % 298.89/43.36 % (2964318)------------------------------ % 300.50/43.63 % (2964325)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2490922927:i=20684:bd=all:gtg=exists_sym_2634 on theBenchmark for (2634ds/20684Mi) % 300.50/43.63 % (2964317)Instruction limit reached! % 300.50/43.63 % (2964317)------------------------------ % 300.50/43.63 % (2964317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.50/43.63 % (2964317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/43.63 % (2964317)CaDiCaL version: 2.1.3 % 300.50/43.63 % (2964317)Termination reason: Instruction limit % 300.50/43.63 % (2964317)Termination phase: Saturation % 300.50/43.63 % (2964317)Time elapsed: 2.001 s % 300.50/43.63 % (2964317)Peak memory usage: 173 MB % 300.50/43.63 % (2964317)Instructions burned: 3290 (million) % 300.50/43.63 % (2964327)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=1675228447: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_2619 on theBenchmark for (2619ds/7222Mi) % 300.50/43.63 % (2964321)Instruction limit reached! % 300.50/43.63 % (2964321)------------------------------ % 300.50/43.63 % (2964321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.50/43.63 % (2964321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.50/43.63 % (2964321)CaDiCaL version: 2.1.3 % 300.50/43.63 % (2964321)Termination reason: Instruction limit % 300.50/43.63 % (2964321)Termination phase: Saturation % 300.50/43.63 % (2964321)Time elapsed: 2.024 s % 300.50/43.63 % (2964321)Peak memory usage: 178 MB % 300.50/43.63 % (2964321)Instructions burned: 3395 (million) % 300.50/43.63 % (2964329)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3474327992:st=4:i=7295:sd=4:ep=R:ss=axioms_2616 on theBenchmark for (2616ds/7295Mi) % 300.50/43.63 [W927 21:40:30.909076463 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909109187 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909148704 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909161964 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909189064 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909201481 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909227611 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/43.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.50/43.63 [W927 21:40:30.909239388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty int % 300.50/43.63 Terminated %------------------------------------------------------------------------------