%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : ITP341_10 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : 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 11:33:39 AM UTC 2026 % Result : Timeout 300.41s 43.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : ITP341_10 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.03/0.30 % Computer : n012.cluster.edu % 0.03/0.30 % Model : x86_64 x86_64 % 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.30 % Memory : 8046.5625MB % 0.03/0.30 % OS : Linux 6.8.0-71-generic % 0.03/0.30 % CPULimit : 300 % 0.03/0.30 % WCLimit : 300 % 0.03/0.30 % DateTime : Sun Sep 27 12:54:49 UTC 2026 % 0.03/0.30 % CPUTime : % 0.03/0.30 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.03/0.32 Running first-order theorem proving % 0.03/0.32 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 % 5.71/1.44 % (2366011)Detected formulas, will run a generic FOF schedule. % 5.71/1.44 % (2366019)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4170524729:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.71/1.44 % (2366022)dis-21_1_sil=8000:lcm=predicate:random_seed=350167165: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) % 5.71/1.44 % (2366017)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=532777337:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.71/1.44 % (2366021)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=407287730:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.71/1.44 % (2366016)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=370741192:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.71/1.44 % (2366018)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=1857625644:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.71/1.44 % (2366020)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1944325396:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.71/1.44 % (2366020)Refutation not found, incomplete strategy % 5.71/1.44 % (2366020)------------------------------ % 5.71/1.44 % (2366020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.44 % (2366020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.44 % (2366019)Refutation not found, incomplete strategy % 5.71/1.44 % (2366019)------------------------------ % 5.71/1.44 % (2366019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.44 % (2366020)CaDiCaL version: 2.1.3 % 5.71/1.44 % (2366020)Termination reason: Refutation not found, incomplete strategy % 5.71/1.44 % (2366020)Time elapsed: 0.0000 s % 5.71/1.44 % (2366020)Peak memory usage: 86 MB % 5.71/1.44 % (2366019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.44 % (2366020)Instructions burned: 1 (million) % 5.71/1.44 % (2366019)CaDiCaL version: 2.1.3 % 5.71/1.44 % (2366019)Termination reason: Refutation not found, incomplete strategy % 5.71/1.44 % (2366019)Time elapsed: 0.0000 s % 5.71/1.44 % (2366019)Peak memory usage: 86 MB % 5.71/1.44 % (2366019)Instructions burned: 1 (million) % 5.71/1.44 % (2366022)Instruction limit reached! % 5.71/1.44 % (2366022)------------------------------ % 5.71/1.44 % (2366022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.44 % (2366022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.44 % (2366022)CaDiCaL version: 2.1.3 % 5.71/1.44 % (2366022)Termination reason: Instruction limit % 5.71/1.44 % (2366022)Termination phase: Saturation % 5.71/1.44 % (2366022)Time elapsed: 0.043 s % 5.71/1.44 % (2366022)Peak memory usage: 90 MB % 5.71/1.44 % (2366022)Instructions burned: 129 (million) % 5.71/1.44 % (2366021)Instruction limit reached! % 5.71/1.44 % (2366021)------------------------------ % 5.71/1.44 % (2366021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.44 % (2366021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.44 % (2366021)CaDiCaL version: 2.1.3 % 5.71/1.44 % (2366021)Termination reason: Instruction limit % 5.71/1.44 % (2366021)Termination phase: Saturation % 5.71/1.44 % (2366021)Time elapsed: 0.046 s % 5.71/1.44 % (2366021)Peak memory usage: 90 MB % 5.71/1.44 % (2366021)Instructions burned: 139 (million) % 5.71/1.44 % (2366030)lrs+10_1_sil=8000:sp=occurrence:random_seed=794275825:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 5.71/1.44 % (2366031)lrs+10_1_sil=32000:urr=on:br=off:random_seed=789912304:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi) % 5.71/1.44 % (2366030)Refutation not found, incomplete strategy % 5.71/1.44 % (2366030)------------------------------ % 5.71/1.44 % (2366030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.71/1.44 % (2366030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.71/1.44 % (2366030)CaDiCaL version: 2.1.3 % 5.71/1.44 % (2366030)Termination reason: Refutation not found, incomplete strategy % 6.65/1.58 % (2366030)Time elapsed: 0.001 s % 6.65/1.58 % (2366030)Peak memory usage: 86 MB % 6.65/1.58 % (2366030)Instructions burned: 1 (million) % 6.65/1.58 % (2366031)Refutation not found, incomplete strategy % 6.65/1.58 % (2366031)------------------------------ % 6.65/1.58 % (2366031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.65/1.58 % (2366031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.58 % (2366031)CaDiCaL version: 2.1.3 % 6.65/1.58 % (2366031)Termination reason: Refutation not found, incomplete strategy % 6.65/1.58 % (2366031)Time elapsed: 0.001 s % 6.65/1.58 % (2366031)Peak memory usage: 87 MB % 6.65/1.58 % (2366031)Instructions burned: 4 (million) % 6.65/1.58 % (2366020)------------------------------ % 6.65/1.58 % (2366020)------------------------------ % 6.65/1.58 % (2366019)------------------------------ % 6.65/1.58 % (2366019)------------------------------ % 6.65/1.58 % (2366035)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=2669551886:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.65/1.58 % (2366034)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1717870590:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.65/1.58 % (2366034)Refutation not found, incomplete strategy % 6.65/1.58 % (2366034)------------------------------ % 6.65/1.58 % (2366034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.65/1.58 % (2366034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.58 % (2366034)CaDiCaL version: 2.1.3 % 6.65/1.58 % (2366034)Termination reason: Refutation not found, incomplete strategy % 6.65/1.58 % (2366034)Time elapsed: 0.001 s % 6.65/1.58 % (2366034)Peak memory usage: 86 MB % 6.65/1.58 % (2366034)Instructions burned: 1 (million) % 6.65/1.58 % (2366031)------------------------------ % 6.65/1.58 % (2366031)------------------------------ % 6.65/1.58 % (2366030)------------------------------ % 6.65/1.58 % (2366030)------------------------------ % 6.65/1.58 % (2366018)Refutation not found, incomplete strategy % 6.65/1.58 % (2366018)------------------------------ % 6.65/1.58 % (2366018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.65/1.58 % (2366018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.58 % (2366018)CaDiCaL version: 2.1.3 % 6.65/1.58 % (2366018)Termination reason: Refutation not found, incomplete strategy % 6.65/1.58 % (2366018)Time elapsed: 0.345 s % 6.65/1.58 % (2366018)Peak memory usage: 132 MB % 6.65/1.58 % (2366018)Instructions burned: 918 (million) % 6.65/1.58 % (2366035)Instruction limit reached! % 6.65/1.58 % (2366035)------------------------------ % 6.65/1.58 % (2366035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.65/1.58 % (2366035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.58 % (2366035)CaDiCaL version: 2.1.3 % 6.65/1.58 % (2366035)Termination reason: Instruction limit % 6.65/1.58 % (2366035)Termination phase: Saturation % 6.65/1.58 % (2366035)Time elapsed: 0.083 s % 6.65/1.58 % (2366035)Peak memory usage: 91 MB % 6.65/1.58 % (2366035)Instructions burned: 251 (million) % 6.65/1.58 % (2366039)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3771515464:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 6.65/1.58 % (2366038)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3374847314:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 6.65/1.58 % (2366038)Refutation not found, incomplete strategy % 6.65/1.58 % (2366038)------------------------------ % 6.65/1.58 % (2366038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.65/1.58 % (2366038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.58 % (2366038)CaDiCaL version: 2.1.3 % 6.65/1.58 % (2366038)Termination reason: Refutation not found, incomplete strategy % 6.65/1.58 % (2366038)Time elapsed: 0.001 s % 6.65/1.58 % (2366038)Peak memory usage: 86 MB % 6.65/1.58 % (2366038)Instructions burned: 1 (million) % 6.65/1.58 % (2366034)------------------------------ % 6.65/1.58 % (2366034)------------------------------ % 6.65/1.58 % (2366040)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=634066382:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 6.65/1.58 % (2366040)Refutation not found, incomplete strategy % 6.65/1.58 % (2366040)------------------------------ % 6.65/1.58 % (2366040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366040)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366040)Termination reason: Refutation not found, incomplete strategy % 7.29/1.76 % (2366040)Time elapsed: 0.010 s % 7.29/1.76 % (2366040)Peak memory usage: 89 MB % 7.29/1.76 % (2366040)Instructions burned: 33 (million) % 7.29/1.76 % (2366018)------------------------------ % 7.29/1.76 % (2366018)------------------------------ % 7.29/1.76 % (2366043)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=42656400:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 7.29/1.76 % (2366043)Refutation not found, incomplete strategy % 7.29/1.76 % (2366043)------------------------------ % 7.29/1.76 % (2366043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366043)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366043)Termination reason: Refutation not found, incomplete strategy % 7.29/1.76 % (2366043)Time elapsed: 0.006 s % 7.29/1.76 % (2366043)Peak memory usage: 88 MB % 7.29/1.76 % (2366043)Instructions burned: 20 (million) % 7.29/1.76 % (2366038)------------------------------ % 7.29/1.76 % (2366038)------------------------------ % 7.29/1.76 % (2366040)------------------------------ % 7.29/1.76 % (2366040)------------------------------ % 7.29/1.76 % (2366045)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4146819868:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 7.29/1.76 % (2366045)Instruction limit reached! % 7.29/1.76 % (2366045)------------------------------ % 7.29/1.76 % (2366045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366045)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366045)Termination reason: Instruction limit % 7.29/1.76 % (2366045)Termination phase: Saturation % 7.29/1.76 % (2366045)Time elapsed: 0.036 s % 7.29/1.76 % (2366045)Peak memory usage: 89 MB % 7.29/1.76 % (2366045)Instructions burned: 116 (million) % 7.29/1.76 % (2366047)lrs+10_1_sil=8000:sp=occurrence:random_seed=980401549:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 7.29/1.76 % (2366047)Refutation not found, incomplete strategy % 7.29/1.76 % (2366047)------------------------------ % 7.29/1.76 % (2366047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366047)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366047)Termination reason: Refutation not found, incomplete strategy % 7.29/1.76 % (2366047)Time elapsed: 0.001 s % 7.29/1.76 % (2366047)Peak memory usage: 86 MB % 7.29/1.76 % (2366047)Instructions burned: 1 (million) % 7.29/1.76 % (2366043)------------------------------ % 7.29/1.76 % (2366043)------------------------------ % 7.29/1.76 % (2366049)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=104791168:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 7.29/1.76 % (2366049)Refutation not found, incomplete strategy % 7.29/1.76 % (2366049)------------------------------ % 7.29/1.76 % (2366049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366049)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366049)Termination reason: Refutation not found, incomplete strategy % 7.29/1.76 % (2366049)Time elapsed: 0.009 s % 7.29/1.76 % (2366049)Peak memory usage: 89 MB % 7.29/1.76 % (2366049)Instructions burned: 31 (million) % 7.29/1.76 % (2366050)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=175640666:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 7.29/1.76 % (2366052)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=377057192:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 7.29/1.76 % (2366052)Instruction limit reached! % 7.29/1.76 % (2366052)------------------------------ % 7.29/1.76 % (2366052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.29/1.76 % (2366052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.29/1.76 % (2366052)CaDiCaL version: 2.1.3 % 7.29/1.76 % (2366052)Termination reason: Instruction limit % 8.09/1.86 % (2366052)Termination phase: Saturation % 8.09/1.86 % (2366052)Time elapsed: 0.042 s % 8.09/1.86 % (2366052)Peak memory usage: 91 MB % 8.09/1.86 % (2366052)Instructions burned: 134 (million) % 8.09/1.86 % (2366047)------------------------------ % 8.09/1.86 % (2366047)------------------------------ % 8.09/1.86 % (2366049)------------------------------ % 8.09/1.86 % (2366049)------------------------------ % 8.09/1.86 % (2366056)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1690402245:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 8.09/1.86 % (2366056)Refutation not found, incomplete strategy % 8.09/1.86 % (2366056)------------------------------ % 8.09/1.86 % (2366056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.09/1.86 % (2366056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.09/1.86 % (2366056)CaDiCaL version: 2.1.3 % 8.09/1.86 % (2366056)Termination reason: Refutation not found, incomplete strategy % 8.09/1.86 % (2366056)Time elapsed: 0.001 s % 8.09/1.86 % (2366056)Peak memory usage: 86 MB % 8.09/1.86 % (2366056)Instructions burned: 1 (million) % 8.09/1.86 % (2366057)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3821509327:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 8.09/1.86 [W927 12:54:51.819124330 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819152870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819177190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819183110 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819195983 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819201508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819215041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819221570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819235267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.09/1.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.09/1.86 [W927 12:54:51.819241939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.819255027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.819260650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 % (2366058)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=787538744:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 11.03/2.19 % (2366058)Refutation not found, incomplete strategy % 11.03/2.19 % (2366058)------------------------------ % 11.03/2.19 % (2366058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.19 % (2366058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.19 % (2366058)CaDiCaL version: 2.1.3 % 11.03/2.19 % (2366058)Termination reason: Refutation not found, incomplete strategy % 11.03/2.19 % (2366058)Time elapsed: 0.002 s % 11.03/2.19 % (2366058)Peak memory usage: 87 MB % 11.03/2.19 % (2366058)Instructions burned: 5 (million) % 11.03/2.19 % (2366050)Refutation not found, incomplete strategy % 11.03/2.19 % (2366050)------------------------------ % 11.03/2.19 % (2366050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.03/2.19 % (2366050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.03/2.19 % (2366050)CaDiCaL version: 2.1.3 % 11.03/2.19 % (2366050)Termination reason: Refutation not found, incomplete strategy % 11.03/2.19 % (2366050)Time elapsed: 0.308 s % 11.03/2.19 % (2366050)Peak memory usage: 126 MB % 11.03/2.19 % (2366050)Instructions burned: 827 (million) % 11.03/2.19 % (2366056)------------------------------ % 11.03/2.19 % (2366056)------------------------------ % 11.03/2.19 % (2366058)------------------------------ % 11.03/2.19 % (2366058)------------------------------ % 11.03/2.19 [W927 12:54:51.000694833 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.000714864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.000736473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.000743682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.000759193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.03/2.19 [W927 12:54:51.000766099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.03/2.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000780873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000786745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000799136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000804888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000817553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 [W927 12:54:51.000823125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.62/3.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.62/3.04 % (2366062)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3217469388:i=134:gtgl=5:slsql=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/134Mi) % 17.62/3.04 % (2366050)------------------------------ % 17.62/3.04 % (2366050)------------------------------ % 17.62/3.04 % (2366063)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2592337689:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/141Mi) % 17.62/3.04 % (2366063)Refutation not found, incomplete strategy % 17.62/3.04 % (2366063)------------------------------ % 17.62/3.04 % (2366063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.62/3.04 % (2366063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.62/3.04 % (2366063)CaDiCaL version: 2.1.3 % 17.62/3.04 % (2366063)Termination reason: Refutation not found, incomplete strategy % 17.62/3.04 % (2366063)Time elapsed: 0.001 s % 17.62/3.04 % (2366063)Peak memory usage: 87 MB % 17.62/3.04 % (2366063)Instructions burned: 1 (million) % 17.62/3.04 % (2366062)Instruction limit reached! % 17.62/3.04 % (2366062)------------------------------ % 17.62/3.04 % (2366062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.62/3.04 % (2366062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.62/3.04 % (2366062)CaDiCaL version: 2.1.3 % 17.62/3.04 % (2366062)Termination reason: Instruction limit % 17.62/3.04 % (2366062)Termination phase: Saturation % 17.62/3.04 % (2366062)Time elapsed: 0.044 s % 17.62/3.04 % (2366062)Peak memory usage: 90 MB % 17.62/3.04 % (2366062)Instructions burned: 134 (million) % 17.62/3.04 % (2366057)Refutation not found, incomplete strategy % 17.62/3.04 % (2366057)------------------------------ % 17.62/3.04 % (2366057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.62/3.04 % (2366057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.62/3.04 % (2366057)CaDiCaL version: 2.1.3 % 17.62/3.04 % (2366057)Termination reason: Refutation not found, incomplete strategy % 17.62/3.04 % (2366057)Time elapsed: 0.313 s % 17.62/3.04 % (2366057)Peak memory usage: 125 MB % 17.62/3.04 % (2366057)Instructions burned: 830 (million) % 17.62/3.04 % (2366039)Instruction limit reached! % 17.62/3.04 % (2366039)------------------------------ % 17.62/3.04 % (2366039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.34 % (2366039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.34 % (2366039)CaDiCaL version: 2.1.3 % 19.61/3.34 % (2366039)Termination reason: Instruction limit % 19.61/3.34 % (2366039)Termination phase: Saturation % 19.61/3.34 % (2366039)Time elapsed: 0.843 s % 19.61/3.34 % (2366039)Peak memory usage: 144 MB % 19.61/3.34 % (2366039)Instructions burned: 2351 (million) % 19.61/3.34 % (2366066)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3285964849:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/431Mi) % 19.61/3.34 % (2366066)Refutation not found, incomplete strategy % 19.61/3.34 % (2366066)------------------------------ % 19.61/3.34 % (2366066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.34 % (2366066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.34 % (2366066)CaDiCaL version: 2.1.3 % 19.61/3.34 % (2366066)Termination reason: Refutation not found, incomplete strategy % 19.61/3.34 % (2366066)Time elapsed: 0.001 s % 19.61/3.34 % (2366066)Peak memory usage: 86 MB % 19.61/3.34 % (2366066)Instructions burned: 1 (million) % 19.61/3.34 % (2366067)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=3154015155:i=6060:aac=none:ins=25_2986 on theBenchmark for (2986ds/6060Mi) % 19.61/3.34 % (2366068)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=1636644125:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2986 on theBenchmark for (2986ds/150Mi) % 19.61/3.34 % (2366063)------------------------------ % 19.61/3.34 % (2366063)------------------------------ % 19.61/3.34 % (2366057)------------------------------ % 19.61/3.34 % (2366057)------------------------------ % 19.61/3.34 % (2366068)Instruction limit reached! % 19.61/3.34 % (2366068)------------------------------ % 19.61/3.34 % (2366068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.34 % (2366068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.34 % (2366068)CaDiCaL version: 2.1.3 % 19.61/3.34 % (2366068)Termination reason: Instruction limit % 19.61/3.34 % (2366068)Termination phase: Saturation % 19.61/3.34 % (2366068)Time elapsed: 0.054 s % 19.61/3.34 % (2366068)Peak memory usage: 91 MB % 19.61/3.34 % (2366068)Instructions burned: 152 (million) % 19.61/3.34 % (2366066)------------------------------ % 19.61/3.34 % (2366066)------------------------------ % 19.61/3.34 % (2366072)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3405043123:i=14155:bd=all_2985 on theBenchmark for (2985ds/14155Mi) % 19.61/3.34 % (2366073)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3617255523:i=667:av=off:fsr=off_2984 on theBenchmark for (2984ds/667Mi) % 19.61/3.34 % (2366073)Refutation not found, incomplete strategy % 19.61/3.34 % (2366073)------------------------------ % 19.61/3.34 % (2366073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.34 % (2366073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.34 % (2366073)CaDiCaL version: 2.1.3 % 19.61/3.34 % (2366073)Termination reason: Refutation not found, incomplete strategy % 19.61/3.34 % (2366073)Time elapsed: 0.008 s % 19.61/3.34 % (2366073)Peak memory usage: 89 MB % 19.61/3.34 % (2366073)Instructions burned: 27 (million) % 19.61/3.34 % (2366074)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=1878070610:s2a=on:i=185:s2at=1.8:fdi=4_2984 on theBenchmark for (2984ds/185Mi) % 19.61/3.34 % (2366075)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2438237152:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2984 on theBenchmark for (2984ds/193Mi) % 19.61/3.34 % (2366075)Refutation not found, incomplete strategy % 19.61/3.34 % (2366075)------------------------------ % 19.61/3.34 % (2366075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.61/3.34 % (2366075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.34 % (2366075)CaDiCaL version: 2.1.3 % 19.61/3.34 % (2366075)Termination reason: Refutation not found, incomplete strategy % 19.61/3.34 % (2366075)Time elapsed: 0.001 s % 19.61/3.34 % (2366075)Peak memory usage: 86 MB % 19.61/3.34 % (2366075)Instructions burned: 2 (million) % 19.61/3.34 % (2366074)Instruction limit reached! % 26.27/4.36 % (2366074)------------------------------ % 26.27/4.36 % (2366074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.36 % (2366074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/4.36 % (2366074)CaDiCaL version: 2.1.3 % 26.27/4.36 % (2366074)Termination reason: Instruction limit % 26.27/4.36 % (2366074)Termination phase: Saturation % 26.27/4.36 % (2366074)Time elapsed: 0.063 s % 26.27/4.36 % (2366074)Peak memory usage: 92 MB % 26.27/4.36 % (2366074)Instructions burned: 186 (million) % 26.27/4.36 % (2366073)------------------------------ % 26.27/4.36 % (2366073)------------------------------ % 26.27/4.36 % (2366080)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1379388753:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2983 on theBenchmark for (2983ds/4850Mi) % 26.27/4.36 % (2366080)Refutation not found, incomplete strategy % 26.27/4.36 % (2366080)------------------------------ % 26.27/4.36 % (2366080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.36 % (2366080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/4.36 % (2366080)CaDiCaL version: 2.1.3 % 26.27/4.36 % (2366080)Termination reason: Refutation not found, incomplete strategy % 26.27/4.36 % (2366080)Time elapsed: 0.006 s % 26.27/4.36 % (2366080)Peak memory usage: 88 MB % 26.27/4.36 % (2366080)Instructions burned: 23 (million) % 26.27/4.36 % (2366075)------------------------------ % 26.27/4.36 % (2366075)------------------------------ % 26.27/4.36 % (2366081)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=782522924:i=12111:sd=1:ss=included_2982 on theBenchmark for (2982ds/12111Mi) % 26.27/4.36 % (2366083)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=300919682:i=319:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/319Mi) % 26.27/4.36 % (2366080)------------------------------ % 26.27/4.36 % (2366080)------------------------------ % 26.27/4.36 % (2366083)Instruction limit reached! % 26.27/4.36 % (2366083)------------------------------ % 26.27/4.36 % (2366083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.36 % (2366083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/4.36 % (2366083)CaDiCaL version: 2.1.3 % 26.27/4.36 % (2366083)Termination reason: Instruction limit % 26.27/4.36 % (2366083)Termination phase: Saturation % 26.27/4.36 % (2366083)Time elapsed: 0.100 s % 26.27/4.36 % (2366083)Peak memory usage: 93 MB % 26.27/4.36 % (2366083)Instructions burned: 320 (million) % 26.27/4.36 % (2366086)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2376822070:i=2064:ep=RST_2980 on theBenchmark for (2980ds/2064Mi) % 26.27/4.36 % (2366086)Refutation not found, incomplete strategy % 26.27/4.36 % (2366086)------------------------------ % 26.27/4.36 % (2366086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.36 % (2366086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/4.36 % (2366086)CaDiCaL version: 2.1.3 % 26.27/4.36 % (2366086)Termination reason: Refutation not found, incomplete strategy % 26.27/4.36 % (2366086)Time elapsed: 0.008 s % 26.27/4.36 % (2366086)Peak memory usage: 89 MB % 26.27/4.36 % (2366086)Instructions burned: 30 (million) % 26.27/4.36 % (2366087)dis-1011_128_sil=32000:random_seed=2041584241:i=3706:ep=RST:av=off_2979 on theBenchmark for (2979ds/3706Mi) % 26.27/4.36 % (2366086)------------------------------ % 26.27/4.36 % (2366086)------------------------------ % 26.27/4.36 % (2366090)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2279841973:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2978 on theBenchmark for (2978ds/757Mi) % 26.27/4.36 % (2366090)Refutation not found, incomplete strategy % 26.27/4.36 % (2366090)------------------------------ % 26.27/4.36 % (2366090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.36 % (2366090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/4.36 % (2366090)CaDiCaL version: 2.1.3 % 26.27/4.36 % (2366090)Termination reason: Refutation not found, incomplete strategy % 26.27/4.36 % (2366090)Time elapsed: 0.001 s % 26.27/4.36 % (2366090)Peak memory usage: 86 MB % 26.27/4.36 % (2366090)Instructions burned: 1 (million) % 26.27/4.36 % (2366090)------------------------------ % 26.27/4.36 % (2366090)------------------------------ % 26.27/4.36 % (2366092)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2142732597:i=13913:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/13913Mi) % 26.27/4.38 [W927 12:54:52.489530949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489550258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489587791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489593976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489608339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489615102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489629856 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489636374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489650646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489657088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489671058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 [W927 12:54:52.489677295 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.27/4.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.27/4.38 % (2366092)Refutation not found, incomplete strategy % 26.27/4.38 % (2366092)------------------------------ % 26.27/4.38 % (2366092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/4.38 % (2366092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366092)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366092)Termination reason: Refutation not found, incomplete strategy % 41.87/6.50 % (2366092)Time elapsed: 0.300 s % 41.87/6.50 % (2366092)Peak memory usage: 126 MB % 41.87/6.50 % (2366092)Instructions burned: 825 (million) % 41.87/6.50 % (2366092)------------------------------ % 41.87/6.50 % (2366092)------------------------------ % 41.87/6.50 % (2366094)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=132588007:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 41.87/6.50 % (2366087)Instruction limit reached! % 41.87/6.50 % (2366087)------------------------------ % 41.87/6.50 % (2366087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.87/6.50 % (2366087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366087)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366087)Termination reason: Instruction limit % 41.87/6.50 % (2366087)Termination phase: Saturation % 41.87/6.50 % (2366087)Time elapsed: 1.237 s % 41.87/6.50 % (2366087)Peak memory usage: 129 MB % 41.87/6.50 % (2366087)Instructions burned: 3708 (million) % 41.87/6.50 % (2366094)Refutation not found, incomplete strategy % 41.87/6.50 % (2366094)------------------------------ % 41.87/6.50 % (2366094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.87/6.50 % (2366094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366094)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366094)Termination reason: Refutation not found, incomplete strategy % 41.87/6.50 % (2366094)Time elapsed: 0.334 s % 41.87/6.50 % (2366094)Peak memory usage: 132 MB % 41.87/6.50 % (2366094)Instructions burned: 914 (million) % 41.87/6.50 % (2366096)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2312111758:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/2479Mi) % 41.87/6.50 % (2366096)Refutation not found, incomplete strategy % 41.87/6.50 % (2366096)------------------------------ % 41.87/6.50 % (2366096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.87/6.50 % (2366096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366096)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366096)Termination reason: Refutation not found, incomplete strategy % 41.87/6.50 % (2366096)Time elapsed: 0.001 s % 41.87/6.50 % (2366096)Peak memory usage: 86 MB % 41.87/6.50 % (2366096)Instructions burned: 2 (million) % 41.87/6.50 % (2366067)Instruction limit reached! % 41.87/6.50 % (2366067)------------------------------ % 41.87/6.50 % (2366067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.87/6.50 % (2366067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366067)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366067)Termination reason: Instruction limit % 41.87/6.50 % (2366067)Termination phase: Saturation % 41.87/6.50 % (2366067)Time elapsed: 2.064 s % 41.87/6.50 % (2366067)Peak memory usage: 186 MB % 41.87/6.50 % (2366067)Instructions burned: 6060 (million) % 41.87/6.50 % (2366094)------------------------------ % 41.87/6.50 % (2366094)------------------------------ % 41.87/6.50 % (2366096)------------------------------ % 41.87/6.50 % (2366096)------------------------------ % 41.87/6.50 % (2366098)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=724089005:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2964 on theBenchmark for (2964ds/440Mi) % 41.87/6.50 % (2366099)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2912564773:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2964 on theBenchmark for (2964ds/11145Mi) % 41.87/6.50 % (2366100)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=2956023284:cts=off:i=3034:av=off:er=known:fsd=on_2964 on theBenchmark for (2964ds/3034Mi) % 41.87/6.50 % (2366098)Instruction limit reached! % 41.87/6.50 % (2366098)------------------------------ % 41.87/6.50 % (2366098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.87/6.50 % (2366098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.87/6.50 % (2366098)CaDiCaL version: 2.1.3 % 41.87/6.50 % (2366098)Termination reason: Instruction limit % 41.87/6.50 % (2366098)Termination phase: Saturation % 41.87/6.50 % (2366098)Time elapsed: 0.137 s % 41.87/6.50 % (2366098)Peak memory usage: 93 MB % 41.87/6.50 % (2366098)Instructions burned: 443 (million) % 41.87/6.50 % (2366104)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=300804400:st=2:s2a=on:i=524:s2at=2:ss=axioms_2962 on theBenchmark for (2962ds/524Mi) % 43.23/6.81 % (2366104)Refutation not found, incomplete strategy % 43.23/6.81 % (2366104)------------------------------ % 43.23/6.81 % (2366104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.23/6.81 % (2366104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.23/6.81 % (2366104)CaDiCaL version: 2.1.3 % 43.23/6.81 % (2366104)Termination reason: Refutation not found, incomplete strategy % 43.23/6.81 % (2366104)Time elapsed: 0.001 s % 43.23/6.81 % (2366104)Peak memory usage: 87 MB % 43.23/6.81 % (2366104)Instructions burned: 3 (million) % 43.23/6.81 [W927 12:54:54.619981327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620021592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620044685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620051039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620066363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620072952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620087848 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620094144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620107824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620114304 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620128724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.23/6.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.23/6.81 [W927 12:54:54.620135101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.64/6.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.64/6.91 % (2366099)Refutation not found, incomplete strategy % 43.64/6.91 % (2366099)------------------------------ % 43.64/6.91 % (2366099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.64/6.91 % (2366099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.64/6.91 % (2366099)CaDiCaL version: 2.1.3 % 43.64/6.91 % (2366099)Termination reason: Refutation not found, incomplete strategy % 43.64/6.91 % (2366099)Time elapsed: 0.304 s % 43.64/6.91 % (2366099)Peak memory usage: 125 MB % 43.64/6.91 % (2366099)Instructions burned: 831 (million) % 43.64/6.91 % (2366104)------------------------------ % 43.64/6.91 % (2366104)------------------------------ % 43.64/6.91 % (2366106)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3031057001:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2960 on theBenchmark for (2960ds/1016Mi) % 43.64/6.91 % (2366106)Refutation not found, incomplete strategy % 43.64/6.91 % (2366106)------------------------------ % 43.64/6.91 % (2366106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.64/6.91 % (2366106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.64/6.91 % (2366106)CaDiCaL version: 2.1.3 % 43.64/6.91 % (2366106)Termination reason: Refutation not found, incomplete strategy % 43.64/6.91 % (2366106)Time elapsed: 0.001 s % 43.64/6.91 % (2366106)Peak memory usage: 87 MB % 43.64/6.91 % (2366106)Instructions burned: 1 (million) % 43.64/6.91 % (2366099)------------------------------ % 43.64/6.91 % (2366099)------------------------------ % 43.64/6.91 % (2366108)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4243022857:i=14123:bd=preordered:ins=4_2958 on theBenchmark for (2958ds/14123Mi) % 43.64/6.91 % (2366106)------------------------------ % 43.64/6.91 % (2366106)------------------------------ % 43.64/6.91 % (2366110)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1217142794:i=5781:kws=precedence:bd=all:rawr=on_2957 on theBenchmark for (2957ds/5781Mi) % 43.64/6.91 % (2366100)Instruction limit reached! % 43.64/6.91 % (2366100)------------------------------ % 43.64/6.91 % (2366100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.64/6.91 % (2366100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.64/6.91 % (2366100)CaDiCaL version: 2.1.3 % 43.64/6.91 % (2366100)Termination reason: Instruction limit % 43.64/6.91 % (2366100)Termination phase: Saturation % 43.64/6.91 % (2366100)Time elapsed: 1.019 s % 43.64/6.91 % (2366100)Peak memory usage: 142 MB % 43.64/6.91 % (2366100)Instructions burned: 3035 (million) % 43.64/6.91 % (2366112)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=226502326:i=2448:gtgl=5:bd=preordered:gtg=all_2952 on theBenchmark for (2952ds/2448Mi) % 43.64/6.91 % (2366112)Instruction limit reached! % 43.64/6.91 % (2366112)------------------------------ % 43.64/6.91 % (2366112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.64/6.91 % (2366112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.64/6.91 % (2366112)CaDiCaL version: 2.1.3 % 43.64/6.91 % (2366112)Termination reason: Instruction limit % 43.64/6.91 % (2366112)Termination phase: Saturation % 43.64/6.91 % (2366112)Time elapsed: 0.850 s % 43.64/6.91 % (2366112)Peak memory usage: 144 MB % 43.64/6.91 % (2366112)Instructions burned: 2448 (million) % 43.64/6.91 % (2366114)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1211950245:i=3223:kws=precedence:fgj=on:av=off_2943 on theBenchmark for (2943ds/3223Mi) % 43.64/6.91 % (2366081)Instruction limit reached! % 43.64/6.91 % (2366081)------------------------------ % 43.64/6.91 % (2366081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.64/6.91 % (2366081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.64/6.91 % (2366081)CaDiCaL version: 2.1.3 % 43.64/6.91 % (2366081)Termination reason: Instruction limit % 43.64/6.91 % (2366081)Termination phase: Saturation % 43.64/6.91 % (2366081)Time elapsed: 4.131 s % 43.64/6.91 % (2366081)Peak memory usage: 241 MB % 43.64/6.91 % (2366081)Instructions burned: 12112 (million) % 46.61/7.29 % (2366116)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3014668210:st=5.6:i=2033:sd=3:ss=axioms_2939 on theBenchmark for (2939ds/2033Mi) % 46.61/7.29 % (2366110)Instruction limit reached! % 46.61/7.29 % (2366110)------------------------------ % 46.61/7.29 % (2366110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.61/7.29 % (2366110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.61/7.29 % (2366110)CaDiCaL version: 2.1.3 % 46.61/7.29 % (2366110)Termination reason: Instruction limit % 46.61/7.29 % (2366110)Termination phase: Saturation % 46.61/7.29 % (2366110)Time elapsed: 1.745 s % 46.61/7.29 % (2366110)Peak memory usage: 128 MB % 46.61/7.29 % (2366110)Instructions burned: 5783 (million) % 46.61/7.29 % (2366118)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2318577259:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2938 on theBenchmark for (2938ds/2055Mi) % 46.61/7.29 [W927 12:54:56.055548751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055584093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055605311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055611619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055626214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055632673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055646660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055652969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055666577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055672832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.61/7.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.61/7.29 [W927 12:54:56.055686419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.055692587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 % (2366116)Refutation not found, incomplete strategy % 49.27/7.70 % (2366116)------------------------------ % 49.27/7.70 % (2366116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.27/7.70 [W927 12:54:56.151037858 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 % (2366116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.27/7.70 [W927 12:54:56.151053062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 % (2366116)CaDiCaL version: 2.1.3 % 49.27/7.70 % (2366116)Termination reason: Refutation not found, incomplete strategy % 49.27/7.70 % (2366116)Time elapsed: 0.304 s % 49.27/7.70 % (2366116)Peak memory usage: 126 MB % 49.27/7.70 [W927 12:54:56.151073932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 % (2366116)Instructions burned: 826 (million) % 49.27/7.70 [W927 12:54:56.151079696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151093205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151106575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151120978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151126214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151140924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 49.27/7.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 49.27/7.70 [W927 12:54:56.151146161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.151159094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.151164482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 % (2366072)Instruction limit reached! % 56.63/9.04 % (2366072)------------------------------ % 56.63/9.04 % (2366072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.63/9.04 % (2366072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.63/9.04 % (2366072)CaDiCaL version: 2.1.3 % 56.63/9.04 % (2366072)Termination reason: Instruction limit % 56.63/9.04 % (2366072)Termination phase: Saturation % 56.63/9.04 % (2366072)Time elapsed: 4.858 s % 56.63/9.04 % (2366072)Peak memory usage: 251 MB % 56.63/9.04 % (2366072)Instructions burned: 14155 (million) % 56.63/9.04 % (2366118)Refutation not found, incomplete strategy % 56.63/9.04 % (2366118)------------------------------ % 56.63/9.04 % (2366118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.63/9.04 % (2366118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.63/9.04 % (2366118)CaDiCaL version: 2.1.3 % 56.63/9.04 % (2366118)Termination reason: Refutation not found, incomplete strategy % 56.63/9.04 % (2366118)Time elapsed: 0.307 s % 56.63/9.04 % (2366118)Peak memory usage: 126 MB % 56.63/9.04 % (2366118)Instructions burned: 832 (million) % 56.63/9.04 % (2366120)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=836529908:i=21611:sd=3:ss=axioms_2935 on theBenchmark for (2935ds/21611Mi) % 56.63/9.04 [W927 12:54:56.531220724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531240807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531279262 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531286991 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531300930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531306892 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 56.63/9.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.63/9.04 [W927 12:54:56.531319824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 [W927 12:54:56.531325811 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 [W927 12:54:56.531343455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 [W927 12:54:56.531365496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 [W927 12:54:56.531379113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 [W927 12:54:56.531385376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.66/9.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.66/9.79 % (2366114)Instruction limit reached! % 60.66/9.79 % (2366114)------------------------------ % 60.66/9.79 % (2366114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.66/9.79 % (2366114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.66/9.79 % (2366114)CaDiCaL version: 2.1.3 % 60.66/9.79 % (2366114)Termination reason: Instruction limit % 60.66/9.79 % (2366114)Termination phase: Saturation % 60.66/9.79 % (2366114)Time elapsed: 1.060 s % 60.66/9.79 % (2366114)Peak memory usage: 159 MB % 60.66/9.79 % (2366114)Instructions burned: 3227 (million) % 60.66/9.79 % (2366120)Refutation not found, incomplete strategy % 60.66/9.79 % (2366120)------------------------------ % 60.66/9.79 % (2366120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.66/9.79 % (2366120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.66/9.79 % (2366120)CaDiCaL version: 2.1.3 % 60.66/9.79 % (2366120)Termination reason: Refutation not found, incomplete strategy % 60.66/9.79 % (2366120)Time elapsed: 0.311 s % 60.66/9.79 % (2366120)Peak memory usage: 126 MB % 60.66/9.79 % (2366120)Instructions burned: 829 (million) % 60.66/9.79 % (2366122)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=93436228:i=4835:sd=13:ss=axioms:sgt=23_2931 on theBenchmark for (2931ds/4835Mi) % 60.66/9.79 % (2366122)Refutation not found, incomplete strategy % 60.66/9.79 % (2366122)------------------------------ % 60.66/9.79 % (2366122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.66/9.79 % (2366122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.66/9.79 % (2366122)CaDiCaL version: 2.1.3 % 60.66/9.79 % (2366122)Termination reason: Refutation not found, incomplete strategy % 60.66/9.79 % (2366122)Time elapsed: 0.001 s % 60.66/9.79 % (2366122)Peak memory usage: 86 MB % 60.66/9.79 % (2366122)Instructions burned: 1 (million) % 60.66/9.79 % (2366118)------------------------------ % 60.66/9.79 % (2366118)------------------------------ % 60.66/9.79 % (2366120)------------------------------ % 60.66/9.79 % (2366120)------------------------------ % 60.66/9.79 % (2366116)------------------------------ % 60.66/9.79 % (2366116)------------------------------ % 60.66/9.79 % (2366122)------------------------------ % 60.66/9.79 % (2366122)------------------------------ % 60.66/9.79 % (2366126)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3444171503:i=6038:nm=6_2928 on theBenchmark for (2928ds/6038Mi) % 60.66/9.79 % (2366124)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=3809979666:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2928 on theBenchmark for (2928ds/797Mi) % 65.80/10.45 % (2366125)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=973633230:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2928 on theBenchmark for (2928ds/2326Mi) % 65.80/10.45 % (2366125)Refutation not found, incomplete strategy % 65.80/10.45 % (2366125)------------------------------ % 65.80/10.45 % (2366125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.80/10.45 % (2366125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.80/10.45 % (2366125)CaDiCaL version: 2.1.3 % 65.80/10.45 % (2366125)Termination reason: Refutation not found, incomplete strategy % 65.80/10.45 % (2366125)Time elapsed: 0.015 s % 65.80/10.45 % (2366125)Peak memory usage: 89 MB % 65.80/10.45 % (2366125)Instructions burned: 47 (million) % 65.80/10.45 % (2366127)lrs+10_1_sil=32000:sp=occurrence:random_seed=2732786656:st=2:i=33334:sd=3:ss=included:sgt=32_2928 on theBenchmark for (2928ds/33334Mi) % 65.80/10.45 % (2366125)------------------------------ % 65.80/10.45 % (2366125)------------------------------ % 65.80/10.45 % (2366124)Instruction limit reached! % 65.80/10.45 % (2366124)------------------------------ % 65.80/10.45 % (2366124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.80/10.45 % (2366124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.80/10.45 % (2366124)CaDiCaL version: 2.1.3 % 65.80/10.45 % (2366124)Termination reason: Instruction limit % 65.80/10.45 % (2366124)Termination phase: Saturation % 65.80/10.45 % (2366124)Time elapsed: 0.193 s % 65.80/10.45 % (2366124)Peak memory usage: 90 MB % 65.80/10.45 % (2366124)Instructions burned: 798 (million) % 65.80/10.45 % (2366133)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=745762115:i=8327:s2at=5:bd=preordered_2926 on theBenchmark for (2926ds/8327Mi) % 65.80/10.45 % (2366132)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=85958009:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2926 on theBenchmark for (2926ds/1008Mi) % 65.80/10.45 % (2366132)Refutation not found, incomplete strategy % 65.80/10.45 % (2366132)------------------------------ % 65.80/10.45 % (2366132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.80/10.45 % (2366132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.80/10.45 % (2366132)CaDiCaL version: 2.1.3 % 65.80/10.45 % (2366132)Termination reason: Refutation not found, incomplete strategy % 65.80/10.45 % (2366132)Time elapsed: 0.001 s % 65.80/10.45 % (2366132)Peak memory usage: 86 MB % 65.80/10.45 % (2366132)Instructions burned: 3 (million) % 65.80/10.45 % (2366126)Refutation not found, incomplete strategy % 65.80/10.45 % (2366126)------------------------------ % 65.80/10.45 % (2366126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.80/10.45 % (2366126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.80/10.45 % (2366126)CaDiCaL version: 2.1.3 % 65.80/10.45 % (2366126)Termination reason: Refutation not found, incomplete strategy % 65.80/10.45 % (2366126)Time elapsed: 1.082 s % 65.80/10.45 % (2366126)Peak memory usage: 133 MB % 65.80/10.45 % (2366126)Instructions burned: 917 (million) % 65.80/10.45 % (2366132)------------------------------ % 65.80/10.45 % (2366132)------------------------------ % 65.80/10.45 % (2366136)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=2801988157:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2916 on theBenchmark for (2916ds/1083Mi) % 65.80/10.45 % (2366126)------------------------------ % 65.80/10.45 % (2366126)------------------------------ % 65.80/10.45 % (2366138)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1529806416:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2915 on theBenchmark for (2915ds/1084Mi) % 65.80/10.45 % (2366138)Refutation not found, incomplete strategy % 65.80/10.45 % (2366138)------------------------------ % 65.80/10.45 % (2366138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.80/10.45 % (2366138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.80/10.45 % (2366138)CaDiCaL version: 2.1.3 % 65.80/10.45 % (2366138)Termination reason: Refutation not found, incomplete strategy % 65.80/10.45 % (2366138)Time elapsed: 0.001 s % 65.80/10.45 % (2366138)Peak memory usage: 86 MB % 66.80/10.69 % (2366138)Instructions burned: 1 (million) % 66.80/10.69 % (2366138)------------------------------ % 66.80/10.69 % (2366138)------------------------------ % 66.80/10.69 % (2366136)Instruction limit reached! % 66.80/10.69 % (2366136)------------------------------ % 66.80/10.69 % (2366136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.80/10.69 % (2366136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.80/10.69 % (2366136)CaDiCaL version: 2.1.3 % 66.80/10.69 % (2366136)Termination reason: Instruction limit % 66.80/10.69 % (2366136)Termination phase: Saturation % 66.80/10.69 % (2366136)Time elapsed: 0.292 s % 66.80/10.69 % (2366136)Peak memory usage: 101 MB % 66.80/10.69 % (2366136)Instructions burned: 1083 (million) % 66.80/10.69 % (2366140)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=970876704:i=6995:s2at=5:gtg=all_2913 on theBenchmark for (2913ds/6995Mi) % 66.80/10.69 % (2366141)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2346279873:st=2:i=6225:sd=15:ss=axioms_2912 on theBenchmark for (2912ds/6225Mi) % 66.80/10.69 % (2366141)Refutation not found, incomplete strategy % 66.80/10.69 % (2366141)------------------------------ % 66.80/10.69 % (2366141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.80/10.69 % (2366141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.80/10.69 % (2366141)CaDiCaL version: 2.1.3 % 66.80/10.69 % (2366141)Termination reason: Refutation not found, incomplete strategy % 66.80/10.69 % (2366141)Time elapsed: 0.001 s % 66.80/10.69 % (2366141)Peak memory usage: 87 MB % 66.80/10.69 % (2366141)Instructions burned: 1 (million) % 66.80/10.69 % (2366141)------------------------------ % 66.80/10.69 % (2366141)------------------------------ % 66.80/10.69 % (2366108)Instruction limit reached! % 66.80/10.69 % (2366108)------------------------------ % 66.80/10.69 % (2366108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.80/10.69 % (2366108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.80/10.69 % (2366108)CaDiCaL version: 2.1.3 % 66.80/10.69 % (2366108)Termination reason: Instruction limit % 66.80/10.69 % (2366108)Termination phase: Saturation % 66.80/10.69 % (2366108)Time elapsed: 4.828 s % 66.80/10.69 % (2366108)Peak memory usage: 260 MB % 66.80/10.69 % (2366108)Instructions burned: 14125 (million) % 66.80/10.69 % (2366144)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3689159504:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2910 on theBenchmark for (2910ds/3372Mi) % 66.80/10.69 % (2366145)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2830420065:st=2.3:i=26457:sd=10:ss=included:sgt=8_2909 on theBenchmark for (2909ds/26457Mi) % 66.80/10.69 [W927 12:54:59.028578987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.80/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.80/10.69 [W927 12:54:59.028600457 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.80/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.80/10.69 [W927 12:54:59.028646882 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.80/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.80/10.69 [W927 12:54:59.028653079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.80/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.80/10.69 [W927 12:54:59.028666910 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.80/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.80/10.69 [W927 12:54:59.028672536 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028687069 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028692736 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028705278 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028718018 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028731898 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 [W927 12:54:59.028737356 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/11.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.73/11.11 % (2366144)Refutation not found, incomplete strategy % 70.73/11.11 % (2366144)------------------------------ % 70.73/11.11 % (2366144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.73/11.11 % (2366144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.73/11.11 % (2366144)CaDiCaL version: 2.1.3 % 70.73/11.11 % (2366144)Termination reason: Refutation not found, incomplete strategy % 70.73/11.11 % (2366144)Time elapsed: 0.307 s % 70.73/11.11 % (2366144)Peak memory usage: 126 MB % 70.73/11.11 % (2366144)Instructions burned: 833 (million) % 70.73/11.11 % (2366145)Refutation not found, incomplete strategy % 70.73/11.11 % (2366145)------------------------------ % 70.73/11.11 % (2366145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.73/11.11 % (2366145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.73/11.11 % (2366145)CaDiCaL version: 2.1.3 % 70.73/11.11 % (2366145)Termination reason: Refutation not found, incomplete strategy % 70.73/11.11 % (2366145)Time elapsed: 0.338 s % 70.73/11.11 % (2366145)Peak memory usage: 133 MB % 70.73/11.11 % (2366145)Instructions burned: 914 (million) % 70.73/11.11 % (2366144)------------------------------ % 70.73/11.11 % (2366144)------------------------------ % 70.73/11.11 % (2366148)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=1834620653:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2904 on theBenchmark for (2904ds/13494Mi) % 70.73/11.11 % (2366145)------------------------------ % 70.73/11.11 % (2366145)------------------------------ % 70.73/11.11 % (2366150)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=2123722835:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2903 on theBenchmark for (2903ds/2503Mi) % 70.73/11.11 [W927 12:55:00.687948902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.687978448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688005792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688013476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688027152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688032895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688045938 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688051555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688064815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688070591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688083871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 [W927 12:55:00.688089541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.57/12.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.57/12.60 % (2366150)Refutation not found, incomplete strategy % 81.57/12.60 % (2366150)------------------------------ % 81.57/12.60 % (2366150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.57/12.60 % (2366150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.57/12.60 % (2366150)CaDiCaL version: 2.1.3 % 81.57/12.60 % (2366150)Termination reason: Refutation not found, incomplete strategy % 81.57/12.60 % (2366150)Time elapsed: 0.307 s % 81.57/12.60 % (2366150)Peak memory usage: 126 MB % 81.57/12.60 % (2366150)Instructions burned: 829 (million) % 81.57/12.60 % (2366150)------------------------------ % 85.50/13.16 % (2366150)------------------------------ % 85.50/13.16 % (2366152)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=33679109:i=2559:sd=1:ep=RSTC:ss=axioms_2898 on theBenchmark for (2898ds/2559Mi) % 85.50/13.16 [W927 12:55:00.252551179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252579611 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252601160 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252607097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252620414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252625960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252638981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252644560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252657098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252662681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252675264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 [W927 12:55:00.252680731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.50/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.50/13.16 % (2366152)Refutation not found, incomplete strategy % 85.50/13.16 % (2366152)------------------------------ % 85.50/13.16 % (2366152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.71 % (2366152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.71 % (2366152)CaDiCaL version: 2.1.3 % 89.33/13.71 % (2366152)Termination reason: Refutation not found, incomplete strategy % 89.33/13.71 % (2366152)Time elapsed: 0.302 s % 89.33/13.71 % (2366152)Peak memory usage: 125 MB % 89.33/13.71 % (2366152)Instructions burned: 829 (million) % 89.33/13.71 % (2366152)------------------------------ % 89.33/13.71 % (2366152)------------------------------ % 89.33/13.71 % (2366154)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=113997717:i=30753:av=off:ss=included_2892 on theBenchmark for (2892ds/30753Mi) % 89.33/13.71 % (2366133)Instruction limit reached! % 89.33/13.71 % (2366133)------------------------------ % 89.33/13.71 % (2366133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.71 % (2366133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.71 % (2366133)CaDiCaL version: 2.1.3 % 89.33/13.71 % (2366133)Termination reason: Instruction limit % 89.33/13.71 % (2366133)Termination phase: Saturation % 89.33/13.71 % (2366133)Time elapsed: 2.956 s % 89.33/13.71 % (2366133)Peak memory usage: 184 MB % 89.33/13.71 % (2366133)Instructions burned: 8328 (million) % 89.33/13.71 % (2366140)Instruction limit reached! % 89.33/13.71 % (2366140)------------------------------ % 89.33/13.71 % (2366140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.71 % (2366140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.71 % (2366140)CaDiCaL version: 2.1.3 % 89.33/13.71 % (2366140)Termination reason: Instruction limit % 89.33/13.71 % (2366140)Termination phase: Saturation % 89.33/13.71 % (2366140)Time elapsed: 2.425 s % 89.33/13.71 % (2366140)Peak memory usage: 187 MB % 89.33/13.71 % (2366140)Instructions burned: 6997 (million) % 89.33/13.71 % (2366156)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=53632413:i=26473:ep=RSTC_2888 on theBenchmark for (2888ds/26473Mi) % 89.33/13.71 % (2366157)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=764248025:cts=off:i=2759:kws=inv_arity:fgj=on_2888 on theBenchmark for (2888ds/2759Mi) % 89.33/13.71 % (2366157)Refutation not found, incomplete strategy % 89.33/13.71 % (2366157)------------------------------ % 89.33/13.71 % (2366157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.33/13.71 % (2366157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.33/13.71 % (2366157)CaDiCaL version: 2.1.3 % 89.33/13.71 % (2366157)Termination reason: Refutation not found, incomplete strategy % 89.33/13.71 % (2366157)Time elapsed: 0.335 s % 89.33/13.71 % (2366157)Peak memory usage: 130 MB % 89.33/13.71 % (2366157)Instructions burned: 924 (million) % 89.33/13.71 % (2366157)------------------------------ % 89.33/13.71 % (2366157)------------------------------ % 89.33/13.71 % (2366160)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=1395560465:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2882 on theBenchmark for (2882ds/5665Mi) % 89.33/13.71 [W927 12:55:02.840705328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.33/13.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.33/13.71 [W927 12:55:02.840724354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.33/13.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.33/13.71 [W927 12:55:02.840763059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.33/13.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.33/13.71 [W927 12:55:02.840769331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840783094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840792121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840805280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840810536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840823066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840828340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840841063 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.840846576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 % (2366160)Refutation not found, incomplete strategy % 90.55/13.96 % (2366160)------------------------------ % 90.55/13.96 % (2366160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.55/13.96 % (2366160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.55/13.96 % (2366160)CaDiCaL version: 2.1.3 % 90.55/13.96 % (2366160)Termination reason: Refutation not found, incomplete strategy % 90.55/13.96 % (2366160)Time elapsed: 0.309 s % 90.55/13.96 % (2366160)Peak memory usage: 126 MB % 90.55/13.96 % (2366160)Instructions burned: 830 (million) % 90.55/13.96 % (2366160)------------------------------ % 90.55/13.96 % (2366160)------------------------------ % 90.55/13.96 % (2366162)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=2261782394:i=1532:ep=RS:ss=axioms_2876 on theBenchmark for (2876ds/1532Mi) % 90.55/13.96 [W927 12:55:02.399339745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.399362543 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.55/13.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.55/13.96 [W927 12:55:02.399383908 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399392238 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399412541 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399418774 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399432109 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399438108 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399450788 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399456871 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399470119 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 [W927 12:55:02.399476159 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/14.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.78/14.94 % (2366162)Refutation not found, incomplete strategy % 97.78/14.94 % (2366162)------------------------------ % 97.78/14.94 % (2366162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/14.94 % (2366162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/14.94 % (2366162)CaDiCaL version: 2.1.3 % 97.78/14.94 % (2366162)Termination reason: Refutation not found, incomplete strategy % 97.78/14.94 % (2366162)Time elapsed: 0.307 s % 97.78/14.94 % (2366162)Peak memory usage: 126 MB % 97.78/14.94 % (2366162)Instructions burned: 830 (million) % 97.78/14.94 % (2366162)------------------------------ % 97.78/14.94 % (2366162)------------------------------ % 97.78/14.94 % (2366164)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=774524721:i=1565:sd=2:ss=axioms:sgt=32_2871 on theBenchmark for (2871ds/1565Mi) % 97.78/14.94 [W927 12:55:03.950713541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950734729 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950772144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950778415 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950792334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950797817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950811235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950818938 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950832308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950837905 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950850487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 [W927 12:55:03.950862994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.98/15.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.98/15.56 % (2366164)Refutation not found, incomplete strategy % 101.98/15.56 % (2366164)------------------------------ % 101.98/15.56 % (2366164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.98/15.56 % (2366164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.98/15.56 % (2366164)CaDiCaL version: 2.1.3 % 101.98/15.56 % (2366164)Termination reason: Refutation not found, incomplete strategy % 101.98/15.56 % (2366164)Time elapsed: 0.309 s % 101.98/15.56 % (2366164)Peak memory usage: 126 MB % 101.98/15.56 % (2366164)Instructions burned: 830 (million) % 101.98/15.56 % (2366164)------------------------------ % 106.65/16.12 % (2366164)------------------------------ % 106.65/16.12 % (2366166)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=2421054548:i=1572:fgj=on:gsp=on_2865 on theBenchmark for (2865ds/1572Mi) % 106.65/16.12 % (2366166)Instruction limit reached! % 106.65/16.12 % (2366166)------------------------------ % 106.65/16.12 % (2366166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.65/16.12 % (2366166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.65/16.12 % (2366166)CaDiCaL version: 2.1.3 % 106.65/16.12 % (2366166)Termination reason: Instruction limit % 106.65/16.12 % (2366166)Termination phase: Saturation % 106.65/16.12 % (2366166)Time elapsed: 0.568 s % 106.65/16.12 % (2366166)Peak memory usage: 136 MB % 106.65/16.12 % (2366166)Instructions burned: 1574 (million) % 106.65/16.12 % (2366300)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2715577031:i=6052:sd=4:ss=axioms:sgt=24_2858 on theBenchmark for (2858ds/6052Mi) % 106.65/16.12 % (2366148)Instruction limit reached! % 106.65/16.12 % (2366148)------------------------------ % 106.65/16.12 % (2366148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.65/16.12 % (2366148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.65/16.12 % (2366148)CaDiCaL version: 2.1.3 % 106.65/16.12 % (2366148)Termination reason: Instruction limit % 106.65/16.12 % (2366148)Termination phase: Saturation % 106.65/16.12 % (2366148)Time elapsed: 4.683 s % 106.65/16.12 % (2366148)Peak memory usage: 249 MB % 106.65/16.12 % (2366148)Instructions burned: 13495 (million) % 106.65/16.12 % (2366302)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=1707288842:i=3500:sd=1:bd=preordered:sup=off:ss=included_2856 on theBenchmark for (2856ds/3500Mi) % 106.65/16.12 [W927 12:55:04.184179791 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184198970 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184219188 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184226104 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184240888 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184247210 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184261456 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.65/16.12 [W927 12:55:04.184267653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:04.184281201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:04.184286807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:04.184299336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:04.184304747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 % (2366300)Refutation not found, incomplete strategy % 122.03/18.30 % (2366300)------------------------------ % 122.03/18.30 % (2366300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.03/18.30 % (2366300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/18.30 % (2366300)CaDiCaL version: 2.1.3 % 122.03/18.30 % (2366300)Termination reason: Refutation not found, incomplete strategy % 122.03/18.30 % (2366300)Time elapsed: 0.306 s % 122.03/18.30 % (2366300)Peak memory usage: 126 MB % 122.03/18.30 % (2366300)Instructions burned: 829 (million) % 122.03/18.30 % (2366300)------------------------------ % 122.03/18.30 % (2366300)------------------------------ % 122.03/18.30 % (2366302)Refutation not found, incomplete strategy % 122.03/18.30 % (2366302)------------------------------ % 122.03/18.30 % (2366302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.03/18.30 % (2366302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/18.30 % (2366302)CaDiCaL version: 2.1.3 % 122.03/18.30 % (2366302)Termination reason: Refutation not found, incomplete strategy % 122.03/18.30 % (2366302)Time elapsed: 0.354 s % 122.03/18.30 % (2366302)Peak memory usage: 134 MB % 122.03/18.30 % (2366302)Instructions burned: 917 (million) % 122.03/18.30 % (2366405)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=2219327941:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2853 on theBenchmark for (2853ds/1842Mi) % 122.03/18.30 % (2366302)------------------------------ % 122.03/18.30 % (2366302)------------------------------ % 122.03/18.30 [W927 12:55:05.805957955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:05.805977863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:05.806022760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.03/18.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.03/18.30 [W927 12:55:05.806029557 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806046774 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806052530 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806065974 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806071474 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806083916 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806089319 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806101996 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.806107454 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 % (2366444)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4233125387:i=66096:add=on_2850 on theBenchmark for (2850ds/66096Mi) % 129.51/19.44 % (2366405)Refutation not found, incomplete strategy % 129.51/19.44 % (2366405)------------------------------ % 129.51/19.44 % (2366405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.51/19.44 % (2366405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.51/19.44 % (2366405)CaDiCaL version: 2.1.3 % 129.51/19.44 % (2366405)Termination reason: Refutation not found, incomplete strategy % 129.51/19.44 % (2366405)Time elapsed: 0.361 s % 129.51/19.44 % (2366405)Peak memory usage: 126 MB % 129.51/19.44 % (2366405)Instructions burned: 834 (million) % 129.51/19.44 % (2366405)------------------------------ % 129.51/19.44 % (2366405)------------------------------ % 129.51/19.44 % (2366544)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=579575899:i=1884:sd=1:nm=60:ss=axioms_2846 on theBenchmark for (2846ds/1884Mi) % 129.51/19.44 [W927 12:55:05.362284712 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/19.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.51/19.44 [W927 12:55:05.362303461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362325223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362331125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362344701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362350103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362362886 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362368193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362380776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362386380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362398897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 [W927 12:55:05.362404250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.26/20.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.26/20.83 % (2366544)Refutation not found, incomplete strategy % 139.26/20.83 % (2366544)------------------------------ % 139.26/20.83 % (2366544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.26/20.83 % (2366544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.26/20.83 % (2366544)CaDiCaL version: 2.1.3 % 139.26/20.83 % (2366544)Termination reason: Refutation not found, incomplete strategy % 139.26/20.83 % (2366544)Time elapsed: 0.310 s % 139.26/20.83 % (2366544)Peak memory usage: 125 MB % 139.26/20.83 % (2366544)Instructions burned: 829 (million) % 139.26/20.83 % (2366544)------------------------------ % 139.26/20.83 % (2366544)------------------------------ % 139.26/20.83 % (2366604)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1349650059:cts=off:i=5469:bs=on:fsr=off_2841 on theBenchmark for (2841ds/5469Mi) % 139.26/20.83 % (2366604)Instruction limit reached! % 139.26/20.83 % (2366604)------------------------------ % 139.26/20.83 % (2366604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.82/21.35 % (2366604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.82/21.35 % (2366604)CaDiCaL version: 2.1.3 % 142.82/21.35 % (2366604)Termination reason: Instruction limit % 142.82/21.35 % (2366604)Termination phase: Saturation % 142.82/21.35 % (2366604)Time elapsed: 1.831 s % 142.82/21.35 % (2366604)Peak memory usage: 114 MB % 142.82/21.35 % (2366604)Instructions burned: 5471 (million) % 142.82/21.35 % (2366606)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=4022914251:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2822 on theBenchmark for (2822ds/2037Mi) % 142.82/21.35 % (2366606)Instruction limit reached! % 142.82/21.35 % (2366606)------------------------------ % 142.82/21.35 % (2366606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.82/21.35 % (2366606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.82/21.35 % (2366606)CaDiCaL version: 2.1.3 % 142.82/21.35 % (2366606)Termination reason: Instruction limit % 142.82/21.35 % (2366606)Termination phase: Saturation % 142.82/21.35 % (2366606)Time elapsed: 0.732 s % 142.82/21.35 % (2366606)Peak memory usage: 139 MB % 142.82/21.35 % (2366606)Instructions burned: 2038 (million) % 142.82/21.35 % (2366608)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2916872505:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2813 on theBenchmark for (2813ds/2110Mi) % 142.82/21.35 [W927 12:55:09.680336414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680356451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680377561 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680384569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680399256 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680405653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680419500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680425684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.82/21.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.82/21.35 [W927 12:55:09.680438989 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.87/22.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/22.18 [W927 12:55:09.680445199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.87/22.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/22.18 [W927 12:55:09.680458264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.87/22.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/22.18 [W927 12:55:09.680463707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.87/22.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/22.18 % (2366608)Refutation not found, incomplete strategy % 148.87/22.18 % (2366608)------------------------------ % 148.87/22.18 % (2366608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.87/22.18 % (2366608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.87/22.18 % (2366608)CaDiCaL version: 2.1.3 % 148.87/22.18 % (2366608)Termination reason: Refutation not found, incomplete strategy % 148.87/22.18 % (2366608)Time elapsed: 0.308 s % 148.87/22.18 % (2366608)Peak memory usage: 125 MB % 148.87/22.18 % (2366608)Instructions burned: 831 (million) % 148.87/22.18 % (2366608)------------------------------ % 148.87/22.18 % (2366608)------------------------------ % 148.87/22.18 % (2366610)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=4060972636:i=2430:add=off:aac=none:nm=16_2808 on theBenchmark for (2808ds/2430Mi) % 148.87/22.18 % (2366127)Instruction limit reached! % 148.87/22.18 % (2366127)------------------------------ % 148.87/22.18 % (2366127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.87/22.18 % (2366127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.87/22.18 % (2366127)CaDiCaL version: 2.1.3 % 148.87/22.18 % (2366127)Termination reason: Instruction limit % 148.87/22.18 % (2366127)Termination phase: Saturation % 148.87/22.18 % (2366127)Time elapsed: 12.248 s % 148.87/22.18 % (2366127)Peak memory usage: 235 MB % 148.87/22.18 % (2366127)Instructions burned: 33335 (million) % 148.87/22.18 % (2366612)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=3100418834:cond=fast:i=4891_2805 on theBenchmark for (2805ds/4891Mi) % 148.87/22.18 % (2366610)Instruction limit reached! % 148.87/22.18 % (2366610)------------------------------ % 148.87/22.18 % (2366610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.87/22.18 % (2366610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.87/22.18 % (2366610)CaDiCaL version: 2.1.3 % 148.87/22.18 % (2366610)Termination reason: Instruction limit % 148.87/22.18 % (2366610)Termination phase: Saturation % 148.87/22.18 % (2366610)Time elapsed: 0.684 s % 148.87/22.18 % (2366610)Peak memory usage: 135 MB % 148.87/22.18 % (2366610)Instructions burned: 2433 (million) % 148.87/22.18 % (2366614)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=527104507:st=2:i=14845:sd=2:ss=included:fsd=on_2800 on theBenchmark for (2800ds/14845Mi) % 148.87/22.18 % (2366156)Instruction limit reached! % 148.87/22.18 % (2366156)------------------------------ % 148.87/22.18 % (2366156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.87/22.18 % (2366156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.87/22.18 % (2366156)CaDiCaL version: 2.1.3 % 148.87/22.18 % (2366156)Termination reason: Instruction limit % 148.87/22.18 % (2366156)Termination phase: Saturation % 148.87/22.18 % (2366156)Time elapsed: 8.938 s % 148.87/22.18 % (2366156)Peak memory usage: 495 MB % 148.87/22.18 % (2366156)Instructions burned: 26473 (million) % 148.87/22.18 % (2366616)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2254172528:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2797 on theBenchmark for (2797ds/7534Mi) % 157.00/23.38 % (2366614)Refutation not found, incomplete strategy % 157.00/23.38 % (2366614)------------------------------ % 157.00/23.38 % (2366614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.00/23.38 % (2366614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/23.38 % (2366614)CaDiCaL version: 2.1.3 % 157.00/23.38 % (2366614)Termination reason: Refutation not found, incomplete strategy % 157.00/23.38 % (2366614)Time elapsed: 0.335 s % 157.00/23.38 % (2366614)Peak memory usage: 133 MB % 157.00/23.38 % (2366614)Instructions burned: 911 (million) % 157.00/23.38 % (2366614)------------------------------ % 157.00/23.38 % (2366614)------------------------------ % 157.00/23.38 % (2366618)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=2664478155:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2794 on theBenchmark for (2794ds/10353Mi) % 157.00/23.38 % (2366154)Instruction limit reached! % 157.00/23.38 % (2366154)------------------------------ % 157.00/23.38 % (2366154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.00/23.38 % (2366154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/23.38 % (2366154)CaDiCaL version: 2.1.3 % 157.00/23.38 % (2366154)Termination reason: Instruction limit % 157.00/23.38 % (2366154)Termination phase: Saturation % 157.00/23.38 % (2366154)Time elapsed: 9.835 s % 157.00/23.38 % (2366154)Peak memory usage: 339 MB % 157.00/23.38 % (2366154)Instructions burned: 30753 (million) % 157.00/23.38 % (2366620)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=607279419:i=7860_2793 on theBenchmark for (2793ds/7860Mi) % 157.00/23.38 % (2366620)Refutation not found, incomplete strategy % 157.00/23.38 % (2366620)------------------------------ % 157.00/23.38 % (2366620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.00/23.38 % (2366620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/23.38 % (2366620)CaDiCaL version: 2.1.3 % 157.00/23.38 % (2366620)Termination reason: Refutation not found, incomplete strategy % 157.00/23.38 % (2366620)Time elapsed: 0.009 s % 157.00/23.38 % (2366620)Peak memory usage: 89 MB % 157.00/23.38 % (2366620)Instructions burned: 31 (million) % 157.00/23.38 [W927 12:55:10.596188451 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596209763 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596231467 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596239108 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596253744 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596260387 register_special_ops.cpp:225] Warning: Creating a tensor from 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.00/23.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.00/23.38 [W927 12:55:10.596275126 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 [W927 12:55:10.596281694 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 [W927 12:55:10.596295122 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 [W927 12:55:10.596344949 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 [W927 12:55:10.596366060 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 [W927 12:55:10.596372087 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/23.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.73/23.74 % (2366618)Refutation not found, incomplete strategy % 159.73/23.74 % (2366618)------------------------------ % 159.73/23.74 % (2366618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.73/23.74 % (2366618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.73/23.74 % (2366618)CaDiCaL version: 2.1.3 % 159.73/23.74 % (2366618)Termination reason: Refutation not found, incomplete strategy % 159.73/23.74 % (2366618)Time elapsed: 0.306 s % 159.73/23.74 % (2366618)Peak memory usage: 126 MB % 159.73/23.74 % (2366618)Instructions burned: 829 (million) % 159.73/23.74 % (2366620)------------------------------ % 159.73/23.74 % (2366620)------------------------------ % 159.73/23.74 % (2366622)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=2161080312:i=7896:sd=2:bs=on:ss=included:sgt=20_2790 on theBenchmark for (2790ds/7896Mi) % 159.73/23.74 % (2366618)------------------------------ % 159.73/23.74 % (2366618)------------------------------ % 159.73/23.74 % (2366624)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=4241659351:i=5812:gtgl=2:gtg=all_2789 on theBenchmark for (2789ds/5812Mi) % 159.73/23.74 % (2366612)Instruction limit reached! % 159.73/23.74 % (2366612)------------------------------ % 159.73/23.74 % (2366612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.73/23.74 % (2366612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.73/23.74 % (2366612)CaDiCaL version: 2.1.3 % 159.73/23.74 % (2366612)Termination reason: Instruction limit % 159.73/23.74 % (2366612)Termination phase: Saturation % 159.73/23.74 % (2366612)Time elapsed: 1.646 s % 159.73/23.74 % (2366612)Peak memory usage: 172 MB % 159.73/23.74 % (2366612)Instructions burned: 4893 (million) % 159.73/23.74 % (2366626)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=2448719515:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2787 on theBenchmark for (2787ds/2965Mi) % 159.73/23.74 % (2366626)Refutation not found, incomplete strategy % 159.73/23.74 % (2366626)------------------------------ % 159.73/23.74 % (2366626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.73/23.74 % (2366626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.73/23.74 % (2366626)CaDiCaL version: 2.1.3 % 159.73/23.74 % (2366626)Termination reason: Refutation not found, incomplete strategy % 159.73/23.74 % (2366626)Time elapsed: 0.336 s % 159.73/23.74 % (2366626)Peak memory usage: 133 MB % 159.73/23.74 % (2366626)Instructions burned: 921 (million) % 162.25/24.08 % (2366626)------------------------------ % 162.25/24.08 % (2366626)------------------------------ % 162.25/24.08 % (2366628)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=4166560299:i=2967:kws=precedence:bd=preordered:av=off_2781 on theBenchmark for (2781ds/2967Mi) % 162.25/24.08 % (2366616)Instruction limit reached! % 162.25/24.08 % (2366616)------------------------------ % 162.25/24.08 % (2366616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.25/24.08 % (2366616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.25/24.08 % (2366616)CaDiCaL version: 2.1.3 % 162.25/24.08 % (2366616)Termination reason: Instruction limit % 162.25/24.08 % (2366616)Termination phase: Saturation % 162.25/24.08 % (2366616)Time elapsed: 2.231 s % 162.25/24.08 % (2366616)Peak memory usage: 167 MB % 162.25/24.08 % (2366616)Instructions burned: 7536 (million) % 162.25/24.08 % (2366630)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=1252145895:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2774 on theBenchmark for (2774ds/3022Mi) % 162.25/24.08 [W927 12:55:13.618386827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618422025 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618443313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618449451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618462960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618469354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618482566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618488770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618502340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.25/24.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.25/24.08 [W927 12:55:13.618508483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.618522411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.618527840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 % (2366628)Instruction limit reached! % 162.87/24.12 % (2366628)------------------------------ % 162.87/24.12 % (2366628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.87/24.12 % (2366628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/24.12 % (2366628)CaDiCaL version: 2.1.3 % 162.87/24.12 % (2366628)Termination reason: Instruction limit % 162.87/24.12 % (2366628)Termination phase: Saturation % 162.87/24.12 % (2366628)Time elapsed: 0.992 s % 162.87/24.12 % (2366628)Peak memory usage: 147 MB % 162.87/24.12 % (2366628)Instructions burned: 2968 (million) % 162.87/24.12 % (2366630)Refutation not found, incomplete strategy % 162.87/24.12 % (2366630)------------------------------ % 162.87/24.12 % (2366630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.87/24.12 % (2366630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.87/24.12 % (2366630)CaDiCaL version: 2.1.3 % 162.87/24.12 % (2366630)Termination reason: Refutation not found, incomplete strategy % 162.87/24.12 % (2366630)Time elapsed: 0.306 s % 162.87/24.12 % (2366630)Peak memory usage: 126 MB % 162.87/24.12 % (2366630)Instructions burned: 830 (million) % 162.87/24.12 % (2366632)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=1228953399:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2770 on theBenchmark for (2770ds/3207Mi) % 162.87/24.12 % (2366630)------------------------------ % 162.87/24.12 % (2366630)------------------------------ % 162.87/24.12 % (2366634)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1556533338:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2768 on theBenchmark for (2768ds/3289Mi) % 162.87/24.12 [W927 12:55:13.981686328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.981701591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.981738755 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.981745453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.981759388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.87/24.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.87/24.12 [W927 12:55:13.981765580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981779571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981785063 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981798296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981803614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981816291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 [W927 12:55:13.981821531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 164.73/24.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.73/24.65 % (2366624)Instruction limit reached! % 164.73/24.65 % (2366624)------------------------------ % 164.73/24.65 % (2366624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.73/24.65 % (2366624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.73/24.65 % (2366624)CaDiCaL version: 2.1.3 % 164.73/24.65 % (2366624)Termination reason: Instruction limit % 164.73/24.65 % (2366624)Termination phase: Saturation % 164.73/24.65 % (2366624)Time elapsed: 2.061 s % 164.73/24.65 % (2366624)Peak memory usage: 188 MB % 164.73/24.65 % (2366624)Instructions burned: 5813 (million) % 164.73/24.65 % (2366632)Refutation not found, incomplete strategy % 164.73/24.65 % (2366632)------------------------------ % 164.73/24.65 % (2366632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.73/24.65 % (2366632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.73/24.65 % (2366632)CaDiCaL version: 2.1.3 % 164.73/24.65 % (2366632)Termination reason: Refutation not found, incomplete strategy % 164.73/24.65 % (2366632)Time elapsed: 0.309 s % 164.73/24.65 % (2366632)Peak memory usage: 126 MB % 164.73/24.65 % (2366632)Instructions burned: 828 (million) % 164.73/24.65 % (2366636)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1059331527:i=38569:sd=3:ss=axioms:sgt=32_2767 on theBenchmark for (2767ds/38569Mi) % 164.73/24.65 % (2366632)------------------------------ % 164.73/24.65 % (2366632)------------------------------ % 164.73/24.65 % (2366634)Refutation not found, incomplete strategy % 164.73/24.65 % (2366634)------------------------------ % 164.73/24.65 % (2366634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.73/24.65 % (2366634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.73/24.65 % (2366634)CaDiCaL version: 2.1.3 % 164.73/24.65 % (2366634)Termination reason: Refutation not found, incomplete strategy % 164.73/24.65 % (2366634)Time elapsed: 0.342 s % 164.73/24.65 % (2366634)Peak memory usage: 134 MB % 164.73/24.65 % (2366634)Instructions burned: 927 (million) % 164.73/24.65 [W927 12:55:13.321851767 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321868347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321906404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321912503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321925609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321931283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321945653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321951453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321964656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321970567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321983353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 [W927 12:55:13.321989293 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 170.56/25.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 170.56/25.22 % (2366638)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1896196405:cts=off:i=3394_2765 on theBenchmark for (2765ds/3394Mi) % 170.56/25.22 % (2366622)Instruction limit reached! % 170.56/25.22 % (2366622)------------------------------ % 170.56/25.22 % (2366622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.56/25.22 % (2366622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.56/25.22 % (2366622)CaDiCaL version: 2.1.3 % 170.56/25.22 % (2366622)Termination reason: Instruction limit % 170.56/25.22 % (2366622)Termination phase: Saturation % 180.42/26.68 % (2366622)Time elapsed: 2.552 s % 180.42/26.68 % (2366622)Peak memory usage: 180 MB % 180.42/26.68 % (2366622)Instructions burned: 7899 (million) % 180.42/26.68 % (2366636)Refutation not found, incomplete strategy % 180.42/26.68 % (2366636)------------------------------ % 180.42/26.68 % (2366636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.42/26.68 % (2366636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.42/26.68 % (2366636)CaDiCaL version: 2.1.3 % 180.42/26.68 % (2366636)Termination reason: Refutation not found, incomplete strategy % 180.42/26.68 % (2366636)Time elapsed: 0.308 s % 180.42/26.68 % (2366636)Peak memory usage: 126 MB % 180.42/26.68 % (2366636)Instructions burned: 829 (million) % 180.42/26.68 % (2366640)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=115349507:i=33824:bd=preordered_2763 on theBenchmark for (2763ds/33824Mi) % 180.42/26.68 % (2366634)------------------------------ % 180.42/26.68 % (2366634)------------------------------ % 180.42/26.68 % (2366636)------------------------------ % 180.42/26.68 % (2366636)------------------------------ % 180.42/26.68 % (2366642)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=381665214:i=20684:bd=all:gtg=exists_sym_2762 on theBenchmark for (2762ds/20684Mi) % 180.42/26.68 % (2366643)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=1550203087: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_2761 on theBenchmark for (2761ds/7222Mi) % 180.42/26.68 [W927 12:55:14.888081199 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888103606 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888124348 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888131529 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888145934 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888152319 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888166894 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.42/26.68 [W927 12:55:14.888173445 register_special_ops.cpp:225] Warning: Creating a tensor from 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.42/26.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.888187085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.888192894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.888205502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.888211264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 % (2366643)Refutation not found, incomplete strategy % 211.64/31.11 % (2366643)------------------------------ % 211.64/31.11 % (2366643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.64/31.11 % (2366643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.64/31.11 % (2366643)CaDiCaL version: 2.1.3 % 211.64/31.11 % (2366643)Termination reason: Refutation not found, incomplete strategy % 211.64/31.11 % (2366643)Time elapsed: 0.310 s % 211.64/31.11 % (2366643)Peak memory usage: 126 MB % 211.64/31.11 % (2366643)Instructions burned: 834 (million) % 211.64/31.11 % (2366643)------------------------------ % 211.64/31.11 % (2366643)------------------------------ % 211.64/31.11 % (2366646)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2207009560:st=4:i=7295:sd=4:ep=R:ss=axioms_2756 on theBenchmark for (2756ds/7295Mi) % 211.64/31.11 [W927 12:55:14.456952526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.456974029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.456995130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.457009173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.457025195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.457031595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.64/31.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.64/31.11 [W927 12:55:14.457046445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 [W927 12:55:14.457052792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 [W927 12:55:14.457065355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 [W927 12:55:14.457082635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 [W927 12:55:14.457097175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 [W927 12:55:14.457102912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.53/31.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.53/31.85 % (2366638)Instruction limit reached! % 216.53/31.85 % (2366638)------------------------------ % 216.53/31.85 % (2366638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.85 % (2366638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.85 % (2366638)CaDiCaL version: 2.1.3 % 216.53/31.85 % (2366638)Termination reason: Instruction limit % 216.53/31.85 % (2366638)Termination phase: Saturation % 216.53/31.85 % (2366638)Time elapsed: 1.123 s % 216.53/31.85 % (2366638)Peak memory usage: 149 MB % 216.53/31.85 % (2366638)Instructions burned: 3397 (million) % 216.53/31.85 % (2366646)Refutation not found, incomplete strategy % 216.53/31.85 % (2366646)------------------------------ % 216.53/31.85 % (2366646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.85 % (2366646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.85 % (2366646)CaDiCaL version: 2.1.3 % 216.53/31.85 % (2366646)Termination reason: Refutation not found, incomplete strategy % 216.53/31.85 % (2366646)Time elapsed: 0.307 s % 216.53/31.85 % (2366646)Peak memory usage: 125 MB % 216.53/31.85 % (2366646)Instructions burned: 829 (million) % 216.53/31.85 % (2366648)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=3725222334:i=4036:ins=10_2752 on theBenchmark for (2752ds/4036Mi) % 216.53/31.85 % (2366646)------------------------------ % 216.53/31.85 % (2366646)------------------------------ % 216.53/31.85 % (2366650)lrs+10_1_sil=128000:lcm=predicate:random_seed=2426857421:st=3:i=43697:sd=5:ss=axioms_2750 on theBenchmark for (2750ds/43697Mi) % 216.53/31.85 % (2366650)Refutation not found, incomplete strategy % 216.53/31.85 % (2366650)------------------------------ % 216.53/31.85 % (2366650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.85 % (2366650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.85 % (2366650)CaDiCaL version: 2.1.3 % 216.53/31.85 % (2366650)Termination reason: Refutation not found, incomplete strategy % 216.53/31.85 % (2366650)Time elapsed: 0.001 s % 216.53/31.85 % (2366650)Peak memory usage: 86 MB % 216.53/31.85 % (2366650)Instructions burned: 1 (million) % 216.53/31.85 % (2366650)------------------------------ % 216.53/31.85 % (2366650)------------------------------ % 216.53/31.85 % (2366652)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=3666733652:i=17599:gtg=all:ss=axioms:fsd=on_2747 on theBenchmark for (2747ds/17599Mi) % 216.53/31.85 % (2366648)Instruction limit reached! % 216.53/31.85 % (2366648)------------------------------ % 220.63/32.33 % (2366648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/32.33 % (2366648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/32.33 % (2366648)CaDiCaL version: 2.1.3 % 220.63/32.33 % (2366648)Termination reason: Instruction limit % 220.63/32.33 % (2366648)Termination phase: Saturation % 220.63/32.33 % (2366648)Time elapsed: 1.356 s % 220.63/32.33 % (2366648)Peak memory usage: 160 MB % 220.63/32.33 % (2366648)Instructions burned: 4037 (million) % 220.63/32.33 % (2366654)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=2532553558:i=4547:bd=preordered_2738 on theBenchmark for (2738ds/4547Mi) % 220.63/32.33 % (2366654)Instruction limit reached! % 220.63/32.33 % (2366654)------------------------------ % 220.63/32.33 % (2366654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/32.33 % (2366654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/32.33 % (2366654)CaDiCaL version: 2.1.3 % 220.63/32.33 % (2366654)Termination reason: Instruction limit % 220.63/32.33 % (2366654)Termination phase: Saturation % 220.63/32.33 % (2366654)Time elapsed: 1.588 s % 220.63/32.33 % (2366654)Peak memory usage: 167 MB % 220.63/32.33 % (2366654)Instructions burned: 4549 (million) % 220.63/32.33 % (2366656)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=2715469469:i=9294:av=off_2721 on theBenchmark for (2721ds/9294Mi) % 220.63/32.33 % (2366444)Instruction limit reached! % 220.63/32.33 % (2366444)------------------------------ % 220.63/32.33 % (2366444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/32.33 % (2366444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/32.33 % (2366444)CaDiCaL version: 2.1.3 % 220.63/32.33 % (2366444)Termination reason: Instruction limit % 220.63/32.33 % (2366444)Termination phase: Saturation % 220.63/32.33 % (2366444)Time elapsed: 14.172 s % 220.63/32.33 % (2366444)Peak memory usage: 256 MB % 220.63/32.33 % (2366444)Instructions burned: 66099 (million) % 220.63/32.33 % (2366790)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=189098338:i=32849:add=on_2707 on theBenchmark for (2707ds/32849Mi) % 220.63/32.33 % (2366652)Instruction limit reached! % 220.63/32.33 % (2366652)------------------------------ % 220.63/32.33 % (2366652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 220.63/32.33 % (2366652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 220.63/32.33 % (2366652)CaDiCaL version: 2.1.3 % 220.63/32.33 % (2366652)Termination reason: Instruction limit % 220.63/32.33 % (2366652)Termination phase: Saturation % 220.63/32.33 % (2366652)Time elapsed: 4.821 s % 220.63/32.33 % (2366652)Peak memory usage: 317 MB % 220.63/32.33 % (2366652)Instructions burned: 17600 (million) % 220.63/32.33 % (2366906)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3069676196:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2698 on theBenchmark for (2698ds/4793Mi) % 220.63/32.33 [W927 12:55:20.346706215 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.63/32.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.63/32.33 [W927 12:55:20.346735651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.63/32.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.63/32.33 [W927 12:55:20.346767990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.63/32.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.63/32.33 [W927 12:55:20.346779652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 220.63/32.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 220.63/32.33 [W927 12:55:20.346804080 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346814871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346838078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346847633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346870701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346879741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346901540 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 [W927 12:55:20.346920174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.90/34.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.90/34.74 % (2366906)Refutation not found, incomplete strategy % 236.90/34.74 % (2366906)------------------------------ % 236.90/34.74 % (2366906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.90/34.74 % (2366906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.90/34.74 % (2366906)CaDiCaL version: 2.1.3 % 236.90/34.74 % (2366906)Termination reason: Refutation not found, incomplete strategy % 236.90/34.74 % (2366906)Time elapsed: 0.417 s % 236.90/34.74 % (2366906)Peak memory usage: 126 MB % 236.90/34.74 % (2366906)Instructions burned: 830 (million) % 236.90/34.74 % (2366906)------------------------------ % 236.90/34.74 % (2366906)------------------------------ % 236.90/34.74 % (2366642)Instruction limit reached! % 236.90/34.74 % (2366642)------------------------------ % 236.90/34.74 % (2366642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.90/34.74 % (2366642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.90/34.74 % (2366642)CaDiCaL version: 2.1.3 % 236.90/34.74 % (2366642)Termination reason: Instruction limit % 236.90/34.74 % (2366642)Termination phase: Saturation % 236.90/34.74 % (2366642)Time elapsed: 7.202 s % 236.90/34.74 % (2366642)Peak memory usage: 335 MB % 236.90/34.74 % (2366642)Instructions burned: 20686 (million) % 236.90/34.74 % (2366956)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=2516507384:i=4840:nm=4:av=off_2690 on theBenchmark for (2690ds/4840Mi) % 236.90/34.74 % (2366972)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=3898149433:cts=off:i=5002_2689 on theBenchmark for (2689ds/5002Mi) % 236.90/34.74 % (2366656)Instruction limit reached! % 236.90/34.74 % (2366656)------------------------------ % 300.41/43.64 % (2366656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.41/43.64 % (2366656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/43.64 % (2366656)CaDiCaL version: 2.1.3 % 300.41/43.64 % (2366656)Termination reason: Instruction limit % 300.41/43.64 % (2366656)Termination phase: Saturation % 300.41/43.64 % (2366656)Time elapsed: 3.363 s % 300.41/43.64 % (2366656)Peak memory usage: 197 MB % 300.41/43.64 % (2366656)Instructions burned: 9295 (million) % 300.41/43.64 % (2366989)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=3180525402:i=30479:sd=3:ss=axioms_2686 on theBenchmark for (2686ds/30479Mi) % 300.41/43.64 % (2366956)Refutation not found, incomplete strategy % 300.41/43.64 % (2366956)------------------------------ % 300.41/43.64 % (2366956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.41/43.64 % (2366956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.41/43.64 % (2366956)CaDiCaL version: 2.1.3 % 300.41/43.64 % (2366956)Termination reason: Refutation not found, incomplete strategy % 300.41/43.64 % (2366956)Time elapsed: 0.476 s % 300.41/43.64 % (2366956)Peak memory usage: 133 MB % 300.41/43.64 % (2366956)Instructions burned: 922 (million) % 300.41/43.64 % (2366956)------------------------------ % 300.41/43.64 % (2366956)------------------------------ % 300.41/43.64 [W927 12:55:21.568967405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.568994457 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569031883 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569042430 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569062878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569071846 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569091277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569099903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21.569120337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.41/43.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.41/43.64 [W927 12:55:21 % 300.41/43.64 Terminated %------------------------------------------------------------------------------