%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM925_20 : 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 : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:32 PM UTC 2026 % Result : Timeout 290.85s 42.12s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM925_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.34 % Computer : n012.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sun Sep 27 21:41:34 UTC 2026 % 0.07/0.34 % CPUTime : % 0.07/0.34 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.37 Running first-order theorem proving % 0.11/0.37 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.61/2.30 % (2773640)Detected formulas, will run a generic FOF schedule. % 10.61/2.30 % (2773655)dis-21_1_sil=8000:lcm=predicate:random_seed=737177959: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.61/2.30 % (2773655)Instruction limit reached! % 10.61/2.30 % (2773655)------------------------------ % 10.61/2.30 % (2773655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.30 % (2773655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.30 % (2773655)CaDiCaL version: 2.1.3 % 10.61/2.30 % (2773655)Termination reason: Instruction limit % 10.61/2.30 % (2773655)Termination phase: Saturation % 10.61/2.30 % (2773655)Time elapsed: 0.041 s % 10.61/2.30 % (2773655)Peak memory usage: 90 MB % 10.61/2.30 % (2773655)Instructions burned: 130 (million) % 10.61/2.30 % (2773651)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=77946896:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.61/2.30 % (2773650)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=385701376:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.61/2.30 % (2773653)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4291039492:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.61/2.30 % (2773652)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=514935940:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.61/2.30 % (2773649)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=4281768293:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.61/2.30 % (2773654)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=238639665:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.61/2.30 % (2773653)Refutation not found, incomplete strategy % 10.61/2.30 % (2773653)------------------------------ % 10.61/2.30 % (2773653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.30 % (2773653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.30 % (2773652)Refutation not found, incomplete strategy % 10.61/2.30 % (2773652)------------------------------ % 10.61/2.30 % (2773652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.30 % (2773653)CaDiCaL version: 2.1.3 % 10.61/2.30 % (2773652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.30 % (2773653)Termination reason: Refutation not found, incomplete strategy % 10.61/2.30 % (2773653)Time elapsed: 0.002 s % 10.61/2.30 % (2773653)Peak memory usage: 86 MB % 10.61/2.30 % (2773652)CaDiCaL version: 2.1.3 % 10.61/2.30 % (2773653)Instructions burned: 3 (million) % 10.61/2.30 % (2773652)Termination reason: Refutation not found, incomplete strategy % 10.61/2.30 % (2773652)Time elapsed: 0.002 s % 10.61/2.30 % (2773652)Peak memory usage: 87 MB % 10.61/2.30 % (2773652)Instructions burned: 2 (million) % 10.61/2.30 % (2773654)Instruction limit reached! % 10.61/2.30 % (2773654)------------------------------ % 10.61/2.30 % (2773654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.30 % (2773654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.30 % (2773654)CaDiCaL version: 2.1.3 % 10.61/2.30 % (2773654)Termination reason: Instruction limit % 10.61/2.30 % (2773654)Termination phase: Saturation % 10.61/2.30 % (2773654)Time elapsed: 0.074 s % 10.61/2.30 % (2773654)Peak memory usage: 90 MB % 10.61/2.30 % (2773654)Instructions burned: 140 (million) % 10.61/2.30 % (2773659)lrs+10_1_sil=8000:sp=occurrence:random_seed=3204549961:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 10.61/2.30 % (2773659)Refutation not found, incomplete strategy % 10.61/2.30 % (2773659)------------------------------ % 10.61/2.30 % (2773659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.61/2.30 % (2773659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.61/2.30 % (2773659)CaDiCaL version: 2.1.3 % 10.61/2.30 % (2773659)Termination reason: Refutation not found, incomplete strategy % 10.61/2.30 % (2773659)Time elapsed: 0.003 s % 10.61/2.30 % (2773659)Peak memory usage: 86 MB % 10.61/2.30 % (2773659)Instructions burned: 2 (million) % 10.61/2.30 % (2773653)------------------------------ % 11.77/2.46 % (2773653)------------------------------ % 11.77/2.46 % (2773652)------------------------------ % 11.77/2.46 % (2773652)------------------------------ % 11.77/2.46 % (2773666)lrs+10_1_sil=32000:urr=on:br=off:random_seed=285657289:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 11.77/2.46 % (2773666)Refutation not found, incomplete strategy % 11.77/2.46 % (2773666)------------------------------ % 11.77/2.46 % (2773666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.46 % (2773666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.46 % (2773666)CaDiCaL version: 2.1.3 % 11.77/2.46 % (2773666)Termination reason: Refutation not found, incomplete strategy % 11.77/2.46 % (2773666)Time elapsed: 0.006 s % 11.77/2.46 % (2773666)Peak memory usage: 88 MB % 11.77/2.46 % (2773666)Instructions burned: 12 (million) % 11.77/2.46 % (2773659)------------------------------ % 11.77/2.46 % (2773659)------------------------------ % 11.77/2.46 % (2773671)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=3598399312:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 11.77/2.46 % (2773670)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1280770178:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.77/2.46 % (2773670)Refutation not found, incomplete strategy % 11.77/2.46 % (2773670)------------------------------ % 11.77/2.46 % (2773670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.46 % (2773670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.46 % (2773670)CaDiCaL version: 2.1.3 % 11.77/2.46 % (2773670)Termination reason: Refutation not found, incomplete strategy % 11.77/2.46 % (2773670)Time elapsed: 0.002 s % 11.77/2.46 % (2773670)Peak memory usage: 87 MB % 11.77/2.46 % (2773670)Instructions burned: 2 (million) % 11.77/2.46 % (2773651)Refutation not found, incomplete strategy % 11.77/2.46 % (2773651)------------------------------ % 11.77/2.46 % (2773651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.46 % (2773651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.46 % (2773651)CaDiCaL version: 2.1.3 % 11.77/2.46 % (2773651)Termination reason: Refutation not found, incomplete strategy % 11.77/2.46 % (2773651)Time elapsed: 0.541 s % 11.77/2.46 % (2773651)Peak memory usage: 136 MB % 11.77/2.46 % (2773651)Instructions burned: 1021 (million) % 11.77/2.46 % (2773666)------------------------------ % 11.77/2.46 % (2773666)------------------------------ % 11.77/2.46 % (2773671)Instruction limit reached! % 11.77/2.46 % (2773671)------------------------------ % 11.77/2.46 % (2773671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.46 % (2773671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.46 % (2773671)CaDiCaL version: 2.1.3 % 11.77/2.46 % (2773671)Termination reason: Instruction limit % 11.77/2.46 % (2773671)Termination phase: Saturation % 11.77/2.46 % (2773671)Time elapsed: 0.132 s % 11.77/2.46 % (2773671)Peak memory usage: 92 MB % 11.77/2.46 % (2773671)Instructions burned: 248 (million) % 11.77/2.46 % (2773673)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3922871513:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 11.77/2.46 % (2773673)Refutation not found, incomplete strategy % 11.77/2.46 % (2773673)------------------------------ % 11.77/2.46 % (2773673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.77/2.46 % (2773673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.77/2.46 % (2773673)CaDiCaL version: 2.1.3 % 11.77/2.46 % (2773673)Termination reason: Refutation not found, incomplete strategy % 11.77/2.46 % (2773673)Time elapsed: 0.003 s % 11.77/2.46 % (2773673)Peak memory usage: 87 MB % 11.77/2.46 % (2773673)Instructions burned: 4 (million) % 11.77/2.46 % (2773670)------------------------------ % 11.77/2.46 % (2773670)------------------------------ % 11.77/2.46 % (2773651)------------------------------ % 11.77/2.46 % (2773651)------------------------------ % 11.77/2.46 % (2773678)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=191922718:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 11.77/2.46 % (2773679)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1894527090:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 11.77/2.46 % (2773673)------------------------------ % 11.77/2.46 % (2773673)------------------------------ % 14.10/2.87 % (2773679)Refutation not found, incomplete strategy % 14.10/2.87 % (2773679)------------------------------ % 14.10/2.87 % (2773679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.87 % (2773679)CaDiCaL version: 2.1.3 % 14.10/2.87 % (2773679)Termination reason: Refutation not found, incomplete strategy % 14.10/2.87 % (2773679)Time elapsed: 0.048 s % 14.10/2.87 % (2773679)Peak memory usage: 90 MB % 14.10/2.87 % (2773679)Instructions burned: 97 (million) % 14.10/2.87 % (2773684)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3121024211:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 14.10/2.87 % (2773683)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=825644338:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi) % 14.10/2.87 % (2773684)Instruction limit reached! % 14.10/2.87 % (2773684)------------------------------ % 14.10/2.87 % (2773684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.87 % (2773684)CaDiCaL version: 2.1.3 % 14.10/2.87 % (2773684)Termination reason: Instruction limit % 14.10/2.87 % (2773684)Termination phase: Saturation % 14.10/2.87 % (2773684)Time elapsed: 0.033 s % 14.10/2.87 % (2773684)Peak memory usage: 89 MB % 14.10/2.87 % (2773684)Instructions burned: 115 (million) % 14.10/2.87 % (2773683)Refutation not found, incomplete strategy % 14.10/2.87 % (2773683)------------------------------ % 14.10/2.87 % (2773683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.87 % (2773683)CaDiCaL version: 2.1.3 % 14.10/2.87 % (2773683)Termination reason: Refutation not found, incomplete strategy % 14.10/2.87 % (2773683)Time elapsed: 0.031 s % 14.10/2.87 % (2773683)Peak memory usage: 89 MB % 14.10/2.87 % (2773683)Instructions burned: 73 (million) % 14.10/2.87 % (2773688)lrs+10_1_sil=8000:sp=occurrence:random_seed=564047853:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 14.10/2.87 % (2773688)Refutation not found, incomplete strategy % 14.10/2.87 % (2773688)------------------------------ % 14.10/2.87 % (2773688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.87 % (2773688)CaDiCaL version: 2.1.3 % 14.10/2.87 % (2773688)Termination reason: Refutation not found, incomplete strategy % 14.10/2.87 % (2773688)Time elapsed: 0.003 s % 14.10/2.87 % (2773688)Peak memory usage: 87 MB % 14.10/2.87 % (2773688)Instructions burned: 4 (million) % 14.10/2.87 % (2773679)------------------------------ % 14.10/2.87 % (2773679)------------------------------ % 14.10/2.87 % (2773691)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3990341046:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 14.10/2.87 % (2773683)------------------------------ % 14.10/2.87 % (2773683)------------------------------ % 14.10/2.87 % (2773691)Refutation not found, incomplete strategy % 14.10/2.87 % (2773691)------------------------------ % 14.10/2.87 % (2773691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.87 % (2773691)CaDiCaL version: 2.1.3 % 14.10/2.87 % (2773691)Termination reason: Refutation not found, incomplete strategy % 14.10/2.87 % (2773691)Time elapsed: 0.038 s % 14.10/2.87 % (2773691)Peak memory usage: 90 MB % 14.10/2.87 % (2773691)Instructions burned: 75 (million) % 14.10/2.87 % (2773688)------------------------------ % 14.10/2.87 % (2773688)------------------------------ % 14.10/2.87 % (2773696)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3728309835:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi) % 14.10/2.87 % (2773699)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=49534240:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 14.10/2.87 % (2773691)------------------------------ % 14.10/2.87 % (2773691)------------------------------ % 14.10/2.87 % (2773699)Instruction limit reached! % 14.10/2.87 % (2773699)------------------------------ % 14.10/2.87 % (2773699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.87 % (2773699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.90 % (2773699)CaDiCaL version: 2.1.3 % 14.10/2.90 % (2773699)Termination reason: Instruction limit % 14.10/2.90 % (2773699)Termination phase: Saturation % 14.10/2.90 % (2773699)Time elapsed: 0.071 s % 14.10/2.90 % (2773699)Peak memory usage: 91 MB % 14.10/2.90 % (2773699)Instructions burned: 135 (million) % 14.10/2.90 % (2773702)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1801354366:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 14.10/2.90 % (2773702)Refutation not found, incomplete strategy % 14.10/2.90 % (2773702)------------------------------ % 14.10/2.90 % (2773702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.10/2.90 % (2773702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.10/2.90 % (2773702)CaDiCaL version: 2.1.3 % 14.10/2.90 % (2773702)Termination reason: Refutation not found, incomplete strategy % 14.10/2.90 % (2773702)Time elapsed: 0.003 s % 14.10/2.90 % (2773702)Peak memory usage: 87 MB % 14.10/2.90 % (2773702)Instructions burned: 4 (million) % 14.10/2.90 [W927 21:41:36.471387841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471412596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471433536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471439593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471452506 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471458726 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471471245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471477739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471490242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 14.10/2.90 [W927 21:41:36.471496342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 14.10/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.71/3.54 [W927 21:41:36.471509433 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.71/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.71/3.54 [W927 21:41:36.471514902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.71/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.71/3.54 % (2773707)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=3055620463:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 18.71/3.54 % (2773705)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1758009728:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 18.71/3.54 % (2773707)Refutation not found, incomplete strategy % 18.71/3.54 % (2773707)------------------------------ % 18.71/3.54 % (2773707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.71/3.54 % (2773707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.71/3.54 % (2773707)CaDiCaL version: 2.1.3 % 18.71/3.54 % (2773707)Termination reason: Refutation not found, incomplete strategy % 18.71/3.54 % (2773707)Time elapsed: 0.007 s % 18.71/3.54 % (2773707)Peak memory usage: 88 MB % 18.71/3.54 % (2773707)Instructions burned: 15 (million) % 18.71/3.54 % (2773696)Refutation not found, incomplete strategy % 18.71/3.54 % (2773696)------------------------------ % 18.71/3.54 % (2773696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.71/3.54 % (2773696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.71/3.54 % (2773696)CaDiCaL version: 2.1.3 % 18.71/3.54 % (2773696)Termination reason: Refutation not found, incomplete strategy % 18.71/3.54 % (2773696)Time elapsed: 0.388 s % 18.71/3.54 % (2773696)Peak memory usage: 126 MB % 18.71/3.54 % (2773696)Instructions burned: 828 (million) % 18.71/3.54 % (2773678)Instruction limit reached! % 18.71/3.54 % (2773678)------------------------------ % 18.71/3.54 % (2773678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.71/3.54 % (2773678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.71/3.54 % (2773678)CaDiCaL version: 2.1.3 % 18.71/3.54 % (2773678)Termination reason: Instruction limit % 18.71/3.54 % (2773678)Termination phase: Saturation % 18.71/3.54 % (2773678)Time elapsed: 0.929 s % 18.71/3.54 % (2773678)Peak memory usage: 135 MB % 18.71/3.54 % (2773678)Instructions burned: 2350 (million) % 18.71/3.54 % (2773702)------------------------------ % 18.71/3.54 % (2773702)------------------------------ % 18.71/3.54 % (2773707)------------------------------ % 18.71/3.54 % (2773707)------------------------------ % 18.71/3.54 % (2773696)------------------------------ % 18.71/3.54 % (2773696)------------------------------ % 18.71/3.54 % (2773715)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1281357348:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi) % 18.71/3.54 % (2773716)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=529664779:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 18.71/3.54 % (2773716)Refutation not found, incomplete strategy % 18.71/3.54 % (2773716)------------------------------ % 18.71/3.54 % (2773716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.71/3.54 % (2773716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.71/3.54 % (2773716)CaDiCaL version: 2.1.3 % 18.71/3.54 % (2773716)Termination reason: Refutation not found, incomplete strategy % 18.71/3.54 % (2773716)Time elapsed: 0.002 s % 18.71/3.54 % (2773716)Peak memory usage: 87 MB % 18.71/3.54 % (2773716)Instructions burned: 2 (million) % 18.71/3.54 [W927 21:41:37.873088791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.71/3.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.71/3.54 [W927 21:41:37.873123914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873161377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873182533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873210771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873220139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873246472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873256169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873280994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873290666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873314852 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 [W927 21:41:37.873324342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.94/5.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.94/5.01 % (2773719)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=1942623750:i=6060:aac=none:ins=25_2979 on theBenchmark for (2979ds/6060Mi) % 28.94/5.01 % (2773715)Instruction limit reached! % 28.94/5.01 % (2773715)------------------------------ % 28.94/5.01 % (2773715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.94/5.01 % (2773715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.94/5.01 % (2773715)CaDiCaL version: 2.1.3 % 28.94/5.01 % (2773715)Termination reason: Instruction limit % 28.94/5.01 % (2773715)Termination phase: Saturation % 28.94/5.01 % (2773715)Time elapsed: 0.064 s % 28.94/5.01 % (2773715)Peak memory usage: 90 MB % 33.96/5.50 % (2773715)Instructions burned: 135 (million) % 33.96/5.50 % (2773718)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1001465963:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi) % 33.96/5.50 % (2773718)Refutation not found, incomplete strategy % 33.96/5.50 % (2773718)------------------------------ % 33.96/5.50 % (2773718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.96/5.50 % (2773718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.96/5.50 % (2773718)CaDiCaL version: 2.1.3 % 33.96/5.50 % (2773718)Termination reason: Refutation not found, incomplete strategy % 33.96/5.50 % (2773718)Time elapsed: 0.002 s % 33.96/5.50 % (2773718)Peak memory usage: 87 MB % 33.96/5.50 % (2773718)Instructions burned: 2 (million) % 33.96/5.50 % (2773705)Refutation not found, incomplete strategy % 33.96/5.50 % (2773705)------------------------------ % 33.96/5.50 % (2773705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.96/5.50 % (2773705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.96/5.50 % (2773705)CaDiCaL version: 2.1.3 % 33.96/5.50 % (2773705)Termination reason: Refutation not found, incomplete strategy % 33.96/5.50 % (2773705)Time elapsed: 0.513 s % 33.96/5.50 % (2773705)Peak memory usage: 126 MB % 33.96/5.50 % (2773705)Instructions burned: 833 (million) % 33.96/5.50 % (2773716)------------------------------ % 33.96/5.50 % (2773716)------------------------------ % 33.96/5.50 % (2773725)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=2392929620:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi) % 33.96/5.50 % (2773718)------------------------------ % 33.96/5.50 % (2773718)------------------------------ % 33.96/5.50 % (2773729)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2370426694:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 33.96/5.50 % (2773725)Instruction limit reached! % 33.96/5.50 % (2773725)------------------------------ % 33.96/5.50 % (2773725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.96/5.50 % (2773725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.96/5.50 % (2773725)CaDiCaL version: 2.1.3 % 33.96/5.50 % (2773725)Termination reason: Instruction limit % 33.96/5.50 % (2773725)Termination phase: Saturation % 33.96/5.50 % (2773725)Time elapsed: 0.079 s % 33.96/5.50 % (2773725)Peak memory usage: 91 MB % 33.96/5.50 % (2773725)Instructions burned: 152 (million) % 33.96/5.50 % (2773705)------------------------------ % 33.96/5.50 % (2773705)------------------------------ % 33.96/5.50 % (2773734)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2542958931:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi) % 33.96/5.50 % (2773734)Refutation not found, incomplete strategy % 33.96/5.50 % (2773734)------------------------------ % 33.96/5.50 % (2773734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.96/5.50 % (2773734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.96/5.50 % (2773734)CaDiCaL version: 2.1.3 % 33.96/5.50 % (2773734)Termination reason: Refutation not found, incomplete strategy % 33.96/5.50 % (2773734)Time elapsed: 0.038 s % 33.96/5.50 % (2773734)Peak memory usage: 89 MB % 33.96/5.50 % (2773734)Instructions burned: 82 (million) % 33.96/5.50 % (2773736)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=3962347128:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi) % 33.96/5.50 % (2773737)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=332071610:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi) % 33.96/5.50 % (2773737)Refutation not found, incomplete strategy % 33.96/5.50 % (2773737)------------------------------ % 33.96/5.50 % (2773737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.96/5.50 % (2773737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.96/5.50 % (2773737)CaDiCaL version: 2.1.3 % 33.96/5.50 % (2773737)Termination reason: Refutation not found, incomplete strategy % 33.96/5.50 % (2773737)Time elapsed: 0.003 s % 33.96/5.50 % (2773737)Peak memory usage: 86 MB % 33.96/5.50 % (2773737)Instructions burned: 5 (million) % 33.96/5.50 % (2773736)Instruction limit reached! % 44.62/7.02 % (2773736)------------------------------ % 44.62/7.02 % (2773736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.02 % (2773736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.62/7.02 % (2773736)CaDiCaL version: 2.1.3 % 44.62/7.02 % (2773736)Termination reason: Instruction limit % 44.62/7.02 % (2773736)Termination phase: Saturation % 44.62/7.02 % (2773736)Time elapsed: 0.100 s % 44.62/7.02 % (2773736)Peak memory usage: 92 MB % 44.62/7.02 % (2773736)Instructions burned: 186 (million) % 44.62/7.02 % (2773734)------------------------------ % 44.62/7.02 % (2773734)------------------------------ % 44.62/7.02 % (2773737)------------------------------ % 44.62/7.02 % (2773737)------------------------------ % 44.62/7.02 % (2773744)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1830214180:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi) % 44.62/7.02 % (2773744)Refutation not found, incomplete strategy % 44.62/7.02 % (2773744)------------------------------ % 44.62/7.02 % (2773744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.02 % (2773744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.62/7.02 % (2773744)CaDiCaL version: 2.1.3 % 44.62/7.02 % (2773744)Termination reason: Refutation not found, incomplete strategy % 44.62/7.02 % (2773744)Time elapsed: 0.028 s % 44.62/7.02 % (2773744)Peak memory usage: 89 MB % 44.62/7.02 % (2773744)Instructions burned: 63 (million) % 44.62/7.02 % (2773746)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3393673093:i=12111:sd=1:ss=included_2970 on theBenchmark for (2970ds/12111Mi) % 44.62/7.02 % (2773749)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3282318670:i=319:kws=precedence:fsr=off_2969 on theBenchmark for (2969ds/319Mi) % 44.62/7.02 % (2773744)------------------------------ % 44.62/7.02 % (2773744)------------------------------ % 44.62/7.02 % (2773749)Instruction limit reached! % 44.62/7.02 % (2773749)------------------------------ % 44.62/7.02 % (2773749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.02 % (2773749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.62/7.02 % (2773749)CaDiCaL version: 2.1.3 % 44.62/7.02 % (2773749)Termination reason: Instruction limit % 44.62/7.02 % (2773749)Termination phase: Saturation % 44.62/7.02 % (2773749)Time elapsed: 0.161 s % 44.62/7.02 % (2773749)Peak memory usage: 91 MB % 44.62/7.02 % (2773749)Instructions burned: 319 (million) % 44.62/7.02 % (2773756)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3453650240:i=2064:ep=RST_2966 on theBenchmark for (2966ds/2064Mi) % 44.62/7.02 % (2773756)Refutation not found, incomplete strategy % 44.62/7.02 % (2773756)------------------------------ % 44.62/7.02 % (2773756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.02 % (2773756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.62/7.02 % (2773756)CaDiCaL version: 2.1.3 % 44.62/7.02 % (2773756)Termination reason: Refutation not found, incomplete strategy % 44.62/7.02 % (2773756)Time elapsed: 0.021 s % 44.62/7.02 % (2773756)Peak memory usage: 89 MB % 44.62/7.02 % (2773756)Instructions burned: 76 (million) % 44.62/7.02 % (2773756)------------------------------ % 44.62/7.02 % (2773756)------------------------------ % 44.62/7.02 % (2773757)dis-1011_128_sil=32000:random_seed=1709485125:i=3706:ep=RST:av=off_2965 on theBenchmark for (2965ds/3706Mi) % 44.62/7.02 % (2773762)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=612493910:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2963 on theBenchmark for (2963ds/757Mi) % 44.62/7.02 % (2773762)Refutation not found, incomplete strategy % 44.62/7.02 % (2773762)------------------------------ % 44.62/7.02 % (2773762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.02 % (2773762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.62/7.02 % (2773762)CaDiCaL version: 2.1.3 % 44.62/7.02 % (2773762)Termination reason: Refutation not found, incomplete strategy % 44.62/7.02 % (2773762)Time elapsed: 0.002 s % 44.62/7.02 % (2773762)Peak memory usage: 87 MB % 44.62/7.02 % (2773762)Instructions burned: 2 (million) % 44.62/7.02 % (2773762)------------------------------ % 44.62/7.02 % (2773762)------------------------------ % 44.62/7.02 % (2773768)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2065639497:i=13913:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/13913Mi) % 44.62/7.03 [W927 21:41:39.366726539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366776616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366812782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366823763 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366849696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366859939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366901978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366912613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366937249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366948991 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366975029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 [W927 21:41:39.366986132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.62/7.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.62/7.03 % (2773768)Refutation not found, incomplete strategy % 44.62/7.03 % (2773768)------------------------------ % 44.62/7.03 % (2773768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.62/7.03 % (2773768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773768)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773768)Termination reason: Refutation not found, incomplete strategy % 55.25/8.60 % (2773768)Time elapsed: 0.496 s % 55.25/8.60 % (2773768)Peak memory usage: 126 MB % 55.25/8.60 % (2773768)Instructions burned: 831 (million) % 55.25/8.60 % (2773768)------------------------------ % 55.25/8.60 % (2773768)------------------------------ % 55.25/8.60 % (2773777)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1774709573:i=9925:aac=none_2949 on theBenchmark for (2949ds/9925Mi) % 55.25/8.60 % (2773719)Instruction limit reached! % 55.25/8.60 % (2773719)------------------------------ % 55.25/8.60 % (2773719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2773719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773719)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773719)Termination reason: Instruction limit % 55.25/8.60 % (2773719)Termination phase: Saturation % 55.25/8.60 % (2773719)Time elapsed: 3.228 s % 55.25/8.60 % (2773719)Peak memory usage: 159 MB % 55.25/8.60 % (2773719)Instructions burned: 6062 (million) % 55.25/8.60 % (2773757)Instruction limit reached! % 55.25/8.60 % (2773757)------------------------------ % 55.25/8.60 % (2773757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2773757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773757)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773757)Termination reason: Instruction limit % 55.25/8.60 % (2773757)Termination phase: Saturation % 55.25/8.60 % (2773757)Time elapsed: 1.950 s % 55.25/8.60 % (2773757)Peak memory usage: 116 MB % 55.25/8.60 % (2773757)Instructions burned: 3707 (million) % 55.25/8.60 % (2773782)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4154918028:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/2479Mi) % 55.25/8.60 % (2773782)Refutation not found, incomplete strategy % 55.25/8.60 % (2773782)------------------------------ % 55.25/8.60 % (2773782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2773782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773782)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773782)Termination reason: Refutation not found, incomplete strategy % 55.25/8.60 % (2773782)Time elapsed: 0.003 s % 55.25/8.60 % (2773782)Peak memory usage: 87 MB % 55.25/8.60 % (2773782)Instructions burned: 5 (million) % 55.25/8.60 % (2773777)Refutation not found, incomplete strategy % 55.25/8.60 % (2773777)------------------------------ % 55.25/8.60 % (2773777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2773777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773777)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773777)Termination reason: Refutation not found, incomplete strategy % 55.25/8.60 % (2773777)Time elapsed: 0.570 s % 55.25/8.60 % (2773777)Peak memory usage: 136 MB % 55.25/8.60 % (2773777)Instructions burned: 1001 (million) % 55.25/8.60 % (2773782)------------------------------ % 55.25/8.60 % (2773782)------------------------------ % 55.25/8.60 % (2773787)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3952116418:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2943 on theBenchmark for (2943ds/440Mi) % 55.25/8.60 % (2773777)------------------------------ % 55.25/8.60 % (2773777)------------------------------ % 55.25/8.60 % (2773791)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3849308382:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/11145Mi) % 55.25/8.60 % (2773787)Instruction limit reached! % 55.25/8.60 % (2773787)------------------------------ % 55.25/8.60 % (2773787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.25/8.60 % (2773787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.25/8.60 % (2773787)CaDiCaL version: 2.1.3 % 55.25/8.60 % (2773787)Termination reason: Instruction limit % 55.25/8.60 % (2773787)Termination phase: Saturation % 55.25/8.60 % (2773787)Time elapsed: 0.242 s % 55.25/8.60 % (2773787)Peak memory usage: 94 MB % 55.25/8.60 % (2773787)Instructions burned: 440 (million) % 55.25/8.60 % (2773796)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=3242771809:cts=off:i=3034:av=off:er=known:fsd=on_2939 on theBenchmark for (2939ds/3034Mi) % 55.25/8.60 % (2773797)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1016745587:st=2:s2a=on:i=524:s2at=2:ss=axioms_2938 on theBenchmark for (2938ds/524Mi) % 58.79/9.10 [W927 21:41:41.032222121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032252496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032281443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032290239 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032309337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032317261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032337339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032345303 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032364777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032372866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032391940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 [W927 21:41:41.032403005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.79/9.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.79/9.10 % (2773797)Refutation not found, incomplete strategy % 58.79/9.10 % (2773797)------------------------------ % 58.79/9.10 % (2773797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.79/9.10 % (2773797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773797)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773797)Termination reason: Refutation not found, incomplete strategy % 64.35/9.94 % (2773797)Time elapsed: 0.005 s % 64.35/9.94 % (2773797)Peak memory usage: 87 MB % 64.35/9.94 % (2773797)Instructions burned: 8 (million) % 64.35/9.94 % (2773791)Refutation not found, incomplete strategy % 64.35/9.94 % (2773791)------------------------------ % 64.35/9.94 % (2773791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.94 % (2773791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773791)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773791)Termination reason: Refutation not found, incomplete strategy % 64.35/9.94 % (2773791)Time elapsed: 0.436 s % 64.35/9.94 % (2773791)Peak memory usage: 126 MB % 64.35/9.94 % (2773791)Instructions burned: 833 (million) % 64.35/9.94 % (2773797)------------------------------ % 64.35/9.94 % (2773797)------------------------------ % 64.35/9.94 % (2773791)------------------------------ % 64.35/9.94 % (2773791)------------------------------ % 64.35/9.94 % (2773805)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3330320261:i=14123:bd=preordered:ins=4_2933 on theBenchmark for (2933ds/14123Mi) % 64.35/9.94 % (2773804)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=354448738:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2934 on theBenchmark for (2934ds/1016Mi) % 64.35/9.94 % (2773804)Refutation not found, incomplete strategy % 64.35/9.94 % (2773804)------------------------------ % 64.35/9.94 % (2773804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.94 % (2773804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773804)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773804)Termination reason: Refutation not found, incomplete strategy % 64.35/9.94 % (2773804)Time elapsed: 0.002 s % 64.35/9.94 % (2773804)Peak memory usage: 87 MB % 64.35/9.94 % (2773804)Instructions burned: 2 (million) % 64.35/9.94 % (2773804)------------------------------ % 64.35/9.94 % (2773804)------------------------------ % 64.35/9.94 % (2773810)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=909384212:i=5781:kws=precedence:bd=all:rawr=on_2929 on theBenchmark for (2929ds/5781Mi) % 64.35/9.94 % (2773796)Instruction limit reached! % 64.35/9.94 % (2773796)------------------------------ % 64.35/9.94 % (2773796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.94 % (2773796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773796)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773796)Termination reason: Instruction limit % 64.35/9.94 % (2773796)Termination phase: Saturation % 64.35/9.94 % (2773796)Time elapsed: 1.526 s % 64.35/9.94 % (2773796)Peak memory usage: 148 MB % 64.35/9.94 % (2773796)Instructions burned: 3035 (million) % 64.35/9.94 % (2773729)Instruction limit reached! % 64.35/9.94 % (2773729)------------------------------ % 64.35/9.94 % (2773729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.94 % (2773729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773729)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773729)Termination reason: Instruction limit % 64.35/9.94 % (2773729)Termination phase: Saturation % 64.35/9.94 % (2773729)Time elapsed: 5.171 s % 64.35/9.94 % (2773729)Peak memory usage: 147 MB % 64.35/9.94 % (2773729)Instructions burned: 14155 (million) % 64.35/9.94 % (2773746)Instruction limit reached! % 64.35/9.94 % (2773746)------------------------------ % 64.35/9.94 % (2773746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.35/9.94 % (2773746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.35/9.94 % (2773746)CaDiCaL version: 2.1.3 % 64.35/9.94 % (2773746)Termination reason: Instruction limit % 64.35/9.94 % (2773746)Termination phase: Saturation % 64.35/9.94 % (2773746)Time elapsed: 4.573 s % 64.35/9.94 % (2773746)Peak memory usage: 180 MB % 64.35/9.94 % (2773746)Instructions burned: 12111 (million) % 64.35/9.94 % (2773814)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=3209008354:i=2448:gtgl=5:bd=preordered:gtg=all_2922 on theBenchmark for (2922ds/2448Mi) % 64.35/9.94 % (2773815)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3019757001:i=3223:kws=precedence:fgj=on:av=off_2922 on theBenchmark for (2922ds/3223Mi) % 67.99/10.44 % (2773816)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3339637515:st=5.6:i=2033:sd=3:ss=axioms_2922 on theBenchmark for (2922ds/2033Mi) % 67.99/10.44 [W927 21:41:43.950043261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950086160 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950125958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950135981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950162558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950171918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950196271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950204973 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950227917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950236837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950260154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 [W927 21:41:43.950269286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.99/10.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.99/10.44 % (2773816)Refutation not found, incomplete strategy % 67.99/10.44 % (2773816)------------------------------ % 67.99/10.44 % (2773816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.85/10.80 % (2773816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.85/10.80 % (2773816)CaDiCaL version: 2.1.3 % 70.85/10.80 % (2773816)Termination reason: Refutation not found, incomplete strategy % 70.85/10.80 % (2773816)Time elapsed: 0.497 s % 70.85/10.80 % (2773816)Peak memory usage: 126 MB % 70.85/10.80 % (2773816)Instructions burned: 832 (million) % 70.85/10.80 % (2773816)------------------------------ % 70.85/10.80 % (2773816)------------------------------ % 70.85/10.80 % (2773823)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=867558656:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2913 on theBenchmark for (2913ds/2055Mi) % 70.85/10.80 % (2773814)Instruction limit reached! % 70.85/10.80 % (2773814)------------------------------ % 70.85/10.80 % (2773814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.85/10.80 % (2773814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.85/10.80 % (2773814)CaDiCaL version: 2.1.3 % 70.85/10.80 % (2773814)Termination reason: Instruction limit % 70.85/10.80 % (2773814)Termination phase: Saturation % 70.85/10.80 % (2773814)Time elapsed: 1.248 s % 70.85/10.80 % (2773814)Peak memory usage: 139 MB % 70.85/10.80 % (2773814)Instructions burned: 2451 (million) % 70.85/10.80 [W927 21:41:44.944756457 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944823294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944859576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944871194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944897470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944908126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944934803 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944945443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944970683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.85/10.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.85/10.80 [W927 21:41:44.944981243 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 [W927 21:41:44.945015972 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 [W927 21:41:44.945037296 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 % (2773823)Refutation not found, incomplete strategy % 77.09/11.82 % (2773823)------------------------------ % 77.09/11.82 % (2773823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.09/11.82 % (2773823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.09/11.82 % (2773823)CaDiCaL version: 2.1.3 % 77.09/11.82 % (2773823)Termination reason: Refutation not found, incomplete strategy % 77.09/11.82 % (2773823)Time elapsed: 0.495 s % 77.09/11.82 % (2773823)Peak memory usage: 126 MB % 77.09/11.82 % (2773823)Instructions burned: 840 (million) % 77.09/11.82 % (2773815)Instruction limit reached! % 77.09/11.82 % (2773815)------------------------------ % 77.09/11.82 % (2773815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.09/11.82 % (2773815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.09/11.82 % (2773815)CaDiCaL version: 2.1.3 % 77.09/11.82 % (2773815)Termination reason: Instruction limit % 77.09/11.82 % (2773815)Termination phase: Saturation % 77.09/11.82 % (2773815)Time elapsed: 1.488 s % 77.09/11.82 % (2773815)Peak memory usage: 138 MB % 77.09/11.82 % (2773815)Instructions burned: 3226 (million) % 77.09/11.82 % (2773825)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=1017368073:i=21611:sd=3:ss=axioms_2908 on theBenchmark for (2908ds/21611Mi) % 77.09/11.82 % (2773823)------------------------------ % 77.09/11.82 % (2773823)------------------------------ % 77.09/11.82 % (2773827)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=449080355:i=4835:sd=13:ss=axioms:sgt=23_2905 on theBenchmark for (2905ds/4835Mi) % 77.09/11.82 % (2773827)Refutation not found, incomplete strategy % 77.09/11.82 % (2773827)------------------------------ % 77.09/11.82 % (2773827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.09/11.82 % (2773827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.09/11.82 % (2773827)CaDiCaL version: 2.1.3 % 77.09/11.82 % (2773827)Termination reason: Refutation not found, incomplete strategy % 77.09/11.82 % (2773827)Time elapsed: 0.002 s % 77.09/11.82 % (2773827)Peak memory usage: 87 MB % 77.09/11.82 % (2773827)Instructions burned: 2 (million) % 77.09/11.82 % (2773828)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=3638499990:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2904 on theBenchmark for (2904ds/797Mi) % 77.09/11.82 [W927 21:41:44.451051423 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 [W927 21:41:44.451083953 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 [W927 21:41:44.451117400 register_special_ops.cpp:225] Warning: Creating a tensor from 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.09/11.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.09/11.82 [W927 21:41:44.451128801 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451154257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451163834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451188117 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451197180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451220403 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451238118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451263360 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 [W927 21:41:44.451272836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.84/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.84/13.02 % (2773827)------------------------------ % 84.84/13.02 % (2773827)------------------------------ % 84.84/13.02 % (2773825)Refutation not found, incomplete strategy % 84.84/13.02 % (2773825)------------------------------ % 84.84/13.02 % (2773825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.84/13.02 % (2773825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.84/13.02 % (2773825)CaDiCaL version: 2.1.3 % 84.84/13.02 % (2773825)Termination reason: Refutation not found, incomplete strategy % 84.84/13.02 % (2773825)Time elapsed: 0.494 s % 84.84/13.02 % (2773825)Peak memory usage: 126 MB % 84.84/13.02 % (2773825)Instructions burned: 827 (million) % 84.84/13.02 % (2773828)Instruction limit reached! % 84.84/13.02 % (2773828)------------------------------ % 84.84/13.02 % (2773828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.84/13.02 % (2773828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.84/13.02 % (2773828)CaDiCaL version: 2.1.3 % 84.84/13.02 % (2773828)Termination reason: Instruction limit % 84.84/13.02 % (2773828)Termination phase: Saturation % 84.84/13.02 % (2773828)Time elapsed: 0.251 s % 84.84/13.02 % (2773828)Peak memory usage: 94 MB % 84.84/13.02 % (2773828)Instructions burned: 797 (million) % 84.84/13.02 % (2773831)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2365697147:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2901 on theBenchmark for (2901ds/2326Mi) % 95.56/14.36 % (2773832)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1188089178:i=6038:nm=6_2900 on theBenchmark for (2900ds/6038Mi) % 95.56/14.36 % (2773825)------------------------------ % 95.56/14.36 % (2773825)------------------------------ % 95.56/14.36 % (2773831)Refutation not found, incomplete strategy % 95.56/14.36 % (2773831)------------------------------ % 95.56/14.36 % (2773831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.56/14.36 % (2773831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.56/14.36 % (2773831)CaDiCaL version: 2.1.3 % 95.56/14.36 % (2773831)Termination reason: Refutation not found, incomplete strategy % 95.56/14.36 % (2773831)Time elapsed: 0.070 s % 95.56/14.36 % (2773831)Peak memory usage: 90 MB % 95.56/14.36 % (2773831)Instructions burned: 133 (million) % 95.56/14.36 % (2773810)Instruction limit reached! % 95.56/14.36 % (2773810)------------------------------ % 95.56/14.36 % (2773810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.56/14.36 % (2773810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.56/14.36 % (2773810)CaDiCaL version: 2.1.3 % 95.56/14.36 % (2773810)Termination reason: Instruction limit % 95.56/14.36 % (2773810)Termination phase: Saturation % 95.56/14.36 % (2773810)Time elapsed: 3.139 s % 95.56/14.36 % (2773810)Peak memory usage: 119 MB % 95.56/14.36 % (2773810)Instructions burned: 5781 (million) % 95.56/14.36 % (2773835)lrs+10_1_sil=32000:sp=occurrence:random_seed=3240356627:st=2:i=33334:sd=3:ss=included:sgt=32_2898 on theBenchmark for (2898ds/33334Mi) % 95.56/14.36 % (2773831)------------------------------ % 95.56/14.36 % (2773831)------------------------------ % 95.56/14.36 % (2773836)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3180916431:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2896 on theBenchmark for (2896ds/1008Mi) % 95.56/14.36 % (2773836)Refutation not found, incomplete strategy % 95.56/14.36 % (2773836)------------------------------ % 95.56/14.36 % (2773836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.56/14.36 % (2773836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.56/14.36 % (2773836)CaDiCaL version: 2.1.3 % 95.56/14.36 % (2773836)Termination reason: Refutation not found, incomplete strategy % 95.56/14.36 % (2773836)Time elapsed: 0.005 s % 95.56/14.36 % (2773836)Peak memory usage: 87 MB % 95.56/14.36 % (2773836)Instructions burned: 8 (million) % 95.56/14.36 % (2773838)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=2340285357:i=8327:s2at=5:bd=preordered_2895 on theBenchmark for (2895ds/8327Mi) % 95.56/14.36 % (2773832)Refutation not found, incomplete strategy % 95.56/14.36 % (2773832)------------------------------ % 95.56/14.36 % (2773832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.56/14.36 % (2773832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.56/14.36 % (2773832)CaDiCaL version: 2.1.3 % 95.56/14.36 % (2773832)Termination reason: Refutation not found, incomplete strategy % 95.56/14.36 % (2773832)Time elapsed: 0.536 s % 95.56/14.36 % (2773832)Peak memory usage: 135 MB % 95.56/14.36 % (2773832)Instructions burned: 1002 (million) % 95.56/14.36 % (2773836)------------------------------ % 95.56/14.36 % (2773836)------------------------------ % 95.56/14.36 % (2773832)------------------------------ % 95.56/14.36 % (2773832)------------------------------ % 95.56/14.36 % (2773841)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=1108153081:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2892 on theBenchmark for (2892ds/1083Mi) % 95.56/14.36 % (2773843)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=349927026:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2890 on theBenchmark for (2890ds/1084Mi) % 95.56/14.36 % (2773843)Refutation not found, incomplete strategy % 95.56/14.36 % (2773843)------------------------------ % 95.56/14.36 % (2773843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.56/14.36 % (2773843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.56/14.36 % (2773843)CaDiCaL version: 2.1.3 % 95.56/14.36 % (2773843)Termination reason: Refutation not found, incomplete strategy % 95.56/14.36 % (2773843)Time elapsed: 0.002 s % 95.56/14.36 % (2773843)Peak memory usage: 86 MB % 96.48/14.51 % (2773843)Instructions burned: 2 (million) % 96.48/14.51 % (2773843)------------------------------ % 96.48/14.51 % (2773843)------------------------------ % 96.48/14.51 % (2773841)Instruction limit reached! % 96.48/14.51 % (2773841)------------------------------ % 96.48/14.51 % (2773841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.48/14.51 % (2773841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.48/14.51 % (2773841)CaDiCaL version: 2.1.3 % 96.48/14.51 % (2773841)Termination reason: Instruction limit % 96.48/14.51 % (2773841)Termination phase: Saturation % 96.48/14.51 % (2773841)Time elapsed: 0.468 s % 96.48/14.51 % (2773841)Peak memory usage: 101 MB % 96.48/14.51 % (2773841)Instructions burned: 1083 (million) % 96.48/14.51 % (2773845)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1932301738:i=6995:s2at=5:gtg=all_2886 on theBenchmark for (2886ds/6995Mi) % 96.48/14.51 % (2773846)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3976530024:st=2:i=6225:sd=15:ss=axioms_2886 on theBenchmark for (2886ds/6225Mi) % 96.48/14.51 % (2773846)Refutation not found, incomplete strategy % 96.48/14.51 % (2773846)------------------------------ % 96.48/14.51 % (2773846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.48/14.51 % (2773846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.48/14.51 % (2773846)CaDiCaL version: 2.1.3 % 96.48/14.51 % (2773846)Termination reason: Refutation not found, incomplete strategy % 96.48/14.51 % (2773846)Time elapsed: 0.003 s % 96.48/14.51 % (2773846)Peak memory usage: 86 MB % 96.48/14.51 % (2773846)Instructions burned: 4 (million) % 96.48/14.51 % (2773846)------------------------------ % 96.48/14.51 % (2773846)------------------------------ % 96.48/14.51 % (2773849)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1205087713:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2881 on theBenchmark for (2881ds/3372Mi) % 96.48/14.51 [W927 21:41:47.019248880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.51 [W927 21:41:47.019287875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.51 [W927 21:41:47.019319271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.51 [W927 21:41:47.019328595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.52 [W927 21:41:47.019351159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.52 [W927 21:41:47.019359802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.52 [W927 21:41:47.019382121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.52 [W927 21:41:47.019390979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.28/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.28/14.72 [W927 21:41:47.019412984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.28/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.28/14.72 [W927 21:41:47.019421959 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.28/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.28/14.72 [W927 21:41:47.019444279 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.28/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.28/14.72 [W927 21:41:47.019453094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.28/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.28/14.72 % (2773849)Refutation not found, incomplete strategy % 97.28/14.72 % (2773849)------------------------------ % 97.28/14.72 % (2773849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.28/14.72 % (2773849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.28/14.72 % (2773849)CaDiCaL version: 2.1.3 % 97.28/14.72 % (2773849)Termination reason: Refutation not found, incomplete strategy % 97.28/14.72 % (2773849)Time elapsed: 0.458 s % 97.28/14.72 % (2773849)Peak memory usage: 126 MB % 97.28/14.72 % (2773849)Instructions burned: 839 (million) % 97.28/14.72 % (2773849)------------------------------ % 97.28/14.72 % (2773849)------------------------------ % 97.28/14.72 % (2773851)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=156243839:st=2.3:i=26457:sd=10:ss=included:sgt=8_2873 on theBenchmark for (2873ds/26457Mi) % 97.28/14.72 % (2773851)Refutation not found, incomplete strategy % 97.28/14.72 % (2773851)------------------------------ % 97.28/14.72 % (2773851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.28/14.72 % (2773851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.28/14.72 % (2773851)CaDiCaL version: 2.1.3 % 97.28/14.72 % (2773851)Termination reason: Refutation not found, incomplete strategy % 97.28/14.72 % (2773851)Time elapsed: 0.358 s % 97.28/14.72 % (2773851)Peak memory usage: 135 MB % 97.28/14.72 % (2773851)Instructions burned: 1002 (million) % 97.28/14.72 % (2773851)------------------------------ % 97.28/14.72 % (2773851)------------------------------ % 97.28/14.72 % (2773838)Instruction limit reached! % 97.28/14.72 % (2773838)------------------------------ % 97.28/14.72 % (2773838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.28/14.72 % (2773838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.28/14.72 % (2773838)CaDiCaL version: 2.1.3 % 97.28/14.72 % (2773838)Termination reason: Instruction limit % 97.28/14.72 % (2773838)Termination phase: Saturation % 97.28/14.72 % (2773838)Time elapsed: 2.925 s % 97.28/14.72 % (2773838)Peak memory usage: 145 MB % 97.28/14.72 % (2773838)Instructions burned: 8330 (million) % 97.28/14.72 % (2773959)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=1659773074:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2866 on theBenchmark for (2866ds/13494Mi) % 97.28/14.72 % (2774001)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=199215648:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2865 on theBenchmark for (2865ds/2503Mi) % 97.28/14.72 % (2773805)Instruction limit reached! % 97.28/14.72 % (2773805)------------------------------ % 97.28/14.72 % (2773805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.28/14.72 % (2773805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.89/15.99 % (2773805)CaDiCaL version: 2.1.3 % 106.89/15.99 % (2773805)Termination reason: Instruction limit % 106.89/15.99 % (2773805)Termination phase: Saturation % 106.89/15.99 % (2773805)Time elapsed: 6.897 s % 106.89/15.99 % (2773805)Peak memory usage: 208 MB % 106.89/15.99 % (2773805)Instructions burned: 14124 (million) % 106.89/15.99 [W927 21:41:48.517103525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517129849 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517151099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517158615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517173251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517179609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517193519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517199812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517212518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517218962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517232538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 [W927 21:41:48.517238985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.89/15.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.89/15.99 % (2774010)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2895765228:i=2559:sd=1:ep=RSTC:ss=axioms_2863 on theBenchmark for (2863ds/2559Mi) % 111.12/16.58 % (2774001)Refutation not found, incomplete strategy % 111.12/16.58 % (2774001)------------------------------ % 111.12/16.58 % (2774001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.12/16.58 % (2774001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.12/16.58 % (2774001)CaDiCaL version: 2.1.3 % 111.12/16.58 % (2774001)Termination reason: Refutation not found, incomplete strategy % 111.12/16.58 % (2774001)Time elapsed: 0.303 s % 111.12/16.58 % (2774001)Peak memory usage: 126 MB % 111.12/16.58 % (2774001)Instructions burned: 827 (million) % 111.12/16.58 [W927 21:41:49.731705301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731731885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731769351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731775651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731788406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731794969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731808467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731814859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731828343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731834490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.12/16.58 [W927 21:41:49.731847870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.12/16.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 115.71/17.17 [W927 21:41:49.731854067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 115.71/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 115.71/17.17 % (2774001)------------------------------ % 115.71/17.17 % (2774001)------------------------------ % 115.71/17.17 % (2774010)Refutation not found, incomplete strategy % 115.71/17.17 % (2774010)------------------------------ % 115.71/17.17 % (2774010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.71/17.17 % (2774010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.71/17.17 % (2774010)CaDiCaL version: 2.1.3 % 115.71/17.17 % (2774010)Termination reason: Refutation not found, incomplete strategy % 115.71/17.17 % (2774010)Time elapsed: 0.305 s % 115.71/17.17 % (2774010)Peak memory usage: 126 MB % 115.71/17.17 % (2774010)Instructions burned: 830 (million) % 115.71/17.17 % (2773845)Instruction limit reached! % 115.71/17.17 % (2773845)------------------------------ % 115.71/17.17 % (2773845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.71/17.17 % (2773845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.71/17.17 % (2773845)CaDiCaL version: 2.1.3 % 115.71/17.17 % (2773845)Termination reason: Instruction limit % 115.71/17.17 % (2773845)Termination phase: Saturation % 115.71/17.17 % (2773845)Time elapsed: 2.571 s % 115.71/17.17 % (2773845)Peak memory usage: 157 MB % 115.71/17.17 % (2773845)Instructions burned: 6998 (million) % 115.71/17.17 % (2774012)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=782189208:i=30753:av=off:ss=included_2859 on theBenchmark for (2859ds/30753Mi) % 115.71/17.17 % (2774010)------------------------------ % 115.71/17.17 % (2774010)------------------------------ % 115.71/17.17 % (2774013)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2160837684:i=26473:ep=RSTC_2858 on theBenchmark for (2858ds/26473Mi) % 115.71/17.17 % (2774015)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=2734297872:cts=off:i=2759:kws=inv_arity:fgj=on_2857 on theBenchmark for (2857ds/2759Mi) % 115.71/17.17 % (2774015)Refutation not found, incomplete strategy % 115.71/17.17 % (2774015)------------------------------ % 115.71/17.17 % (2774015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.71/17.17 % (2774015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.71/17.17 % (2774015)CaDiCaL version: 2.1.3 % 115.71/17.17 % (2774015)Termination reason: Refutation not found, incomplete strategy % 115.71/17.17 % (2774015)Time elapsed: 0.369 s % 115.71/17.17 % (2774015)Peak memory usage: 137 MB % 115.71/17.17 % (2774015)Instructions burned: 1028 (million) % 115.71/17.17 % (2774015)------------------------------ % 115.71/17.17 % (2774015)------------------------------ % 115.71/17.17 % (2774018)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=651645058:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2850 on theBenchmark for (2850ds/5665Mi) % 115.71/17.17 [W927 21:41:50.998328906 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 115.71/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 115.71/17.17 [W927 21:41:50.998350884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 115.71/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 115.71/17.17 [W927 21:41:50.998389075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 115.71/17.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 115.71/17.17 [W927 21:41:50.998395735 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998409715 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998415417 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998428862 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998434622 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998447548 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998452961 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998465832 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.998471425 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 % (2774018)Refutation not found, incomplete strategy % 116.30/17.26 % (2774018)------------------------------ % 116.30/17.26 % (2774018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.30/17.26 % (2774018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.30/17.26 % (2774018)CaDiCaL version: 2.1.3 % 116.30/17.26 % (2774018)Termination reason: Refutation not found, incomplete strategy % 116.30/17.26 % (2774018)Time elapsed: 0.306 s % 116.30/17.26 % (2774018)Peak memory usage: 126 MB % 116.30/17.26 % (2774018)Instructions burned: 828 (million) % 116.30/17.26 % (2774018)------------------------------ % 116.30/17.26 % (2774018)------------------------------ % 116.30/17.26 % (2774020)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=2746400992:i=1532:ep=RS:ss=axioms_2844 on theBenchmark for (2844ds/1532Mi) % 116.30/17.26 [W927 21:41:50.584531015 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.30/17.26 [W927 21:41:50.584552331 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/17.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584590246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584596191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584609678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584615162 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584628126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584633439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584645557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584650831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584663291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 [W927 21:41:50.584668727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 124.36/18.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 124.36/18.44 % (2774020)Refutation not found, incomplete strategy % 124.36/18.44 % (2774020)------------------------------ % 124.36/18.44 % (2774020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.36/18.44 % (2774020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.36/18.44 % (2774020)CaDiCaL version: 2.1.3 % 124.36/18.44 % (2774020)Termination reason: Refutation not found, incomplete strategy % 124.36/18.44 % (2774020)Time elapsed: 0.303 s % 124.36/18.44 % (2774020)Peak memory usage: 126 MB % 124.36/18.44 % (2774020)Instructions burned: 831 (million) % 124.36/18.44 % (2774020)------------------------------ % 124.36/18.44 % (2774020)------------------------------ % 124.36/18.44 % (2774022)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3375739887:i=1565:sd=2:ss=axioms:sgt=32_2838 on theBenchmark for (2838ds/1565Mi) % 124.36/18.44 [W927 21:41:51.173234702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173255807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173275966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173282390 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173295455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173301009 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173314380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173319990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173332976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173338529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173351652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 [W927 21:41:51.173357069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.06/19.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.06/19.05 % (2774022)Refutation not found, incomplete strategy % 129.06/19.05 % (2774022)------------------------------ % 129.06/19.05 % (2774022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.06/19.05 % (2774022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.06/19.05 % (2774022)CaDiCaL version: 2.1.3 % 129.06/19.05 % (2774022)Termination reason: Refutation not found, incomplete strategy % 129.06/19.05 % (2774022)Time elapsed: 0.306 s % 129.06/19.05 % (2774022)Peak memory usage: 126 MB % 129.06/19.05 % (2774022)Instructions burned: 833 (million) % 132.89/19.64 % (2774022)------------------------------ % 132.89/19.64 % (2774022)------------------------------ % 132.89/19.64 % (2774024)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=1144784509:i=1572:fgj=on:gsp=on_2832 on theBenchmark for (2832ds/1572Mi) % 132.89/19.64 % (2774024)Instruction limit reached! % 132.89/19.64 % (2774024)------------------------------ % 132.89/19.64 % (2774024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.89/19.64 % (2774024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.89/19.64 % (2774024)CaDiCaL version: 2.1.3 % 132.89/19.64 % (2774024)Termination reason: Instruction limit % 132.89/19.64 % (2774024)Termination phase: Saturation % 132.89/19.64 % (2774024)Time elapsed: 0.539 s % 132.89/19.64 % (2774024)Peak memory usage: 138 MB % 132.89/19.64 % (2774024)Instructions burned: 1572 (million) % 132.89/19.64 % (2774026)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3665066208:i=6052:sd=4:ss=axioms:sgt=24_2826 on theBenchmark for (2826ds/6052Mi) % 132.89/19.64 % (2773959)Instruction limit reached! % 132.89/19.64 % (2773959)------------------------------ % 132.89/19.64 % (2773959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.89/19.64 % (2773959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.89/19.64 % (2773959)CaDiCaL version: 2.1.3 % 132.89/19.64 % (2773959)Termination reason: Instruction limit % 132.89/19.64 % (2773959)Termination phase: Saturation % 132.89/19.64 % (2773959)Time elapsed: 4.093 s % 132.89/19.64 % (2773959)Peak memory usage: 241 MB % 132.89/19.64 % (2773959)Instructions burned: 13494 (million) % 132.89/19.64 [W927 21:41:52.443840211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443865478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443903880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443910218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443923738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443929251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443942671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443957431 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.89/19.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.89/19.64 [W927 21:41:52.443972173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:52.443977669 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:52.443990679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:52.443996091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 % (2774028)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=2712651797:i=3500:sd=1:bd=preordered:sup=off:ss=included_2823 on theBenchmark for (2823ds/3500Mi) % 144.46/21.28 % (2774026)Refutation not found, incomplete strategy % 144.46/21.28 % (2774026)------------------------------ % 144.46/21.28 % (2774026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.46/21.28 % (2774026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.46/21.28 % (2774026)CaDiCaL version: 2.1.3 % 144.46/21.28 % (2774026)Termination reason: Refutation not found, incomplete strategy % 144.46/21.28 % (2774026)Time elapsed: 0.310 s % 144.46/21.28 % (2774026)Peak memory usage: 126 MB % 144.46/21.28 % (2774026)Instructions burned: 829 (million) % 144.46/21.28 % (2774026)------------------------------ % 144.46/21.28 % (2774026)------------------------------ % 144.46/21.28 % (2774028)Refutation not found, incomplete strategy % 144.46/21.28 % (2774028)------------------------------ % 144.46/21.28 % (2774028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.46/21.28 % (2774028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.46/21.28 % (2774028)CaDiCaL version: 2.1.3 % 144.46/21.28 % (2774028)Termination reason: Refutation not found, incomplete strategy % 144.46/21.28 % (2774028)Time elapsed: 0.362 s % 144.46/21.28 % (2774028)Peak memory usage: 136 MB % 144.46/21.28 % (2774028)Instructions burned: 1007 (million) % 144.46/21.28 % (2774030)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=4028119531:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2819 on theBenchmark for (2819ds/1842Mi) % 144.46/21.28 % (2774028)------------------------------ % 144.46/21.28 % (2774028)------------------------------ % 144.46/21.28 [W927 21:41:53.056342058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:53.056364811 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:53.056403212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 144.46/21.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 144.46/21.28 [W927 21:41:53.056409527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056424258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056430199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056453850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056459874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056473298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056478820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056491925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:53.056497561 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 % (2774032)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1942915543:i=66096:add=on_2817 on theBenchmark for (2817ds/66096Mi) % 150.90/22.12 % (2774030)Refutation not found, incomplete strategy % 150.90/22.12 % (2774030)------------------------------ % 150.90/22.12 % (2774030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.90/22.12 % (2774030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.90/22.12 % (2774030)CaDiCaL version: 2.1.3 % 150.90/22.12 % (2774030)Termination reason: Refutation not found, incomplete strategy % 150.90/22.12 % (2774030)Time elapsed: 0.312 s % 150.90/22.12 % (2774030)Peak memory usage: 126 MB % 150.90/22.12 % (2774030)Instructions burned: 839 (million) % 150.90/22.12 % (2774030)------------------------------ % 150.90/22.12 % (2774030)------------------------------ % 150.90/22.12 % (2774034)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2766481875:i=1884:sd=1:nm=60:ss=axioms_2813 on theBenchmark for (2813ds/1884Mi) % 150.90/22.12 [W927 21:41:54.647010507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 150.90/22.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 150.90/22.12 [W927 21:41:54.647050875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647072609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647078955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647103065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647109261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647122952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647128661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647141508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647147079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647160528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 [W927 21:41:54.647166074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.30/23.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.30/23.04 % (2774034)Refutation not found, incomplete strategy % 157.30/23.04 % (2774034)------------------------------ % 157.30/23.04 % (2774034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.30/23.04 % (2774034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.30/23.04 % (2774034)CaDiCaL version: 2.1.3 % 157.30/23.04 % (2774034)Termination reason: Refutation not found, incomplete strategy % 157.30/23.04 % (2774034)Time elapsed: 0.298 s % 157.30/23.04 % (2774034)Peak memory usage: 126 MB % 157.30/23.04 % (2774034)Instructions burned: 827 (million) % 157.30/23.04 % (2774034)------------------------------ % 157.30/23.04 % (2774034)------------------------------ % 157.30/23.04 % (2774036)lrs-1011_4:1_sil=16000:bsr=on:random_seed=64020110:cts=off:i=5469:bs=on:fsr=off_2807 on theBenchmark for (2807ds/5469Mi) % 157.30/23.04 % (2774012)Instruction limit reached! % 157.30/23.04 % (2774012)------------------------------ % 157.30/23.04 % (2774012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.27/23.44 % (2774012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.27/23.44 % (2774012)CaDiCaL version: 2.1.3 % 159.27/23.44 % (2774012)Termination reason: Instruction limit % 159.27/23.44 % (2774012)Termination phase: Saturation % 159.27/23.44 % (2774012)Time elapsed: 6.393 s % 159.27/23.44 % (2774012)Peak memory usage: 145 MB % 159.27/23.44 % (2774012)Instructions burned: 30754 (million) % 159.27/23.44 % (2774038)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=2195653671:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2794 on theBenchmark for (2794ds/2037Mi) % 159.27/23.44 % (2774036)Instruction limit reached! % 159.27/23.44 % (2774036)------------------------------ % 159.27/23.44 % (2774036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.27/23.44 % (2774036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.27/23.44 % (2774036)CaDiCaL version: 2.1.3 % 159.27/23.44 % (2774036)Termination reason: Instruction limit % 159.27/23.44 % (2774036)Termination phase: Saturation % 159.27/23.44 % (2774036)Time elapsed: 1.756 s % 159.27/23.44 % (2774036)Peak memory usage: 108 MB % 159.27/23.44 % (2774036)Instructions burned: 5474 (million) % 159.27/23.44 % (2774040)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3158239788:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2789 on theBenchmark for (2789ds/2110Mi) % 159.27/23.44 % (2774038)Instruction limit reached! % 159.27/23.44 % (2774038)------------------------------ % 159.27/23.44 % (2774038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.27/23.44 % (2774038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.27/23.44 % (2774038)CaDiCaL version: 2.1.3 % 159.27/23.44 % (2774038)Termination reason: Instruction limit % 159.27/23.44 % (2774038)Termination phase: Saturation % 159.27/23.44 % (2774038)Time elapsed: 0.670 s % 159.27/23.44 % (2774038)Peak memory usage: 140 MB % 159.27/23.44 % (2774038)Instructions burned: 2039 (million) % 159.27/23.44 [W927 21:41:56.126468691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126491361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126511851 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126519054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126533775 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126540301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.27/23.44 [W927 21:41:56.126554664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.27/23.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 [W927 21:41:56.126560997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.23/24.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 [W927 21:41:56.126573838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.23/24.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 [W927 21:41:56.126586921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.23/24.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 [W927 21:41:56.126601661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.23/24.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 [W927 21:41:56.126607400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.23/24.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.23/24.39 % (2774040)Refutation not found, incomplete strategy % 166.23/24.39 % (2774040)------------------------------ % 166.23/24.39 % (2774040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.23/24.39 % (2774040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.23/24.39 % (2774040)CaDiCaL version: 2.1.3 % 166.23/24.39 % (2774040)Termination reason: Refutation not found, incomplete strategy % 166.23/24.39 % (2774040)Time elapsed: 0.307 s % 166.23/24.39 % (2774040)Peak memory usage: 126 MB % 166.23/24.39 % (2774040)Instructions burned: 829 (million) % 166.23/24.39 % (2774042)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=4224799238:i=2430:add=off:aac=none:nm=16_2785 on theBenchmark for (2785ds/2430Mi) % 166.23/24.39 % (2774040)------------------------------ % 166.23/24.39 % (2774040)------------------------------ % 166.23/24.39 % (2773835)Instruction limit reached! % 166.23/24.39 % (2773835)------------------------------ % 166.23/24.39 % (2773835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.23/24.39 % (2773835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.23/24.39 % (2773835)CaDiCaL version: 2.1.3 % 166.23/24.39 % (2773835)Termination reason: Instruction limit % 166.23/24.39 % (2773835)Termination phase: Saturation % 166.23/24.39 % (2773835)Time elapsed: 11.383 s % 166.23/24.39 % (2773835)Peak memory usage: 203 MB % 166.23/24.39 % (2773835)Instructions burned: 33336 (million) % 166.23/24.39 % (2774044)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=2292930199:cond=fast:i=4891_2783 on theBenchmark for (2783ds/4891Mi) % 166.23/24.39 % (2774045)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=2802327147:st=2:i=14845:sd=2:ss=included:fsd=on_2782 on theBenchmark for (2782ds/14845Mi) % 166.23/24.39 % (2774045)Refutation not found, incomplete strategy % 166.23/24.39 % (2774045)------------------------------ % 166.23/24.39 % (2774045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.23/24.39 % (2774045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.23/24.39 % (2774045)CaDiCaL version: 2.1.3 % 166.23/24.39 % (2774045)Termination reason: Refutation not found, incomplete strategy % 166.23/24.39 % (2774045)Time elapsed: 0.359 s % 166.23/24.39 % (2774045)Peak memory usage: 136 MB % 166.23/24.39 % (2774045)Instructions burned: 981 (million) % 166.23/24.39 % (2774042)Instruction limit reached! % 166.23/24.39 % (2774042)------------------------------ % 166.23/24.39 % (2774042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.10/25.63 % (2774042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.10/25.63 % (2774042)CaDiCaL version: 2.1.3 % 175.10/25.63 % (2774042)Termination reason: Instruction limit % 175.10/25.63 % (2774042)Termination phase: Saturation % 175.10/25.63 % (2774042)Time elapsed: 0.807 s % 175.10/25.63 % (2774042)Peak memory usage: 144 MB % 175.10/25.63 % (2774042)Instructions burned: 2431 (million) % 175.10/25.63 % (2774045)------------------------------ % 175.10/25.63 % (2774045)------------------------------ % 175.10/25.63 % (2774048)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2304592094:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2776 on theBenchmark for (2776ds/7534Mi) % 175.10/25.63 % (2774049)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=965211380:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2775 on theBenchmark for (2775ds/10353Mi) % 175.10/25.63 % (2774013)Instruction limit reached! % 175.10/25.63 % (2774013)------------------------------ % 175.10/25.63 % (2774013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.10/25.63 % (2774013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.10/25.63 % (2774013)CaDiCaL version: 2.1.3 % 175.10/25.63 % (2774013)Termination reason: Instruction limit % 175.10/25.63 % (2774013)Termination phase: Saturation % 175.10/25.63 % (2774013)Time elapsed: 8.444 s % 175.10/25.63 % (2774013)Peak memory usage: 379 MB % 175.10/25.63 % (2774013)Instructions burned: 26475 (million) % 175.10/25.63 [W927 21:41:57.451923722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.451940795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.451980165 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.451986429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.452008708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.452016435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.452032439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.452038951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 175.10/25.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 175.10/25.63 [W927 21:41:57.452053409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.24/26.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.24/26.00 [W927 21:41:57.452059866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.24/26.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.24/26.00 [W927 21:41:57.452073516 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.24/26.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.24/26.00 [W927 21:41:57.452086394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.24/26.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.24/26.00 % (2774049)Refutation not found, incomplete strategy % 177.24/26.00 % (2774049)------------------------------ % 177.24/26.00 % (2774049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.24/26.00 % (2774049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.24/26.00 % (2774049)CaDiCaL version: 2.1.3 % 177.24/26.00 % (2774049)Termination reason: Refutation not found, incomplete strategy % 177.24/26.00 % (2774049)Time elapsed: 0.309 s % 177.24/26.00 % (2774049)Peak memory usage: 126 MB % 177.24/26.00 % (2774049)Instructions burned: 831 (million) % 177.24/26.00 % (2774052)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2349841389:i=7860_2772 on theBenchmark for (2772ds/7860Mi) % 177.24/26.00 % (2774052)Refutation not found, incomplete strategy % 177.24/26.00 % (2774052)------------------------------ % 177.24/26.00 % (2774052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.24/26.00 % (2774052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.24/26.00 % (2774052)CaDiCaL version: 2.1.3 % 177.24/26.00 % (2774052)Termination reason: Refutation not found, incomplete strategy % 177.24/26.00 % (2774052)Time elapsed: 0.022 s % 177.24/26.00 % (2774052)Peak memory usage: 90 MB % 177.24/26.00 % (2774052)Instructions burned: 84 (million) % 177.24/26.00 % (2774049)------------------------------ % 177.24/26.00 % (2774049)------------------------------ % 177.24/26.00 % (2774052)------------------------------ % 177.24/26.00 % (2774052)------------------------------ % 177.24/26.00 % (2774054)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=2278733012:i=7896:sd=2:bs=on:ss=included:sgt=20_2769 on theBenchmark for (2769ds/7896Mi) % 177.24/26.00 % (2774055)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3063413601:i=5812:gtgl=2:gtg=all_2769 on theBenchmark for (2769ds/5812Mi) % 177.24/26.00 % (2774044)Instruction limit reached! % 177.24/26.00 % (2774044)------------------------------ % 177.24/26.00 % (2774044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.24/26.00 % (2774044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.24/26.00 % (2774044)CaDiCaL version: 2.1.3 % 177.24/26.00 % (2774044)Termination reason: Instruction limit % 177.24/26.00 % (2774044)Termination phase: Saturation % 177.24/26.00 % (2774044)Time elapsed: 1.379 s % 177.24/26.00 % (2774044)Peak memory usage: 142 MB % 177.24/26.00 % (2774044)Instructions burned: 4895 (million) % 177.24/26.00 % (2774058)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=704401046:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2767 on theBenchmark for (2767ds/2965Mi) % 177.24/26.00 % (2774058)Refutation not found, incomplete strategy % 177.24/26.00 % (2774058)------------------------------ % 177.24/26.00 % (2774058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.24/26.00 % (2774058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.24/26.00 % (2774058)CaDiCaL version: 2.1.3 % 177.24/26.00 % (2774058)Termination reason: Refutation not found, incomplete strategy % 177.24/26.00 % (2774058)Time elapsed: 0.364 s % 177.24/26.00 % (2774058)Peak memory usage: 136 MB % 179.60/26.27 % (2774058)Instructions burned: 1029 (million) % 179.60/26.27 % (2774058)------------------------------ % 179.60/26.27 % (2774058)------------------------------ % 179.60/26.27 % (2774060)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=3705318539:i=2967:kws=precedence:bd=preordered:av=off_2761 on theBenchmark for (2761ds/2967Mi) % 179.60/26.27 % (2774048)Instruction limit reached! % 179.60/26.27 % (2774048)------------------------------ % 179.60/26.27 % (2774048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 179.60/26.27 % (2774048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.60/26.27 % (2774048)CaDiCaL version: 2.1.3 % 179.60/26.27 % (2774048)Termination reason: Instruction limit % 179.60/26.27 % (2774048)Termination phase: Saturation % 179.60/26.27 % (2774048)Time elapsed: 2.101 s % 179.60/26.27 % (2774048)Peak memory usage: 154 MB % 179.60/26.27 % (2774048)Instructions burned: 7535 (million) % 179.60/26.27 % (2774062)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=2076384376:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2754 on theBenchmark for (2754ds/3022Mi) % 179.60/26.27 [W927 21:42:00.639406357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639427977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639448970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639456319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639470735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639477433 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639491843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639498396 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639512021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 179.60/26.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 179.60/26.27 [W927 21:42:00.639518615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.639532176 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.639538016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 % (2774060)Instruction limit reached! % 180.28/26.39 % (2774060)------------------------------ % 180.28/26.39 % (2774060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.28/26.39 % (2774060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/26.39 % (2774060)CaDiCaL version: 2.1.3 % 180.28/26.39 % (2774060)Termination reason: Instruction limit % 180.28/26.39 % (2774060)Termination phase: Saturation % 180.28/26.39 % (2774060)Time elapsed: 0.972 s % 180.28/26.39 % (2774060)Peak memory usage: 146 MB % 180.28/26.39 % (2774060)Instructions burned: 2967 (million) % 180.28/26.39 % (2774062)Refutation not found, incomplete strategy % 180.28/26.39 % (2774062)------------------------------ % 180.28/26.39 % (2774062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.28/26.39 % (2774062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/26.39 % (2774062)CaDiCaL version: 2.1.3 % 180.28/26.39 % (2774062)Termination reason: Refutation not found, incomplete strategy % 180.28/26.39 % (2774062)Time elapsed: 0.303 s % 180.28/26.39 % (2774062)Peak memory usage: 126 MB % 180.28/26.39 % (2774062)Instructions burned: 832 (million) % 180.28/26.39 % (2774064)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=3074767833:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2750 on theBenchmark for (2750ds/3207Mi) % 180.28/26.39 % (2774062)------------------------------ % 180.28/26.39 % (2774062)------------------------------ % 180.28/26.39 % (2774055)Instruction limit reached! % 180.28/26.39 % (2774055)------------------------------ % 180.28/26.39 % (2774055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.28/26.39 % (2774055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.28/26.39 % (2774055)CaDiCaL version: 2.1.3 % 180.28/26.39 % (2774055)Termination reason: Instruction limit % 180.28/26.39 % (2774055)Termination phase: Saturation % 180.28/26.39 % (2774055)Time elapsed: 2.029 s % 180.28/26.39 % (2774055)Peak memory usage: 170 MB % 180.28/26.39 % (2774055)Instructions burned: 5812 (million) % 180.28/26.39 [W927 21:42:00.007618901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.007649916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.007672777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.007679370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.28/26.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.28/26.39 [W927 21:42:00.007693173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007698973 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007712263 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007718133 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007731037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007736800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007749847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.007755633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 % (2774066)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1753509688:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2748 on theBenchmark for (2748ds/3289Mi) % 182.42/26.88 % (2774067)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2904054398:i=38569:sd=3:ss=axioms:sgt=32_2747 on theBenchmark for (2747ds/38569Mi) % 182.42/26.88 % (2774064)Refutation not found, incomplete strategy % 182.42/26.88 % (2774064)------------------------------ % 182.42/26.88 % (2774064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.42/26.88 % (2774064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.42/26.88 % (2774064)CaDiCaL version: 2.1.3 % 182.42/26.88 % (2774064)Termination reason: Refutation not found, incomplete strategy % 182.42/26.88 % (2774064)Time elapsed: 0.307 s % 182.42/26.88 % (2774064)Peak memory usage: 126 MB % 182.42/26.88 % (2774064)Instructions burned: 832 (million) % 182.42/26.88 % (2774064)------------------------------ % 182.42/26.88 % (2774064)------------------------------ % 182.42/26.88 [W927 21:42:00.274065800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.274088988 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.42/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.42/26.88 [W927 21:42:00.274110230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274117183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274130668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274136533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274149650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274155428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274168374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274174226 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274186963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 [W927 21:42:00.274192814 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 187.79/27.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 187.79/27.48 % (2774067)Refutation not found, incomplete strategy % 187.79/27.48 % (2774067)------------------------------ % 187.79/27.48 % (2774067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.79/27.48 % (2774067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.79/27.48 % (2774067)CaDiCaL version: 2.1.3 % 187.79/27.48 % (2774067)Termination reason: Refutation not found, incomplete strategy % 187.79/27.48 % (2774067)Time elapsed: 0.304 s % 187.79/27.48 % (2774067)Peak memory usage: 126 MB % 187.79/27.48 % (2774067)Instructions burned: 827 (million) % 187.79/27.48 % (2774066)Refutation not found, incomplete strategy % 187.79/27.48 % (2774066)------------------------------ % 187.79/27.48 % (2774066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.79/27.48 % (2774066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.79/27.48 % (2774066)CaDiCaL version: 2.1.3 % 187.79/27.48 % (2774066)Termination reason: Refutation not found, incomplete strategy % 187.79/27.48 % (2774066)Time elapsed: 0.373 s % 187.79/27.48 % (2774066)Peak memory usage: 136 MB % 187.79/27.48 % (2774066)Instructions burned: 1035 (million) % 187.79/27.48 % (2774070)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3052465866:cts=off:i=3394_2744 on theBenchmark for (2744ds/3394Mi) % 195.32/28.56 % (2774054)Instruction limit reached! % 195.32/28.56 % (2774054)------------------------------ % 195.32/28.56 % (2774054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.32/28.56 % (2774054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.32/28.56 % (2774054)CaDiCaL version: 2.1.3 % 195.32/28.56 % (2774054)Termination reason: Instruction limit % 195.32/28.56 % (2774054)Termination phase: Saturation % 195.32/28.56 % (2774054)Time elapsed: 2.572 s % 195.32/28.56 % (2774054)Peak memory usage: 188 MB % 195.32/28.56 % (2774054)Instructions burned: 7897 (million) % 195.32/28.56 % (2774067)------------------------------ % 195.32/28.56 % (2774067)------------------------------ % 195.32/28.56 % (2774066)------------------------------ % 195.32/28.56 % (2774066)------------------------------ % 195.32/28.56 % (2774072)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=2253124530:i=33824:bd=preordered_2742 on theBenchmark for (2742ds/33824Mi) % 195.32/28.56 % (2774073)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=375489724:i=20684:bd=all:gtg=exists_sym_2741 on theBenchmark for (2741ds/20684Mi) % 195.32/28.56 % (2774074)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=2242286920: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_2741 on theBenchmark for (2741ds/7222Mi) % 195.32/28.56 [W927 21:42:01.886932099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.886955365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.886995176 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.887007853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.887022443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.887029719 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.887043355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.32/28.56 [W927 21:42:01.887049698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.32/28.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.887063435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.887068956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.887081488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.887087435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 % (2774074)Refutation not found, incomplete strategy % 225.15/32.79 % (2774074)------------------------------ % 225.15/32.79 % (2774074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.15/32.79 % (2774074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.15/32.79 % (2774074)CaDiCaL version: 2.1.3 % 225.15/32.79 % (2774074)Termination reason: Refutation not found, incomplete strategy % 225.15/32.79 % (2774074)Time elapsed: 0.310 s % 225.15/32.79 % (2774074)Peak memory usage: 126 MB % 225.15/32.79 % (2774074)Instructions burned: 843 (million) % 225.15/32.79 % (2774074)------------------------------ % 225.15/32.79 % (2774074)------------------------------ % 225.15/32.79 % (2774078)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3713394251:st=4:i=7295:sd=4:ep=R:ss=axioms_2735 on theBenchmark for (2735ds/7295Mi) % 225.15/32.79 % (2774070)Instruction limit reached! % 225.15/32.79 % (2774070)------------------------------ % 225.15/32.79 % (2774070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.15/32.79 % (2774070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.15/32.79 % (2774070)CaDiCaL version: 2.1.3 % 225.15/32.79 % (2774070)Termination reason: Instruction limit % 225.15/32.79 % (2774070)Termination phase: Saturation % 225.15/32.79 % (2774070)Time elapsed: 1.014 s % 225.15/32.79 % (2774070)Peak memory usage: 137 MB % 225.15/32.79 % (2774070)Instructions burned: 3395 (million) % 225.15/32.79 [W927 21:42:01.487487365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.487511745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.487532214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.487540008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.15/32.79 [W927 21:42:01.487554662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.15/32.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487561525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487576271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487582338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487595701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487601778 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487615074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 [W927 21:42:01.487621015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 226.04/32.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 226.04/32.91 % (2774080)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=808739038:i=4036:ins=10_2732 on theBenchmark for (2732ds/4036Mi) % 226.04/32.91 % (2774078)Refutation not found, incomplete strategy % 226.04/32.91 % (2774078)------------------------------ % 226.04/32.91 % (2774078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.04/32.91 % (2774078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.04/32.91 % (2774078)CaDiCaL version: 2.1.3 % 226.04/32.91 % (2774078)Termination reason: Refutation not found, incomplete strategy % 226.04/32.91 % (2774078)Time elapsed: 0.305 s % 226.04/32.91 % (2774078)Peak memory usage: 126 MB % 226.04/32.91 % (2774078)Instructions burned: 828 (million) % 226.04/32.91 % (2774078)------------------------------ % 226.04/32.91 % (2774078)------------------------------ % 226.04/32.91 % (2774082)lrs+10_1_sil=128000:lcm=predicate:random_seed=1421039642:st=3:i=43697:sd=5:ss=axioms_2729 on theBenchmark for (2729ds/43697Mi) % 226.04/32.91 % (2774082)Refutation not found, incomplete strategy % 226.04/32.91 % (2774082)------------------------------ % 226.04/32.91 % (2774082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.04/32.91 % (2774082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.04/32.91 % (2774082)CaDiCaL version: 2.1.3 % 226.04/32.91 % (2774082)Termination reason: Refutation not found, incomplete strategy % 226.04/32.91 % (2774082)Time elapsed: 0.002 s % 226.04/32.91 % (2774082)Peak memory usage: 87 MB % 226.04/32.91 % (2774082)Instructions burned: 4 (million) % 226.04/32.91 % (2774082)------------------------------ % 226.04/32.91 % (2774082)------------------------------ % 226.04/32.91 % (2774084)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=1318676742:i=17599:gtg=all:ss=axioms:fsd=on_2726 on theBenchmark for (2726ds/17599Mi) % 226.04/32.91 % (2774080)Instruction limit reached! % 226.04/32.91 % (2774080)------------------------------ % 229.84/33.43 % (2774080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2774080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2774080)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2774080)Termination reason: Instruction limit % 229.84/33.43 % (2774080)Termination phase: Saturation % 229.84/33.43 % (2774080)Time elapsed: 1.016 s % 229.84/33.43 % (2774080)Peak memory usage: 136 MB % 229.84/33.43 % (2774080)Instructions burned: 4042 (million) % 229.84/33.43 % (2774086)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=1249806214:i=4547:bd=preordered_2721 on theBenchmark for (2721ds/4547Mi) % 229.84/33.43 % (2774086)Instruction limit reached! % 229.84/33.43 % (2774086)------------------------------ % 229.84/33.43 % (2774086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2774086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2774086)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2774086)Termination reason: Instruction limit % 229.84/33.43 % (2774086)Termination phase: Saturation % 229.84/33.43 % (2774086)Time elapsed: 1.527 s % 229.84/33.43 % (2774086)Peak memory usage: 161 MB % 229.84/33.43 % (2774086)Instructions burned: 4548 (million) % 229.84/33.43 % (2774150)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=3033725248:i=9294:av=off_2704 on theBenchmark for (2704ds/9294Mi) % 229.84/33.43 % (2774032)Instruction limit reached! % 229.84/33.43 % (2774032)------------------------------ % 229.84/33.43 % (2774032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2774032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2774032)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2774032)Termination reason: Instruction limit % 229.84/33.43 % (2774032)Termination phase: Saturation % 229.84/33.43 % (2774032)Time elapsed: 12.633 s % 229.84/33.43 % (2774032)Peak memory usage: 144 MB % 229.84/33.43 % (2774032)Instructions burned: 66101 (million) % 229.84/33.43 % (2774152)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=419725455:i=32849:add=on_2689 on theBenchmark for (2689ds/32849Mi) % 229.84/33.43 % (2773649)Instruction limit reached! % 229.84/33.43 % (2773649)------------------------------ % 229.84/33.43 % (2773649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2773649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2773649)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2773649)Termination reason: Instruction limit % 229.84/33.43 % (2773649)Termination phase: Saturation % 229.84/33.43 % (2773649)Time elapsed: 31.567 s % 229.84/33.43 % (2773649)Peak memory usage: 145 MB % 229.84/33.43 % (2773649)Instructions burned: 141197 (million) % 229.84/33.43 % (2774154)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=802944396:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2682 on theBenchmark for (2682ds/4793Mi) % 229.84/33.43 % (2774150)Instruction limit reached! % 229.84/33.43 % (2774150)------------------------------ % 229.84/33.43 % (2774150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2774150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2774150)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2774150)Termination reason: Instruction limit % 229.84/33.43 % (2774150)Termination phase: Saturation % 229.84/33.43 % (2774150)Time elapsed: 2.324 s % 229.84/33.43 % (2774150)Peak memory usage: 151 MB % 229.84/33.43 % (2774150)Instructions burned: 9298 (million) % 229.84/33.43 % (2774084)Instruction limit reached! % 229.84/33.43 % (2774084)------------------------------ % 229.84/33.43 % (2774084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.84/33.43 % (2774084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.84/33.43 % (2774084)CaDiCaL version: 2.1.3 % 229.84/33.43 % (2774084)Termination reason: Instruction limit % 229.84/33.43 % (2774084)Termination phase: Saturation % 229.84/33.43 % (2774084)Time elapsed: 4.601 s % 229.84/33.43 % (2774084)Peak memory usage: 238 MB % 229.84/33.43 % (2774084)Instructions burned: 17599 (million) % 229.84/33.43 % (2774156)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=1243726970:i=4840:nm=4:av=off_2680 on theBenchmark for (2680ds/4840Mi) % 234.62/34.12 [W927 21:42:07.822687419 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822709831 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822748866 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822755045 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822768574 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822775459 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822789137 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822795585 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822810288 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822816691 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822831008 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 [W927 21:42:07.822837417 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/34.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.62/34.12 % (2774157)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=3346752903:cts=off:i=5002_2679 on theBenchmark for (2679ds/5002Mi) % 234.62/34.12 % (2774154)Refutation not found, incomplete strategy % 234.62/34.12 % (2774154)------------------------------ % 234.62/34.12 % (2774154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.72/38.07 % (2774154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.72/38.07 % (2774154)CaDiCaL version: 2.1.3 % 262.72/38.07 % (2774154)Termination reason: Refutation not found, incomplete strategy % 262.72/38.07 % (2774154)Time elapsed: 0.308 s % 262.72/38.07 % (2774154)Peak memory usage: 126 MB % 262.72/38.07 % (2774154)Instructions burned: 829 (million) % 262.72/38.07 % (2774154)------------------------------ % 262.72/38.07 % (2774154)------------------------------ % 262.72/38.07 % (2774156)Refutation not found, incomplete strategy % 262.72/38.07 % (2774156)------------------------------ % 262.72/38.07 % (2774156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.72/38.07 % (2774156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.72/38.07 % (2774156)CaDiCaL version: 2.1.3 % 262.72/38.07 % (2774156)Termination reason: Refutation not found, incomplete strategy % 262.72/38.07 % (2774156)Time elapsed: 0.367 s % 262.72/38.07 % (2774156)Peak memory usage: 136 MB % 262.72/38.07 % (2774156)Instructions burned: 1027 (million) % 262.72/38.07 % (2774160)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1200944829:i=30479:sd=3:ss=axioms_2676 on theBenchmark for (2676ds/30479Mi) % 265.10/38.45 % (2774072)Instruction limit reached! % 265.10/38.45 % (2774072)------------------------------ % 265.10/38.45 % (2774072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.10/38.45 % (2774072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.10/38.45 % (2774072)CaDiCaL version: 2.1.3 % 265.10/38.45 % (2774072)Termination reason: Instruction limit % 265.10/38.45 % (2774072)Termination phase: Saturation % 265.10/38.45 % (2774072)Time elapsed: 6.748 s % 265.10/38.45 % (2774072)Peak memory usage: 153 MB % 265.10/38.45 % (2774072)Instructions burned: 33831 (million) % 265.10/38.45 % (2774156)------------------------------ % 265.10/38.45 % (2774156)------------------------------ % 265.10/38.45 % (2774073)Instruction limit reached! % 265.10/38.45 % (2774073)------------------------------ % 265.10/38.45 % (2774073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.10/38.45 % (2774073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.10/38.45 % (2774073)CaDiCaL version: 2.1.3 % 265.10/38.45 % (2774073)Termination reason: Instruction limit % 265.10/38.45 % (2774073)Termination phase: Saturation % 265.10/38.45 % (2774073)Time elapsed: 6.772 s % 265.10/38.45 % (2774073)Peak memory usage: 205 MB % 265.10/38.45 % (2774073)Instructions burned: 20684 (million) % 265.10/38.45 [W927 21:42:07.434576710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 265.10/38.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 265.10/38.45 [W927 21:42:07.434600267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 265.10/38.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 265.10/38.45 [W927 21:42:07.434637890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 265.10/38.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 265.10/38.45 [W927 21:42:07.434644232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 265.10/38.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 265.10/38.45 [W927 21:42:07.434657222 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 265.10/38.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 265.10/38.45 [W927 21:42:07.434664140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434678777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434684736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434697480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434703255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434716139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 [W927 21:42:07.434721865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 270.46/39.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 270.46/39.15 % (2774163)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=70444103:i=5835_2673 on theBenchmark for (2673ds/5835Mi) % 270.46/39.15 % (2774162)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=1014319238:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2673 on theBenchmark for (2673ds/11035Mi) % 270.46/39.15 % (2774160)Refutation not found, incomplete strategy % 270.46/39.15 % (2774160)------------------------------ % 270.46/39.15 % (2774160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.46/39.15 % (2774160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.46/39.15 % (2774160)CaDiCaL version: 2.1.3 % 270.46/39.15 % (2774160)Termination reason: Refutation not found, incomplete strategy % 270.46/39.15 % (2774160)Time elapsed: 0.310 s % 270.46/39.15 % (2774160)Peak memory usage: 126 MB % 270.46/39.15 % (2774160)Instructions burned: 831 (million) % 270.46/39.15 % (2774164)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2842366890:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2672 on theBenchmark for (2672ds/5890Mi) % 270.46/39.15 % (2774160)------------------------------ % 270.46/39.15 % (2774160)------------------------------ % 270.46/39.15 % (2774168)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2807798947:cts=off:i=19910:ep=RS_2670 on theBenchmark for (2670ds/19910Mi) % 270.46/39.15 % (2774168)Refutation not found, incomplete strategy % 270.46/39.15 % (2774168)------------------------------ % 270.46/39.15 % (2774168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.46/39.15 % (2774168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.46/39.15 % (2774168)CaDiCaL version: 2.1.3 % 270.46/39.15 % (2774168)Termination reason: Refutation not found, incomplete strategy % 270.46/39.15 % (2774168)Time elapsed: 0.018 s % 270.46/39.15 % (2774168)Peak memory usage: 89 MB % 270.46/39.15 % (2774168)Instructions burned: 74 (million) % 270.46/39.15 % (2774168)------------------------------ % 270.46/39.15 % (2774168)------------------------------ % 270.46/39.15 % (2774170)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=2691339192:i=20312:bd=preordered:fsr=off:er=filter_2666 on theBenchmark for (2666ds/20312Mi) % 277.49/40.17 % (2774157)Instruction limit reached! % 277.49/40.17 % (2774157)------------------------------ % 277.49/40.17 % (2774157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.49/40.17 % (2774157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.49/40.17 % (2774157)CaDiCaL version: 2.1.3 % 277.49/40.17 % (2774157)Termination reason: Instruction limit % 277.49/40.17 % (2774157)Termination phase: Saturation % 277.49/40.17 % (2774157)Time elapsed: 1.592 s % 277.49/40.17 % (2774157)Peak memory usage: 155 MB % 277.49/40.17 % (2774157)Instructions burned: 5004 (million) % 277.49/40.17 % (2774172)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=3630209616:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2662 on theBenchmark for (2662ds/13822Mi) % 277.49/40.17 % (2774163)Instruction limit reached! % 277.49/40.17 % (2774163)------------------------------ % 277.49/40.17 % (2774163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.49/40.17 % (2774163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.49/40.17 % (2774163)CaDiCaL version: 2.1.3 % 277.49/40.17 % (2774163)Termination reason: Instruction limit % 277.49/40.17 % (2774163)Termination phase: Saturation % 277.49/40.17 % (2774163)Time elapsed: 1.629 s % 277.49/40.17 % (2774163)Peak memory usage: 143 MB % 277.49/40.17 % (2774163)Instructions burned: 5836 (million) % 277.49/40.17 % (2774164)Instruction limit reached! % 277.49/40.17 % (2774164)------------------------------ % 277.49/40.17 % (2774164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.49/40.17 % (2774164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.49/40.17 % (2774164)CaDiCaL version: 2.1.3 % 277.49/40.17 % (2774164)Termination reason: Instruction limit % 277.49/40.17 % (2774164)Termination phase: Saturation % 277.49/40.17 % (2774164)Time elapsed: 1.623 s % 277.49/40.17 % (2774164)Peak memory usage: 176 MB % 277.49/40.17 % (2774164)Instructions burned: 5891 (million) % 277.49/40.17 % (2774174)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3734330764:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2656 on theBenchmark for (2656ds/7144Mi) % 277.49/40.18 % (2774176)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2241408013:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2654 on theBenchmark for (2654ds/15184Mi) % 277.49/40.18 % (2774162)Instruction limit reached! % 277.49/40.18 % (2774162)------------------------------ % 277.49/40.18 % (2774162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.49/40.18 % (2774162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.49/40.18 % (2774162)CaDiCaL version: 2.1.3 % 277.49/40.18 % (2774162)Termination reason: Instruction limit % 277.49/40.18 % (2774162)Termination phase: Saturation % 277.49/40.18 % (2774162)Time elapsed: 3.915 s % 277.49/40.18 % (2774162)Peak memory usage: 203 MB % 277.49/40.18 % (2774162)Instructions burned: 11036 (million) % 277.49/40.18 % (2774178)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=3902582417:i=107375_2633 on theBenchmark for (2633ds/107375Mi) % 277.49/40.18 % (2774174)Instruction limit reached! % 277.49/40.18 % (2774174)------------------------------ % 277.49/40.18 % (2774174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.49/40.18 % (2774174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.49/40.18 % (2774174)CaDiCaL version: 2.1.3 % 277.49/40.18 % (2774174)Termination reason: Instruction limit % 277.49/40.18 % (2774174)Termination phase: Saturation % 277.49/40.18 % (2774174)Time elapsed: 2.423 s % 277.49/40.18 % (2774174)Peak memory usage: 132 MB % 277.49/40.18 % (2774174)Instructions burned: 7146 (million) % 277.49/40.18 % (2774180)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=1281275041:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2630 on theBenchmark for (2630ds/7958Mi) % 277.49/40.18 % (2773650)Instruction limit reached! % 277.49/40.18 % (2773650)------------------------------ % 277.49/40.18 % (2773650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.93/40.82 % (2773650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.93/40.82 % (2773650)CaDiCaL version: 2.1.3 % 280.93/40.82 % (2773650)Termination reason: Instruction limit % 280.93/40.82 % (2773650)Termination phase: Saturation % 280.93/40.82 % (2773650)Time elapsed: 37.157 s % 280.93/40.82 % (2773650)Peak memory usage: 248 MB % 280.93/40.82 % (2773650)Instructions burned: 134678 (million) % 280.93/40.82 % (2774182)dis+10_128_sil=16000:nwc=0.7:random_seed=113278609:i=15999:nm=2:gsp=on_2626 on theBenchmark for (2626ds/15999Mi) % 280.93/40.82 % (2774152)Instruction limit reached! % 280.93/40.82 % (2774152)------------------------------ % 280.93/40.82 % (2774152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.93/40.82 % (2774152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.93/40.82 % (2774152)CaDiCaL version: 2.1.3 % 280.93/40.82 % (2774152)Termination reason: Instruction limit % 280.93/40.82 % (2774152)Termination phase: Saturation % 280.93/40.82 % (2774152)Time elapsed: 6.538 s % 280.93/40.82 % (2774152)Peak memory usage: 140 MB % 280.93/40.82 % (2774152)Instructions burned: 32852 (million) % 280.93/40.82 % (2774184)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1156071881:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2622 on theBenchmark for (2622ds/8139Mi) % 280.93/40.82 % (2774172)Instruction limit reached! % 280.93/40.82 % (2774172)------------------------------ % 280.93/40.82 % (2774172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.93/40.82 % (2774172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.93/40.82 % (2774172)CaDiCaL version: 2.1.3 % 280.93/40.82 % (2774172)Termination reason: Instruction limit % 280.93/40.82 % (2774172)Termination phase: Saturation % 280.93/40.82 % (2774172)Time elapsed: 4.188 s % 280.93/40.82 % (2774172)Peak memory usage: 227 MB % 280.93/40.82 % (2774172)Instructions burned: 13825 (million) % 280.93/40.82 % (2774186)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3240480883:st=4:i=8950:sd=5:ss=axioms_2618 on theBenchmark for (2618ds/8950Mi) % 280.93/40.82 [W927 21:42:13.157838641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157876306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157896969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157903114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157916877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157924470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.93/40.82 [W927 21:42:13.157937547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.93/40.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 [W927 21:42:13.157950710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.85/42.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 [W927 21:42:13.157966377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.85/42.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 [W927 21:42:13.157972312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.85/42.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 [W927 21:42:13.157985474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.85/42.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 [W927 21:42:13.157991472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.85/42.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.85/42.12 % (2774186)Refutation not found, incomplete strategy % 290.85/42.12 % (2774186)------------------------------ % 290.85/42.12 % (2774186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.85/42.12 % (2774186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.85/42.12 % (2774186)CaDiCaL version: 2.1.3 % 290.85/42.12 % (2774186)Termination reason: Refutation not found, incomplete strategy % 290.85/42.12 % (2774186)Time elapsed: 0.303 s % 290.85/42.12 % (2774186)Peak memory usage: 126 MB % 290.85/42.12 % (2774186)Instructions burned: 831 (million) % 290.85/42.12 % (2774186)------------------------------ % 290.85/42.12 % (2774186)------------------------------ % 290.85/42.12 % (2774170)Instruction limit reached! % 290.85/42.12 % (2774170)------------------------------ % 290.85/42.12 % (2774170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.85/42.12 % (2774170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.85/42.12 % (2774170)CaDiCaL version: 2.1.3 % 290.85/42.12 % (2774170)Termination reason: Instruction limit % 290.85/42.12 % (2774170)Termination phase: Saturation % 290.85/42.12 % (2774170)Time elapsed: 5.287 s % 290.85/42.12 % (2774170)Peak memory usage: 205 MB % 290.85/42.12 % (2774170)Instructions burned: 20312 (million) % 290.85/42.12 % (2774188)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3474112806:i=9809:ins=10:av=off_2612 on theBenchmark for (2612ds/9809Mi) % 290.85/42.12 % (2774189)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2983391156:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2612 on theBenchmark for (2612ds/9885Mi) % 290.85/42.12 % (2774180)Instruction limit reached! % 290.85/42.12 % (2774180)------------------------------ % 290.85/42.12 % (2774180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.85/42.12 % (2774180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.85/42.12 % (2774180)CaDiCaL version: 2.1.3 % 290.85/42.12 % (2774180)Termination reason: Instruction limit % 290.85/42.12 % (2774180)Termination phase: Saturation % 290.85/42.12 % (2774180)Time elapsed: 2.326 s % 290.85/42.12 % (2774180)Peak memory usage: 198 MB % 290.85/42.12 % (2774180)Instructions burned: 7960 (million) % 290.85/42.12 % (2774176)Instruction limit reached! % 290.85/42.12 % (2774176)------------------------------ % 290.85/42.12 % (2774176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.85/42.12 % (2774176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.85/42.12 % (2774176)CaDiCaL version: 2.1.3 % 290.85/42.12 % (2774176)Termination reason: Instruction limit % 290.85/42.12 % (2774176)Termination phase: Saturation % 290.85/42.12 % (2774176)Time elapsed: 4.830 s % 290.85/42.12 % (2774176)Peak memory usage: 255 MB % 293.55/42.49 % (2774176)Instructions burned: 15185 (million) % 293.55/42.49 % (2774192)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=89417181:cond=fast:i=32078:fgj=on:av=off_2605 on theBenchmark for (2605ds/32078Mi) % 293.55/42.49 % (2774193)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3387617687:i=11101:bd=all:ss=axioms:sgt=8_2605 on theBenchmark for (2605ds/11101Mi) % 293.55/42.49 % (2774193)Refutation not found, incomplete strategy % 293.55/42.49 % (2774193)------------------------------ % 293.55/42.49 % (2774193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.55/42.49 % (2774193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.55/42.49 % (2774193)CaDiCaL version: 2.1.3 % 293.55/42.49 % (2774193)Termination reason: Refutation not found, incomplete strategy % 293.55/42.49 % (2774193)Time elapsed: 0.001 s % 293.55/42.49 % (2774193)Peak memory usage: 87 MB % 293.55/42.49 % (2774193)Instructions burned: 2 (million) % 293.55/42.49 % (2774184)Instruction limit reached! % 293.55/42.49 % (2774184)------------------------------ % 293.55/42.49 % (2774184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.55/42.49 % (2774184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.55/42.49 % (2774184)CaDiCaL version: 2.1.3 % 293.55/42.49 % (2774184)Termination reason: Instruction limit % 293.55/42.49 % (2774184)Termination phase: Saturation % 293.55/42.49 % (2774184)Time elapsed: 1.825 s % 293.55/42.49 % (2774184)Peak memory usage: 97 MB % 293.55/42.49 % (2774184)Instructions burned: 8140 (million) % 293.55/42.49 % (2774193)------------------------------ % 293.55/42.49 % (2774193)------------------------------ % 293.55/42.49 % (2774196)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=2481211354:cond=on:i=13220:s2at=3:aac=none:fsd=on_2603 on theBenchmark for (2603ds/13220Mi) % 293.55/42.49 % (2774197)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3957548795:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2602 on theBenchmark for (2602ds/13528Mi) % 293.55/42.49 [W927 21:42:15.825146713 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825169660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825191516 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825198809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825213171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825219438 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 293.55/42.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 293.55/42.49 [W927 21:42:15.825234194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int inTerminated %------------------------------------------------------------------------------