%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM923_10 : 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 : n003.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:27 PM UTC 2026 % Result : Timeout 300.17s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM923_10 : 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.36 % Computer : n003.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sun Sep 27 21:41:26 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.40 Running first-order theorem proving % 0.09/0.40 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 % 10.45/2.49 % (940920)Detected formulas, will run a generic FOF schedule. % 10.45/2.49 % (940926)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=1598100454:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.45/2.49 % (940925)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=3107085561:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.45/2.49 % (940927)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=4130672903:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.45/2.49 % (940928)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3009513777:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.45/2.49 % (940928)Refutation not found, incomplete strategy % 10.45/2.49 % (940928)------------------------------ % 10.45/2.49 % (940928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.45/2.49 % (940928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.45/2.49 % (940928)CaDiCaL version: 2.1.3 % 10.45/2.49 % (940928)Termination reason: Refutation not found, incomplete strategy % 10.45/2.49 % (940928)Time elapsed: 0.001 s % 10.45/2.49 % (940928)Peak memory usage: 86 MB % 10.45/2.49 % (940930)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1413366204:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.45/2.49 % (940929)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1030032807:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.45/2.49 % (940931)dis-21_1_sil=8000:lcm=predicate:random_seed=419748592:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 10.45/2.49 % (940929)Refutation not found, incomplete strategy % 10.45/2.49 % (940929)------------------------------ % 10.45/2.49 % (940929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.45/2.49 % (940929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.45/2.49 % (940929)CaDiCaL version: 2.1.3 % 10.45/2.49 % (940929)Termination reason: Refutation not found, incomplete strategy % 10.45/2.49 % (940929)Time elapsed: 0.001 s % 10.45/2.49 % (940929)Peak memory usage: 86 MB % 10.45/2.49 % (940930)Instruction limit reached! % 10.45/2.49 % (940930)------------------------------ % 10.45/2.49 % (940930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.45/2.49 % (940930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.45/2.49 % (940930)CaDiCaL version: 2.1.3 % 10.45/2.49 % (940930)Termination reason: Instruction limit % 10.45/2.49 % (940930)Termination phase: Saturation % 10.45/2.49 % (940930)Time elapsed: 0.078 s % 10.45/2.49 % (940930)Peak memory usage: 89 MB % 10.45/2.49 % (940930)Instructions burned: 140 (million) % 10.45/2.49 % (940931)Instruction limit reached! % 10.45/2.49 % (940931)------------------------------ % 10.45/2.49 % (940931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.45/2.49 % (940931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.45/2.49 % (940931)CaDiCaL version: 2.1.3 % 10.45/2.49 % (940931)Termination reason: Instruction limit % 10.45/2.49 % (940931)Termination phase: Saturation % 10.45/2.49 % (940931)Time elapsed: 0.079 s % 10.45/2.49 % (940931)Peak memory usage: 89 MB % 10.45/2.49 % (940931)Instructions burned: 130 (million) % 10.45/2.49 % (940928)------------------------------ % 10.45/2.49 % (940928)------------------------------ % 10.45/2.49 % (940939)lrs+10_1_sil=8000:sp=occurrence:random_seed=1260694642:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 10.45/2.49 % (940940)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4212838550:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 10.45/2.49 % (940939)Refutation not found, incomplete strategy % 10.45/2.49 % (940939)------------------------------ % 10.45/2.49 % (940939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.45/2.49 % (940939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.45/2.49 % (940939)CaDiCaL version: 2.1.3 % 10.45/2.49 % (940939)Termination reason: Refutation not found, incomplete strategy % 10.45/2.49 % (940939)Time elapsed: 0.001 s % 10.45/2.49 % (940939)Peak memory usage: 86 MB % 11.70/2.60 % (940940)Refutation not found, incomplete strategy % 11.70/2.60 % (940940)------------------------------ % 11.70/2.60 % (940940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940940)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940940)Termination reason: Refutation not found, incomplete strategy % 11.70/2.60 % (940940)Time elapsed: 0.001 s % 11.70/2.60 % (940940)Peak memory usage: 87 MB % 11.70/2.60 % (940940)Instructions burned: 1 (million) % 11.70/2.60 % (940929)------------------------------ % 11.70/2.60 % (940929)------------------------------ % 11.70/2.60 % (940943)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2318731919:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.70/2.60 % (940943)Refutation not found, incomplete strategy % 11.70/2.60 % (940943)------------------------------ % 11.70/2.60 % (940943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940943)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940943)Termination reason: Refutation not found, incomplete strategy % 11.70/2.60 % (940943)Time elapsed: 0.001 s % 11.70/2.60 % (940943)Peak memory usage: 86 MB % 11.70/2.60 % (940944)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=1037798023:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 11.70/2.60 % (940939)------------------------------ % 11.70/2.60 % (940939)------------------------------ % 11.70/2.60 % (940940)------------------------------ % 11.70/2.60 % (940940)------------------------------ % 11.70/2.60 % (940944)Instruction limit reached! % 11.70/2.60 % (940944)------------------------------ % 11.70/2.60 % (940944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940944)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940944)Termination reason: Instruction limit % 11.70/2.60 % (940944)Termination phase: Saturation % 11.70/2.60 % (940944)Time elapsed: 0.135 s % 11.70/2.60 % (940944)Peak memory usage: 91 MB % 11.70/2.60 % (940944)Instructions burned: 249 (million) % 11.70/2.60 % (940927)Refutation not found, incomplete strategy % 11.70/2.60 % (940927)------------------------------ % 11.70/2.60 % (940927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940927)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940927)Termination reason: Refutation not found, incomplete strategy % 11.70/2.60 % (940927)Time elapsed: 0.568 s % 11.70/2.60 % (940927)Peak memory usage: 127 MB % 11.70/2.60 % (940927)Instructions burned: 842 (million) % 11.70/2.60 % (940943)------------------------------ % 11.70/2.60 % (940943)------------------------------ % 11.70/2.60 % (940948)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4227168066:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 11.70/2.60 % (940947)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3448824146:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 11.70/2.60 % (940947)Refutation not found, incomplete strategy % 11.70/2.60 % (940947)------------------------------ % 11.70/2.60 % (940947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940947)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940947)Termination reason: Refutation not found, incomplete strategy % 11.70/2.60 % (940947)Time elapsed: 0.001 s % 11.70/2.60 % (940947)Peak memory usage: 86 MB % 11.70/2.60 % (940949)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2001420875:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 11.70/2.60 % (940949)Refutation not found, incomplete strategy % 11.70/2.60 % (940949)------------------------------ % 11.70/2.60 % (940949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.70/2.60 % (940949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.70/2.60 % (940949)CaDiCaL version: 2.1.3 % 11.70/2.60 % (940949)Termination reason: Refutation not found, incomplete strategy % 11.70/2.60 % (940949)Time elapsed: 0.004 s % 11.70/2.60 % (940949)Peak memory usage: 88 MB % 11.70/2.60 % (940949)Instructions burned: 5 (million) % 13.04/2.95 % (940950)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1477313269:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 13.04/2.95 % (940950)Refutation not found, incomplete strategy % 13.04/2.95 % (940950)------------------------------ % 13.04/2.95 % (940950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.95 % (940950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.95 % (940950)CaDiCaL version: 2.1.3 % 13.04/2.95 % (940950)Termination reason: Refutation not found, incomplete strategy % 13.04/2.95 % (940950)Time elapsed: 0.002 s % 13.04/2.95 % (940950)Peak memory usage: 88 MB % 13.04/2.95 % (940950)Instructions burned: 3 (million) % 13.04/2.95 % (940927)------------------------------ % 13.04/2.95 % (940927)------------------------------ % 13.04/2.95 % (940947)------------------------------ % 13.04/2.95 % (940947)------------------------------ % 13.04/2.95 % (940949)------------------------------ % 13.04/2.95 % (940949)------------------------------ % 13.04/2.95 % (940955)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2085751548:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 13.04/2.95 % (940955)Refutation not found, incomplete strategy % 13.04/2.95 % (940955)------------------------------ % 13.04/2.95 % (940955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.95 % (940955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.95 % (940955)CaDiCaL version: 2.1.3 % 13.04/2.95 % (940955)Termination reason: Refutation not found, incomplete strategy % 13.04/2.95 % (940955)Time elapsed: 0.003 s % 13.04/2.95 % (940955)Peak memory usage: 89 MB % 13.04/2.95 % (940955)Instructions burned: 2 (million) % 13.04/2.95 % (940950)------------------------------ % 13.04/2.95 % (940950)------------------------------ % 13.04/2.95 % (940956)lrs+10_1_sil=8000:sp=occurrence:random_seed=1271279304:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 13.04/2.95 % (940956)Refutation not found, incomplete strategy % 13.04/2.95 % (940956)------------------------------ % 13.04/2.95 % (940956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.95 % (940956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.95 % (940956)CaDiCaL version: 2.1.3 % 13.04/2.95 % (940956)Termination reason: Refutation not found, incomplete strategy % 13.04/2.95 % (940956)Time elapsed: 0.001 s % 13.04/2.95 % (940956)Peak memory usage: 86 MB % 13.04/2.95 % (940957)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1025084320:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi) % 13.04/2.95 % (940957)Refutation not found, incomplete strategy % 13.04/2.95 % (940957)------------------------------ % 13.04/2.95 % (940957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.95 % (940957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.95 % (940957)CaDiCaL version: 2.1.3 % 13.04/2.95 % (940957)Termination reason: Refutation not found, incomplete strategy % 13.04/2.95 % (940957)Time elapsed: 0.004 s % 13.04/2.95 % (940957)Peak memory usage: 88 MB % 13.04/2.95 % (940957)Instructions burned: 6 (million) % 13.04/2.95 % (940959)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=400272781:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi) % 13.04/2.95 % (940955)------------------------------ % 13.04/2.95 % (940955)------------------------------ % 13.04/2.95 % (940956)------------------------------ % 13.04/2.95 % (940956)------------------------------ % 13.04/2.95 % (940957)------------------------------ % 13.04/2.95 % (940957)------------------------------ % 13.04/2.95 % (940963)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3110465625:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi) % 13.04/2.95 % (940964)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1984946161:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 13.04/2.95 % (940964)Refutation not found, incomplete strategy % 13.04/2.95 % (940964)------------------------------ % 13.04/2.95 % (940964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.95 % (940964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.95 % (940964)CaDiCaL version: 2.1.3 % 13.04/2.95 % (940964)Termination reason: Refutation not found, incomplete strategy % 16.51/3.16 % (940964)Time elapsed: 0.001 s % 16.51/3.16 % (940964)Peak memory usage: 86 MB % 16.51/3.16 % (940963)Instruction limit reached! % 16.51/3.16 % (940963)------------------------------ % 16.51/3.16 % (940963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.51/3.16 % (940963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.51/3.16 % (940963)CaDiCaL version: 2.1.3 % 16.51/3.16 % (940963)Termination reason: Instruction limit % 16.51/3.16 % (940963)Termination phase: Saturation % 16.51/3.16 % (940963)Time elapsed: 0.079 s % 16.51/3.16 % (940963)Peak memory usage: 90 MB % 16.51/3.16 % (940963)Instructions burned: 134 (million) % 16.51/3.16 % (940965)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1062964373:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 16.51/3.16 [W927 21:41:28.852452443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852491847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852527967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852540907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852568151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852592895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852623735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852634892 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852660145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852670872 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.51/3.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.51/3.16 [W927 21:41:28.852695453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.852706459 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 % (940968)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=166349422:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 19.54/3.82 % (940968)Refutation not found, incomplete strategy % 19.54/3.82 % (940968)------------------------------ % 19.54/3.82 % (940968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.82 % (940968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.82 % (940968)CaDiCaL version: 2.1.3 % 19.54/3.82 % (940968)Termination reason: Refutation not found, incomplete strategy % 19.54/3.82 % (940968)Time elapsed: 0.001 s % 19.54/3.82 % (940968)Peak memory usage: 87 MB % 19.54/3.82 % (940968)Instructions burned: 1 (million) % 19.54/3.82 % (940964)------------------------------ % 19.54/3.82 % (940964)------------------------------ % 19.54/3.82 % (940959)Refutation not found, incomplete strategy % 19.54/3.82 % (940959)------------------------------ % 19.54/3.82 % (940959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.82 % (940959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.82 % (940959)CaDiCaL version: 2.1.3 % 19.54/3.82 % (940959)Termination reason: Refutation not found, incomplete strategy % 19.54/3.82 % (940959)Time elapsed: 0.574 s % 19.54/3.82 % (940959)Peak memory usage: 125 MB % 19.54/3.82 % (940959)Instructions burned: 826 (million) % 19.54/3.82 % (940968)------------------------------ % 19.54/3.82 % (940968)------------------------------ % 19.54/3.82 % (940971)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1236484306:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi) % 19.54/3.82 [W927 21:41:28.204355940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204390031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204425605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204437118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204468762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204480009 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.54/3.82 [W927 21:41:28.204506212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.54/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 [W927 21:41:28.204517312 register_special_ops.cpp:225] Warning: Creating a tensor from 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.97/5.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 [W927 21:41:28.204549276 register_special_ops.cpp:225] Warning: Creating a tensor from 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.97/5.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 [W927 21:41:28.204559143 register_special_ops.cpp:225] Warning: Creating a tensor from 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.97/5.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 [W927 21:41:28.204582603 register_special_ops.cpp:225] Warning: Creating a tensor from 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.97/5.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 [W927 21:41:28.204592253 register_special_ops.cpp:225] Warning: Creating a tensor from 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.97/5.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.97/5.05 % (940971)Instruction limit reached! % 29.97/5.05 % (940971)------------------------------ % 29.97/5.05 % (940971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.97/5.05 % (940971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.97/5.05 % (940971)CaDiCaL version: 2.1.3 % 29.97/5.05 % (940971)Termination reason: Instruction limit % 29.97/5.05 % (940971)Termination phase: Saturation % 29.97/5.05 % (940971)Time elapsed: 0.073 s % 29.97/5.05 % (940971)Peak memory usage: 89 MB % 29.97/5.05 % (940971)Instructions burned: 136 (million) % 29.97/5.05 % (940959)------------------------------ % 29.97/5.05 % (940959)------------------------------ % 29.97/5.05 % (940972)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4096281573:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi) % 29.97/5.05 % (940972)Refutation not found, incomplete strategy % 29.97/5.05 % (940972)------------------------------ % 29.97/5.05 % (940972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.97/5.05 % (940972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.97/5.05 % (940972)CaDiCaL version: 2.1.3 % 29.97/5.05 % (940972)Termination reason: Refutation not found, incomplete strategy % 29.97/5.05 % (940972)Time elapsed: 0.001 s % 29.97/5.05 % (940972)Peak memory usage: 86 MB % 29.97/5.05 % (940965)Refutation not found, incomplete strategy % 29.97/5.05 % (940965)------------------------------ % 29.97/5.05 % (940965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.97/5.05 % (940965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.97/5.05 % (940965)CaDiCaL version: 2.1.3 % 29.97/5.05 % (940965)Termination reason: Refutation not found, incomplete strategy % 29.97/5.05 % (940965)Time elapsed: 0.554 s % 29.97/5.05 % (940965)Peak memory usage: 125 MB % 29.97/5.05 % (940965)Instructions burned: 822 (million) % 29.97/5.05 % (940974)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1877382970:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 29.97/5.05 % (940974)Refutation not found, incomplete strategy % 29.97/5.05 % (940974)------------------------------ % 29.97/5.05 % (940974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.97/5.05 % (940974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.97/5.05 % (940974)CaDiCaL version: 2.1.3 % 29.97/5.05 % (940974)Termination reason: Refutation not found, incomplete strategy % 29.97/5.05 % (940974)Time elapsed: 0.001 s % 29.97/5.05 % (940974)Peak memory usage: 86 MB % 29.97/5.05 % (940948)Instruction limit reached! % 29.97/5.05 % (940948)------------------------------ % 31.16/5.27 % (940948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.16/5.27 % (940948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.16/5.27 % (940948)CaDiCaL version: 2.1.3 % 31.16/5.27 % (940948)Termination reason: Instruction limit % 31.16/5.27 % (940948)Termination phase: Saturation % 31.16/5.27 % (940948)Time elapsed: 1.503 s % 31.16/5.27 % (940948)Peak memory usage: 140 MB % 31.16/5.27 % (940948)Instructions burned: 2350 (million) % 31.16/5.27 % (940975)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=1398419431:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 31.16/5.27 % (940972)------------------------------ % 31.16/5.27 % (940972)------------------------------ % 31.16/5.27 % (940978)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=3053675066:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi) % 31.16/5.27 % (940965)------------------------------ % 31.16/5.27 % (940965)------------------------------ % 31.16/5.27 % (940974)------------------------------ % 31.16/5.27 % (940974)------------------------------ % 31.16/5.27 % (940978)Instruction limit reached! % 31.16/5.27 % (940978)------------------------------ % 31.16/5.27 % (940978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.16/5.27 % (940978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.16/5.27 % (940978)CaDiCaL version: 2.1.3 % 31.16/5.27 % (940978)Termination reason: Instruction limit % 31.16/5.27 % (940978)Termination phase: Saturation % 31.16/5.27 % (940978)Time elapsed: 0.097 s % 31.16/5.27 % (940978)Peak memory usage: 90 MB % 31.16/5.27 % (940978)Instructions burned: 150 (million) % 31.16/5.27 % (940980)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1659790619:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi) % 31.16/5.27 % (940983)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=2367043463:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi) % 31.16/5.27 % (940982)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=64685560:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi) % 31.16/5.27 % (940982)Refutation not found, incomplete strategy % 31.16/5.27 % (940982)------------------------------ % 31.16/5.27 % (940982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.16/5.27 % (940982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.16/5.27 % (940982)CaDiCaL version: 2.1.3 % 31.16/5.27 % (940982)Termination reason: Refutation not found, incomplete strategy % 31.16/5.27 % (940982)Time elapsed: 0.004 s % 31.16/5.27 % (940982)Peak memory usage: 88 MB % 31.16/5.27 % (940982)Instructions burned: 5 (million) % 31.16/5.27 % (940984)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1983955650:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi) % 31.16/5.27 % (940984)Refutation not found, incomplete strategy % 31.16/5.27 % (940984)------------------------------ % 31.16/5.27 % (940984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.16/5.27 % (940984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.16/5.27 % (940984)CaDiCaL version: 2.1.3 % 31.16/5.27 % (940984)Termination reason: Refutation not found, incomplete strategy % 31.16/5.27 % (940984)Time elapsed: 0.001 s % 31.16/5.27 % (940984)Peak memory usage: 86 MB % 31.16/5.27 % (940983)Instruction limit reached! % 31.16/5.27 % (940983)------------------------------ % 31.16/5.27 % (940983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.16/5.27 % (940983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.16/5.27 % (940983)CaDiCaL version: 2.1.3 % 31.16/5.27 % (940983)Termination reason: Instruction limit % 31.16/5.27 % (940983)Termination phase: Saturation % 31.16/5.27 % (940983)Time elapsed: 0.109 s % 31.16/5.27 % (940983)Peak memory usage: 90 MB % 31.16/5.27 % (940983)Instructions burned: 185 (million) % 31.16/5.27 % (940982)------------------------------ % 31.16/5.27 % (940982)------------------------------ % 31.16/5.27 % (940989)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1120466352:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi) % 39.55/6.48 % (940984)------------------------------ % 39.55/6.48 % (940984)------------------------------ % 39.55/6.48 % (940989)Refutation not found, incomplete strategy % 39.55/6.48 % (940989)------------------------------ % 39.55/6.48 % (940989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.48 % (940989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.48 % (940989)CaDiCaL version: 2.1.3 % 39.55/6.48 % (940989)Termination reason: Refutation not found, incomplete strategy % 39.55/6.48 % (940989)Time elapsed: 0.003 s % 39.55/6.48 % (940989)Peak memory usage: 88 MB % 39.55/6.48 % (940989)Instructions burned: 4 (million) % 39.55/6.48 % (940990)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=818942004:i=12111:sd=1:ss=included_2970 on theBenchmark for (2970ds/12111Mi) % 39.55/6.48 % (940992)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2024941563:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi) % 39.55/6.48 % (940989)------------------------------ % 39.55/6.48 % (940989)------------------------------ % 39.55/6.48 % (940992)Instruction limit reached! % 39.55/6.48 % (940992)------------------------------ % 39.55/6.48 % (940992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.48 % (940992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.48 % (940992)CaDiCaL version: 2.1.3 % 39.55/6.48 % (940992)Termination reason: Instruction limit % 39.55/6.48 % (940992)Termination phase: Saturation % 39.55/6.48 % (940992)Time elapsed: 0.184 s % 39.55/6.48 % (940992)Peak memory usage: 92 MB % 39.55/6.48 % (940992)Instructions burned: 320 (million) % 39.55/6.48 % (940995)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1604552204:i=2064:ep=RST_2967 on theBenchmark for (2967ds/2064Mi) % 39.55/6.48 % (940995)Refutation not found, incomplete strategy % 39.55/6.48 % (940995)------------------------------ % 39.55/6.48 % (940995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.48 % (940995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.48 % (940995)CaDiCaL version: 2.1.3 % 39.55/6.48 % (940995)Termination reason: Refutation not found, incomplete strategy % 39.55/6.48 % (940995)Time elapsed: 0.004 s % 39.55/6.48 % (940995)Peak memory usage: 88 MB % 39.55/6.48 % (940995)Instructions burned: 6 (million) % 39.55/6.48 % (940996)dis-1011_128_sil=32000:random_seed=3231511589:i=3706:ep=RST:av=off_2966 on theBenchmark for (2966ds/3706Mi) % 39.55/6.48 % (940996)Refutation not found, incomplete strategy % 39.55/6.48 % (940996)------------------------------ % 39.55/6.48 % (940996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.48 % (940996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.48 % (940996)CaDiCaL version: 2.1.3 % 39.55/6.48 % (940996)Termination reason: Refutation not found, incomplete strategy % 39.55/6.48 % (940996)Time elapsed: 0.004 s % 39.55/6.48 % (940996)Peak memory usage: 88 MB % 39.55/6.48 % (940996)Instructions burned: 6 (million) % 39.55/6.48 % (940995)------------------------------ % 39.55/6.48 % (940995)------------------------------ % 39.55/6.48 % (940996)------------------------------ % 39.55/6.48 % (940996)------------------------------ % 39.55/6.48 % (941000)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2794654709:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2963 on theBenchmark for (2963ds/757Mi) % 39.55/6.48 % (941000)Refutation not found, incomplete strategy % 39.55/6.48 % (941000)------------------------------ % 39.55/6.48 % (941000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.55/6.48 % (941000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.55/6.48 % (941000)CaDiCaL version: 2.1.3 % 39.55/6.48 % (941000)Termination reason: Refutation not found, incomplete strategy % 39.55/6.48 % (941000)Time elapsed: 0.001 s % 39.55/6.48 % (941000)Peak memory usage: 86 MB % 39.55/6.48 % (941001)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=387181756:i=13913:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/13913Mi) % 39.55/6.48 % (941000)------------------------------ % 39.55/6.48 % (941000)------------------------------ % 39.55/6.48 % (941004)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=654876716:i=9925:aac=none_2959 on theBenchmark for (2959ds/9925Mi) % 42.44/6.95 [W927 21:41:31.360198244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360242527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360281318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360295638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360321198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360333059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360359019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360370789 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360395679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360407426 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360432046 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 [W927 21:41:31.360443783 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.44/6.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.44/6.95 % (941001)Refutation not found, incomplete strategy % 42.44/6.95 % (941001)------------------------------ % 42.44/6.95 % (941001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.44/6.95 % (941001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/10.21 % (941001)CaDiCaL version: 2.1.3 % 66.62/10.21 % (941001)Termination reason: Refutation not found, incomplete strategy % 66.62/10.21 % (941001)Time elapsed: 0.540 s % 66.62/10.21 % (941001)Peak memory usage: 125 MB % 66.62/10.21 % (941001)Instructions burned: 821 (million) % 66.62/10.21 % (941001)------------------------------ % 66.62/10.21 % (941001)------------------------------ % 66.62/10.21 % (941004)Refutation not found, incomplete strategy % 66.62/10.21 % (941004)------------------------------ % 66.62/10.21 % (941004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.62/10.21 % (941004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/10.21 % (941004)CaDiCaL version: 2.1.3 % 66.62/10.21 % (941004)Termination reason: Refutation not found, incomplete strategy % 66.62/10.21 % (941004)Time elapsed: 0.557 s % 66.62/10.21 % (941004)Peak memory usage: 128 MB % 66.62/10.21 % (941004)Instructions burned: 841 (million) % 66.62/10.21 % (941006)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=396524698:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2953 on theBenchmark for (2953ds/2479Mi) % 66.62/10.21 % (941006)Refutation not found, incomplete strategy % 66.62/10.21 % (941006)------------------------------ % 66.62/10.21 % (941006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.62/10.21 % (941006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/10.21 % (941006)CaDiCaL version: 2.1.3 % 66.62/10.21 % (941006)Termination reason: Refutation not found, incomplete strategy % 66.62/10.21 % (941006)Time elapsed: 0.001 s % 66.62/10.21 % (941006)Peak memory usage: 86 MB % 66.62/10.21 % (941004)------------------------------ % 66.62/10.21 % (941004)------------------------------ % 66.62/10.21 % (941006)------------------------------ % 66.62/10.21 % (941006)------------------------------ % 66.62/10.21 % (941008)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2838528213:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2949 on theBenchmark for (2949ds/440Mi) % 66.62/10.21 % (941009)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1883823339:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2948 on theBenchmark for (2948ds/11145Mi) % 66.62/10.21 % (941008)Instruction limit reached! % 66.62/10.21 % (941008)------------------------------ % 66.62/10.21 % (941008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.62/10.21 % (941008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.62/10.21 % (941008)CaDiCaL version: 2.1.3 % 66.62/10.21 % (941008)Termination reason: Instruction limit % 66.62/10.21 % (941008)Termination phase: Saturation % 66.62/10.21 % (941008)Time elapsed: 0.229 s % 66.62/10.21 % (941008)Peak memory usage: 93 MB % 66.62/10.21 % (941008)Instructions burned: 443 (million) % 66.62/10.21 % (941012)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=3207641161:cts=off:i=3034:av=off:er=known:fsd=on_2945 on theBenchmark for (2945ds/3034Mi) % 66.62/10.21 [W927 21:41:32.735152863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.62/10.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.62/10.21 [W927 21:41:32.735186154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.62/10.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.62/10.21 [W927 21:41:32.735223644 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.62/10.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.62/10.21 [W927 21:41:32.735250644 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.62/10.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.62/10.21 [W927 21:41:32.735277821 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735288625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735313219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735323462 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735347932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735358252 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735382386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 [W927 21:41:32.735392703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.29/10.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.29/10.61 % (941009)Refutation not found, incomplete strategy % 69.29/10.61 % (941009)------------------------------ % 69.29/10.61 % (941009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.29/10.61 % (941009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.29/10.61 % (941009)CaDiCaL version: 2.1.3 % 69.29/10.61 % (941009)Termination reason: Refutation not found, incomplete strategy % 69.29/10.61 % (941009)Time elapsed: 0.546 s % 69.29/10.61 % (941009)Peak memory usage: 125 MB % 69.29/10.61 % (941009)Instructions burned: 825 (million) % 69.29/10.61 % (940975)Instruction limit reached! % 69.29/10.61 % (940975)------------------------------ % 69.29/10.61 % (940975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.29/10.61 % (940975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.29/10.61 % (940975)CaDiCaL version: 2.1.3 % 69.29/10.61 % (940975)Termination reason: Instruction limit % 69.29/10.61 % (940975)Termination phase: Saturation % 69.29/10.61 % (940975)Time elapsed: 3.575 s % 69.29/10.61 % (940975)Peak memory usage: 169 MB % 69.29/10.61 % (940975)Instructions burned: 6061 (million) % 69.29/10.61 % (941009)------------------------------ % 69.29/10.61 % (941009)------------------------------ % 69.29/10.61 % (941014)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3020264271:st=2:s2a=on:i=524:s2at=2:ss=axioms_2940 on theBenchmark for (2940ds/524Mi) % 69.29/10.61 % (941014)Refutation not found, incomplete strategy % 69.29/10.61 % (941014)------------------------------ % 69.29/10.61 % (941014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.29/10.61 % (941014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.29/10.61 % (941014)CaDiCaL version: 2.1.3 % 69.29/10.61 % (941014)Termination reason: Refutation not found, incomplete strategy % 69.29/10.61 % (941014)Time elapsed: 0.001 s % 69.29/10.61 % (941014)Peak memory usage: 86 MB % 63.66/10.99 % (941015)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=299276897:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2939 on theBenchmark for (2939ds/1016Mi) % 63.66/10.99 % (941015)Refutation not found, incomplete strategy % 63.66/10.99 % (941015)------------------------------ % 63.66/10.99 % (941015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.66/10.99 % (941015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.66/10.99 % (941015)CaDiCaL version: 2.1.3 % 63.66/10.99 % (941015)Termination reason: Refutation not found, incomplete strategy % 63.66/10.99 % (941015)Time elapsed: 0.001 s % 63.66/10.99 % (941015)Peak memory usage: 86 MB % 63.66/10.99 % (941014)------------------------------ % 63.66/10.99 % (941014)------------------------------ % 63.66/10.99 % (941015)------------------------------ % 63.66/10.99 % (941015)------------------------------ % 63.66/10.99 % (941018)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2393556074:i=14123:bd=preordered:ins=4_2936 on theBenchmark for (2936ds/14123Mi) % 63.66/10.99 % (941019)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3883081080:i=5781:kws=precedence:bd=all:rawr=on_2935 on theBenchmark for (2935ds/5781Mi) % 63.66/10.99 % (941012)Instruction limit reached! % 63.66/10.99 % (941012)------------------------------ % 63.66/10.99 % (941012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.66/10.99 % (941012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.66/10.99 % (941012)CaDiCaL version: 2.1.3 % 63.66/10.99 % (941012)Termination reason: Instruction limit % 63.66/10.99 % (941012)Termination phase: Saturation % 63.66/10.99 % (941012)Time elapsed: 1.650 s % 63.66/10.99 % (941012)Peak memory usage: 136 MB % 63.66/10.99 % (941012)Instructions burned: 3034 (million) % 63.66/10.99 % (941022)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=3048547704:i=2448:gtgl=5:bd=preordered:gtg=all_2927 on theBenchmark for (2927ds/2448Mi) % 63.66/10.99 % (940980)Instruction limit reached! % 63.66/10.99 % (940980)------------------------------ % 63.66/10.99 % (940980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.66/10.99 % (940980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.66/10.99 % (940980)CaDiCaL version: 2.1.3 % 63.66/10.99 % (940980)Termination reason: Instruction limit % 63.66/10.99 % (940980)Termination phase: Saturation % 63.66/10.99 % (940980)Time elapsed: 6.156 s % 63.66/10.99 % (940980)Peak memory usage: 139 MB % 63.66/10.99 % (940980)Instructions burned: 14156 (million) % 63.66/10.99 % (941022)Instruction limit reached! % 63.66/10.99 % (941022)------------------------------ % 63.66/10.99 % (941022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.66/10.99 % (941022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.66/10.99 % (941022)CaDiCaL version: 2.1.3 % 63.66/10.99 % (941022)Termination reason: Instruction limit % 63.66/10.99 % (941022)Termination phase: Saturation % 63.66/10.99 % (941022)Time elapsed: 1.424 s % 63.66/10.99 % (941022)Peak memory usage: 140 MB % 63.66/10.99 % (941022)Instructions burned: 2449 (million) % 63.66/10.99 % (941024)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3442845426:i=3223:kws=precedence:fgj=on:av=off_2912 on theBenchmark for (2912ds/3223Mi) % 63.66/10.99 % (941025)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1292063614:st=5.6:i=2033:sd=3:ss=axioms_2911 on theBenchmark for (2911ds/2033Mi) % 63.66/10.99 [W927 21:41:36.456863395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.66/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.66/10.99 [W927 21:41:36.456900213 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.66/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.66/10.99 [W927 21:41:36.456936263 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.456948010 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.456977220 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457064288 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457105112 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457116592 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457141805 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457152189 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457176326 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 [W927 21:41:36.457186709 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/11.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.23/11.19 % (941025)Refutation not found, incomplete strategy % 73.23/11.19 % (941025)------------------------------ % 73.23/11.19 % (941025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.19 % (941025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.19 % (941025)CaDiCaL version: 2.1.3 % 73.23/11.19 % (941025)Termination reason: Refutation not found, incomplete strategy % 73.23/11.19 % (941025)Time elapsed: 0.547 s % 73.23/11.19 % (941025)Peak memory usage: 125 MB % 73.23/11.19 % (941025)Instructions burned: 823 (million) % 73.23/11.19 % (941019)Instruction limit reached! % 73.23/11.19 % (941019)------------------------------ % 73.23/11.19 % (941019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.23/11.19 % (941019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.23/11.19 % (941019)CaDiCaL version: 2.1.3 % 73.23/11.19 % (941019)Termination reason: Instruction limit % 73.23/11.19 % (941019)Termination phase: Saturation % 73.23/11.19 % (941019)Time elapsed: 2.929 s % 73.23/11.19 % (941019)Peak memory usage: 112 MB % 73.23/11.19 % (941019)Instructions burned: 5783 (million) % 73.23/11.19 % (941028)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1289595460:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2904 on theBenchmark for (2904ds/2055Mi) % 77.67/11.98 % (941025)------------------------------ % 77.67/11.98 % (941025)------------------------------ % 77.67/11.98 % (941030)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=3688940274:i=21611:sd=3:ss=axioms_2902 on theBenchmark for (2902ds/21611Mi) % 77.67/11.98 % (940990)Instruction limit reached! % 77.67/11.98 % (940990)------------------------------ % 77.67/11.98 % (940990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.67/11.98 % (940990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.67/11.98 % (940990)CaDiCaL version: 2.1.3 % 77.67/11.98 % (940990)Termination reason: Instruction limit % 77.67/11.98 % (940990)Termination phase: Saturation % 77.67/11.98 % (940990)Time elapsed: 6.957 s % 77.67/11.98 % (940990)Peak memory usage: 214 MB % 77.67/11.98 % (940990)Instructions burned: 12113 (million) % 77.67/11.98 [W927 21:41:37.238075306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238109553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238146224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238158484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238185427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238196714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238221938 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238233018 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238257628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238268735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.67/11.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.67/11.98 [W927 21:41:37.238293112 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.238304192 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 % (941032)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1102068985:i=4835:sd=13:ss=axioms:sgt=23_2899 on theBenchmark for (2899ds/4835Mi) % 87.28/13.16 % (941032)Refutation not found, incomplete strategy % 87.28/13.16 % (941032)------------------------------ % 87.28/13.16 % (941032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.28/13.16 % (941032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.28/13.16 % (941032)CaDiCaL version: 2.1.3 % 87.28/13.16 % (941032)Termination reason: Refutation not found, incomplete strategy % 87.28/13.16 % (941032)Time elapsed: 0.001 s % 87.28/13.16 % (941032)Peak memory usage: 86 MB % 87.28/13.16 % (941028)Refutation not found, incomplete strategy % 87.28/13.16 % (941028)------------------------------ % 87.28/13.16 % (941028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.28/13.16 % (941028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.28/13.16 % (941028)CaDiCaL version: 2.1.3 % 87.28/13.16 % (941028)Termination reason: Refutation not found, incomplete strategy % 87.28/13.16 % (941028)Time elapsed: 0.550 s % 87.28/13.16 % (941028)Peak memory usage: 126 MB % 87.28/13.16 % (941028)Instructions burned: 826 (million) % 87.28/13.16 [W927 21:41:37.439671390 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439719510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439758004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439769111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439793915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439805668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439830242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.28/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.28/13.16 [W927 21:41:37.439842032 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.33/13.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.33/13.94 [W927 21:41:37.439866939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.33/13.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.33/13.94 [W927 21:41:37.439877152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.33/13.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.33/13.94 [W927 21:41:37.439901149 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.33/13.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.33/13.94 [W927 21:41:37.439911016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.33/13.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.33/13.94 % (941032)------------------------------ % 92.33/13.94 % (941032)------------------------------ % 92.33/13.94 % (941030)Refutation not found, incomplete strategy % 92.33/13.94 % (941030)------------------------------ % 92.33/13.94 % (941030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.33/13.94 % (941030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.33/13.94 % (941030)CaDiCaL version: 2.1.3 % 92.33/13.94 % (941030)Termination reason: Refutation not found, incomplete strategy % 92.33/13.94 % (941030)Time elapsed: 0.552 s % 92.33/13.94 % (941030)Peak memory usage: 125 MB % 92.33/13.94 % (941030)Instructions burned: 825 (million) % 92.33/13.94 % (941028)------------------------------ % 92.33/13.94 % (941028)------------------------------ % 92.33/13.94 % (941034)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=1451541923:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2895 on theBenchmark for (2895ds/797Mi) % 92.33/13.94 % (941035)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2647515781:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2894 on theBenchmark for (2894ds/2326Mi) % 92.33/13.94 % (941035)Refutation not found, incomplete strategy % 92.33/13.94 % (941035)------------------------------ % 92.33/13.94 % (941035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.33/13.94 % (941035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.33/13.94 % (941035)CaDiCaL version: 2.1.3 % 92.33/13.94 % (941035)Termination reason: Refutation not found, incomplete strategy % 92.33/13.94 % (941035)Time elapsed: 0.004 s % 92.33/13.94 % (941035)Peak memory usage: 88 MB % 92.33/13.94 % (941035)Instructions burned: 7 (million) % 92.33/13.94 % (941030)------------------------------ % 92.33/13.94 % (941030)------------------------------ % 92.33/13.94 % (941038)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2123915494:i=6038:nm=6_2892 on theBenchmark for (2892ds/6038Mi) % 92.33/13.94 % (941035)------------------------------ % 92.33/13.94 % (941035)------------------------------ % 92.33/13.94 % (941024)Instruction limit reached! % 92.33/13.94 % (941024)------------------------------ % 92.33/13.94 % (941024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.33/13.94 % (941024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.33/13.94 % (941024)CaDiCaL version: 2.1.3 % 92.33/13.94 % (941024)Termination reason: Instruction limit % 92.33/13.94 % (941024)Termination phase: Saturation % 92.33/13.94 % (941024)Time elapsed: 2.046 s % 92.33/13.94 % (941024)Peak memory usage: 147 MB % 92.33/13.94 % (941024)Instructions burned: 3224 (million) % 92.33/13.94 % (941040)lrs+10_1_sil=32000:sp=occurrence:random_seed=3106937922:st=2:i=33334:sd=3:ss=included:sgt=32_2890 on theBenchmark for (2890ds/33334Mi) % 92.33/13.94 % (941034)Instruction limit reached! % 92.33/13.94 % (941034)------------------------------ % 92.33/13.94 % (941034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.87/15.87 % (941034)CaDiCaL version: 2.1.3 % 105.87/15.87 % (941034)Termination reason: Instruction limit % 105.87/15.87 % (941034)Termination phase: Saturation % 105.87/15.87 % (941034)Time elapsed: 0.504 s % 105.87/15.87 % (941034)Peak memory usage: 94 MB % 105.87/15.87 % (941034)Instructions burned: 797 (million) % 105.87/15.87 % (941041)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4165459990:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2890 on theBenchmark for (2890ds/1008Mi) % 105.87/15.87 % (941041)Refutation not found, incomplete strategy % 105.87/15.87 % (941041)------------------------------ % 105.87/15.87 % (941041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.87/15.87 % (941041)CaDiCaL version: 2.1.3 % 105.87/15.87 % (941041)Termination reason: Refutation not found, incomplete strategy % 105.87/15.87 % (941041)Time elapsed: 0.001 s % 105.87/15.87 % (941041)Peak memory usage: 86 MB % 105.87/15.87 % (941043)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=2788632332:i=8327:s2at=5:bd=preordered_2888 on theBenchmark for (2888ds/8327Mi) % 105.87/15.87 % (941041)------------------------------ % 105.87/15.87 % (941041)------------------------------ % 105.87/15.87 % (941038)Refutation not found, incomplete strategy % 105.87/15.87 % (941038)------------------------------ % 105.87/15.87 % (941038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.87/15.87 % (941038)CaDiCaL version: 2.1.3 % 105.87/15.87 % (941038)Termination reason: Refutation not found, incomplete strategy % 105.87/15.87 % (941038)Time elapsed: 0.570 s % 105.87/15.87 % (941038)Peak memory usage: 128 MB % 105.87/15.87 % (941038)Instructions burned: 846 (million) % 105.87/15.87 % (941046)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=507903924:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2885 on theBenchmark for (2885ds/1083Mi) % 105.87/15.87 % (941038)------------------------------ % 105.87/15.87 % (941038)------------------------------ % 105.87/15.87 % (941048)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2105886374:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2882 on theBenchmark for (2882ds/1084Mi) % 105.87/15.87 % (941048)Refutation not found, incomplete strategy % 105.87/15.87 % (941048)------------------------------ % 105.87/15.87 % (941048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.87/15.87 % (941048)CaDiCaL version: 2.1.3 % 105.87/15.87 % (941048)Termination reason: Refutation not found, incomplete strategy % 105.87/15.87 % (941048)Time elapsed: 0.0000 s % 105.87/15.87 % (941048)Peak memory usage: 86 MB % 105.87/15.87 % (941046)Instruction limit reached! % 105.87/15.87 % (941046)------------------------------ % 105.87/15.87 % (941046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.87/15.87 % (941046)CaDiCaL version: 2.1.3 % 105.87/15.87 % (941046)Termination reason: Instruction limit % 105.87/15.87 % (941046)Termination phase: Saturation % 105.87/15.87 % (941046)Time elapsed: 0.511 s % 105.87/15.87 % (941046)Peak memory usage: 99 MB % 105.87/15.87 % (941046)Instructions burned: 1084 (million) % 105.87/15.87 % (941048)------------------------------ % 105.87/15.87 % (941048)------------------------------ % 105.87/15.87 % (941050)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=17092095:i=6995:s2at=5:gtg=all_2879 on theBenchmark for (2879ds/6995Mi) % 105.87/15.87 % (941051)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2611520793:st=2:i=6225:sd=15:ss=axioms_2878 on theBenchmark for (2878ds/6225Mi) % 105.87/15.87 % (941051)Refutation not found, incomplete strategy % 105.87/15.87 % (941051)------------------------------ % 105.87/15.87 % (941051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.87/15.87 % (941051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.50/16.83 % (941051)CaDiCaL version: 2.1.3 % 112.50/16.83 % (941051)Termination reason: Refutation not found, incomplete strategy % 112.50/16.83 % (941051)Time elapsed: 0.001 s % 112.50/16.83 % (941051)Peak memory usage: 86 MB % 112.50/16.83 % (941051)------------------------------ % 112.50/16.83 % (941051)------------------------------ % 112.50/16.83 % (941054)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2902034268:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2874 on theBenchmark for (2874ds/3372Mi) % 112.50/16.83 [W927 21:41:39.188825033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188863477 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188900018 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188911755 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188937928 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188949682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188974375 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.188985569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.189022946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.189034799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.189060610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.50/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.50/16.83 [W927 21:41:39.189071693 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.21/17.25 % (941054)Refutation not found, incomplete strategy % 116.21/17.25 % (941054)------------------------------ % 116.21/17.25 % (941054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.21/17.25 % (941054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.21/17.25 % (941054)CaDiCaL version: 2.1.3 % 116.21/17.25 % (941054)Termination reason: Refutation not found, incomplete strategy % 116.21/17.25 % (941054)Time elapsed: 0.545 s % 116.21/17.25 % (941054)Peak memory usage: 126 MB % 116.21/17.25 % (941054)Instructions burned: 825 (million) % 116.21/17.25 % (941054)------------------------------ % 116.21/17.25 % (941054)------------------------------ % 116.21/17.25 % (941018)Instruction limit reached! % 116.21/17.25 % (941018)------------------------------ % 116.21/17.25 % (941018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.21/17.25 % (941018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.21/17.25 % (941018)CaDiCaL version: 2.1.3 % 116.21/17.25 % (941018)Termination reason: Instruction limit % 116.21/17.25 % (941018)Termination phase: Saturation % 116.21/17.25 % (941018)Time elapsed: 7.137 s % 116.21/17.25 % (941018)Peak memory usage: 166 MB % 116.21/17.25 % (941018)Instructions burned: 14124 (million) % 116.21/17.25 % (941056)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1610865192:st=2.3:i=26457:sd=10:ss=included:sgt=8_2864 on theBenchmark for (2864ds/26457Mi) % 116.21/17.25 % (941057)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=4213234896:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2863 on theBenchmark for (2863ds/13494Mi) % 116.21/17.25 % (941056)Refutation not found, incomplete strategy % 116.21/17.25 % (941056)------------------------------ % 116.21/17.25 % (941056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.21/17.25 % (941056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.21/17.25 % (941056)CaDiCaL version: 2.1.3 % 116.21/17.25 % (941056)Termination reason: Refutation not found, incomplete strategy % 116.21/17.25 % (941056)Time elapsed: 0.561 s % 116.21/17.25 % (941056)Peak memory usage: 128 MB % 116.21/17.25 % (941056)Instructions burned: 841 (million) % 116.21/17.25 % (941056)------------------------------ % 116.21/17.25 % (941056)------------------------------ % 116.21/17.25 % (941060)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=3687906504:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2855 on theBenchmark for (2855ds/2503Mi) % 116.21/17.25 [W927 21:41:41.125644545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.21/17.25 [W927 21:41:41.125687538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.21/17.25 [W927 21:41:41.125724499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.21/17.25 [W927 21:41:41.125742372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.21/17.25 [W927 21:41:41.125767156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.21/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125778619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125817900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125838710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125864854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125875671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125900084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:41.125909998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 % (941060)Refutation not found, incomplete strategy % 126.38/18.76 % (941060)------------------------------ % 126.38/18.76 % (941060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.38/18.76 % (941060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.38/18.76 % (941060)CaDiCaL version: 2.1.3 % 126.38/18.76 % (941060)Termination reason: Refutation not found, incomplete strategy % 126.38/18.76 % (941060)Time elapsed: 0.551 s % 126.38/18.76 % (941060)Peak memory usage: 126 MB % 126.38/18.76 % (941060)Instructions burned: 825 (million) % 126.38/18.76 % (941060)------------------------------ % 126.38/18.76 % (941060)------------------------------ % 126.38/18.76 % (941043)Instruction limit reached! % 126.38/18.76 % (941043)------------------------------ % 126.38/18.76 % (941043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.38/18.76 % (941043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.38/18.76 % (941043)CaDiCaL version: 2.1.3 % 126.38/18.76 % (941043)Termination reason: Instruction limit % 126.38/18.76 % (941043)Termination phase: Saturation % 126.38/18.76 % (941043)Time elapsed: 4.255 s % 126.38/18.76 % (941043)Peak memory usage: 143 MB % 126.38/18.76 % (941043)Instructions burned: 8329 (million) % 126.38/18.76 % (941062)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3960170209:i=2559:sd=1:ep=RSTC:ss=axioms_2845 on theBenchmark for (2845ds/2559Mi) % 126.38/18.76 % (941063)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1835925801:i=30753:av=off:ss=included_2844 on theBenchmark for (2844ds/30753Mi) % 126.38/18.76 [W927 21:41:42.086189109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.38/18.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.38/18.76 [W927 21:41:42.086223400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086260690 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086272507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086297234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086308004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086332574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086343251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086367065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086377902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086402025 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 [W927 21:41:42.086412822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.43/19.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.43/19.71 % (941062)Refutation not found, incomplete strategy % 133.43/19.71 % (941062)------------------------------ % 133.43/19.71 % (941062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.43/19.71 % (941062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.43/19.71 % (941062)CaDiCaL version: 2.1.3 % 133.43/19.71 % (941062)Termination reason: Refutation not found, incomplete strategy % 133.43/19.71 % (941062)Time elapsed: 0.544 s % 133.43/19.71 % (941062)Peak memory usage: 125 MB % 133.43/19.71 % (941062)Instructions burned: 825 (million) % 133.43/19.71 % (941050)Instruction limit reached! % 133.43/19.71 % (941050)------------------------------ % 133.43/19.71 % (941050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.43/19.71 % (941050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.83/20.68 % (941050)CaDiCaL version: 2.1.3 % 139.83/20.68 % (941050)Termination reason: Instruction limit % 139.83/20.68 % (941050)Termination phase: Saturation % 139.83/20.68 % (941050)Time elapsed: 4.149 s % 139.83/20.68 % (941050)Peak memory usage: 170 MB % 139.83/20.68 % (941050)Instructions burned: 6997 (million) % 139.83/20.68 % (941062)------------------------------ % 139.83/20.68 % (941062)------------------------------ % 139.83/20.68 % (941066)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=4202334882:i=26473:ep=RSTC_2835 on theBenchmark for (2835ds/26473Mi) % 139.83/20.68 % (941067)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=3516245323:cts=off:i=2759:kws=inv_arity:fgj=on_2835 on theBenchmark for (2835ds/2759Mi) % 139.83/20.68 % (941067)Refutation not found, incomplete strategy % 139.83/20.68 % (941067)------------------------------ % 139.83/20.68 % (941067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.83/20.68 % (941067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.83/20.68 % (941067)CaDiCaL version: 2.1.3 % 139.83/20.68 % (941067)Termination reason: Refutation not found, incomplete strategy % 139.83/20.68 % (941067)Time elapsed: 0.562 s % 139.83/20.68 % (941067)Peak memory usage: 128 MB % 139.83/20.68 % (941067)Instructions burned: 846 (million) % 139.83/20.68 % (941067)------------------------------ % 139.83/20.68 % (941067)------------------------------ % 139.83/20.68 % (941070)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=2420770526:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2826 on theBenchmark for (2826ds/5665Mi) % 139.83/20.68 [W927 21:41:44.015079369 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015113673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015151210 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015162487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015186553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015211180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015236874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.83/20.68 [W927 21:41:44.015246978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.83/20.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:44.015271114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:44.015281168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:44.015304698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:44.015317168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 % (941070)Refutation not found, incomplete strategy % 146.91/21.64 % (941070)------------------------------ % 146.91/21.64 % (941070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.91/21.64 % (941070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.91/21.64 % (941070)CaDiCaL version: 2.1.3 % 146.91/21.64 % (941070)Termination reason: Refutation not found, incomplete strategy % 146.91/21.64 % (941070)Time elapsed: 0.546 s % 146.91/21.64 % (941070)Peak memory usage: 125 MB % 146.91/21.64 % (941070)Instructions burned: 825 (million) % 146.91/21.64 % (941070)------------------------------ % 146.91/21.64 % (941070)------------------------------ % 146.91/21.64 % (941072)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=3110720346:i=1532:ep=RS:ss=axioms_2816 on theBenchmark for (2816ds/1532Mi) % 146.91/21.64 [W927 21:41:45.961871293 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.961907480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.961942900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.961956380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.961981201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.961992801 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.91/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.91/21.64 [W927 21:41:45.962029024 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:45.962041191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:45.962070178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:45.962080005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:45.962103322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:45.962113159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 % (941072)Refutation not found, incomplete strategy % 148.11/21.81 % (941072)------------------------------ % 148.11/21.81 % (941072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.11/21.81 % (941072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.11/21.81 % (941072)CaDiCaL version: 2.1.3 % 148.11/21.81 % (941072)Termination reason: Refutation not found, incomplete strategy % 148.11/21.81 % (941072)Time elapsed: 0.545 s % 148.11/21.81 % (941072)Peak memory usage: 125 MB % 148.11/21.81 % (941072)Instructions burned: 825 (million) % 148.11/21.81 % (941072)------------------------------ % 148.11/21.81 % (941072)------------------------------ % 148.11/21.81 % (941074)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3630427015:i=1565:sd=2:ss=axioms:sgt=32_2807 on theBenchmark for (2807ds/1565Mi) % 148.11/21.81 % (941057)Instruction limit reached! % 148.11/21.81 % (941057)------------------------------ % 148.11/21.81 % (941057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.11/21.81 % (941057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.11/21.81 % (941057)CaDiCaL version: 2.1.3 % 148.11/21.81 % (941057)Termination reason: Instruction limit % 148.11/21.81 % (941057)Termination phase: Saturation % 148.11/21.81 % (941057)Time elapsed: 5.863 s % 148.11/21.81 % (941057)Peak memory usage: 143 MB % 148.11/21.81 % (941057)Instructions burned: 13494 (million) % 148.11/21.81 [W927 21:41:46.929013420 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:46.929050193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:46.929087140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.11/21.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.11/21.81 [W927 21:41:46.929100007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929127334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929137474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929162265 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929172701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929195945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929205792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929231029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:46.929252392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 % (941076)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=1870435261:i=1572:fgj=on:gsp=on_2803 on theBenchmark for (2803ds/1572Mi) % 153.99/22.62 % (941074)Refutation not found, incomplete strategy % 153.99/22.62 % (941074)------------------------------ % 153.99/22.62 % (941074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.99/22.62 % (941074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.99/22.62 % (941074)CaDiCaL version: 2.1.3 % 153.99/22.62 % (941074)Termination reason: Refutation not found, incomplete strategy % 153.99/22.62 % (941074)Time elapsed: 0.548 s % 153.99/22.62 % (941074)Peak memory usage: 125 MB % 153.99/22.62 % (941074)Instructions burned: 825 (million) % 153.99/22.62 % (941074)------------------------------ % 153.99/22.62 % (941074)------------------------------ % 153.99/22.62 % (941078)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=565214554:i=6052:sd=4:ss=axioms:sgt=24_2797 on theBenchmark for (2797ds/6052Mi) % 153.99/22.62 [W927 21:41:47.894185190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.99/22.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.99/22.62 [W927 21:41:47.894220380 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894257201 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894268347 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894293218 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894303448 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894327175 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894337055 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894359952 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894369889 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894392915 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 [W927 21:41:47.894402909 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.42/23.58 % (941076)Instruction limit reached! % 160.42/23.58 % (941076)------------------------------ % 160.42/23.58 % (941076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.42/23.58 % (941076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.42/23.58 % (941076)CaDiCaL version: 2.1.3 % 160.42/23.58 % (941076)Termination reason: Instruction limit % 160.42/23.58 % (941076)Termination phase: Saturation % 160.42/23.58 % (941076)Time elapsed: 1.024 s % 160.42/23.58 % (941076)Peak memory usage: 135 MB % 160.42/23.58 % (941076)Instructions burned: 1572 (million) % 160.42/23.58 % (941078)Refutation not found, incomplete strategy % 160.42/23.58 % (941078)------------------------------ % 160.42/23.58 % (941078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.42/23.58 % (941078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.79/29.01 % (941078)CaDiCaL version: 2.1.3 % 198.79/29.01 % (941078)Termination reason: Refutation not found, incomplete strategy % 198.79/29.01 % (941078)Time elapsed: 0.545 s % 198.79/29.01 % (941078)Peak memory usage: 125 MB % 198.79/29.01 % (941078)Instructions burned: 821 (million) % 198.79/29.01 % (941080)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=1094071217:i=3500:sd=1:bd=preordered:sup=off:ss=included_2791 on theBenchmark for (2791ds/3500Mi) % 198.79/29.01 % (941078)------------------------------ % 198.79/29.01 % (941078)------------------------------ % 198.79/29.01 % (941082)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=660314233:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2787 on theBenchmark for (2787ds/1842Mi) % 198.79/29.01 % (941080)Refutation not found, incomplete strategy % 198.79/29.01 % (941080)------------------------------ % 198.79/29.01 % (941080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.79/29.01 % (941080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.79/29.01 % (941080)CaDiCaL version: 2.1.3 % 198.79/29.01 % (941080)Termination reason: Refutation not found, incomplete strategy % 198.79/29.01 % (941080)Time elapsed: 0.566 s % 198.79/29.01 % (941080)Peak memory usage: 128 MB % 198.79/29.01 % (941080)Instructions burned: 844 (million) % 198.79/29.01 [W927 21:41:48.871064570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871102144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871140361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871152968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871180445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871191678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871216335 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871226315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 198.79/29.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 198.79/29.01 [W927 21:41:48.871249909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:48.871270172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:48.871295279 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:48.871305109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 % (941080)------------------------------ % 200.89/29.18 % (941080)------------------------------ % 200.89/29.18 % (941082)Refutation not found, incomplete strategy % 200.89/29.18 % (941082)------------------------------ % 200.89/29.18 % (941082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.89/29.18 % (941082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.89/29.18 % (941082)CaDiCaL version: 2.1.3 % 200.89/29.18 % (941082)Termination reason: Refutation not found, incomplete strategy % 200.89/29.18 % (941082)Time elapsed: 0.546 s % 200.89/29.18 % (941082)Peak memory usage: 125 MB % 200.89/29.18 % (941082)Instructions burned: 822 (million) % 200.89/29.18 % (941084)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1754567175:i=66096:add=on_2781 on theBenchmark for (2781ds/66096Mi) % 200.89/29.18 % (941082)------------------------------ % 200.89/29.18 % (941082)------------------------------ % 200.89/29.18 % (941086)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3585187354:i=1884:sd=1:nm=60:ss=axioms_2778 on theBenchmark for (2778ds/1884Mi) % 200.89/29.18 [W927 21:41:49.828423446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828457484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828494157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828507284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828533914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828545385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.89/29.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.89/29.18 [W927 21:41:49.828570912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 [W927 21:41:49.828582675 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 [W927 21:41:49.828606612 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 [W927 21:41:49.828616699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 [W927 21:41:49.828640422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 [W927 21:41:49.828650926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.15/33.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.15/33.44 % (941086)Refutation not found, incomplete strategy % 231.15/33.44 % (941086)------------------------------ % 231.15/33.44 % (941086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.15/33.44 % (941086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.15/33.44 % (941086)CaDiCaL version: 2.1.3 % 231.15/33.44 % (941086)Termination reason: Refutation not found, incomplete strategy % 231.15/33.44 % (941086)Time elapsed: 0.544 s % 231.15/33.44 % (941086)Peak memory usage: 125 MB % 231.15/33.44 % (941086)Instructions burned: 825 (million) % 231.15/33.44 % (941086)------------------------------ % 231.15/33.44 % (941086)------------------------------ % 231.15/33.44 % (941088)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3637468975:cts=off:i=5469:bs=on:fsr=off_2768 on theBenchmark for (2768ds/5469Mi) % 231.15/33.44 % (941088)Instruction limit reached! % 231.15/33.44 % (941088)------------------------------ % 231.15/33.44 % (941088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.15/33.44 % (941088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.15/33.44 % (941088)CaDiCaL version: 2.1.3 % 231.15/33.44 % (941088)Termination reason: Instruction limit % 231.15/33.44 % (941088)Termination phase: Saturation % 231.15/33.44 % (941088)Time elapsed: 2.959 s % 231.15/33.44 % (941088)Peak memory usage: 108 MB % 231.15/33.44 % (941088)Instructions burned: 5471 (million) % 231.15/33.44 % (941090)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=2291008161:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2737 on theBenchmark for (2737ds/2037Mi) % 231.15/33.44 % (941090)Instruction limit reached! % 231.15/33.44 % (941090)------------------------------ % 231.15/33.44 % (941090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.15/33.44 % (941090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.15/33.44 % (941090)CaDiCaL version: 2.1.3 % 231.15/33.44 % (941090)Termination reason: Instruction limit % 231.15/33.44 % (941090)Termination phase: Saturation % 231.15/33.44 % (941090)Time elapsed: 1.185 s % 231.15/33.44 % (941090)Peak memory usage: 135 MB % 231.15/33.44 % (941090)Instructions burned: 2039 (million) % 231.15/33.44 % (941092)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4273824261:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2723 on theBenchmark for (2723ds/2110Mi) % 231.15/33.44 [W927 21:41:55.257636201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257680495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257719089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257730826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257755633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257765546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.02 [W927 21:41:55.257789976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 [W927 21:41:55.257800266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 [W927 21:41:55.257824217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 [W927 21:41:55.257834190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 [W927 21:41:55.257857900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 [W927 21:41:55.257867751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.67/34.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.67/34.03 % (941092)Refutation not found, incomplete strategy % 234.67/34.03 % (941092)------------------------------ % 234.67/34.03 % (941092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.67/34.03 % (941092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.67/34.03 % (941092)CaDiCaL version: 2.1.3 % 234.67/34.03 % (941092)Termination reason: Refutation not found, incomplete strategy % 234.67/34.03 % (941092)Time elapsed: 0.547 s % 234.67/34.03 % (941092)Peak memory usage: 125 MB % 234.67/34.03 % (941092)Instructions burned: 825 (million) % 258.10/37.21 % (941092)------------------------------ % 258.10/37.21 % (941092)------------------------------ % 258.10/37.21 % (941094)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=2307882200:i=2430:add=off:aac=none:nm=16_2714 on theBenchmark for (2714ds/2430Mi) % 258.10/37.21 % (941094)Instruction limit reached! % 258.10/37.21 % (941094)------------------------------ % 258.10/37.21 % (941094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.10/37.21 % (941094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.10/37.21 % (941094)CaDiCaL version: 2.1.3 % 258.10/37.21 % (941094)Termination reason: Instruction limit % 258.10/37.21 % (941094)Termination phase: Saturation % 258.10/37.21 % (941094)Time elapsed: 1.502 s % 258.10/37.21 % (941094)Peak memory usage: 140 MB % 258.10/37.21 % (941094)Instructions burned: 2431 (million) % 258.10/37.21 % (941040)Instruction limit reached! % 258.10/37.21 % (941040)------------------------------ % 258.10/37.21 % (941040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.10/37.21 % (941040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.10/37.21 % (941040)CaDiCaL version: 2.1.3 % 258.10/37.21 % (941040)Termination reason: Instruction limit % 258.10/37.21 % (941040)Termination phase: Saturation % 258.10/37.21 % (941040)Time elapsed: 19.120 s % 258.10/37.21 % (941040)Peak memory usage: 224 MB % 258.10/37.21 % (941040)Instructions burned: 33334 (million) % 258.10/37.21 % (941096)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=1488009296:cond=fast:i=4891_2697 on theBenchmark for (2697ds/4891Mi) % 258.10/37.21 % (941097)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=2587970251:st=2:i=14845:sd=2:ss=included:fsd=on_2697 on theBenchmark for (2697ds/14845Mi) % 258.10/37.21 % (941097)Refutation not found, incomplete strategy % 258.10/37.21 % (941097)------------------------------ % 258.10/37.21 % (941097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.10/37.21 % (941097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.10/37.21 % (941097)CaDiCaL version: 2.1.3 % 258.10/37.21 % (941097)Termination reason: Refutation not found, incomplete strategy % 258.10/37.21 % (941097)Time elapsed: 0.560 s % 258.10/37.21 % (941097)Peak memory usage: 128 MB % 258.10/37.21 % (941097)Instructions burned: 840 (million) % 258.10/37.21 % (941097)------------------------------ % 258.10/37.21 % (941097)------------------------------ % 258.10/37.21 % (941100)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3157387535:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2687 on theBenchmark for (2687ds/7534Mi) % 258.10/37.21 % (941066)Instruction limit reached! % 258.10/37.21 % (941066)------------------------------ % 258.10/37.21 % (941066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.10/37.21 % (941066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.10/37.21 % (941066)CaDiCaL version: 2.1.3 % 258.10/37.21 % (941066)Termination reason: Instruction limit % 258.10/37.21 % (941066)Termination phase: Saturation % 258.10/37.21 % (941066)Time elapsed: 15.422 s % 258.10/37.21 % (941066)Peak memory usage: 549 MB % 258.10/37.21 % (941066)Instructions burned: 26473 (million) % 258.10/37.21 % (941102)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=2144226721:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2679 on theBenchmark for (2679ds/10353Mi) % 258.10/37.21 [W927 21:41:59.687041488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.10/37.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.10/37.21 [W927 21:41:59.687075899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.10/37.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.10/37.21 [W927 21:41:59.687114189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687125633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687151106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687172756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687200197 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687211100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687234434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687245131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687269391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 [W927 21:41:59.687280384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 261.59/37.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 261.59/37.79 % (941102)Refutation not found, incomplete strategy % 261.59/37.79 % (941102)------------------------------ % 261.59/37.79 % (941102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.59/37.79 % (941102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.79 % (941102)CaDiCaL version: 2.1.3 % 261.59/37.79 % (941102)Termination reason: Refutation not found, incomplete strategy % 261.59/37.79 % (941102)Time elapsed: 0.550 s % 261.59/37.79 % (941102)Peak memory usage: 125 MB % 261.59/37.79 % (941102)Instructions burned: 825 (million) % 261.59/37.79 % (941102)------------------------------ % 261.59/37.79 % (941102)------------------------------ % 261.59/37.79 % (941104)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3073702512:i=7860_2669 on theBenchmark for (2669ds/7860Mi) % 261.59/37.79 % (941104)Refutation not found, incomplete strategy % 261.59/37.79 % (941104)------------------------------ % 261.59/37.79 % (941104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.59/37.79 % (941104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.73/38.17 % (941104)CaDiCaL version: 2.1.3 % 262.73/38.17 % (941104)Termination reason: Refutation not found, incomplete strategy % 262.73/38.17 % (941104)Time elapsed: 0.005 s % 262.73/38.17 % (941104)Peak memory usage: 88 MB % 262.73/38.17 % (941104)Instructions burned: 6 (million) % 262.73/38.17 % (941096)Instruction limit reached! % 262.73/38.17 % (941096)------------------------------ % 262.73/38.17 % (941096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.73/38.17 % (941096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.73/38.17 % (941096)CaDiCaL version: 2.1.3 % 262.73/38.17 % (941096)Termination reason: Instruction limit % 262.73/38.17 % (941096)Termination phase: Saturation % 262.73/38.17 % (941096)Time elapsed: 2.980 s % 262.73/38.17 % (941096)Peak memory usage: 159 MB % 262.73/38.17 % (941096)Instructions burned: 4891 (million) % 262.73/38.17 % (941104)------------------------------ % 262.73/38.17 % (941104)------------------------------ % 262.73/38.17 % (941106)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=182141287:i=7896:sd=2:bs=on:ss=included:sgt=20_2666 on theBenchmark for (2666ds/7896Mi) % 262.73/38.17 % (941107)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3034456407:i=5812:gtgl=2:gtg=all_2665 on theBenchmark for (2665ds/5812Mi) % 262.73/38.17 % (941063)Instruction limit reached! % 262.73/38.17 % (941063)------------------------------ % 262.73/38.17 % (941063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.73/38.17 % (941063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.73/38.17 % (941063)CaDiCaL version: 2.1.3 % 262.73/38.17 % (941063)Termination reason: Instruction limit % 262.73/38.17 % (941063)Termination phase: Saturation % 262.73/38.17 % (941063)Time elapsed: 18.568 s % 262.73/38.17 % (941063)Peak memory usage: 267 MB % 262.73/38.17 % (941063)Instructions burned: 30753 (million) % 262.73/38.17 % (941110)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=1515025259:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2656 on theBenchmark for (2656ds/2965Mi) % 262.73/38.17 % (941110)Refutation not found, incomplete strategy % 262.73/38.17 % (941110)------------------------------ % 262.73/38.17 % (941110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.73/38.17 % (941110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.73/38.17 % (941110)CaDiCaL version: 2.1.3 % 262.73/38.17 % (941110)Termination reason: Refutation not found, incomplete strategy % 262.73/38.17 % (941110)Time elapsed: 0.558 s % 262.73/38.17 % (941110)Peak memory usage: 128 MB % 262.73/38.17 % (941110)Instructions burned: 844 (million) % 262.73/38.17 % (941110)------------------------------ % 262.73/38.17 % (941110)------------------------------ % 262.73/38.17 % (941112)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=2509238827:i=2967:kws=precedence:bd=preordered:av=off_2646 on theBenchmark for (2646ds/2967Mi) % 262.73/38.17 % (941100)Instruction limit reached! % 262.73/38.17 % (941100)------------------------------ % 262.73/38.17 % (941100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.73/38.17 % (941100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.73/38.17 % (941100)CaDiCaL version: 2.1.3 % 262.73/38.17 % (941100)Termination reason: Instruction limit % 262.73/38.17 % (941100)Termination phase: Saturation % 262.73/38.17 % (941100)Time elapsed: 4.410 s % 262.73/38.17 % (941100)Peak memory usage: 187 MB % 262.73/38.17 % (941100)Instructions burned: 7535 (million) % 262.73/38.17 % (941114)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=2372021224:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2641 on theBenchmark for (2641ds/3022Mi) % 262.73/38.17 [W927 21:42:03.463476581 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 262.73/38.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 262.73/38.17 [W927 21:42:03.463512508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463548482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463559282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463584166 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463594299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463618566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463628573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463652383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463662550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463686367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 [W927 21:42:03.463696417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 267.60/38.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 267.60/38.69 % (941114)Refutation not found, incomplete strategy % 267.60/38.69 % (941114)------------------------------ % 267.60/38.69 % (941114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.60/38.69 % (941114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.60/38.69 % (941114)CaDiCaL version: 2.1.3 % 267.60/38.69 % (941114)Termination reason: Refutation not found, incomplete strategy % 267.60/38.69 % (941114)Time elapsed: 0.548 s % 267.60/38.69 % (941114)Peak memory usage: 125 MB % 267.60/38.69 % (941114)Instructions burned: 825 (million) % 267.60/38.69 % (941114)------------------------------ % 267.60/38.69 % (941114)------------------------------ % 267.60/38.69 % (941116)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=623597745:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2632 on theBenchmark for (2632ds/3207Mi) % 274.75/39.76 % (941107)Instruction limit reached! % 274.75/39.76 % (941107)------------------------------ % 274.75/39.76 % (941107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.75/39.76 % (941107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.75/39.76 % (941107)CaDiCaL version: 2.1.3 % 274.75/39.76 % (941107)Termination reason: Instruction limit % 274.75/39.76 % (941107)Termination phase: Saturation % 274.75/39.76 % (941107)Time elapsed: 3.476 s % 274.75/39.76 % (941107)Peak memory usage: 166 MB % 274.75/39.76 % (941107)Instructions burned: 5813 (million) % 274.75/39.76 % (941118)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2841798608:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2629 on theBenchmark for (2629ds/3289Mi) % 274.75/39.76 % (941112)Instruction limit reached! % 274.75/39.76 % (941112)------------------------------ % 274.75/39.76 % (941112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 274.75/39.76 % (941112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.75/39.76 % (941112)CaDiCaL version: 2.1.3 % 274.75/39.76 % (941112)Termination reason: Instruction limit % 274.75/39.76 % (941112)Termination phase: Saturation % 274.75/39.76 % (941112)Time elapsed: 1.811 s % 274.75/39.76 % (941112)Peak memory usage: 145 MB % 274.75/39.76 % (941112)Instructions burned: 2969 (million) % 274.75/39.76 [W927 21:42:04.422948560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.422993164 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423042961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423067528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423092718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423104605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423130669 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423142046 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 274.75/39.76 [W927 21:42:04.423167089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 274.75/39.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.423178323 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.423202536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.423271794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 % (941120)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1171795819:i=38569:sd=3:ss=axioms:sgt=32_2627 on theBenchmark for (2627ds/38569Mi) % 275.78/39.93 % (941116)Refutation not found, incomplete strategy % 275.78/39.93 % (941116)------------------------------ % 275.78/39.93 % (941116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.78/39.93 % (941116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.78/39.93 % (941116)CaDiCaL version: 2.1.3 % 275.78/39.93 % (941116)Termination reason: Refutation not found, incomplete strategy % 275.78/39.93 % (941116)Time elapsed: 0.548 s % 275.78/39.93 % (941116)Peak memory usage: 125 MB % 275.78/39.93 % (941116)Instructions burned: 825 (million) % 275.78/39.93 % (941116)------------------------------ % 275.78/39.93 % (941116)------------------------------ % 275.78/39.93 % (941118)Refutation not found, incomplete strategy % 275.78/39.93 % (941118)------------------------------ % 275.78/39.93 % (941118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.78/39.93 % (941118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.78/39.93 % (941118)CaDiCaL version: 2.1.3 % 275.78/39.93 % (941118)Termination reason: Refutation not found, incomplete strategy % 275.78/39.93 % (941118)Time elapsed: 0.566 s % 275.78/39.93 % (941118)Peak memory usage: 128 MB % 275.78/39.93 % (941118)Instructions burned: 847 (million) % 275.78/39.93 [W927 21:42:04.941607005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941643665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941680666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941694079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941720319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941732050 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.78/39.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.78/39.93 [W927 21:42:04.941757056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 [W927 21:42:04.941768830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 [W927 21:42:04.941792070 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 [W927 21:42:04.941813434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 [W927 21:42:04.941839004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 [W927 21:42:04.941850121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.37/40.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.37/40.77 % (941122)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3903212328:cts=off:i=3394_2622 on theBenchmark for (2622ds/3394Mi) % 282.37/40.77 % (941120)Refutation not found, incomplete strategy % 282.37/40.77 % (941120)------------------------------ % 282.37/40.77 % (941120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.77 % (941120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.77 % (941120)CaDiCaL version: 2.1.3 % 282.37/40.77 % (941120)Termination reason: Refutation not found, incomplete strategy % 282.37/40.77 % (941120)Time elapsed: 0.553 s % 282.37/40.77 % (941120)Peak memory usage: 125 MB % 282.37/40.77 % (941120)Instructions burned: 826 (million) % 282.37/40.77 % (941118)------------------------------ % 282.37/40.77 % (941118)------------------------------ % 282.37/40.77 % (941124)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=1210342937:i=33824:bd=preordered_2619 on theBenchmark for (2619ds/33824Mi) % 282.37/40.77 % (941120)------------------------------ % 282.37/40.77 % (941120)------------------------------ % 282.37/40.77 % (941106)Instruction limit reached! % 282.37/40.77 % (941106)------------------------------ % 282.37/40.77 % (941106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.77 % (941106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.77 % (941106)CaDiCaL version: 2.1.3 % 282.37/40.77 % (941106)Termination reason: Instruction limit % 282.37/40.77 % (941106)Termination phase: Saturation % 282.37/40.77 % (941106)Time elapsed: 4.811 s % 282.37/40.77 % (941106)Peak memory usage: 181 MB % 282.37/40.77 % (941106)Instructions burned: 7897 (million) % 282.37/40.77 % (941126)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=4106521527:i=20684:bd=all:gtg=exists_sym_2617 on theBenchmark for (2617ds/20684Mi) % 282.37/40.77 % (941127)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=4040135763: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_2616 on theBenchmark for (2616ds/7222Mi) % 282.37/40.77 [W927 21:42:05.014403272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlisTerminated %------------------------------------------------------------------------------