%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW478_10 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:37 PM UTC 2026 % Result : Timeout 300.63s 43.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : SWW478_10 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.27/0.32 % Computer : n009.cluster.edu % 0.27/0.32 % Model : x86_64 x86_64 % 0.27/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.27/0.32 % Memory : 8046.5625MB % 0.27/0.32 % OS : Linux 6.8.0-71-generic % 0.27/0.32 % CPULimit : 300 % 0.27/0.32 % WCLimit : 300 % 0.27/0.32 % DateTime : Mon Sep 28 14:13:00 UTC 2026 % 0.27/0.32 % CPUTime : % 0.27/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.27/0.38 Running first-order theorem proving % 0.27/0.38 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.55/3.60 % (3048925)Detected formulas, will run a generic FOF schedule. % 16.55/3.60 % (3048936)dis-21_1_sil=8000:lcm=predicate:random_seed=3940737811: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) % 16.55/3.60 % (3048930)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=1506593443:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 16.55/3.60 % (3048931)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=716865664:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 16.55/3.60 % (3048932)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=832110701:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 16.55/3.60 % (3048933)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2908668769:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 16.55/3.60 % (3048933)Refutation not found, incomplete strategy % 16.55/3.60 % (3048933)------------------------------ % 16.55/3.60 % (3048933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.55/3.60 % (3048933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.55/3.60 % (3048933)CaDiCaL version: 2.1.3 % 16.55/3.60 % (3048933)Termination reason: Refutation not found, incomplete strategy % 16.55/3.60 % (3048933)Time elapsed: 0.002 s % 16.55/3.60 % (3048933)Peak memory usage: 87 MB % 16.55/3.60 % (3048933)Instructions burned: 1 (million) % 16.55/3.60 % (3048936)Instruction limit reached! % 16.55/3.60 % (3048936)------------------------------ % 16.55/3.60 % (3048936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.55/3.60 % (3048936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.55/3.60 % (3048936)CaDiCaL version: 2.1.3 % 16.55/3.60 % (3048936)Termination reason: Instruction limit % 16.55/3.60 % (3048936)Termination phase: Saturation % 16.55/3.60 % (3048936)Time elapsed: 0.064 s % 16.55/3.60 % (3048936)Peak memory usage: 89 MB % 16.55/3.60 % (3048936)Instructions burned: 130 (million) % 16.55/3.60 % (3048934)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2276835086:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 16.55/3.60 % (3048934)Refutation not found, incomplete strategy % 16.55/3.60 % (3048934)------------------------------ % 16.55/3.60 % (3048934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.55/3.60 % (3048934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.55/3.60 % (3048934)CaDiCaL version: 2.1.3 % 16.55/3.60 % (3048934)Termination reason: Refutation not found, incomplete strategy % 16.55/3.60 % (3048934)Time elapsed: 0.002 s % 16.55/3.60 % (3048934)Peak memory usage: 86 MB % 16.55/3.60 % (3048934)Instructions burned: 1 (million) % 16.55/3.60 % (3048935)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=321161046:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 16.55/3.60 % (3048935)Instruction limit reached! % 16.55/3.60 % (3048935)------------------------------ % 16.55/3.60 % (3048935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.55/3.60 % (3048935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.55/3.60 % (3048935)CaDiCaL version: 2.1.3 % 16.55/3.60 % (3048935)Termination reason: Instruction limit % 16.55/3.60 % (3048935)Termination phase: Saturation % 16.55/3.60 % (3048935)Time elapsed: 0.149 s % 16.55/3.60 % (3048935)Peak memory usage: 90 MB % 16.55/3.60 % (3048935)Instructions burned: 139 (million) % 16.55/3.60 % (3048943)lrs+10_1_sil=8000:sp=occurrence:random_seed=3563258316:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 16.55/3.60 % (3048943)Refutation not found, incomplete strategy % 16.55/3.60 % (3048943)------------------------------ % 16.55/3.60 % (3048943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.55/3.60 % (3048943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.55/3.60 % (3048943)CaDiCaL version: 2.1.3 % 16.55/3.60 % (3048943)Termination reason: Refutation not found, incomplete strategy % 16.55/3.60 % (3048943)Time elapsed: 0.002 s % 16.55/3.60 % (3048943)Peak memory usage: 87 MB % 16.55/3.60 % (3048943)Instructions burned: 1 (million) % 16.55/3.60 % (3048933)------------------------------ % 17.90/3.92 % (3048933)------------------------------ % 17.90/3.92 % (3048934)------------------------------ % 17.90/3.92 % (3048934)------------------------------ % 17.90/3.92 % (3048946)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3725421804:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 17.90/3.92 % (3048946)Refutation not found, incomplete strategy % 17.90/3.92 % (3048946)------------------------------ % 17.90/3.92 % (3048946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.92 % (3048946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.92 % (3048946)CaDiCaL version: 2.1.3 % 17.90/3.92 % (3048946)Termination reason: Refutation not found, incomplete strategy % 17.90/3.92 % (3048946)Time elapsed: 0.005 s % 17.90/3.92 % (3048946)Peak memory usage: 87 MB % 17.90/3.92 % (3048946)Instructions burned: 4 (million) % 17.90/3.92 % (3048943)------------------------------ % 17.90/3.92 % (3048943)------------------------------ % 17.90/3.92 % (3048948)lrs+1011_1_sil=32000:sp=occurrence:random_seed=339740867:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi) % 17.90/3.92 % (3048948)Refutation not found, incomplete strategy % 17.90/3.92 % (3048948)------------------------------ % 17.90/3.92 % (3048948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.92 % (3048948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.92 % (3048948)CaDiCaL version: 2.1.3 % 17.90/3.92 % (3048948)Termination reason: Refutation not found, incomplete strategy % 17.90/3.92 % (3048948)Time elapsed: 0.002 s % 17.90/3.92 % (3048948)Peak memory usage: 87 MB % 17.90/3.92 % (3048948)Instructions burned: 1 (million) % 17.90/3.92 % (3048949)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=3902132218:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi) % 17.90/3.92 % (3048951)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2493521213:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi) % 17.90/3.92 % (3048951)Refutation not found, incomplete strategy % 17.90/3.92 % (3048951)------------------------------ % 17.90/3.92 % (3048951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.92 % (3048951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.92 % (3048951)CaDiCaL version: 2.1.3 % 17.90/3.92 % (3048951)Termination reason: Refutation not found, incomplete strategy % 17.90/3.92 % (3048951)Time elapsed: 0.001 s % 17.90/3.92 % (3048951)Peak memory usage: 86 MB % 17.90/3.92 % (3048951)Instructions burned: 1 (million) % 17.90/3.92 % (3048946)------------------------------ % 17.90/3.92 % (3048946)------------------------------ % 17.90/3.92 % (3048949)Instruction limit reached! % 17.90/3.92 % (3048949)------------------------------ % 17.90/3.92 % (3048949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.92 % (3048949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.92 % (3048949)CaDiCaL version: 2.1.3 % 17.90/3.92 % (3048949)Termination reason: Instruction limit % 17.90/3.92 % (3048949)Termination phase: Saturation % 17.90/3.92 % (3048949)Time elapsed: 0.239 s % 17.90/3.92 % (3048949)Peak memory usage: 91 MB % 17.90/3.92 % (3048949)Instructions burned: 249 (million) % 17.90/3.92 % (3048932)Refutation not found, incomplete strategy % 17.90/3.92 % (3048932)------------------------------ % 17.90/3.92 % (3048932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.90/3.92 % (3048932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.90/3.92 % (3048932)CaDiCaL version: 2.1.3 % 17.90/3.92 % (3048932)Termination reason: Refutation not found, incomplete strategy % 17.90/3.92 % (3048932)Time elapsed: 0.997 s % 17.90/3.92 % (3048932)Peak memory usage: 133 MB % 17.90/3.92 % (3048932)Instructions burned: 917 (million) % 17.90/3.92 % (3048951)------------------------------ % 17.90/3.92 % (3048951)------------------------------ % 17.90/3.92 % (3048948)------------------------------ % 17.90/3.92 % (3048948)------------------------------ % 17.90/3.92 % (3048955)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3766958696:i=2350_2987 on theBenchmark for (2987ds/2350Mi) % 17.90/3.92 % (3048957)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2234417642:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi) % 17.90/3.92 % (3048957)Refutation not found, incomplete strategy % 17.90/3.92 % (3048957)------------------------------ % 22.85/4.43 % (3048957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.85/4.43 % (3048957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.85/4.43 % (3048957)CaDiCaL version: 2.1.3 % 22.85/4.43 % (3048957)Termination reason: Refutation not found, incomplete strategy % 22.85/4.43 % (3048957)Time elapsed: 0.006 s % 22.85/4.43 % (3048957)Peak memory usage: 88 MB % 22.85/4.43 % (3048957)Instructions burned: 19 (million) % 22.85/4.43 % (3048956)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1534710687:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi) % 22.85/4.43 % (3048956)Refutation not found, incomplete strategy % 22.85/4.43 % (3048956)------------------------------ % 22.85/4.43 % (3048956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.85/4.43 % (3048956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.85/4.43 % (3048956)CaDiCaL version: 2.1.3 % 22.85/4.43 % (3048956)Termination reason: Refutation not found, incomplete strategy % 22.85/4.43 % (3048956)Time elapsed: 0.033 s % 22.85/4.43 % (3048956)Peak memory usage: 89 MB % 22.85/4.43 % (3048956)Instructions burned: 32 (million) % 22.85/4.43 % (3048932)------------------------------ % 22.85/4.43 % (3048932)------------------------------ % 22.85/4.43 % (3048958)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=221717772:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi) % 22.85/4.43 % (3048957)------------------------------ % 22.85/4.43 % (3048957)------------------------------ % 22.85/4.43 % (3048958)Instruction limit reached! % 22.85/4.43 % (3048958)------------------------------ % 22.85/4.43 % (3048958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.85/4.43 % (3048958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.85/4.43 % (3048958)CaDiCaL version: 2.1.3 % 22.85/4.43 % (3048958)Termination reason: Instruction limit % 22.85/4.43 % (3048958)Termination phase: Saturation % 22.85/4.43 % (3048958)Time elapsed: 0.110 s % 22.85/4.43 % (3048958)Peak memory usage: 89 MB % 22.85/4.43 % (3048958)Instructions burned: 114 (million) % 22.85/4.43 % (3048962)lrs+10_1_sil=8000:sp=occurrence:random_seed=3197551580:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi) % 22.85/4.43 % (3048962)Refutation not found, incomplete strategy % 22.85/4.43 % (3048962)------------------------------ % 22.85/4.43 % (3048962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.85/4.43 % (3048962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.85/4.43 % (3048962)CaDiCaL version: 2.1.3 % 22.85/4.43 % (3048962)Termination reason: Refutation not found, incomplete strategy % 22.85/4.43 % (3048962)Time elapsed: 0.002 s % 22.85/4.43 % (3048962)Peak memory usage: 87 MB % 22.85/4.43 % (3048962)Instructions burned: 1 (million) % 22.85/4.43 % (3048964)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2845739594:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi) % 22.85/4.43 % (3048956)------------------------------ % 22.85/4.43 % (3048956)------------------------------ % 22.85/4.43 % (3048964)Refutation not found, incomplete strategy % 22.85/4.43 % (3048964)------------------------------ % 22.85/4.43 % (3048964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.85/4.43 % (3048964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.85/4.43 % (3048964)CaDiCaL version: 2.1.3 % 22.85/4.43 % (3048964)Termination reason: Refutation not found, incomplete strategy % 22.85/4.43 % (3048964)Time elapsed: 0.015 s % 22.85/4.43 % (3048964)Peak memory usage: 89 MB % 22.85/4.43 % (3048964)Instructions burned: 27 (million) % 22.85/4.43 % (3048965)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2543926207:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi) % 22.85/4.43 % (3048964)------------------------------ % 22.85/4.43 % (3048964)------------------------------ % 22.85/4.43 % (3048968)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2937533884:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi) % 22.85/4.43 % (3048962)------------------------------ % 22.85/4.43 % (3048962)------------------------------ % 22.85/4.43 % (3048968)Instruction limit reached! % 22.85/4.43 % (3048968)------------------------------ % 22.85/4.43 % (3048968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.99/4.64 % (3048968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/4.64 % (3048968)CaDiCaL version: 2.1.3 % 23.99/4.64 % (3048968)Termination reason: Instruction limit % 23.99/4.64 % (3048968)Termination phase: Saturation % 23.99/4.64 % (3048968)Time elapsed: 0.128 s % 23.99/4.64 % (3048968)Peak memory usage: 90 MB % 23.99/4.64 % (3048968)Instructions burned: 135 (million) % 23.99/4.64 % (3048970)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=70460991:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi) % 23.99/4.64 % (3048970)Refutation not found, incomplete strategy % 23.99/4.64 % (3048970)------------------------------ % 23.99/4.64 % (3048970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.99/4.64 % (3048970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/4.64 % (3048970)CaDiCaL version: 2.1.3 % 23.99/4.64 % (3048970)Termination reason: Refutation not found, incomplete strategy % 23.99/4.64 % (3048970)Time elapsed: 0.002 s % 23.99/4.64 % (3048970)Peak memory usage: 86 MB % 23.99/4.64 % (3048970)Instructions burned: 1 (million) % 23.99/4.64 % (3048973)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=2538793200:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi) % 23.99/4.64 % (3048973)Refutation not found, incomplete strategy % 23.99/4.64 % (3048973)------------------------------ % 23.99/4.64 % (3048973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.99/4.64 % (3048973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.99/4.64 % (3048973)CaDiCaL version: 2.1.3 % 23.99/4.64 % (3048973)Termination reason: Refutation not found, incomplete strategy % 23.99/4.64 % (3048973)Time elapsed: 0.003 s % 23.99/4.64 % (3048973)Peak memory usage: 88 MB % 23.99/4.64 % (3048973)Instructions burned: 5 (million) % 23.99/4.64 % (3048972)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1702558704:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi) % 23.99/4.64 [W928 14:13:04.065331359 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065379173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065437353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065457324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065503327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065522467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.99/4.64 [W928 14:13:04.065567188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.99/4.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 [W928 14:13:04.065602961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.49/5.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 [W928 14:13:04.065647278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.49/5.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 [W928 14:13:04.065665445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.49/5.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 [W928 14:13:04.065708389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.49/5.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 [W928 14:13:04.065726342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.49/5.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.49/5.49 % (3048970)------------------------------ % 29.49/5.49 % (3048970)------------------------------ % 29.49/5.49 % (3048973)------------------------------ % 29.49/5.49 % (3048973)------------------------------ % 29.49/5.49 % (3048965)Refutation not found, incomplete strategy % 29.49/5.49 % (3048965)------------------------------ % 29.49/5.49 % (3048965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.49/5.49 % (3048965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/5.49 % (3048965)CaDiCaL version: 2.1.3 % 29.49/5.49 % (3048965)Termination reason: Refutation not found, incomplete strategy % 29.49/5.49 % (3048965)Time elapsed: 0.894 s % 29.49/5.49 % (3048965)Peak memory usage: 127 MB % 29.49/5.49 % (3048965)Instructions burned: 829 (million) % 29.49/5.49 % (3048977)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4200498378:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi) % 29.49/5.49 % (3048978)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3589822358:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi) % 29.49/5.49 % (3048978)Refutation not found, incomplete strategy % 29.49/5.49 % (3048978)------------------------------ % 29.49/5.49 % (3048978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.49/5.49 % (3048978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/5.49 % (3048978)CaDiCaL version: 2.1.3 % 29.49/5.49 % (3048978)Termination reason: Refutation not found, incomplete strategy % 29.49/5.49 % (3048978)Time elapsed: 0.002 s % 29.49/5.49 % (3048978)Peak memory usage: 87 MB % 29.49/5.50 % (3048978)Instructions burned: 1 (million) % 29.49/5.50 % (3048955)Instruction limit reached! % 29.49/5.50 % (3048955)------------------------------ % 29.49/5.50 % (3048955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.49/5.50 % (3048955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/5.50 % (3048955)CaDiCaL version: 2.1.3 % 29.49/5.50 % (3048955)Termination reason: Instruction limit % 29.49/5.50 % (3048955)Termination phase: Saturation % 29.49/5.50 % (3048955)Time elapsed: 1.698 s % 29.49/5.50 % (3048955)Peak memory usage: 141 MB % 29.49/5.50 % (3048955)Instructions burned: 2351 (million) % 29.49/5.50 % (3048977)Instruction limit reached! % 29.49/5.50 % (3048977)------------------------------ % 29.49/5.50 % (3048977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.49/5.50 % (3048977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.49/5.50 % (3048977)CaDiCaL version: 2.1.3 % 29.49/5.50 % (3048977)Termination reason: Instruction limit % 29.49/5.50 % (3048977)Termination phase: Saturation % 29.49/5.50 % (3048977)Time elapsed: 0.153 s % 41.85/7.06 % (3048977)Peak memory usage: 91 MB % 41.85/7.06 % (3048977)Instructions burned: 134 (million) % 41.85/7.06 [W928 14:13:04.575300836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575346276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575403120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575433854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575477577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575502274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575546174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575574598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575616245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575640489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575682246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 [W928 14:13:04.575700879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.85/7.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.85/7.06 % (3048978)------------------------------ % 41.85/7.06 % (3048978)------------------------------ % 41.85/7.06 % (3048965)------------------------------ % 41.85/7.06 % (3048965)------------------------------ % 41.85/7.06 % (3048981)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2246965538:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi) % 45.88/7.61 % (3048981)Refutation not found, incomplete strategy % 45.88/7.61 % (3048981)------------------------------ % 45.88/7.61 % (3048981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.88/7.61 % (3048981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.88/7.61 % (3048981)CaDiCaL version: 2.1.3 % 45.88/7.61 % (3048981)Termination reason: Refutation not found, incomplete strategy % 45.88/7.61 % (3048981)Time elapsed: 0.001 s % 45.88/7.61 % (3048981)Peak memory usage: 86 MB % 45.88/7.61 % (3048981)Instructions burned: 1 (million) % 45.88/7.61 % (3048982)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=3186738051:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi) % 45.88/7.61 % (3048972)Refutation not found, incomplete strategy % 45.88/7.61 % (3048972)------------------------------ % 45.88/7.61 % (3048972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.88/7.61 % (3048972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.88/7.61 % (3048972)CaDiCaL version: 2.1.3 % 45.88/7.61 % (3048972)Termination reason: Refutation not found, incomplete strategy % 45.88/7.61 % (3048972)Time elapsed: 0.899 s % 45.88/7.61 % (3048972)Peak memory usage: 126 MB % 45.88/7.61 % (3048972)Instructions burned: 829 (million) % 45.88/7.61 % (3048984)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3761150738:i=14155:bd=all_2965 on theBenchmark for (2965ds/14155Mi) % 45.88/7.61 % (3048983)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=2181987776:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi) % 45.88/7.61 % (3048981)------------------------------ % 45.88/7.61 % (3048981)------------------------------ % 45.88/7.61 % (3048983)Instruction limit reached! % 45.88/7.61 % (3048983)------------------------------ % 45.88/7.61 % (3048983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.88/7.61 % (3048983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.88/7.61 % (3048983)CaDiCaL version: 2.1.3 % 45.88/7.61 % (3048983)Termination reason: Instruction limit % 45.88/7.61 % (3048983)Termination phase: Saturation % 45.88/7.61 % (3048983)Time elapsed: 0.164 s % 45.88/7.61 % (3048983)Peak memory usage: 91 MB % 45.88/7.61 % (3048983)Instructions burned: 151 (million) % 45.88/7.61 % (3048972)------------------------------ % 45.88/7.61 % (3048972)------------------------------ % 45.88/7.61 % (3048990)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=1023475412:s2a=on:i=185:s2at=1.8:fdi=4_2961 on theBenchmark for (2961ds/185Mi) % 45.88/7.61 % (3048989)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2908031270:i=667:av=off:fsr=off_2961 on theBenchmark for (2961ds/667Mi) % 45.88/7.61 % (3048989)Refutation not found, incomplete strategy % 45.88/7.61 % (3048989)------------------------------ % 45.88/7.61 % (3048989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.88/7.61 % (3048989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.88/7.61 % (3048989)CaDiCaL version: 2.1.3 % 45.88/7.61 % (3048989)Termination reason: Refutation not found, incomplete strategy % 45.88/7.61 % (3048989)Time elapsed: 0.026 s % 45.88/7.61 % (3048989)Peak memory usage: 88 MB % 45.88/7.61 % (3048989)Instructions burned: 27 (million) % 45.88/7.61 % (3048991)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3241387528:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2960 on theBenchmark for (2960ds/193Mi) % 45.88/7.61 % (3048991)Refutation not found, incomplete strategy % 45.88/7.61 % (3048991)------------------------------ % 45.88/7.61 % (3048991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.88/7.61 % (3048991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.88/7.61 % (3048991)CaDiCaL version: 2.1.3 % 45.88/7.61 % (3048991)Termination reason: Refutation not found, incomplete strategy % 45.88/7.61 % (3048991)Time elapsed: 0.003 s % 45.88/7.61 % (3048991)Peak memory usage: 86 MB % 45.88/7.61 % (3048991)Instructions burned: 2 (million) % 45.88/7.61 % (3048990)Instruction limit reached! % 53.99/8.86 % (3048990)------------------------------ % 53.99/8.86 % (3048990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.99/8.86 % (3048990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.99/8.86 % (3048990)CaDiCaL version: 2.1.3 % 53.99/8.86 % (3048990)Termination reason: Instruction limit % 53.99/8.86 % (3048990)Termination phase: Saturation % 53.99/8.86 % (3048990)Time elapsed: 0.187 s % 53.99/8.86 % (3048990)Peak memory usage: 91 MB % 53.99/8.86 % (3048990)Instructions burned: 185 (million) % 53.99/8.86 % (3048995)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1272080014:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi) % 53.99/8.86 % (3048995)Refutation not found, incomplete strategy % 53.99/8.86 % (3048995)------------------------------ % 53.99/8.86 % (3048995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.99/8.86 % (3048995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.99/8.86 % (3048995)CaDiCaL version: 2.1.3 % 53.99/8.86 % (3048995)Termination reason: Refutation not found, incomplete strategy % 54.44/8.90 % (3048995)Time elapsed: 0.015 s % 54.44/8.90 % (3048995)Peak memory usage: 88 MB % 54.44/8.90 % (3048995)Instructions burned: 21 (million) % 54.44/8.90 % (3048989)------------------------------ % 54.44/8.90 % (3048989)------------------------------ % 54.44/8.90 % (3048991)------------------------------ % 54.44/8.90 % (3048991)------------------------------ % 54.44/8.90 % (3048997)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3791519321:i=12111:sd=1:ss=included_2954 on theBenchmark for (2954ds/12111Mi) % 54.44/8.90 % (3048998)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=777123619:i=319:kws=precedence:fsr=off_2953 on theBenchmark for (2953ds/319Mi) % 54.44/8.90 % (3048995)------------------------------ % 54.44/8.90 % (3048995)------------------------------ % 54.44/8.90 % (3049001)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3953426057:i=2064:ep=RST_2951 on theBenchmark for (2951ds/2064Mi) % 54.44/8.90 % (3049001)Refutation not found, incomplete strategy % 54.44/8.90 % (3049001)------------------------------ % 54.44/8.90 % (3049001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.44/8.90 % (3049001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.44/8.90 % (3049001)CaDiCaL version: 2.1.3 % 54.44/8.90 % (3049001)Termination reason: Refutation not found, incomplete strategy % 54.44/8.90 % (3049001)Time elapsed: 0.014 s % 54.44/8.90 % (3049001)Peak memory usage: 89 MB % 54.44/8.90 % (3049001)Instructions burned: 27 (million) % 54.44/8.90 % (3048998)Instruction limit reached! % 54.44/8.90 % (3048998)------------------------------ % 54.44/8.90 % (3048998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.44/8.90 % (3048998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.44/8.90 % (3048998)CaDiCaL version: 2.1.3 % 54.44/8.90 % (3048998)Termination reason: Instruction limit % 54.44/8.90 % (3048998)Termination phase: Saturation % 54.44/8.90 % (3048998)Time elapsed: 0.206 s % 54.44/8.90 % (3048998)Peak memory usage: 93 MB % 54.44/8.90 % (3048998)Instructions burned: 320 (million) % 54.44/8.90 % (3049003)dis-1011_128_sil=32000:random_seed=267454994:i=3706:ep=RST:av=off_2949 on theBenchmark for (2949ds/3706Mi) % 54.44/8.90 % (3049001)------------------------------ % 54.44/8.90 % (3049001)------------------------------ % 54.44/8.90 % (3049005)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2380107555:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2946 on theBenchmark for (2946ds/757Mi) % 54.44/8.90 % (3049005)Refutation not found, incomplete strategy % 54.44/8.90 % (3049005)------------------------------ % 54.44/8.90 % (3049005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.44/8.90 % (3049005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.44/8.90 % (3049005)CaDiCaL version: 2.1.3 % 54.44/8.90 % (3049005)Termination reason: Refutation not found, incomplete strategy % 54.44/8.90 % (3049005)Time elapsed: 0.001 s % 54.44/8.90 % (3049005)Peak memory usage: 86 MB % 54.44/8.90 % (3049005)Instructions burned: 1 (million) % 54.44/8.90 % (3049005)------------------------------ % 54.44/8.90 % (3049005)------------------------------ % 54.44/8.90 % (3049007)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3953949655:i=13913:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/13913Mi) % 56.53/9.17 [W928 14:13:07.581014956 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581051190 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581090407 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581103450 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581130451 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581142697 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581169174 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581181138 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581206998 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581219055 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581244415 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 [W928 14:13:07.581256301 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/9.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.53/9.17 % (3049007)Refutation not found, incomplete strategy % 56.53/9.17 % (3049007)------------------------------ % 56.53/9.17 % (3049007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.53/9.17 % (3049007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3049007)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3049007)Termination reason: Refutation not found, incomplete strategy % 72.39/11.47 % (3049007)Time elapsed: 0.549 s % 72.39/11.47 % (3049007)Peak memory usage: 126 MB % 72.39/11.47 % (3049007)Instructions burned: 828 (million) % 72.39/11.47 % (3049007)------------------------------ % 72.39/11.47 % (3049007)------------------------------ % 72.39/11.47 % (3049009)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1341154626:i=9925:aac=none_2933 on theBenchmark for (2933ds/9925Mi) % 72.39/11.47 % (3048982)Instruction limit reached! % 72.39/11.47 % (3048982)------------------------------ % 72.39/11.47 % (3048982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3048982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3048982)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3048982)Termination reason: Instruction limit % 72.39/11.47 % (3048982)Termination phase: Saturation % 72.39/11.47 % (3048982)Time elapsed: 3.533 s % 72.39/11.47 % (3048982)Peak memory usage: 167 MB % 72.39/11.47 % (3048982)Instructions burned: 6060 (million) % 72.39/11.47 % (3049003)Instruction limit reached! % 72.39/11.47 % (3049003)------------------------------ % 72.39/11.47 % (3049003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3049003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3049003)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3049003)Termination reason: Instruction limit % 72.39/11.47 % (3049003)Termination phase: Saturation % 72.39/11.47 % (3049003)Time elapsed: 1.920 s % 72.39/11.47 % (3049003)Peak memory usage: 106 MB % 72.39/11.47 % (3049003)Instructions burned: 3708 (million) % 72.39/11.47 % (3049011)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=112653930:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/2479Mi) % 72.39/11.47 % (3049011)Refutation not found, incomplete strategy % 72.39/11.47 % (3049011)------------------------------ % 72.39/11.47 % (3049011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3049011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3049011)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3049011)Termination reason: Refutation not found, incomplete strategy % 72.39/11.47 % (3049011)Time elapsed: 0.002 s % 72.39/11.47 % (3049011)Peak memory usage: 87 MB % 72.39/11.47 % (3049011)Instructions burned: 2 (million) % 72.39/11.47 % (3049012)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2601755574:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2928 on theBenchmark for (2928ds/440Mi) % 72.39/11.47 % (3049011)------------------------------ % 72.39/11.47 % (3049011)------------------------------ % 72.39/11.47 % (3049012)Instruction limit reached! % 72.39/11.47 % (3049012)------------------------------ % 72.39/11.47 % (3049012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3049012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3049012)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3049012)Termination reason: Instruction limit % 72.39/11.47 % (3049012)Termination phase: Saturation % 72.39/11.47 % (3049012)Time elapsed: 0.252 s % 72.39/11.47 % (3049012)Peak memory usage: 94 MB % 72.39/11.47 % (3049012)Instructions burned: 441 (million) % 72.39/11.47 % (3049009)Refutation not found, incomplete strategy % 72.39/11.47 % (3049009)------------------------------ % 72.39/11.47 % (3049009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3049009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3049009)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3049009)Termination reason: Refutation not found, incomplete strategy % 72.39/11.47 % (3049009)Time elapsed: 0.703 s % 72.39/11.47 % (3049009)Peak memory usage: 133 MB % 72.39/11.47 % (3049009)Instructions burned: 912 (million) % 72.39/11.47 % (3049015)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2082281107:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2925 on theBenchmark for (2925ds/11145Mi) % 72.39/11.47 % (3048984)Instruction limit reached! % 72.39/11.47 % (3048984)------------------------------ % 72.39/11.47 % (3048984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.39/11.47 % (3048984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.39/11.47 % (3048984)CaDiCaL version: 2.1.3 % 72.39/11.47 % (3048984)Termination reason: Instruction limit % 77.59/12.16 % (3048984)Termination phase: Saturation % 77.59/12.16 % (3048984)Time elapsed: 4.103 s % 77.59/12.16 % (3048984)Peak memory usage: 252 MB % 77.59/12.16 % (3048984)Instructions burned: 14156 (million) % 77.59/12.16 % (3049016)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=4242038654:cts=off:i=3034:av=off:er=known:fsd=on_2924 on theBenchmark for (2924ds/3034Mi) % 77.59/12.16 % (3049018)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=965959891:st=2:s2a=on:i=524:s2at=2:ss=axioms_2922 on theBenchmark for (2922ds/524Mi) % 77.59/12.16 % (3049018)Refutation not found, incomplete strategy % 77.59/12.16 % (3049018)------------------------------ % 77.59/12.16 % (3049018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.59/12.16 % (3049018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.59/12.16 % (3049018)CaDiCaL version: 2.1.3 % 77.59/12.16 % (3049018)Termination reason: Refutation not found, incomplete strategy % 77.59/12.16 % (3049018)Time elapsed: 0.001 s % 77.59/12.16 % (3049018)Peak memory usage: 87 MB % 77.59/12.16 % (3049018)Instructions burned: 3 (million) % 77.59/12.16 % (3049009)------------------------------ % 77.59/12.16 % (3049009)------------------------------ % 77.59/12.16 % (3049018)------------------------------ % 77.59/12.16 % (3049018)------------------------------ % 77.59/12.16 [W928 14:13:09.314808824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314855401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314895178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314907818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314932682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314944065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314969389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.314980822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.315018683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.59/12.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.59/12.16 [W928 14:13:09.315031826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.61/12.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.61/12.73 [W928 14:13:09.315059776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.61/12.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.61/12.73 [W928 14:13:09.315070623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.61/12.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.61/12.73 % (3049021)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3122431936:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2920 on theBenchmark for (2920ds/1016Mi) % 80.61/12.73 % (3049021)Refutation not found, incomplete strategy % 80.61/12.73 % (3049021)------------------------------ % 80.61/12.73 % (3049021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.61/12.73 % (3049021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.61/12.73 % (3049021)CaDiCaL version: 2.1.3 % 80.61/12.73 % (3049021)Termination reason: Refutation not found, incomplete strategy % 80.61/12.73 % (3049021)Time elapsed: 0.001 s % 80.61/12.73 % (3049021)Peak memory usage: 87 MB % 80.61/12.73 % (3049021)Instructions burned: 1 (million) % 80.61/12.73 % (3049022)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1212055592:i=14123:bd=preordered:ins=4_2920 on theBenchmark for (2920ds/14123Mi) % 80.61/12.73 % (3049015)Refutation not found, incomplete strategy % 80.61/12.73 % (3049015)------------------------------ % 80.61/12.73 % (3049015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.61/12.73 % (3049015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.61/12.73 % (3049015)CaDiCaL version: 2.1.3 % 80.61/12.73 % (3049015)Termination reason: Refutation not found, incomplete strategy % 80.61/12.73 % (3049015)Time elapsed: 0.561 s % 80.61/12.73 % (3049015)Peak memory usage: 126 MB % 80.61/12.73 % (3049015)Instructions burned: 833 (million) % 80.61/12.73 % (3049021)------------------------------ % 80.61/12.73 % (3049021)------------------------------ % 80.61/12.73 % (3049015)------------------------------ % 80.61/12.73 % (3049015)------------------------------ % 80.61/12.73 % (3049025)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3208440043:i=5781:kws=precedence:bd=all:rawr=on_2916 on theBenchmark for (2916ds/5781Mi) % 80.61/12.73 % (3049026)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=3045099502:i=2448:gtgl=5:bd=preordered:gtg=all_2915 on theBenchmark for (2915ds/2448Mi) % 80.61/12.73 % (3049016)Instruction limit reached! % 80.61/12.73 % (3049016)------------------------------ % 80.61/12.73 % (3049016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.61/12.73 % (3049016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.61/12.73 % (3049016)CaDiCaL version: 2.1.3 % 80.61/12.73 % (3049016)Termination reason: Instruction limit % 80.61/12.73 % (3049016)Termination phase: Saturation % 80.61/12.73 % (3049016)Time elapsed: 1.740 s % 80.61/12.73 % (3049016)Peak memory usage: 144 MB % 80.61/12.73 % (3049016)Instructions burned: 3035 (million) % 80.61/12.73 % (3049029)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2720536557:i=3223:kws=precedence:fgj=on:av=off_2905 on theBenchmark for (2905ds/3223Mi) % 80.61/12.73 % (3049026)Instruction limit reached! % 80.61/12.73 % (3049026)------------------------------ % 80.61/12.73 % (3049026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.61/12.73 % (3049026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.61/12.73 % (3049026)CaDiCaL version: 2.1.3 % 80.61/12.73 % (3049026)Termination reason: Instruction limit % 80.61/12.73 % (3049026)Termination phase: Saturation % 80.61/12.73 % (3049026)Time elapsed: 1.699 s % 80.61/12.73 % (3049026)Peak memory usage: 144 MB % 80.61/12.73 % (3049026)Instructions burned: 2449 (million) % 81.81/12.98 % (3049031)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3855398658:st=5.6:i=2033:sd=3:ss=axioms_2896 on theBenchmark for (2896ds/2033Mi) % 81.81/12.98 [W928 14:13:12.160132120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160180797 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160221817 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160233370 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160258777 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160269007 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160293661 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160303784 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160327378 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160337415 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160361051 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 [W928 14:13:12.160371041 register_special_ops.cpp:225] Warning: Creating a tensor from 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.81/12.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.98 % (3048997)Instruction limit reached! % 81.81/12.98 % (3048997)------------------------------ % 81.81/12.98 % (3048997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.65/13.16 % (3048997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.65/13.16 % (3048997)CaDiCaL version: 2.1.3 % 84.65/13.16 % (3048997)Termination reason: Instruction limit % 84.65/13.16 % (3048997)Termination phase: Saturation % 84.65/13.16 % (3048997)Time elapsed: 6.211 s % 84.65/13.16 % (3048997)Peak memory usage: 263 MB % 84.65/13.16 % (3048997)Instructions burned: 12114 (million) % 84.65/13.16 % (3049031)Refutation not found, incomplete strategy % 84.65/13.16 % (3049031)------------------------------ % 84.65/13.16 % (3049031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.65/13.16 % (3049031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.65/13.16 % (3049031)CaDiCaL version: 2.1.3 % 84.65/13.16 % (3049031)Termination reason: Refutation not found, incomplete strategy % 84.65/13.16 % (3049031)Time elapsed: 0.551 s % 84.65/13.16 % (3049031)Peak memory usage: 126 MB % 84.65/13.16 % (3049031)Instructions burned: 832 (million) % 84.65/13.16 % (3049033)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2572026899:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2889 on theBenchmark for (2889ds/2055Mi) % 84.65/13.16 % (3049031)------------------------------ % 84.65/13.16 % (3049031)------------------------------ % 84.65/13.16 % (3049025)Instruction limit reached! % 84.65/13.16 % (3049025)------------------------------ % 84.65/13.16 % (3049025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.65/13.16 % (3049025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.65/13.16 % (3049025)CaDiCaL version: 2.1.3 % 84.65/13.16 % (3049025)Termination reason: Instruction limit % 84.65/13.16 % (3049025)Termination phase: Saturation % 84.65/13.16 % (3049025)Time elapsed: 2.797 s % 84.65/13.16 % (3049025)Peak memory usage: 101 MB % 84.65/13.16 % (3049025)Instructions burned: 5783 (million) % 84.65/13.16 % (3049035)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=2543995884:i=21611:sd=3:ss=axioms_2887 on theBenchmark for (2887ds/21611Mi) % 84.65/13.16 % (3049036)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=275220484:i=4835:sd=13:ss=axioms:sgt=23_2887 on theBenchmark for (2887ds/4835Mi) % 84.65/13.16 % (3049036)Refutation not found, incomplete strategy % 84.65/13.16 % (3049036)------------------------------ % 84.65/13.16 % (3049036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.65/13.16 % (3049036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.65/13.16 % (3049036)CaDiCaL version: 2.1.3 % 84.65/13.16 % (3049036)Termination reason: Refutation not found, incomplete strategy % 84.65/13.16 % (3049036)Time elapsed: 0.001 s % 84.65/13.16 % (3049036)Peak memory usage: 87 MB % 84.65/13.16 % (3049036)Instructions burned: 1 (million) % 84.65/13.16 [W928 14:13:13.878497795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.65/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.65/13.16 [W928 14:13:13.878530495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.65/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.65/13.16 [W928 14:13:13.878571439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.65/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.65/13.16 [W928 14:13:13.878584122 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.65/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.65/13.16 [W928 14:13:13.878610646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.65/13.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878621879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878655193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878666250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878690633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878700587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878724370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.878734484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 % (3049029)Instruction limit reached! % 87.91/13.97 % (3049029)------------------------------ % 87.91/13.97 % (3049029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.91/13.97 % (3049029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.91/13.97 % (3049029)CaDiCaL version: 2.1.3 % 87.91/13.97 % (3049029)Termination reason: Instruction limit % 87.91/13.97 % (3049029)Termination phase: Saturation % 87.91/13.97 % (3049029)Time elapsed: 2.022 s % 87.91/13.97 % (3049029)Peak memory usage: 146 MB % 87.91/13.97 % (3049029)Instructions burned: 3223 (million) % 87.91/13.97 % (3049036)------------------------------ % 87.91/13.97 % (3049036)------------------------------ % 87.91/13.97 % (3049033)Refutation not found, incomplete strategy % 87.91/13.97 % (3049033)------------------------------ % 87.91/13.97 % (3049033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.91/13.97 % (3049033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.91/13.97 % (3049033)CaDiCaL version: 2.1.3 % 87.91/13.97 % (3049033)Termination reason: Refutation not found, incomplete strategy % 87.91/13.97 % (3049033)Time elapsed: 0.557 s % 87.91/13.97 % (3049033)Peak memory usage: 127 MB % 87.91/13.97 % (3049033)Instructions burned: 835 (million) % 87.91/13.97 [W928 14:13:13.124917085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.124964036 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 87.91/13.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 87.91/13.97 [W928 14:13:13.125017973 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125036589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125073553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125084997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125110720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125122030 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125146837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125158077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125182951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 [W928 14:13:13.125194231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.56/14.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.56/14.74 % (3049039)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=1272795195:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2883 on theBenchmark for (2883ds/797Mi) % 94.56/14.74 % (3049040)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3421003926:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2882 on theBenchmark for (2882ds/2326Mi) % 94.56/14.74 % (3049040)Refutation not found, incomplete strategy % 94.56/14.74 % (3049040)------------------------------ % 94.56/14.74 % (3049040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.56/14.74 % (3049040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.56/14.74 % (3049040)CaDiCaL version: 2.1.3 % 94.56/14.74 % (3049040)Termination reason: Refutation not found, incomplete strategy % 94.56/14.74 % (3049040)Time elapsed: 0.022 s % 94.56/14.74 % (3049040)Peak memory usage: 89 MB % 94.56/14.74 % (3049040)Instructions burned: 37 (million) % 94.56/14.74 % (3049033)------------------------------ % 94.56/14.74 % (3049033)------------------------------ % 105.16/16.13 % (3049035)Refutation not found, incomplete strategy % 105.16/16.13 % (3049035)------------------------------ % 105.16/16.13 % (3049035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/16.13 % (3049035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/16.13 % (3049035)CaDiCaL version: 2.1.3 % 105.16/16.13 % (3049035)Termination reason: Refutation not found, incomplete strategy % 105.16/16.13 % (3049035)Time elapsed: 0.560 s % 105.16/16.13 % (3049035)Peak memory usage: 126 MB % 105.16/16.13 % (3049035)Instructions burned: 832 (million) % 105.16/16.13 % (3049040)------------------------------ % 105.16/16.13 % (3049040)------------------------------ % 105.16/16.13 % (3049043)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2090740664:i=6038:nm=6_2880 on theBenchmark for (2880ds/6038Mi) % 105.16/16.13 % (3049035)------------------------------ % 105.16/16.13 % (3049035)------------------------------ % 105.16/16.13 % (3049039)Instruction limit reached! % 105.16/16.13 % (3049039)------------------------------ % 105.16/16.13 % (3049039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/16.13 % (3049039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/16.13 % (3049039)CaDiCaL version: 2.1.3 % 105.16/16.13 % (3049039)Termination reason: Instruction limit % 105.16/16.13 % (3049039)Termination phase: Saturation % 105.16/16.13 % (3049039)Time elapsed: 0.395 s % 105.16/16.13 % (3049039)Peak memory usage: 92 MB % 105.16/16.13 % (3049039)Instructions burned: 798 (million) % 105.16/16.13 % (3049044)lrs+10_1_sil=32000:sp=occurrence:random_seed=249326151:st=2:i=33334:sd=3:ss=included:sgt=32_2878 on theBenchmark for (2878ds/33334Mi) % 105.16/16.13 % (3049047)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=1912040562:i=8327:s2at=5:bd=preordered_2877 on theBenchmark for (2877ds/8327Mi) % 105.16/16.13 % (3049046)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1799898898:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2877 on theBenchmark for (2877ds/1008Mi) % 105.16/16.13 % (3049046)Refutation not found, incomplete strategy % 105.16/16.13 % (3049046)------------------------------ % 105.16/16.13 % (3049046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/16.13 % (3049046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/16.13 % (3049046)CaDiCaL version: 2.1.3 % 105.16/16.13 % (3049046)Termination reason: Refutation not found, incomplete strategy % 105.16/16.13 % (3049046)Time elapsed: 0.002 s % 105.16/16.13 % (3049046)Peak memory usage: 86 MB % 105.16/16.13 % (3049046)Instructions burned: 2 (million) % 105.16/16.13 % (3049022)Instruction limit reached! % 105.16/16.13 % (3049022)------------------------------ % 105.16/16.13 % (3049022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/16.13 % (3049022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/16.13 % (3049022)CaDiCaL version: 2.1.3 % 105.16/16.13 % (3049022)Termination reason: Instruction limit % 105.16/16.13 % (3049022)Termination phase: Saturation % 105.16/16.13 % (3049022)Time elapsed: 4.321 s % 105.16/16.13 % (3049022)Peak memory usage: 188 MB % 105.16/16.13 % (3049022)Instructions burned: 14123 (million) % 105.16/16.13 % (3049051)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=2884620634:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2875 on theBenchmark for (2875ds/1083Mi) % 105.16/16.13 % (3049046)------------------------------ % 105.16/16.13 % (3049046)------------------------------ % 105.16/16.13 % (3049043)Refutation not found, incomplete strategy % 105.16/16.13 % (3049043)------------------------------ % 105.16/16.13 % (3049043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.16/16.13 % (3049043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.16/16.13 % (3049043)CaDiCaL version: 2.1.3 % 105.16/16.13 % (3049043)Termination reason: Refutation not found, incomplete strategy % 105.16/16.13 % (3049043)Time elapsed: 0.615 s % 105.16/16.13 % (3049043)Peak memory usage: 133 MB % 105.16/16.13 % (3049043)Instructions burned: 913 (million) % 105.16/16.13 % (3049053)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=140597159:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2873 on theBenchmark for (2873ds/1084Mi) % 105.16/16.13 % (3049053)Refutation not found, incomplete strategy % 108.48/16.54 % (3049053)------------------------------ % 108.48/16.54 % (3049053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.48/16.54 % (3049053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.48/16.54 % (3049053)CaDiCaL version: 2.1.3 % 108.48/16.54 % (3049053)Termination reason: Refutation not found, incomplete strategy % 108.48/16.54 % (3049053)Time elapsed: 0.001 s % 108.48/16.54 % (3049053)Peak memory usage: 86 MB % 108.48/16.54 % (3049053)Instructions burned: 1 (million) % 108.48/16.54 % (3049051)Instruction limit reached! % 108.48/16.54 % (3049051)------------------------------ % 108.48/16.54 % (3049051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.48/16.54 % (3049051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.48/16.54 % (3049051)CaDiCaL version: 2.1.3 % 108.48/16.54 % (3049051)Termination reason: Instruction limit % 108.48/16.54 % (3049051)Termination phase: Saturation % 108.48/16.54 % (3049051)Time elapsed: 0.342 s % 108.48/16.54 % (3049051)Peak memory usage: 104 MB % 108.48/16.54 % (3049051)Instructions burned: 1087 (million) % 108.48/16.54 % (3049043)------------------------------ % 108.48/16.54 % (3049043)------------------------------ % 108.48/16.54 % (3049055)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2967235797:i=6995:s2at=5:gtg=all_2871 on theBenchmark for (2871ds/6995Mi) % 108.48/16.54 % (3049053)------------------------------ % 108.48/16.54 % (3049053)------------------------------ % 108.48/16.54 % (3049057)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2604548073:st=2:i=6225:sd=15:ss=axioms_2869 on theBenchmark for (2869ds/6225Mi) % 108.48/16.54 % (3049058)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=4004948497:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2869 on theBenchmark for (2869ds/3372Mi) % 108.48/16.54 % (3049057)Refutation not found, incomplete strategy % 108.48/16.54 % (3049057)------------------------------ % 108.48/16.54 % (3049057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.48/16.54 % (3049057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.48/16.54 % (3049057)CaDiCaL version: 2.1.3 % 108.48/16.54 % (3049057)Termination reason: Refutation not found, incomplete strategy % 108.48/16.54 % (3049057)Time elapsed: 0.001 s % 108.48/16.54 % (3049057)Peak memory usage: 87 MB % 108.48/16.54 % (3049057)Instructions burned: 1 (million) % 108.48/16.54 % (3049057)------------------------------ % 108.48/16.54 % (3049057)------------------------------ % 108.48/16.54 [W928 14:13:15.887497051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.54 [W928 14:13:15.887533525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.54 [W928 14:13:15.887572265 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.54 [W928 14:13:15.887584142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.54 [W928 14:13:15.887611609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.48/16.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.48/16.54 [W928 14:13:15.887623909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887650432 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887661326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887684843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887705673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887731343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 [W928 14:13:15.887742157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/17.09 % (3049061)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3535052960:st=2.3:i=26457:sd=10:ss=included:sgt=8_2865 on theBenchmark for (2865ds/26457Mi) % 112.26/17.09 % (3049058)Refutation not found, incomplete strategy % 112.26/17.09 % (3049058)------------------------------ % 112.26/17.09 % (3049058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.26/17.09 % (3049058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/17.09 % (3049058)CaDiCaL version: 2.1.3 % 112.26/17.09 % (3049058)Termination reason: Refutation not found, incomplete strategy % 112.26/17.09 % (3049058)Time elapsed: 0.553 s % 112.26/17.09 % (3049058)Peak memory usage: 126 MB % 112.26/17.09 % (3049058)Instructions burned: 835 (million) % 112.26/17.09 % (3049058)------------------------------ % 112.26/17.09 % (3049058)------------------------------ % 112.26/17.09 % (3049063)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=82835801:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2860 on theBenchmark for (2860ds/13494Mi) % 112.26/17.09 % (3049061)Refutation not found, incomplete strategy % 112.26/17.09 % (3049061)------------------------------ % 112.26/17.09 % (3049061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.26/17.09 % (3049061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/17.09 % (3049061)CaDiCaL version: 2.1.3 % 112.26/17.09 % (3049061)Termination reason: Refutation not found, incomplete strategy % 112.26/17.09 % (3049061)Time elapsed: 0.591 s % 112.26/17.09 % (3049061)Peak memory usage: 130 MB % 112.26/17.09 % (3049061)Instructions burned: 912 (million) % 112.26/17.09 % (3049061)------------------------------ % 112.26/17.09 % (3049061)------------------------------ % 112.26/17.09 % (3049065)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=2215099931:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2855 on theBenchmark for (2855ds/2503Mi) % 112.26/17.09 [W928 14:13:16.270675563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270710997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270758627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270782671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270810741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270821744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270847101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270858208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270883225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270894205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270918598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 [W928 14:13:16.270929545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 131.44/19.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.44/19.89 % (3049065)Refutation not found, incomplete strategy % 131.44/19.89 % (3049065)------------------------------ % 131.44/19.89 % (3049065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.44/19.89 % (3049065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.44/19.89 % (3049065)CaDiCaL version: 2.1.3 % 131.44/19.89 % (3049065)Termination reason: Refutation not found, incomplete strategy % 131.44/19.89 % (3049065)Time elapsed: 0.548 s % 131.44/19.89 % (3049065)Peak memory usage: 126 MB % 131.44/19.89 % (3049065)Instructions burned: 832 (million) % 131.44/19.89 % (3049065)------------------------------ % 138.52/20.87 % (3049065)------------------------------ % 138.52/20.87 % (3049055)Instruction limit reached! % 138.52/20.87 % (3049055)------------------------------ % 138.52/20.87 % (3049055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.52/20.87 % (3049055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.52/20.87 % (3049055)CaDiCaL version: 2.1.3 % 138.52/20.87 % (3049055)Termination reason: Instruction limit % 138.52/20.87 % (3049055)Termination phase: Saturation % 138.52/20.87 % (3049055)Time elapsed: 2.498 s % 138.52/20.87 % (3049055)Peak memory usage: 184 MB % 138.52/20.87 % (3049055)Instructions burned: 6996 (million) % 138.52/20.87 % (3049067)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3273093735:i=2559:sd=1:ep=RSTC:ss=axioms_2846 on theBenchmark for (2846ds/2559Mi) % 138.52/20.87 % (3049069)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=178669036:i=30753:av=off:ss=included_2844 on theBenchmark for (2844ds/30753Mi) % 138.52/20.87 [W928 14:13:17.232706441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232746622 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232785132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232797629 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232825092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232836599 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232862879 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232874439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232899416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232910639 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.52/20.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.52/20.87 [W928 14:13:17.232937173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.56/21.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.56/21.83 [W928 14:13:17.232948490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.56/21.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.56/21.83 % (3049067)Refutation not found, incomplete strategy % 145.56/21.83 % (3049067)------------------------------ % 145.56/21.83 % (3049067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.56/21.83 % (3049067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.56/21.83 % (3049067)CaDiCaL version: 2.1.3 % 145.56/21.83 % (3049067)Termination reason: Refutation not found, incomplete strategy % 145.56/21.83 % (3049067)Time elapsed: 0.550 s % 145.56/21.83 % (3049067)Peak memory usage: 126 MB % 145.56/21.83 % (3049067)Instructions burned: 828 (million) % 145.56/21.83 % (3049067)------------------------------ % 145.56/21.83 % (3049067)------------------------------ % 145.56/21.83 % (3049071)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1098736805:i=26473:ep=RSTC_2836 on theBenchmark for (2836ds/26473Mi) % 145.56/21.83 % (3049047)Instruction limit reached! % 145.56/21.83 % (3049047)------------------------------ % 145.56/21.83 % (3049047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.56/21.83 % (3049047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.56/21.83 % (3049047)CaDiCaL version: 2.1.3 % 145.56/21.83 % (3049047)Termination reason: Instruction limit % 145.56/21.83 % (3049047)Termination phase: Saturation % 145.56/21.83 % (3049047)Time elapsed: 4.761 s % 145.56/21.83 % (3049047)Peak memory usage: 190 MB % 145.56/21.83 % (3049047)Instructions burned: 8327 (million) % 145.56/21.83 % (3049073)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=3182875685:cts=off:i=2759:kws=inv_arity:fgj=on_2828 on theBenchmark for (2828ds/2759Mi) % 145.56/21.83 % (3049073)Refutation not found, incomplete strategy % 145.56/21.83 % (3049073)------------------------------ % 145.56/21.83 % (3049073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.56/21.83 % (3049073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.56/21.83 % (3049073)CaDiCaL version: 2.1.3 % 145.56/21.83 % (3049073)Termination reason: Refutation not found, incomplete strategy % 145.56/21.83 % (3049073)Time elapsed: 0.604 s % 145.56/21.83 % (3049073)Peak memory usage: 130 MB % 145.56/21.83 % (3049073)Instructions burned: 923 (million) % 145.56/21.83 % (3049073)------------------------------ % 145.56/21.83 % (3049073)------------------------------ % 145.56/21.83 % (3049075)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=275898967:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2818 on theBenchmark for (2818ds/5665Mi) % 145.56/21.83 [W928 14:13:20.038667895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.56/21.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.56/21.83 [W928 14:13:20.038708035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.56/21.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.56/21.83 [W928 14:13:20.038749106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.56/21.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.56/21.83 [W928 14:13:20.038762826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038790919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038801809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038826763 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038837523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038861300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038871680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038896040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:20.038906223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 % (3049075)Refutation not found, incomplete strategy % 146.17/22.01 % (3049075)------------------------------ % 146.17/22.01 % (3049075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.17/22.01 % (3049075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.17/22.01 % (3049075)CaDiCaL version: 2.1.3 % 146.17/22.01 % (3049075)Termination reason: Refutation not found, incomplete strategy % 146.17/22.01 % (3049075)Time elapsed: 0.553 s % 146.17/22.01 % (3049075)Peak memory usage: 127 MB % 146.17/22.01 % (3049075)Instructions burned: 833 (million) % 146.17/22.01 % (3049075)------------------------------ % 146.17/22.01 % (3049075)------------------------------ % 146.17/22.01 % (3049077)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=1993159179:i=1532:ep=RS:ss=axioms_2808 on theBenchmark for (2808ds/1532Mi) % 146.17/22.01 [W928 14:13:21.015457112 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:21.015491182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.17/22.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.17/22.01 [W928 14:13:21.015531609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015543716 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015569782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015580346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015606326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015616683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015641210 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015651546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015676153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 [W928 14:13:21.015686623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.48/22.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.48/22.80 % (3049077)Refutation not found, incomplete strategy % 151.48/22.80 % (3049077)------------------------------ % 151.48/22.80 % (3049077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.48/22.80 % (3049077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.48/22.80 % (3049077)CaDiCaL version: 2.1.3 % 151.48/22.80 % (3049077)Termination reason: Refutation not found, incomplete strategy % 151.48/22.80 % (3049077)Time elapsed: 0.557 s % 151.48/22.80 % (3049077)Peak memory usage: 127 MB % 151.48/22.80 % (3049077)Instructions burned: 832 (million) % 151.48/22.80 % (3049077)------------------------------ % 151.48/22.80 % (3049077)------------------------------ % 151.48/22.80 % (3049079)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3150833053:i=1565:sd=2:ss=axioms:sgt=32_2798 on theBenchmark for (2798ds/1565Mi) % 151.48/22.80 [W928 14:13:22.976126796 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976162033 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976201637 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976213563 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976238310 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976249077 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976273220 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976284060 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976308161 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976319111 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976347911 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 [W928 14:13:22.976358754 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/23.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.24/23.87 % (3049079)Refutation not found, incomplete strategy % 159.24/23.87 % (3049079)------------------------------ % 159.24/23.87 % (3049079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.24/23.87 % (3049079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.24/23.87 % (3049079)CaDiCaL version: 2.1.3 % 159.24/23.87 % (3049079)Termination reason: Refutation not found, incomplete strategy % 159.24/23.87 % (3049079)Time elapsed: 0.553 s % 159.24/23.87 % (3049079)Peak memory usage: 126 MB % 159.24/23.87 % (3049079)Instructions burned: 832 (million) % 164.24/24.49 % (3049063)Instruction limit reached! % 164.24/24.49 % (3049063)------------------------------ % 164.24/24.49 % (3049063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.24/24.49 % (3049063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.24/24.49 % (3049063)CaDiCaL version: 2.1.3 % 164.24/24.49 % (3049063)Termination reason: Instruction limit % 164.24/24.49 % (3049063)Termination phase: Saturation % 164.24/24.49 % (3049063)Time elapsed: 6.792 s % 164.24/24.49 % (3049063)Peak memory usage: 252 MB % 164.24/24.49 % (3049063)Instructions burned: 13496 (million) % 164.24/24.49 % (3049079)------------------------------ % 164.24/24.49 % (3049079)------------------------------ % 164.24/24.49 % (3049081)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=505130987:i=1572:fgj=on:gsp=on_2790 on theBenchmark for (2790ds/1572Mi) % 164.24/24.49 % (3049082)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3017822947:i=6052:sd=4:ss=axioms:sgt=24_2789 on theBenchmark for (2789ds/6052Mi) % 164.24/24.49 [W928 14:13:23.941572927 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941606350 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941644437 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941656244 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941681367 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941693211 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941717734 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941728954 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941754251 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 164.24/24.49 [W928 14:13:23.941765641 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/24.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:23.941790972 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:23.941801392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 % (3049082)Refutation not found, incomplete strategy % 166.41/25.00 % (3049082)------------------------------ % 166.41/25.00 % (3049082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.41/25.00 % (3049082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/25.00 % (3049082)CaDiCaL version: 2.1.3 % 166.41/25.00 % (3049082)Termination reason: Refutation not found, incomplete strategy % 166.41/25.00 % (3049082)Time elapsed: 0.551 s % 166.41/25.00 % (3049082)Peak memory usage: 126 MB % 166.41/25.00 % (3049082)Instructions burned: 832 (million) % 166.41/25.00 % (3049082)------------------------------ % 166.41/25.00 % (3049082)------------------------------ % 166.41/25.00 % (3049081)Instruction limit reached! % 166.41/25.00 % (3049081)------------------------------ % 166.41/25.00 % (3049081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.41/25.00 % (3049081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/25.00 % (3049081)CaDiCaL version: 2.1.3 % 166.41/25.00 % (3049081)Termination reason: Instruction limit % 166.41/25.00 % (3049081)Termination phase: Saturation % 166.41/25.00 % (3049081)Time elapsed: 1.026 s % 166.41/25.00 % (3049081)Peak memory usage: 135 MB % 166.41/25.00 % (3049081)Instructions burned: 1573 (million) % 166.41/25.00 % (3049085)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=3817032279:i=3500:sd=1:bd=preordered:sup=off:ss=included_2779 on theBenchmark for (2779ds/3500Mi) % 166.41/25.00 % (3049086)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=2498661651:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2778 on theBenchmark for (2778ds/1842Mi) % 166.41/25.00 [W928 14:13:24.018795331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:24.018831861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:24.018870214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:24.018883325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:24.018909205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.41/25.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.41/25.00 [W928 14:13:24.018920582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.018946715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.018957098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.018981772 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.018992295 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.019029842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 [W928 14:13:24.019041346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.22/26.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.22/26.88 % (3049085)Refutation not found, incomplete strategy % 181.22/26.88 % (3049085)------------------------------ % 181.22/26.88 % (3049085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.22/26.88 % (3049085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.88 % (3049085)CaDiCaL version: 2.1.3 % 181.22/26.88 % (3049085)Termination reason: Refutation not found, incomplete strategy % 181.22/26.88 % (3049085)Time elapsed: 0.603 s % 181.22/26.88 % (3049085)Peak memory usage: 134 MB % 181.22/26.88 % (3049085)Instructions burned: 914 (million) % 181.22/26.88 % (3049086)Refutation not found, incomplete strategy % 181.22/26.88 % (3049086)------------------------------ % 181.22/26.88 % (3049086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.22/26.88 % (3049086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.88 % (3049086)CaDiCaL version: 2.1.3 % 181.22/26.88 % (3049086)Termination reason: Refutation not found, incomplete strategy % 181.22/26.88 % (3049086)Time elapsed: 0.549 s % 181.22/26.88 % (3049086)Peak memory usage: 127 MB % 181.22/26.88 % (3049086)Instructions burned: 832 (million) % 181.22/26.88 % (3049085)------------------------------ % 181.22/26.88 % (3049085)------------------------------ % 181.22/26.88 % (3049086)------------------------------ % 181.22/26.88 % (3049086)------------------------------ % 181.22/26.88 % (3049089)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3252700332:i=66096:add=on_2769 on theBenchmark for (2769ds/66096Mi) % 181.22/26.88 % (3049090)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2330686988:i=1884:sd=1:nm=60:ss=axioms_2768 on theBenchmark for (2768ds/1884Mi) % 181.22/26.88 % (3049069)Instruction limit reached! % 181.22/26.88 % (3049069)------------------------------ % 181.22/26.88 % (3049069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.22/26.88 % (3049069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.22/26.88 % (3049069)CaDiCaL version: 2.1.3 % 181.22/26.88 % (3049069)Termination reason: Instruction limit % 181.22/26.88 % (3049069)Termination phase: Saturation % 181.22/26.88 % (3049069)Time elapsed: 7.664 s % 181.22/26.88 % (3049069)Peak memory usage: 219 MB % 181.22/26.88 % (3049069)Instructions burned: 30753 (million) % 195.79/28.94 % (3049093)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3470207298:cts=off:i=5469:bs=on:fsr=off_2766 on theBenchmark for (2766ds/5469Mi) % 195.79/28.94 [W928 14:13:25.973792859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973837699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973876069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973888296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973912993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973938176 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973964980 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973975880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.973999597 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.974024827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.974051194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 [W928 14:13:25.974063281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 195.79/28.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 195.79/28.94 % (3049090)Refutation not found, incomplete strategy % 195.79/28.94 % (3049090)------------------------------ % 195.79/28.94 % (3049090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.79/28.94 % (3049090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.98/29.94 % (3049090)CaDiCaL version: 2.1.3 % 202.98/29.94 % (3049090)Termination reason: Refutation not found, incomplete strategy % 202.98/29.94 % (3049090)Time elapsed: 0.551 s % 202.98/29.94 % (3049090)Peak memory usage: 126 MB % 202.98/29.94 % (3049090)Instructions burned: 831 (million) % 202.98/29.94 % (3049090)------------------------------ % 202.98/29.94 % (3049090)------------------------------ % 202.98/29.94 % (3049095)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=2578050661:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2759 on theBenchmark for (2759ds/2037Mi) % 202.98/29.94 % (3049093)Instruction limit reached! % 202.98/29.94 % (3049093)------------------------------ % 202.98/29.94 % (3049093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.98/29.94 % (3049093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.98/29.94 % (3049093)CaDiCaL version: 2.1.3 % 202.98/29.94 % (3049093)Termination reason: Instruction limit % 202.98/29.94 % (3049093)Termination phase: Saturation % 202.98/29.94 % (3049093)Time elapsed: 1.920 s % 202.98/29.94 % (3049093)Peak memory usage: 117 MB % 202.98/29.94 % (3049093)Instructions burned: 5469 (million) % 202.98/29.94 % (3049097)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3494887118:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2746 on theBenchmark for (2746ds/2110Mi) % 202.98/29.94 % (3049095)Instruction limit reached! % 202.98/29.94 % (3049095)------------------------------ % 202.98/29.94 % (3049095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.98/29.94 % (3049095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.98/29.94 % (3049095)CaDiCaL version: 2.1.3 % 202.98/29.94 % (3049095)Termination reason: Instruction limit % 202.98/29.94 % (3049095)Termination phase: Saturation % 202.98/29.94 % (3049095)Time elapsed: 1.306 s % 202.98/29.94 % (3049095)Peak memory usage: 140 MB % 202.98/29.94 % (3049095)Instructions burned: 2038 (million) % 202.98/29.94 [W928 14:13:27.027784005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027823593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027845111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027851203 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027864012 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027869597 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.98/29.94 [W928 14:13:27.027889022 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 202.98/29.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 [W928 14:13:27.027895549 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.08/32.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 [W928 14:13:27.027908433 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.08/32.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 [W928 14:13:27.027913923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.08/32.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 [W928 14:13:27.027926575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.08/32.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 [W928 14:13:27.027932002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 224.08/32.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 224.08/32.94 % (3049099)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=719527326:i=2430:add=off:aac=none:nm=16_2744 on theBenchmark for (2744ds/2430Mi) % 224.08/32.94 % (3049097)Refutation not found, incomplete strategy % 224.08/32.94 % (3049097)------------------------------ % 224.08/32.94 % (3049097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.08/32.94 % (3049097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.08/32.94 % (3049097)CaDiCaL version: 2.1.3 % 224.08/32.94 % (3049097)Termination reason: Refutation not found, incomplete strategy % 224.08/32.94 % (3049097)Time elapsed: 0.320 s % 224.08/32.94 % (3049097)Peak memory usage: 126 MB % 224.08/32.94 % (3049097)Instructions burned: 832 (million) % 224.08/32.94 % (3049097)------------------------------ % 224.08/32.94 % (3049097)------------------------------ % 224.08/32.94 % (3049101)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=3627070990:cond=fast:i=4891_2740 on theBenchmark for (2740ds/4891Mi) % 224.08/32.94 % (3049099)Instruction limit reached! % 224.08/32.94 % (3049099)------------------------------ % 224.08/32.94 % (3049099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.08/32.94 % (3049099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.08/32.94 % (3049099)CaDiCaL version: 2.1.3 % 224.08/32.94 % (3049099)Termination reason: Instruction limit % 224.08/32.94 % (3049099)Termination phase: Saturation % 224.08/32.94 % (3049099)Time elapsed: 1.466 s % 224.08/32.94 % (3049099)Peak memory usage: 142 MB % 224.08/32.94 % (3049099)Instructions burned: 2431 (million) % 224.08/32.94 % (3049103)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=2821618208:st=2:i=14845:sd=2:ss=included:fsd=on_2727 on theBenchmark for (2727ds/14845Mi) % 224.08/32.94 % (3049101)Instruction limit reached! % 224.08/32.94 % (3049101)------------------------------ % 224.08/32.94 % (3049101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.08/32.94 % (3049101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.08/32.94 % (3049101)CaDiCaL version: 2.1.3 % 224.08/32.94 % (3049101)Termination reason: Instruction limit % 224.08/32.94 % (3049101)Termination phase: Saturation % 224.08/32.94 % (3049101)Time elapsed: 1.531 s % 224.08/32.94 % (3049101)Peak memory usage: 155 MB % 224.08/32.94 % (3049101)Instructions burned: 4893 (million) % 224.08/32.94 % (3049105)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2951549429:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2723 on theBenchmark for (2723ds/7534Mi) % 228.48/33.60 % (3049103)Refutation not found, incomplete strategy % 228.48/33.60 % (3049103)------------------------------ % 228.48/33.60 % (3049103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.60 % (3049103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.60 % (3049103)CaDiCaL version: 2.1.3 % 228.48/33.60 % (3049103)Termination reason: Refutation not found, incomplete strategy % 228.48/33.60 % (3049103)Time elapsed: 0.603 s % 228.48/33.60 % (3049103)Peak memory usage: 134 MB % 228.48/33.60 % (3049103)Instructions burned: 907 (million) % 228.48/33.60 % (3049103)------------------------------ % 228.48/33.60 % (3049103)------------------------------ % 228.48/33.60 % (3049107)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=3129759533:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2717 on theBenchmark for (2717ds/10353Mi) % 228.48/33.60 [W928 14:13:30.083733090 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083782240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083819737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083833107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083858474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083871578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083898435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083910478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083935915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083947738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.60 [W928 14:13:30.083972098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.89/33.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.89/33.73 [W928 14:13:30.083983102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.89/33.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.89/33.73 % (3049107)Refutation not found, incomplete strategy % 228.89/33.73 % (3049107)------------------------------ % 228.89/33.73 % (3049107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.89/33.73 % (3049107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.89/33.73 % (3049107)CaDiCaL version: 2.1.3 % 228.89/33.73 % (3049107)Termination reason: Refutation not found, incomplete strategy % 228.89/33.73 % (3049107)Time elapsed: 0.551 s % 228.89/33.73 % (3049107)Peak memory usage: 126 MB % 228.89/33.73 % (3049107)Instructions burned: 832 (million) % 228.89/33.73 % (3049107)------------------------------ % 228.89/33.73 % (3049107)------------------------------ % 228.89/33.73 % (3049109)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2062492936:i=7860_2708 on theBenchmark for (2708ds/7860Mi) % 228.89/33.73 % (3049109)Refutation not found, incomplete strategy % 228.89/33.73 % (3049109)------------------------------ % 228.89/33.73 % (3049109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.89/33.73 % (3049109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.89/33.73 % (3049109)CaDiCaL version: 2.1.3 % 228.89/33.73 % (3049109)Termination reason: Refutation not found, incomplete strategy % 228.89/33.73 % (3049109)Time elapsed: 0.015 s % 228.89/33.73 % (3049109)Peak memory usage: 89 MB % 228.89/33.73 % (3049109)Instructions burned: 28 (million) % 228.89/33.73 % (3049109)------------------------------ % 228.89/33.73 % (3049109)------------------------------ % 228.89/33.73 % (3049111)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=242941745:i=7896:sd=2:bs=on:ss=included:sgt=20_2703 on theBenchmark for (2703ds/7896Mi) % 228.89/33.73 % (3049105)Instruction limit reached! % 228.89/33.73 % (3049105)------------------------------ % 228.89/33.73 % (3049105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.89/33.73 % (3049105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.89/33.73 % (3049105)CaDiCaL version: 2.1.3 % 228.89/33.73 % (3049105)Termination reason: Instruction limit % 228.89/33.73 % (3049105)Termination phase: Saturation % 228.89/33.73 % (3049105)Time elapsed: 2.248 s % 228.89/33.73 % (3049105)Peak memory usage: 174 MB % 228.89/33.73 % (3049105)Instructions burned: 7536 (million) % 228.89/33.73 % (3049113)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=666903911:i=5812:gtgl=2:gtg=all_2699 on theBenchmark for (2699ds/5812Mi) % 228.89/33.73 % (3049044)Instruction limit reached! % 228.89/33.73 % (3049044)------------------------------ % 228.89/33.73 % (3049044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.89/33.73 % (3049044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.89/33.73 % (3049044)CaDiCaL version: 2.1.3 % 228.89/33.73 % (3049044)Termination reason: Instruction limit % 228.89/33.73 % (3049044)Termination phase: Saturation % 228.89/33.73 % (3049044)Time elapsed: 18.689 s % 228.89/33.73 % (3049044)Peak memory usage: 253 MB % 228.89/33.73 % (3049044)Instructions burned: 33336 (million) % 228.89/33.73 % (3049115)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=1516687795:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2689 on theBenchmark for (2689ds/2965Mi) % 228.89/33.73 % (3049115)Refutation not found, incomplete strategy % 228.89/33.73 % (3049115)------------------------------ % 228.89/33.73 % (3049115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.89/33.73 % (3049115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.89/33.73 % (3049115)CaDiCaL version: 2.1.3 % 228.89/33.73 % (3049115)Termination reason: Refutation not found, incomplete strategy % 228.89/33.73 % (3049115)Time elapsed: 0.592 s % 228.89/33.73 % (3049115)Peak memory usage: 130 MB % 234.44/34.38 % (3049115)Instructions burned: 913 (million) % 234.44/34.38 % (3049071)Instruction limit reached! % 234.44/34.38 % (3049071)------------------------------ % 234.44/34.38 % (3049071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.44/34.38 % (3049071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.44/34.38 % (3049071)CaDiCaL version: 2.1.3 % 234.44/34.38 % (3049071)Termination reason: Instruction limit % 234.44/34.38 % (3049071)Termination phase: Saturation % 234.44/34.38 % (3049071)Time elapsed: 15.320 s % 234.44/34.38 % (3049071)Peak memory usage: 514 MB % 234.44/34.38 % (3049071)Instructions burned: 26473 (million) % 234.44/34.38 % (3049115)------------------------------ % 234.44/34.38 % (3049115)------------------------------ % 234.44/34.38 % (3049117)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=3395688100:i=2967:kws=precedence:bd=preordered:av=off_2681 on theBenchmark for (2681ds/2967Mi) % 234.44/34.38 % (3049113)Instruction limit reached! % 234.44/34.38 % (3049113)------------------------------ % 234.44/34.38 % (3049113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.44/34.38 % (3049113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.44/34.38 % (3049113)CaDiCaL version: 2.1.3 % 234.44/34.38 % (3049113)Termination reason: Instruction limit % 234.44/34.38 % (3049113)Termination phase: Saturation % 234.44/34.38 % (3049113)Time elapsed: 1.953 s % 234.44/34.38 % (3049113)Peak memory usage: 175 MB % 234.44/34.38 % (3049113)Instructions burned: 5814 (million) % 234.44/34.38 % (3049118)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=1844918694:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2679 on theBenchmark for (2679ds/3022Mi) % 234.44/34.38 % (3049120)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=3549150489:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2678 on theBenchmark for (2678ds/3207Mi) % 234.44/34.38 [W928 14:13:34.743730708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743760299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743782601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743789014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743802545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743808011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.44/34.38 [W928 14:13:34.743821257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.44/34.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.743826825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.743839588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.743845093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.743857698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.743863017 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 % (3049120)Refutation not found, incomplete strategy % 239.87/35.08 % (3049120)------------------------------ % 239.87/35.08 % (3049120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.87/35.08 % (3049120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.87/35.08 % (3049120)CaDiCaL version: 2.1.3 % 239.87/35.08 % (3049120)Termination reason: Refutation not found, incomplete strategy % 239.87/35.08 % (3049120)Time elapsed: 0.311 s % 239.87/35.08 % (3049120)Peak memory usage: 127 MB % 239.87/35.08 % (3049120)Instructions burned: 829 (million) % 239.87/35.08 [W928 14:13:34.876446219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876481656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876519330 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876531940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876558687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876570093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.87/35.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.87/35.08 [W928 14:13:34.876596674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.876608087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.876632171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.876642571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.876667661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.876678498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 % (3049120)------------------------------ % 248.30/36.33 % (3049120)------------------------------ % 248.30/36.33 % (3049118)Refutation not found, incomplete strategy % 248.30/36.33 % (3049118)------------------------------ % 248.30/36.33 % (3049118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.30/36.33 % (3049118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.30/36.33 % (3049118)CaDiCaL version: 2.1.3 % 248.30/36.33 % (3049118)Termination reason: Refutation not found, incomplete strategy % 248.30/36.33 % (3049118)Time elapsed: 0.537 s % 248.30/36.33 % (3049118)Peak memory usage: 126 MB % 248.30/36.33 % (3049118)Instructions burned: 829 (million) % 248.30/36.33 % (3049123)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3307792390:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2673 on theBenchmark for (2673ds/3289Mi) % 248.30/36.33 % (3049118)------------------------------ % 248.30/36.33 % (3049118)------------------------------ % 248.30/36.33 % (3049125)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3998975356:i=38569:sd=3:ss=axioms:sgt=32_2671 on theBenchmark for (2671ds/38569Mi) % 248.30/36.33 [W928 14:13:34.522208148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.522231325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.522252677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.30/36.33 [W928 14:13:34.522260238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 248.30/36.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522274566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522280270 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522293576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522298999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522311552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522316869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522329725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 [W928 14:13:34.522335206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 249.33/36.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 249.33/36.58 % (3049125)Refutation not found, incomplete strategy % 249.33/36.58 % (3049125)------------------------------ % 249.33/36.58 % (3049125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.33/36.58 % (3049125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.33/36.58 % (3049125)CaDiCaL version: 2.1.3 % 249.33/36.58 % (3049125)Termination reason: Refutation not found, incomplete strategy % 249.33/36.58 % (3049125)Time elapsed: 0.319 s % 249.33/36.58 % (3049125)Peak memory usage: 126 MB % 249.33/36.58 % (3049125)Instructions burned: 832 (million) % 249.33/36.58 % (3049125)------------------------------ % 249.33/36.58 % (3049125)------------------------------ % 249.33/36.58 % (3049123)Refutation not found, incomplete strategy % 249.33/36.58 % (3049123)------------------------------ % 249.33/36.58 % (3049123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.33/36.58 % (3049123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 249.33/36.58 % (3049123)CaDiCaL version: 2.1.3 % 249.33/36.58 % (3049123)Termination reason: Refutation not found, incomplete strategy % 249.33/36.58 % (3049123)Time elapsed: 0.619 s % 249.33/36.58 % (3049123)Peak memory usage: 133 MB % 249.33/36.58 % (3049123)Instructions burned: 924 (million) % 249.33/36.58 % (3049127)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=108919562:cts=off:i=3394_2665 on theBenchmark for (2665ds/3394Mi) % 249.33/36.58 % (3049123)------------------------------ % 249.33/36.58 % (3049123)------------------------------ % 249.33/36.58 % (3049117)Instruction limit reached! % 249.33/36.58 % (3049117)------------------------------ % 249.33/36.58 % (3049117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 249.33/36.58 % (3049117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.71/37.98 % (3049117)CaDiCaL version: 2.1.3 % 259.71/37.98 % (3049117)Termination reason: Instruction limit % 259.71/37.98 % (3049117)Termination phase: Saturation % 259.71/37.98 % (3049117)Time elapsed: 1.856 s % 259.71/37.98 % (3049117)Peak memory usage: 144 MB % 259.71/37.98 % (3049117)Instructions burned: 2968 (million) % 259.71/37.98 % (3049129)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=1504920627:i=33824:bd=preordered_2662 on theBenchmark for (2662ds/33824Mi) % 259.71/37.98 % (3049131)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3144515790:i=20684:bd=all:gtg=exists_sym_2660 on theBenchmark for (2660ds/20684Mi) % 259.71/37.98 % (3049127)Instruction limit reached! % 259.71/37.98 % (3049127)------------------------------ % 259.71/37.98 % (3049127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.71/37.98 % (3049127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.71/37.98 % (3049127)CaDiCaL version: 2.1.3 % 259.71/37.98 % (3049127)Termination reason: Instruction limit % 259.71/37.98 % (3049127)Termination phase: Saturation % 259.71/37.98 % (3049127)Time elapsed: 1.225 s % 259.71/37.98 % (3049127)Peak memory usage: 144 MB % 259.71/37.98 % (3049127)Instructions burned: 3395 (million) % 259.71/37.98 % (3049111)Instruction limit reached! % 259.71/37.98 % (3049111)------------------------------ % 259.71/37.98 % (3049111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.71/37.98 % (3049111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.71/37.98 % (3049111)CaDiCaL version: 2.1.3 % 259.71/37.98 % (3049111)Termination reason: Instruction limit % 259.71/37.98 % (3049111)Termination phase: Saturation % 259.71/37.98 % (3049111)Time elapsed: 5.057 s % 259.71/37.98 % (3049111)Peak memory usage: 185 MB % 259.71/37.98 % (3049111)Instructions burned: 7897 (million) % 259.71/37.98 % (3049133)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=628985138: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_2651 on theBenchmark for (2651ds/7222Mi) % 259.71/37.98 % (3049134)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1723002367:st=4:i=7295:sd=4:ep=R:ss=axioms_2651 on theBenchmark for (2651ds/7295Mi) % 259.71/37.98 [W928 14:13:36.474692986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.71/37.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.71/37.98 [W928 14:13:36.474730961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.71/37.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.71/37.98 [W928 14:13:36.474752064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.71/37.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.71/37.98 [W928 14:13:36.474758644 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.71/37.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.71/37.98 [W928 14:13:36.474772506 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.71/37.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.71/37.98 [W928 14:13:36.474784784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensoTerminated %------------------------------------------------------------------------------