%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : MSC026-1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:05:42 PM UTC 2026 % Result : Timeout 300.13s 43.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : MSC026-1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.05/0.31 % Computer : n012.cluster.edu % 0.05/0.31 % Model : x86_64 x86_64 % 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.31 % Memory : 8046.5625MB % 0.05/0.31 % OS : Linux 6.8.0-71-generic % 0.05/0.32 % CPULimit : 300 % 0.05/0.32 % WCLimit : 300 % 0.05/0.32 % DateTime : Sun Sep 27 17:43:34 UTC 2026 % 0.05/0.32 % CPUTime : % 0.05/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.34 Running first-order theorem proving % 0.07/0.34 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.82/1.51 % (2617822)Input is clausal, will run a generic CNF schedule. % 5.82/1.51 % (2617827)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=936417646:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 5.82/1.51 % (2617828)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1885224885:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 5.82/1.51 % (2617829)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3183395225:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 5.82/1.51 % (2617833)dis-21_1_sil=8000:lcm=predicate:random_seed=1907695960:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 5.82/1.51 % (2617831)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2039986817:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 5.82/1.51 % (2617830)lrs+10_1_sil=8000:sp=occurrence:random_seed=3343625318:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 5.82/1.51 % (2617830)Refutation not found, incomplete strategy % 5.82/1.51 % (2617830)------------------------------ % 5.82/1.51 % (2617830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.82/1.51 % (2617830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.51 % (2617830)CaDiCaL version: 2.1.3 % 5.82/1.51 % (2617830)Termination reason: Refutation not found, incomplete strategy % 5.82/1.51 % (2617830)Time elapsed: 0.003 s % 5.82/1.51 % (2617830)Peak memory usage: 88 MB % 5.82/1.51 % (2617830)Instructions burned: 7 (million) % 5.82/1.51 % (2617831)Refutation not found, incomplete strategy % 5.82/1.51 % (2617831)------------------------------ % 5.82/1.51 % (2617831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.82/1.51 % (2617831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.51 % (2617831)CaDiCaL version: 2.1.3 % 5.82/1.51 % (2617831)Termination reason: Refutation not found, incomplete strategy % 5.82/1.51 % (2617831)Time elapsed: 0.004 s % 5.82/1.51 % (2617831)Peak memory usage: 88 MB % 5.82/1.51 % (2617831)Instructions burned: 10 (million) % 5.82/1.51 % (2617833)Refutation not found, incomplete strategy % 5.82/1.51 % (2617833)------------------------------ % 5.82/1.51 % (2617833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.82/1.51 % (2617833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.51 % (2617833)CaDiCaL version: 2.1.3 % 5.82/1.51 % (2617833)Termination reason: Refutation not found, incomplete strategy % 5.82/1.51 % (2617833)Time elapsed: 0.004 s % 5.82/1.51 % (2617833)Peak memory usage: 88 MB % 5.82/1.51 % (2617833)Instructions burned: 10 (million) % 5.82/1.51 % (2617832)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=979534731:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 5.82/1.51 % (2617832)Instruction limit reached! % 5.82/1.51 % (2617832)------------------------------ % 5.82/1.51 % (2617832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.82/1.51 % (2617832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.82/1.51 % (2617832)CaDiCaL version: 2.1.3 % 5.82/1.51 % (2617832)Termination reason: Instruction limit % 5.82/1.51 % (2617832)Termination phase: Saturation % 5.82/1.51 % (2617832)Time elapsed: 0.064 s % 5.82/1.51 % (2617832)Peak memory usage: 91 MB % 5.82/1.51 % (2617832)Instructions burned: 180 (million) % 5.82/1.51 % (2617831)------------------------------ % 5.82/1.51 % (2617831)------------------------------ % 5.82/1.51 % (2617833)------------------------------ % 5.82/1.51 % (2617833)------------------------------ % 5.82/1.51 % (2617830)------------------------------ % 5.82/1.51 % (2617830)------------------------------ % 5.82/1.51 % (2617841)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3552116126:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 5.82/1.51 % (2617841)Refutation not found, incomplete strategy % 5.82/1.51 % (2617841)------------------------------ % 5.82/1.51 % (2617841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.82/1.51 % (2617841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617841)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617841)Termination reason: Refutation not found, incomplete strategy % 7.98/1.82 % (2617841)Time elapsed: 0.003 s % 7.98/1.82 % (2617841)Peak memory usage: 88 MB % 7.98/1.82 % (2617841)Instructions burned: 7 (million) % 7.98/1.82 % (2617843)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2097442334:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi) % 7.98/1.82 % (2617844)lrs+10_64_to=lpo:sil=8000:random_seed=2978318853:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 7.98/1.82 % (2617842)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4083390776:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 7.98/1.82 % (2617843)Refutation not found, incomplete strategy % 7.98/1.82 % (2617843)------------------------------ % 7.98/1.82 % (2617843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.82 % (2617843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617843)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617843)Termination reason: Refutation not found, incomplete strategy % 7.98/1.82 % (2617843)Time elapsed: 0.004 s % 7.98/1.82 % (2617843)Peak memory usage: 88 MB % 7.98/1.82 % (2617843)Instructions burned: 10 (million) % 7.98/1.82 % (2617842)Refutation not found, incomplete strategy % 7.98/1.82 % (2617842)------------------------------ % 7.98/1.82 % (2617842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.82 % (2617842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617842)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617842)Termination reason: Refutation not found, incomplete strategy % 7.98/1.82 % (2617842)Time elapsed: 0.007 s % 7.98/1.82 % (2617842)Peak memory usage: 87 MB % 7.98/1.82 % (2617842)Instructions burned: 20 (million) % 7.98/1.82 % (2617844)Instruction limit reached! % 7.98/1.82 % (2617844)------------------------------ % 7.98/1.82 % (2617844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.82 % (2617844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617844)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617844)Termination reason: Instruction limit % 7.98/1.82 % (2617844)Termination phase: Saturation % 7.98/1.82 % (2617844)Time elapsed: 0.042 s % 7.98/1.82 % (2617844)Peak memory usage: 91 MB % 7.98/1.82 % (2617844)Instructions burned: 127 (million) % 7.98/1.82 % (2617841)------------------------------ % 7.98/1.82 % (2617841)------------------------------ % 7.98/1.82 % (2617843)------------------------------ % 7.98/1.82 % (2617843)------------------------------ % 7.98/1.82 % (2617842)------------------------------ % 7.98/1.82 % (2617842)------------------------------ % 7.98/1.82 % (2617849)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1484230723:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi) % 7.98/1.82 % (2617850)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4024979360:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 7.98/1.82 % (2617849)Instruction limit reached! % 7.98/1.82 % (2617849)------------------------------ % 7.98/1.82 % (2617849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.82 % (2617849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617849)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617849)Termination reason: Instruction limit % 7.98/1.82 % (2617849)Termination phase: Saturation % 7.98/1.82 % (2617849)Time elapsed: 0.062 s % 7.98/1.82 % (2617849)Peak memory usage: 92 MB % 7.98/1.82 % (2617849)Instructions burned: 195 (million) % 7.98/1.82 % (2617850)Instruction limit reached! % 7.98/1.82 % (2617850)------------------------------ % 7.98/1.82 % (2617850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.98/1.82 % (2617850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.82 % (2617850)CaDiCaL version: 2.1.3 % 7.98/1.82 % (2617850)Termination reason: Instruction limit % 7.98/1.82 % (2617850)Termination phase: Saturation % 7.98/1.82 % (2617850)Time elapsed: 0.047 s % 7.98/1.82 % (2617850)Peak memory usage: 92 MB % 7.98/1.82 % (2617850)Instructions burned: 158 (million) % 7.98/1.82 % (2617851)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2049858906:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi) % 7.98/1.82 % (2617852)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=762902394:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 12.20/2.32 % (2617852)Refutation not found, incomplete strategy % 12.20/2.32 % (2617852)------------------------------ % 12.20/2.32 % (2617852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.20/2.32 % (2617852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.20/2.32 % (2617852)CaDiCaL version: 2.1.3 % 12.20/2.32 % (2617852)Termination reason: Refutation not found, incomplete strategy % 12.20/2.32 % (2617852)Time elapsed: 0.005 s % 12.20/2.32 % (2617852)Peak memory usage: 88 MB % 12.20/2.32 % (2617852)Instructions burned: 13 (million) % 12.20/2.32 % (2617856)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=348101310:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 12.20/2.32 % (2617855)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2701448845:i=107_2992 on theBenchmark for (2992ds/107Mi) % 12.20/2.32 % (2617856)Refutation not found, incomplete strategy % 12.20/2.32 % (2617856)------------------------------ % 12.20/2.32 % (2617856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.20/2.32 % (2617856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.20/2.32 % (2617856)CaDiCaL version: 2.1.3 % 12.20/2.32 % (2617856)Termination reason: Refutation not found, incomplete strategy % 12.20/2.32 % (2617856)Time elapsed: 0.012 s % 12.20/2.32 % (2617856)Peak memory usage: 88 MB % 12.20/2.32 % (2617856)Instructions burned: 50 (million) % 12.20/2.32 % (2617855)Refutation not found, incomplete strategy % 12.20/2.32 % (2617855)------------------------------ % 12.20/2.32 % (2617855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.20/2.32 % (2617855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.20/2.32 % (2617855)CaDiCaL version: 2.1.3 % 12.20/2.32 % (2617855)Termination reason: Refutation not found, incomplete strategy % 12.20/2.32 % (2617855)Time elapsed: 0.024 s % 12.20/2.32 % (2617855)Peak memory usage: 91 MB % 12.20/2.32 % (2617855)Instructions burned: 74 (million) % 12.20/2.32 % (2617852)------------------------------ % 12.20/2.32 % (2617852)------------------------------ % 12.20/2.32 [W927 17:43:36.745422351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745445119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745466519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745473790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745488276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745494703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.20/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.20/2.32 [W927 17:43:36.745509119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 [W927 17:43:36.745515587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 [W927 17:43:36.745534993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 [W927 17:43:36.745576723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 [W927 17:43:36.745598829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 [W927 17:43:36.745605029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 21.11/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 21.11/3.66 % (2617856)------------------------------ % 21.11/3.66 % (2617856)------------------------------ % 21.11/3.66 % (2617855)------------------------------ % 21.11/3.66 % (2617855)------------------------------ % 21.11/3.66 % (2617861)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3426161969:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi) % 21.11/3.66 % (2617851)Refutation not found, incomplete strategy % 21.11/3.66 % (2617851)------------------------------ % 21.11/3.66 % (2617851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.11/3.66 % (2617851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.11/3.66 % (2617851)CaDiCaL version: 2.1.3 % 21.11/3.66 % (2617851)Termination reason: Refutation not found, incomplete strategy % 21.11/3.66 % (2617851)Time elapsed: 0.320 s % 21.11/3.66 % (2617851)Peak memory usage: 128 MB % 21.11/3.66 % (2617851)Instructions burned: 845 (million) % 21.11/3.66 % (2617862)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4010958785:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi) % 21.11/3.66 % (2617862)Refutation not found, incomplete strategy % 21.11/3.66 % (2617862)------------------------------ % 21.11/3.66 % (2617862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.11/3.66 % (2617862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.11/3.66 % (2617862)CaDiCaL version: 2.1.3 % 21.11/3.66 % (2617862)Termination reason: Refutation not found, incomplete strategy % 21.11/3.66 % (2617862)Time elapsed: 0.003 s % 21.11/3.66 % (2617862)Peak memory usage: 88 MB % 21.11/3.66 % (2617862)Instructions burned: 7 (million) % 21.11/3.66 % (2617863)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4265180777:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 21.11/3.66 % (2617851)------------------------------ % 21.11/3.66 % (2617851)------------------------------ % 21.11/3.66 % (2617862)------------------------------ % 21.11/3.66 % (2617862)------------------------------ % 21.11/3.66 % (2617863)Instruction limit reached! % 21.11/3.66 % (2617863)------------------------------ % 21.11/3.66 % (2617863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.11/3.66 % (2617863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.11/3.66 % (2617863)CaDiCaL version: 2.1.3 % 21.11/3.66 % (2617863)Termination reason: Instruction limit % 21.11/3.66 % (2617863)Termination phase: Saturation % 23.22/3.97 % (2617863)Time elapsed: 0.146 s % 23.22/3.97 % (2617863)Peak memory usage: 99 MB % 23.22/3.97 % (2617863)Instructions burned: 500 (million) % 23.22/3.97 % (2617867)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1671310954:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi) % 23.22/3.97 % (2617868)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4198845195:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi) % 23.22/3.97 % (2617869)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3758377994:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 23.22/3.97 % (2617867)Instruction limit reached! % 23.22/3.97 % (2617867)------------------------------ % 23.22/3.97 % (2617867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.22/3.97 % (2617867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.22/3.97 % (2617867)CaDiCaL version: 2.1.3 % 23.22/3.97 % (2617867)Termination reason: Instruction limit % 23.22/3.97 % (2617867)Termination phase: Saturation % 23.22/3.97 % (2617867)Time elapsed: 0.065 s % 23.22/3.97 % (2617867)Peak memory usage: 92 MB % 23.22/3.97 % (2617867)Instructions burned: 191 (million) % 23.22/3.97 % (2617869)Instruction limit reached! % 23.22/3.97 % (2617869)------------------------------ % 23.22/3.97 % (2617869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.22/3.97 % (2617869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.22/3.97 % (2617869)CaDiCaL version: 2.1.3 % 23.22/3.97 % (2617869)Termination reason: Instruction limit % 23.22/3.97 % (2617869)Termination phase: Saturation % 23.22/3.97 % (2617869)Time elapsed: 0.048 s % 23.22/3.97 % (2617869)Peak memory usage: 91 MB % 23.22/3.97 % (2617869)Instructions burned: 158 (million) % 23.22/3.97 % (2617868)Instruction limit reached! % 23.22/3.97 % (2617868)------------------------------ % 23.22/3.97 % (2617868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.22/3.97 % (2617868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.22/3.97 % (2617868)CaDiCaL version: 2.1.3 % 23.22/3.97 % (2617868)Termination reason: Instruction limit % 23.22/3.97 % (2617868)Termination phase: Saturation % 23.22/3.97 % (2617868)Time elapsed: 0.069 s % 23.22/3.97 % (2617868)Peak memory usage: 93 MB % 23.22/3.97 % (2617868)Instructions burned: 269 (million) % 23.22/3.97 % (2617873)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3864549713:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi) % 23.22/3.97 % (2617875)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=997388376:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi) % 23.22/3.97 % (2617874)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4110741960:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi) % 23.22/3.97 % (2617874)Refutation not found, incomplete strategy % 23.22/3.97 % (2617874)------------------------------ % 23.22/3.97 % (2617874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.22/3.97 % (2617874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.22/3.97 % (2617874)CaDiCaL version: 2.1.3 % 23.22/3.97 % (2617874)Termination reason: Refutation not found, incomplete strategy % 23.22/3.97 % (2617874)Time elapsed: 0.003 s % 23.22/3.97 % (2617874)Peak memory usage: 88 MB % 23.22/3.97 % (2617874)Instructions burned: 7 (million) % 23.22/3.97 % (2617875)Instruction limit reached! % 23.22/3.97 % (2617875)------------------------------ % 23.22/3.97 % (2617875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.22/3.97 % (2617875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.22/3.97 % (2617875)CaDiCaL version: 2.1.3 % 23.22/3.97 % (2617875)Termination reason: Instruction limit % 23.22/3.97 % (2617875)Termination phase: Saturation % 23.22/3.97 % (2617875)Time elapsed: 0.058 s % 23.22/3.97 % (2617875)Peak memory usage: 92 MB % 23.22/3.97 % (2617875)Instructions burned: 183 (million) % 23.22/3.97 % (2617874)------------------------------ % 23.22/3.97 % (2617874)------------------------------ % 23.22/3.97 % (2617879)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1370982475:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi) % 34.39/5.54 % (2617880)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2934469199:i=412:gtgl=4:gtg=exists_all_2982 on theBenchmark for (2982ds/412Mi) % 34.39/5.54 % (2617880)Instruction limit reached! % 34.39/5.54 % (2617880)------------------------------ % 34.39/5.54 % (2617880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.39/5.54 % (2617880)CaDiCaL version: 2.1.3 % 34.39/5.54 % (2617880)Termination reason: Instruction limit % 34.39/5.54 % (2617880)Termination phase: Saturation % 34.39/5.54 % (2617880)Time elapsed: 0.126 s % 34.39/5.54 % (2617880)Peak memory usage: 95 MB % 34.39/5.54 % (2617880)Instructions burned: 412 (million) % 34.39/5.54 % (2617883)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=4120414252:s2pl=no:i=8478:s2at=4:nm=6_2979 on theBenchmark for (2979ds/8478Mi) % 34.39/5.54 % (2617873)Instruction limit reached! % 34.39/5.54 % (2617873)------------------------------ % 34.39/5.54 % (2617873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.39/5.54 % (2617873)CaDiCaL version: 2.1.3 % 34.39/5.54 % (2617873)Termination reason: Instruction limit % 34.39/5.54 % (2617873)Termination phase: Saturation % 34.39/5.54 % (2617873)Time elapsed: 1.142 s % 34.39/5.54 % (2617873)Peak memory usage: 155 MB % 34.39/5.54 % (2617873)Instructions burned: 3258 (million) % 34.39/5.54 % (2617861)Instruction limit reached! % 34.39/5.54 % (2617861)------------------------------ % 34.39/5.54 % (2617861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.39/5.54 % (2617861)CaDiCaL version: 2.1.3 % 34.39/5.54 % (2617861)Termination reason: Instruction limit % 34.39/5.54 % (2617861)Termination phase: Saturation % 34.39/5.54 % (2617861)Time elapsed: 1.728 s % 34.39/5.54 % (2617861)Peak memory usage: 166 MB % 34.39/5.54 % (2617861)Instructions burned: 5210 (million) % 34.39/5.54 % (2617885)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=431628152:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi) % 34.39/5.54 % (2617885)Refutation not found, incomplete strategy % 34.39/5.54 % (2617885)------------------------------ % 34.39/5.54 % (2617885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.39/5.54 % (2617885)CaDiCaL version: 2.1.3 % 34.39/5.54 % (2617885)Termination reason: Refutation not found, incomplete strategy % 34.39/5.54 % (2617885)Time elapsed: 0.005 s % 34.39/5.54 % (2617885)Peak memory usage: 88 MB % 34.39/5.54 % (2617885)Instructions burned: 15 (million) % 34.39/5.54 % (2617886)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3122234466:st=4:i=720:sd=3:fsr=off:ss=axioms_2972 on theBenchmark for (2972ds/720Mi) % 34.39/5.54 % (2617886)Refutation not found, incomplete strategy % 34.39/5.54 % (2617886)------------------------------ % 34.39/5.54 % (2617886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.39/5.54 % (2617886)CaDiCaL version: 2.1.3 % 34.39/5.54 % (2617886)Termination reason: Refutation not found, incomplete strategy % 34.39/5.54 % (2617886)Time elapsed: 0.004 s % 34.39/5.54 % (2617886)Peak memory usage: 88 MB % 34.39/5.54 % (2617886)Instructions burned: 10 (million) % 34.39/5.54 % (2617885)------------------------------ % 34.39/5.54 % (2617885)------------------------------ % 34.39/5.54 % (2617886)------------------------------ % 34.39/5.54 % (2617886)------------------------------ % 34.39/5.54 % (2617889)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=565401583:i=598:bs=on:bd=preordered:av=off:ss=axioms_2970 on theBenchmark for (2970ds/598Mi) % 34.39/5.54 % (2617889)Refutation not found, incomplete strategy % 34.39/5.54 % (2617889)------------------------------ % 34.39/5.54 % (2617889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.39/5.54 % (2617889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.26/5.76 % (2617889)CaDiCaL version: 2.1.3 % 32.26/5.76 % (2617889)Termination reason: Refutation not found, incomplete strategy % 32.26/5.76 % (2617889)Time elapsed: 0.003 s % 32.26/5.76 % (2617889)Peak memory usage: 88 MB % 32.26/5.76 % (2617889)Instructions burned: 7 (million) % 32.26/5.76 % (2617890)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=340823073:i=2989:sd=3:ss=axioms:sgt=60_2969 on theBenchmark for (2969ds/2989Mi) % 32.26/5.76 % (2617889)------------------------------ % 32.26/5.76 % (2617889)------------------------------ % 32.26/5.76 % (2617893)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3618578795:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi) % 32.26/5.76 [W927 17:43:38.204119006 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204138568 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204159126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204166145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204179579 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204185706 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204199982 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204206596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204220299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204226621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.26/5.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.26/5.76 [W927 17:43:38.204239888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.70/6.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.70/6.35 [W927 17:43:38.204246078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.70/6.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.70/6.35 % (2617890)Refutation not found, incomplete strategy % 39.70/6.35 % (2617890)------------------------------ % 39.70/6.35 % (2617890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.70/6.35 % (2617890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.70/6.35 % (2617890)CaDiCaL version: 2.1.3 % 39.70/6.35 % (2617890)Termination reason: Refutation not found, incomplete strategy % 39.70/6.35 % (2617890)Time elapsed: 0.317 s % 39.70/6.35 % (2617890)Peak memory usage: 127 MB % 39.70/6.35 % (2617890)Instructions burned: 845 (million) % 39.70/6.35 % (2617890)------------------------------ % 39.70/6.35 % (2617890)------------------------------ % 39.70/6.35 % (2617895)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2834581698:i=2088:bd=preordered:av=off_2963 on theBenchmark for (2963ds/2088Mi) % 39.70/6.35 % (2617893)Instruction limit reached! % 39.70/6.35 % (2617893)------------------------------ % 39.70/6.35 % (2617893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.70/6.35 % (2617893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.70/6.35 % (2617893)CaDiCaL version: 2.1.3 % 39.70/6.35 % (2617893)Termination reason: Instruction limit % 39.70/6.35 % (2617893)Termination phase: Saturation % 39.70/6.35 % (2617893)Time elapsed: 0.685 s % 39.70/6.35 % (2617893)Peak memory usage: 159 MB % 39.70/6.35 % (2617893)Instructions burned: 2000 (million) % 39.70/6.35 % (2617897)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3473068933:i=1098:nicw=on_2958 on theBenchmark for (2958ds/1098Mi) % 39.70/6.35 % (2617895)Instruction limit reached! % 39.70/6.35 % (2617895)------------------------------ % 39.70/6.35 % (2617895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.70/6.35 % (2617895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.70/6.35 % (2617895)CaDiCaL version: 2.1.3 % 39.70/6.35 % (2617895)Termination reason: Instruction limit % 39.70/6.35 % (2617895)Termination phase: Saturation % 39.70/6.35 % (2617895)Time elapsed: 0.724 s % 39.70/6.35 % (2617895)Peak memory usage: 153 MB % 39.70/6.35 % (2617895)Instructions burned: 2088 (million) % 39.70/6.35 % (2617897)Instruction limit reached! % 39.70/6.35 % (2617897)------------------------------ % 39.70/6.35 % (2617897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.70/6.35 % (2617897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.70/6.35 % (2617897)CaDiCaL version: 2.1.3 % 39.70/6.35 % (2617897)Termination reason: Instruction limit % 39.70/6.35 % (2617897)Termination phase: Saturation % 39.70/6.35 % (2617897)Time elapsed: 0.353 s % 39.70/6.35 % (2617897)Peak memory usage: 105 MB % 39.70/6.35 % (2617897)Instructions burned: 1100 (million) % 39.70/6.35 % (2617899)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3725906990:i=433:bd=preordered_2954 on theBenchmark for (2954ds/433Mi) % 39.70/6.35 % (2617900)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1977093760:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2954 on theBenchmark for (2954ds/2942Mi) % 39.70/6.35 % (2617899)Refutation not found, incomplete strategy % 39.70/6.35 % (2617899)------------------------------ % 39.70/6.35 % (2617899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.70/6.35 % (2617899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.70/6.35 % (2617899)CaDiCaL version: 2.1.3 % 39.70/6.35 % (2617899)Termination reason: Refutation not found, incomplete strategy % 39.70/6.35 % (2617899)Time elapsed: 0.053 s % 39.70/6.35 % (2617899)Peak memory usage: 92 MB % 39.70/6.35 % (2617899)Instructions burned: 155 (million) % 39.70/6.35 % (2617899)------------------------------ % 39.70/6.35 % (2617899)------------------------------ % 39.70/6.35 % (2617903)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=742629492:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2951 on theBenchmark for (2951ds/6922Mi) % 40.67/6.69 % (2617883)Instruction limit reached! % 40.67/6.69 % (2617883)------------------------------ % 40.67/6.69 % (2617883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.67/6.69 % (2617883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.67/6.69 % (2617883)CaDiCaL version: 2.1.3 % 40.67/6.69 % (2617883)Termination reason: Instruction limit % 40.67/6.69 % (2617883)Termination phase: Saturation % 40.67/6.69 % (2617883)Time elapsed: 3.0000 s % 40.67/6.69 % (2617883)Peak memory usage: 195 MB % 40.67/6.69 % (2617883)Instructions burned: 8479 (million) % 40.67/6.69 [W927 17:43:40.996417692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996456671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996479032 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996485384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996499505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996505968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996520078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996526191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996539549 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996545592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 40.67/6.69 [W927 17:43:40.996559225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 40.67/6.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.54/6.74 [W927 17:43:40.996565257 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/6.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.54/6.74 % (2617905)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3485111245:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2948 on theBenchmark for (2948ds/596Mi) % 41.54/6.74 % (2617903)Refutation not found, incomplete strategy % 41.54/6.74 % (2617903)------------------------------ % 41.54/6.74 % (2617903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.74 % (2617903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.74 % (2617903)CaDiCaL version: 2.1.3 % 41.54/6.74 % (2617903)Termination reason: Refutation not found, incomplete strategy % 41.54/6.74 % (2617903)Time elapsed: 0.310 s % 41.54/6.74 % (2617903)Peak memory usage: 128 MB % 41.54/6.74 % (2617903)Instructions burned: 845 (million) % 41.54/6.74 % (2617903)------------------------------ % 41.54/6.74 % (2617903)------------------------------ % 41.54/6.74 % (2617905)Instruction limit reached! % 41.54/6.74 % (2617905)------------------------------ % 41.54/6.74 % (2617905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.74 % (2617905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.74 % (2617905)CaDiCaL version: 2.1.3 % 41.54/6.74 % (2617905)Termination reason: Instruction limit % 41.54/6.74 % (2617905)Termination phase: Saturation % 41.54/6.74 % (2617905)Time elapsed: 0.188 s % 41.54/6.74 % (2617905)Peak memory usage: 97 MB % 41.54/6.74 % (2617905)Instructions burned: 597 (million) % 41.54/6.74 % (2617879)Instruction limit reached! % 41.54/6.74 % (2617879)------------------------------ % 41.54/6.74 % (2617879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.74 % (2617879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.74 % (2617879)CaDiCaL version: 2.1.3 % 41.54/6.74 % (2617879)Termination reason: Instruction limit % 41.54/6.74 % (2617879)Termination phase: Saturation % 41.54/6.74 % (2617879)Time elapsed: 3.715 s % 41.54/6.74 % (2617879)Peak memory usage: 203 MB % 41.54/6.74 % (2617879)Instructions burned: 10309 (million) % 41.54/6.74 % (2617907)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3700144781:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2945 on theBenchmark for (2945ds/4123Mi) % 41.54/6.74 % (2617908)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1073030199:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2945 on theBenchmark for (2945ds/16411Mi) % 41.54/6.74 % (2617909)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3749492572:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2944 on theBenchmark for (2944ds/1670Mi) % 41.54/6.74 % (2617900)Instruction limit reached! % 41.54/6.74 % (2617900)------------------------------ % 41.54/6.74 % (2617900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.74 % (2617900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.74 % (2617900)CaDiCaL version: 2.1.3 % 41.54/6.74 % (2617900)Termination reason: Instruction limit % 41.54/6.74 % (2617900)Termination phase: Saturation % 41.54/6.74 % (2617900)Time elapsed: 1.078 s % 41.54/6.74 % (2617900)Peak memory usage: 153 MB % 41.54/6.74 % (2617900)Instructions burned: 2943 (million) % 41.54/6.74 [W927 17:43:40.592209220 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/6.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.54/6.74 [W927 17:43:40.592239787 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/6.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.54/6.74 [W927 17:43:40.592261517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592267340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592280305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592293142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592306408 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592311665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592324195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592334261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592348218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 [W927 17:43:40.592353511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.51/7.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.51/7.09 % (2617908)Refutation not found, incomplete strategy % 45.51/7.09 % (2617908)------------------------------ % 45.51/7.09 % (2617908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.51/7.09 % (2617908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.51/7.09 % (2617908)CaDiCaL version: 2.1.3 % 45.51/7.09 % (2617908)Termination reason: Refutation not found, incomplete strategy % 45.51/7.09 % (2617908)Time elapsed: 0.314 s % 45.51/7.09 % (2617908)Peak memory usage: 127 MB % 45.51/7.09 % (2617908)Instructions burned: 847 (million) % 45.51/7.09 % (2617913)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3927280517:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2942 on theBenchmark for (2942ds/1722Mi) % 45.51/7.09 % (2617908)------------------------------ % 45.51/7.09 % (2617908)------------------------------ % 45.51/7.09 [W927 17:43:41.923998613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924027684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924051917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924058494 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924082624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924088810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924102477 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924108266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924120969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924126842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924139687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 [W927 17:43:41.924145547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.93/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.93/8.65 % (2617909)Instruction limit reached! % 55.93/8.65 % (2617909)------------------------------ % 55.93/8.65 % (2617909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.93/8.65 % (2617909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.93/8.65 % (2617909)CaDiCaL version: 2.1.3 % 55.93/8.65 % (2617909)Termination reason: Instruction limit % 55.93/8.65 % (2617909)Termination phase: Saturation % 55.93/8.65 % (2617909)Time elapsed: 0.563 s % 55.93/8.65 % (2617909)Peak memory usage: 155 MB % 55.93/8.65 % (2617909)Instructions burned: 1672 (million) % 56.44/8.70 % (2617915)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=456364796:cts=off:cond=on:i=9530:bs=on:fsd=on_2939 on theBenchmark for (2939ds/9530Mi) % 56.44/8.70 % (2617913)Refutation not found, incomplete strategy % 56.44/8.70 % (2617913)------------------------------ % 56.44/8.70 % (2617913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.44/8.70 % (2617913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.44/8.70 % (2617913)CaDiCaL version: 2.1.3 % 56.44/8.70 % (2617913)Termination reason: Refutation not found, incomplete strategy % 56.44/8.70 % (2617913)Time elapsed: 0.320 s % 56.44/8.70 % (2617913)Peak memory usage: 128 MB % 56.44/8.70 % (2617913)Instructions burned: 849 (million) % 56.44/8.70 % (2617917)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1632652854:st=2:i=4495:sd=10:ss=included_2937 on theBenchmark for (2937ds/4495Mi) % 56.44/8.70 % (2617913)------------------------------ % 56.44/8.70 % (2617913)------------------------------ % 56.44/8.70 % (2617919)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1287842586:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2935 on theBenchmark for (2935ds/4920Mi) % 56.44/8.70 [W927 17:43:41.324692544 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324711775 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324733354 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324740935 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324755840 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324762093 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324776333 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324782608 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 56.44/8.70 [W927 17:43:41.324796097 register_special_ops.cpp:225] Warning: Creating a tensor from 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.44/8.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.27/9.14 [W927 17:43:41.324802456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.27/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.27/9.14 [W927 17:43:41.324820504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.27/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.27/9.14 [W927 17:43:41.324825978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.27/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.27/9.14 % (2617917)Refutation not found, incomplete strategy % 60.27/9.14 % (2617917)------------------------------ % 60.27/9.14 % (2617917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.27/9.14 % (2617917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.27/9.14 % (2617917)CaDiCaL version: 2.1.3 % 60.27/9.14 % (2617917)Termination reason: Refutation not found, incomplete strategy % 60.27/9.14 % (2617917)Time elapsed: 0.313 s % 60.27/9.14 % (2617917)Peak memory usage: 127 MB % 60.27/9.14 % (2617917)Instructions burned: 845 (million) % 60.27/9.14 % (2617917)------------------------------ % 60.27/9.14 % (2617917)------------------------------ % 60.27/9.14 % (2617921)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2087983553:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2931 on theBenchmark for (2931ds/2083Mi) % 60.27/9.14 % (2617907)Instruction limit reached! % 60.27/9.14 % (2617907)------------------------------ % 60.27/9.14 % (2617907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.27/9.14 % (2617907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.27/9.14 % (2617907)CaDiCaL version: 2.1.3 % 60.27/9.14 % (2617907)Termination reason: Instruction limit % 60.27/9.14 % (2617907)Termination phase: Saturation % 60.27/9.14 % (2617907)Time elapsed: 1.441 s % 60.27/9.14 % (2617907)Peak memory usage: 162 MB % 60.27/9.14 % (2617907)Instructions burned: 4126 (million) % 60.27/9.14 % (2617923)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1050957950:i=4629:av=off:gsp=on_2929 on theBenchmark for (2929ds/4629Mi) % 60.27/9.14 % (2617923)Refutation not found, incomplete strategy % 60.27/9.14 % (2617923)------------------------------ % 60.27/9.14 % (2617923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.27/9.14 % (2617923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.27/9.14 % (2617923)CaDiCaL version: 2.1.3 % 60.27/9.14 % (2617923)Termination reason: Refutation not found, incomplete strategy % 60.27/9.14 % (2617923)Time elapsed: 0.417 s % 60.27/9.14 % (2617923)Peak memory usage: 150 MB % 60.27/9.14 % (2617923)Instructions burned: 1146 (million) % 60.27/9.14 % (2617921)Instruction limit reached! % 60.27/9.14 % (2617921)------------------------------ % 60.27/9.14 % (2617921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.27/9.14 % (2617921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.27/9.14 % (2617921)CaDiCaL version: 2.1.3 % 60.27/9.14 % (2617921)Termination reason: Instruction limit % 60.27/9.14 % (2617921)Termination phase: Saturation % 60.27/9.14 % (2617921)Time elapsed: 0.699 s % 60.27/9.14 % (2617921)Peak memory usage: 146 MB % 60.27/9.14 % (2617921)Instructions burned: 2083 (million) % 60.27/9.14 % (2617923)------------------------------ % 60.27/9.14 % (2617923)------------------------------ % 60.27/9.14 % (2617925)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1557220526:i=1258:av=off_2923 on theBenchmark for (2923ds/1258Mi) % 60.27/9.14 % (2617926)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1441432828:i=7343:av=off:ss=included_2922 on theBenchmark for (2922ds/7343Mi) % 60.27/9.14 [W927 17:43:43.886037574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886058594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886083194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886089782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886141573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886161850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886179340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886185450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886198116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886203898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886216666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 [W927 17:43:43.886222579 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.84/9.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.84/9.26 % (2617925)Instruction limit reached! % 60.84/9.26 % (2617925)------------------------------ % 60.84/9.26 % (2617925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.84/9.26 % (2617925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.84/9.26 % (2617925)CaDiCaL version: 2.1.3 % 60.84/9.26 % (2617925)Termination reason: Instruction limit % 60.84/9.26 % (2617925)Termination phase: Saturation % 63.45/9.65 % (2617925)Time elapsed: 0.394 s % 63.45/9.65 % (2617925)Peak memory usage: 98 MB % 63.45/9.65 % (2617925)Instructions burned: 1261 (million) % 63.45/9.65 % (2617926)Refutation not found, incomplete strategy % 63.45/9.65 % (2617926)------------------------------ % 63.45/9.65 % (2617926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.45/9.65 % (2617926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.45/9.65 % (2617926)CaDiCaL version: 2.1.3 % 63.45/9.65 % (2617926)Termination reason: Refutation not found, incomplete strategy % 63.45/9.65 % (2617926)Time elapsed: 0.311 s % 63.45/9.65 % (2617926)Peak memory usage: 128 MB % 63.45/9.65 % (2617926)Instructions burned: 845 (million) % 63.45/9.65 % (2617919)Instruction limit reached! % 63.45/9.65 % (2617919)------------------------------ % 63.45/9.65 % (2617919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.45/9.65 % (2617919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.45/9.65 % (2617919)CaDiCaL version: 2.1.3 % 63.45/9.65 % (2617919)Termination reason: Instruction limit % 63.45/9.65 % (2617919)Termination phase: Saturation % 63.45/9.65 % (2617919)Time elapsed: 1.704 s % 63.45/9.65 % (2617919)Peak memory usage: 168 MB % 63.45/9.65 % (2617919)Instructions burned: 4922 (million) % 63.45/9.65 % (2617929)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1543046428:i=1325:sd=2:ss=axioms:sgt=16_2918 on theBenchmark for (2918ds/1325Mi) % 63.45/9.65 % (2617929)Refutation not found, incomplete strategy % 63.45/9.65 % (2617929)------------------------------ % 63.45/9.65 % (2617929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.45/9.65 % (2617929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.45/9.65 % (2617929)CaDiCaL version: 2.1.3 % 63.45/9.65 % (2617929)Termination reason: Refutation not found, incomplete strategy % 63.45/9.65 % (2617929)Time elapsed: 0.003 s % 63.45/9.65 % (2617929)Peak memory usage: 88 MB % 63.45/9.65 % (2617929)Instructions burned: 7 (million) % 63.45/9.65 % (2617926)------------------------------ % 63.45/9.65 % (2617926)------------------------------ % 63.45/9.65 % (2617930)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3770080639:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2917 on theBenchmark for (2917ds/2646Mi) % 63.45/9.65 % (2617929)------------------------------ % 63.45/9.65 % (2617929)------------------------------ % 63.45/9.65 % (2617932)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3601589425:i=1489:sd=2:ep=R:ss=axioms_2916 on theBenchmark for (2916ds/1489Mi) % 63.45/9.65 % (2617934)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=393850785:i=1503_2915 on theBenchmark for (2915ds/1503Mi) % 63.45/9.65 [W927 17:43:43.378520971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.45/9.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.45/9.65 [W927 17:43:43.378538640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.45/9.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.45/9.65 [W927 17:43:43.378576890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.45/9.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.45/9.65 [W927 17:43:43.378583249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.45/9.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.45/9.65 [W927 17:43:43.378596310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378601597 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378616880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378622526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378635872 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378642677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378655722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.378661169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 % (2617930)Refutation not found, incomplete strategy % 66.60/10.06 % (2617930)------------------------------ % 66.60/10.06 % (2617930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.60/10.06 % (2617930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.60/10.06 % (2617930)CaDiCaL version: 2.1.3 % 66.60/10.06 % (2617930)Termination reason: Refutation not found, incomplete strategy % 66.60/10.06 % (2617930)Time elapsed: 0.324 s % 66.60/10.06 % (2617930)Peak memory usage: 129 MB % 66.60/10.06 % (2617930)Instructions burned: 870 (million) % 66.60/10.06 [W927 17:43:43.498969287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.498991502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.499038660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.499045458 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.60/10.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.60/10.06 [W927 17:43:43.499060988 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499067484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499081470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499095394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499110090 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499115884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499129004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 [W927 17:43:43.499134726 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.89/10.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.89/10.43 % (2617932)Refutation not found, incomplete strategy % 68.89/10.43 % (2617932)------------------------------ % 68.89/10.43 % (2617932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.89/10.43 % (2617932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.89/10.43 % (2617932)CaDiCaL version: 2.1.3 % 68.89/10.43 % (2617932)Termination reason: Refutation not found, incomplete strategy % 68.89/10.43 % (2617932)Time elapsed: 0.309 s % 68.89/10.43 % (2617932)Peak memory usage: 128 MB % 68.89/10.43 % (2617932)Instructions burned: 841 (million) % 68.89/10.43 % (2617930)------------------------------ % 68.89/10.43 % (2617930)------------------------------ % 68.89/10.43 % (2617932)------------------------------ % 68.89/10.43 % (2617932)------------------------------ % 68.89/10.43 % (2617937)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3191243957:i=13942:kws=frequency_2911 on theBenchmark for (2911ds/13942Mi) % 68.89/10.43 % (2617934)Refutation not found, incomplete strategy % 68.89/10.43 % (2617934)------------------------------ % 68.89/10.43 % (2617934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.89/10.43 % (2617934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.89/10.43 % (2617934)CaDiCaL version: 2.1.3 % 68.89/10.43 % (2617934)Termination reason: Refutation not found, incomplete strategy % 68.89/10.43 % (2617934)Time elapsed: 0.412 s % 68.89/10.43 % (2617934)Peak memory usage: 149 MB % 68.89/10.43 % (2617934)Instructions burned: 1098 (million) % 68.89/10.43 % (2617938)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=1774781633:i=3604:fsr=off:er=filter_2910 on theBenchmark for (2910ds/3604Mi) % 73.64/11.04 % (2617934)------------------------------ % 73.64/11.04 % (2617934)------------------------------ % 73.64/11.04 % (2617941)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2749299071:i=1876:sd=1:ss=included:sgt=32_2908 on theBenchmark for (2908ds/1876Mi) % 73.64/11.04 [W927 17:43:44.279207233 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279229824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279250434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279257665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279271902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279278089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279291854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279298061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279311374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279317434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279330898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 [W927 17:43:44.279337074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.64/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.64/11.04 % (2617915)Instruction limit reached! % 73.64/11.04 % (2617915)------------------------------ % 81.95/12.21 % (2617915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.95/12.21 % (2617915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.95/12.21 % (2617915)CaDiCaL version: 2.1.3 % 81.95/12.21 % (2617915)Termination reason: Instruction limit % 81.95/12.21 % (2617915)Termination phase: Saturation % 81.95/12.21 % (2617915)Time elapsed: 3.314 s % 81.95/12.21 % (2617915)Peak memory usage: 188 MB % 81.95/12.21 % (2617915)Instructions burned: 9533 (million) % 81.95/12.21 % (2617941)Refutation not found, incomplete strategy % 81.95/12.21 % (2617941)------------------------------ % 81.95/12.21 % (2617941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.95/12.21 % (2617941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.95/12.21 % (2617941)CaDiCaL version: 2.1.3 % 81.95/12.21 % (2617941)Termination reason: Refutation not found, incomplete strategy % 81.95/12.21 % (2617941)Time elapsed: 0.312 s % 81.95/12.21 % (2617941)Peak memory usage: 129 MB % 81.95/12.21 % (2617941)Instructions burned: 841 (million) % 81.95/12.21 % (2617943)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2364849362:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2904 on theBenchmark for (2904ds/1932Mi) % 81.95/12.21 % (2617941)------------------------------ % 81.95/12.21 % (2617941)------------------------------ % 81.95/12.21 [W927 17:43:45.665242828 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665263868 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665285238 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665292035 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665307115 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665313319 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665327481 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665333681 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.95/12.21 [W927 17:43:45.665347332 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.665353479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.665372095 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.665414505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 % (2617945)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=3752333727:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2902 on theBenchmark for (2902ds/1980Mi) % 88.39/13.12 % (2617943)Refutation not found, incomplete strategy % 88.39/13.12 % (2617943)------------------------------ % 88.39/13.12 % (2617943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.39/13.12 % (2617943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.39/13.12 % (2617943)CaDiCaL version: 2.1.3 % 88.39/13.12 % (2617943)Termination reason: Refutation not found, incomplete strategy % 88.39/13.12 % (2617943)Time elapsed: 0.316 s % 88.39/13.12 % (2617943)Peak memory usage: 128 MB % 88.39/13.12 % (2617943)Instructions burned: 841 (million) % 88.39/13.12 % (2617943)------------------------------ % 88.39/13.12 % (2617943)------------------------------ % 88.39/13.12 % (2617938)Instruction limit reached! % 88.39/13.12 % (2617938)------------------------------ % 88.39/13.12 % (2617938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.39/13.12 % (2617938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.39/13.12 % (2617938)CaDiCaL version: 2.1.3 % 88.39/13.12 % (2617938)Termination reason: Instruction limit % 88.39/13.12 % (2617938)Termination phase: Saturation % 88.39/13.12 % (2617938)Time elapsed: 1.148 s % 88.39/13.12 % (2617938)Peak memory usage: 153 MB % 88.39/13.12 % (2617938)Instructions burned: 3609 (million) % 88.39/13.12 % (2617947)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=740517822:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2898 on theBenchmark for (2898ds/3902Mi) % 88.39/13.12 % (2617948)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1601414430:avsq=on:i=3916:aac=none:amm=off_2897 on theBenchmark for (2897ds/3916Mi) % 88.39/13.12 [W927 17:43:45.282517041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.282555934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.282576999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.282583444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.39/13.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.39/13.12 [W927 17:43:45.282597817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282604678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282624445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282639311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282653481 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282658924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282671395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 [W927 17:43:45.282676740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.55/14.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.55/14.31 % (2617945)Instruction limit reached! % 96.55/14.31 % (2617945)------------------------------ % 96.55/14.31 % (2617945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.55/14.31 % (2617945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.55/14.31 % (2617945)CaDiCaL version: 2.1.3 % 96.55/14.31 % (2617945)Termination reason: Instruction limit % 96.55/14.31 % (2617945)Termination phase: Saturation % 96.55/14.31 % (2617945)Time elapsed: 0.685 s % 96.55/14.31 % (2617945)Peak memory usage: 155 MB % 96.55/14.31 % (2617945)Instructions burned: 1983 (million) % 96.55/14.31 % (2617947)Refutation not found, incomplete strategy % 96.55/14.31 % (2617947)------------------------------ % 96.55/14.31 % (2617947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.55/14.31 % (2617947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.55/14.31 % (2617947)CaDiCaL version: 2.1.3 % 96.55/14.31 % (2617947)Termination reason: Refutation not found, incomplete strategy % 96.55/14.31 % (2617947)Time elapsed: 0.314 s % 96.55/14.31 % (2617947)Peak memory usage: 128 MB % 96.55/14.31 % (2617947)Instructions burned: 845 (million) % 96.55/14.31 % (2617951)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3581753986:cond=on:i=3940:av=off:er=known_2894 on theBenchmark for (2894ds/3940Mi) % 96.55/14.31 % (2617947)------------------------------ % 96.55/14.31 % (2617947)------------------------------ % 96.55/14.31 % (2617953)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=201193963:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2892 on theBenchmark for (2892ds/3980Mi) % 96.55/14.31 % (2617948)Instruction limit reached! % 96.55/14.31 % (2617948)------------------------------ % 96.55/14.31 % (2617948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.29/14.77 % (2617948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.29/14.77 % (2617948)CaDiCaL version: 2.1.3 % 98.29/14.77 % (2617948)Termination reason: Instruction limit % 98.29/14.77 % (2617948)Termination phase: Saturation % 98.29/14.77 % (2617948)Time elapsed: 1.275 s % 98.29/14.77 % (2617948)Peak memory usage: 129 MB % 98.29/14.77 % (2617948)Instructions burned: 3916 (million) % 98.29/14.77 % (2617955)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1294033965:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2883 on theBenchmark for (2883ds/2087Mi) % 98.29/14.77 % (2617951)Instruction limit reached! % 98.29/14.77 % (2617951)------------------------------ % 98.29/14.77 % (2617951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.29/14.77 % (2617951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.29/14.77 % (2617951)CaDiCaL version: 2.1.3 % 98.29/14.77 % (2617951)Termination reason: Instruction limit % 98.29/14.77 % (2617951)Termination phase: Saturation % 98.29/14.77 % (2617951)Time elapsed: 1.270 s % 98.29/14.77 % (2617951)Peak memory usage: 158 MB % 98.29/14.77 % (2617951)Instructions burned: 3943 (million) % 98.29/14.77 % (2617957)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=996566399:cts=off:cond=on:i=4272:bs=on:fsd=on_2879 on theBenchmark for (2879ds/4272Mi) % 98.29/14.77 % (2617953)Instruction limit reached! % 98.29/14.77 % (2617953)------------------------------ % 98.29/14.77 % (2617953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.29/14.77 % (2617953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.29/14.77 % (2617953)CaDiCaL version: 2.1.3 % 98.29/14.77 % (2617953)Termination reason: Instruction limit % 98.29/14.77 % (2617953)Termination phase: Saturation % 98.29/14.77 % (2617953)Time elapsed: 1.320 s % 98.29/14.77 % (2617953)Peak memory usage: 163 MB % 98.29/14.77 % (2617953)Instructions burned: 3981 (million) % 98.29/14.77 % (2617959)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=324419141:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2877 on theBenchmark for (2877ds/2197Mi) % 98.29/14.77 % (2617955)Instruction limit reached! % 98.29/14.77 % (2617955)------------------------------ % 98.29/14.77 % (2617955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.29/14.77 % (2617955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.29/14.77 % (2617955)CaDiCaL version: 2.1.3 % 98.29/14.77 % (2617955)Termination reason: Instruction limit % 98.29/14.77 % (2617955)Termination phase: Saturation % 98.29/14.77 % (2617955)Time elapsed: 0.731 s % 98.29/14.77 % (2617955)Peak memory usage: 150 MB % 98.29/14.77 % (2617955)Instructions burned: 2089 (million) % 98.29/14.77 [W927 17:43:47.355682768 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.29/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.29/14.77 [W927 17:43:47.355740140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.29/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.29/14.77 [W927 17:43:47.355765723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.29/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.29/14.77 [W927 17:43:47.355777842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.29/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.29/14.77 [W927 17:43:47.355793157 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355798643 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355812537 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355818253 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355831600 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355837365 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355850483 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 [W927 17:43:47.355856177 register_special_ops.cpp:225] Warning: Creating a tensor from 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.75/16.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.75/16.03 % (2617961)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2417022989:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2874 on theBenchmark for (2874ds/6508Mi) % 108.75/16.03 % (2617959)Refutation not found, incomplete strategy % 108.75/16.03 % (2617959)------------------------------ % 108.75/16.03 % (2617959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.75/16.03 % (2617959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.75/16.03 % (2617959)CaDiCaL version: 2.1.3 % 108.75/16.03 % (2617959)Termination reason: Refutation not found, incomplete strategy % 108.75/16.03 % (2617959)Time elapsed: 0.316 s % 108.75/16.03 % (2617959)Peak memory usage: 127 MB % 108.75/16.03 % (2617959)Instructions burned: 846 (million) % 108.75/16.03 % (2617959)------------------------------ % 108.75/16.03 % (2617959)------------------------------ % 108.75/16.03 % (2617963)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2166729546:i=2330:fgj=on:av=off:fsr=off_2871 on theBenchmark for (2871ds/2330Mi) % 108.75/16.03 % (2617957)Instruction limit reached! % 108.75/16.03 % (2617957)------------------------------ % 108.75/16.03 % (2617957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.75/16.03 % (2617957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.75/16.03 % (2617957)CaDiCaL version: 2.1.3 % 108.75/16.03 % (2617957)Termination reason: Instruction limit % 108.75/16.03 % (2617957)Termination phase: Saturation % 108.75/16.03 % (2617957)Time elapsed: 1.411 s % 108.75/16.03 % (2617957)Peak memory usage: 159 MB % 108.75/16.03 % (2617957)Instructions burned: 4273 (million) % 108.75/16.03 % (2617965)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=390860961:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2864 on theBenchmark for (2864ds/7592Mi) % 108.75/16.03 % (2617963)Instruction limit reached! % 108.75/16.03 % (2617963)------------------------------ % 110.00/16.25 % (2617963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.00/16.25 % (2617963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.00/16.25 % (2617963)CaDiCaL version: 2.1.3 % 110.00/16.25 % (2617963)Termination reason: Instruction limit % 110.00/16.25 % (2617963)Termination phase: Saturation % 110.00/16.25 % (2617963)Time elapsed: 0.796 s % 110.00/16.25 % (2617963)Peak memory usage: 154 MB % 110.00/16.25 % (2617963)Instructions burned: 2330 (million) % 110.00/16.25 % (2617937)Instruction limit reached! % 110.00/16.25 % (2617937)------------------------------ % 110.00/16.25 % (2617937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.00/16.25 % (2617937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.00/16.25 % (2617937)CaDiCaL version: 2.1.3 % 110.00/16.25 % (2617937)Termination reason: Instruction limit % 110.00/16.25 % (2617937)Termination phase: Saturation % 110.00/16.25 % (2617937)Time elapsed: 4.837 s % 110.00/16.25 % (2617937)Peak memory usage: 243 MB % 110.00/16.25 % (2617937)Instructions burned: 13944 (million) % 110.00/16.25 % (2617967)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3570984872:i=2693:kws=precedence:ins=1:av=off_2862 on theBenchmark for (2862ds/2693Mi) % 110.00/16.25 % (2617968)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2240353878:i=28651:sd=4:ss=included:sgt=64_2861 on theBenchmark for (2861ds/28651Mi) % 110.00/16.25 [W927 17:43:49.003566644 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003590791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003612043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003619346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003633382 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003639606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003654043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003660267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.00/16.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.00/16.25 [W927 17:43:49.003673816 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.17/16.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.17/16.48 [W927 17:43:49.003680083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.17/16.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.17/16.48 [W927 17:43:49.003692989 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.17/16.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.17/16.48 [W927 17:43:49.003705182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.17/16.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.17/16.48 % (2617968)Refutation not found, incomplete strategy % 111.17/16.48 % (2617968)------------------------------ % 111.17/16.48 % (2617968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.17/16.48 % (2617968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.17/16.48 % (2617968)CaDiCaL version: 2.1.3 % 111.17/16.48 % (2617968)Termination reason: Refutation not found, incomplete strategy % 111.17/16.48 % (2617968)Time elapsed: 0.347 s % 111.17/16.48 % (2617968)Peak memory usage: 128 MB % 111.17/16.48 % (2617968)Instructions burned: 841 (million) % 111.17/16.48 % (2617968)------------------------------ % 111.17/16.48 % (2617968)------------------------------ % 111.17/16.48 % (2617971)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3132661203:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2855 on theBenchmark for (2855ds/2700Mi) % 111.17/16.48 % (2617961)Instruction limit reached! % 111.17/16.48 % (2617961)------------------------------ % 111.17/16.48 % (2617961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.17/16.48 % (2617961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.17/16.48 % (2617961)CaDiCaL version: 2.1.3 % 111.17/16.48 % (2617961)Termination reason: Instruction limit % 111.17/16.48 % (2617961)Termination phase: Saturation % 111.17/16.48 % (2617961)Time elapsed: 1.960 s % 111.17/16.48 % (2617961)Peak memory usage: 130 MB % 111.17/16.48 % (2617961)Instructions burned: 6508 (million) % 111.17/16.48 % (2617973)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=4268527491:i=3196:nm=4_2853 on theBenchmark for (2853ds/3196Mi) % 111.17/16.48 % (2617967)Instruction limit reached! % 111.17/16.48 % (2617967)------------------------------ % 111.17/16.48 % (2617967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.17/16.48 % (2617967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.17/16.48 % (2617967)CaDiCaL version: 2.1.3 % 111.17/16.48 % (2617967)Termination reason: Instruction limit % 111.17/16.48 % (2617967)Termination phase: Saturation % 111.17/16.48 % (2617967)Time elapsed: 0.954 s % 111.17/16.48 % (2617967)Peak memory usage: 155 MB % 111.17/16.48 % (2617967)Instructions burned: 2696 (million) % 111.17/16.48 % (2617975)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=262492430:cts=off:i=3254:av=off_2851 on theBenchmark for (2851ds/3254Mi) % 111.17/16.48 % (2617973)Refutation not found, incomplete strategy % 111.17/16.48 % (2617973)------------------------------ % 111.17/16.48 % (2617973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.17/16.48 % (2617973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.17/16.48 % (2617973)CaDiCaL version: 2.1.3 % 111.17/16.48 % (2617973)Termination reason: Refutation not found, incomplete strategy % 111.17/16.48 % (2617973)Time elapsed: 0.419 s % 111.17/16.48 % (2617973)Peak memory usage: 138 MB % 111.17/16.48 % (2617973)Instructions burned: 1178 (million) % 111.17/16.48 % (2617973)------------------------------ % 111.17/16.48 % (2617973)------------------------------ % 111.17/16.48 % (2617977)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1579144751:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2846 on theBenchmark for (2846ds/3264Mi) % 121.23/18.14 % (2617971)Instruction limit reached! % 121.23/18.14 % (2617971)------------------------------ % 121.23/18.14 % (2617971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.23/18.14 % (2617971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.23/18.14 % (2617971)CaDiCaL version: 2.1.3 % 121.23/18.14 % (2617971)Termination reason: Instruction limit % 121.23/18.14 % (2617971)Termination phase: Saturation % 121.23/18.14 % (2617971)Time elapsed: 0.962 s % 121.23/18.14 % (2617971)Peak memory usage: 158 MB % 121.23/18.14 % (2617971)Instructions burned: 2701 (million) % 121.23/18.14 [W927 17:43:50.491987138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492032338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492052908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492058839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492071774 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492078094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492092107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492098184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492112624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492118824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492132294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.23/18.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.23/18.14 [W927 17:43:50.492138688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 % (2617979)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=3546145913:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2844 on theBenchmark for (2844ds/9708Mi) % 126.27/18.95 % (2617977)Refutation not found, incomplete strategy % 126.27/18.95 % (2617977)------------------------------ % 126.27/18.95 % (2617977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.27/18.95 % (2617977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.27/18.95 % (2617977)CaDiCaL version: 2.1.3 % 126.27/18.95 % (2617977)Termination reason: Refutation not found, incomplete strategy % 126.27/18.95 % (2617977)Time elapsed: 0.321 s % 126.27/18.95 % (2617977)Peak memory usage: 129 MB % 126.27/18.95 % (2617977)Instructions burned: 886 (million) % 126.27/18.95 [W927 17:43:51.721868647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721905266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721931712 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721937523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721951002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721957365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721970482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721976392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721989768 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.27/18.95 [W927 17:43:51.721995720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.27/18.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.32/21.64 [W927 17:43:51.722031455 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.32/21.64 [W927 17:43:51.722037593 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.32/21.64 % (2617979)Refutation not found, incomplete strategy % 145.32/21.64 % (2617979)------------------------------ % 145.32/21.64 % (2617979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.32/21.64 % (2617979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.32/21.64 % (2617979)CaDiCaL version: 2.1.3 % 145.32/21.64 % (2617979)Termination reason: Refutation not found, incomplete strategy % 145.32/21.64 % (2617979)Time elapsed: 0.318 s % 145.32/21.64 % (2617979)Peak memory usage: 129 MB % 145.32/21.64 % (2617979)Instructions burned: 849 (million) % 145.32/21.64 % (2617975)Instruction limit reached! % 145.32/21.64 % (2617975)------------------------------ % 145.32/21.64 % (2617975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.32/21.64 % (2617975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.32/21.64 % (2617975)CaDiCaL version: 2.1.3 % 145.32/21.64 % (2617975)Termination reason: Instruction limit % 145.32/21.64 % (2617975)Termination phase: Saturation % 145.32/21.64 % (2617975)Time elapsed: 1.081 s % 145.32/21.64 % (2617975)Peak memory usage: 155 MB % 145.32/21.64 % (2617975)Instructions burned: 3255 (million) % 145.32/21.64 % (2617981)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3173095642:i=21997:s2at=5:gtg=all_2839 on theBenchmark for (2839ds/21997Mi) % 145.32/21.64 % (2617965)Instruction limit reached! % 145.32/21.64 % (2617965)------------------------------ % 145.32/21.64 % (2617965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.32/21.64 % (2617965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.32/21.64 % (2617965)CaDiCaL version: 2.1.3 % 145.32/21.64 % (2617965)Termination reason: Instruction limit % 145.32/21.64 % (2617965)Termination phase: Saturation % 145.32/21.64 % (2617965)Time elapsed: 2.620 s % 145.32/21.64 % (2617965)Peak memory usage: 135 MB % 145.32/21.64 % (2617965)Instructions burned: 7592 (million) % 145.32/21.64 % (2617983)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3115957174:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2836 on theBenchmark for (2836ds/7551Mi) % 145.32/21.64 % (2617977)------------------------------ % 145.32/21.64 % (2617977)------------------------------ % 145.32/21.64 % (2617979)------------------------------ % 145.32/21.64 % (2617979)------------------------------ % 145.32/21.64 % (2617986)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=4277760813:i=9638:kws=frequency:bd=preordered_2835 on theBenchmark for (2835ds/9638Mi) % 145.32/21.64 % (2617985)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2031115769:i=8924:sd=1:ss=included_2835 on theBenchmark for (2835ds/8924Mi) % 145.32/21.64 [W927 17:43:52.379861489 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.32/21.64 [W927 17:43:52.379882944 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.32/21.64 [W927 17:43:52.379920652 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/21.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379926740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379939776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379956566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379971109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379976496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379989131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.379994448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.380013881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 [W927 17:43:52.380019869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.74/24.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.74/24.55 % (2617985)Refutation not found, incomplete strategy % 165.74/24.55 % (2617985)------------------------------ % 165.74/24.55 % (2617985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.74/24.55 % (2617985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.74/24.55 % (2617985)CaDiCaL version: 2.1.3 % 165.74/24.55 % (2617985)Termination reason: Refutation not found, incomplete strategy % 165.74/24.55 % (2617985)Time elapsed: 1.109 s % 165.74/24.55 % (2617985)Peak memory usage: 127 MB % 165.74/24.55 % (2617985)Instructions burned: 842 (million) % 165.74/24.55 % (2617985)------------------------------ % 165.74/24.55 % (2617985)------------------------------ % 165.74/24.55 % (2617989)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=2984280707:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2821 on theBenchmark for (2821ds/5177Mi) % 165.74/24.55 % (2617989)Refutation not found, incomplete strategy % 165.74/24.55 % (2617989)------------------------------ % 165.74/24.55 % (2617989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.74/24.55 % (2617989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.74/24.55 % (2617989)CaDiCaL version: 2.1.3 % 165.74/24.55 % (2617989)Termination reason: Refutation not found, incomplete strategy % 165.74/24.55 % (2617989)Time elapsed: 0.417 s % 184.74/27.64 % (2617989)Peak memory usage: 151 MB % 184.74/27.64 % (2617989)Instructions burned: 1147 (million) % 184.74/27.64 % (2617983)Instruction limit reached! % 184.74/27.64 % (2617983)------------------------------ % 184.74/27.64 % (2617983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.74/27.64 % (2617983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.74/27.64 % (2617983)CaDiCaL version: 2.1.3 % 184.74/27.64 % (2617983)Termination reason: Instruction limit % 184.74/27.64 % (2617983)Termination phase: Saturation % 184.74/27.64 % (2617983)Time elapsed: 2.043 s % 184.74/27.64 % (2617983)Peak memory usage: 117 MB % 184.74/27.64 % (2617983)Instructions burned: 7554 (million) % 184.74/27.64 % (2617989)------------------------------ % 184.74/27.64 % (2617989)------------------------------ % 184.74/27.64 % (2617991)lrs-1011_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:sas=cadical:sp=unary_first:acc=on:alpa=false:random_seed=3735862863:i=6464:aac=none:ins=10_2815 on theBenchmark for (2815ds/6464Mi) % 184.74/27.64 % (2617992)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=3577155008:i=19192:av=off_2814 on theBenchmark for (2814ds/19192Mi) % 184.74/27.64 % (2617986)Instruction limit reached! % 184.74/27.64 % (2617986)------------------------------ % 184.74/27.64 % (2617986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.74/27.64 % (2617986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.74/27.64 % (2617986)CaDiCaL version: 2.1.3 % 184.74/27.64 % (2617986)Termination reason: Instruction limit % 184.74/27.64 % (2617986)Termination phase: Saturation % 184.74/27.64 % (2617986)Time elapsed: 4.136 s % 184.74/27.64 % (2617986)Peak memory usage: 196 MB % 184.74/27.64 % (2617986)Instructions burned: 9641 (million) % 184.74/27.64 % (2617995)lrs+10_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=8000:npcc=on:prc=on:fde=unused:sp=const_min:random_seed=1304770327:i=7136:fgj=on:bd=preordered:ins=3:ss=included_2792 on theBenchmark for (2792ds/7136Mi) % 184.74/27.64 % (2617991)Instruction limit reached! % 184.74/27.64 % (2617991)------------------------------ % 184.74/27.64 % (2617991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.74/27.64 % (2617991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.74/27.64 % (2617991)CaDiCaL version: 2.1.3 % 184.74/27.64 % (2617991)Termination reason: Instruction limit % 184.74/27.64 % (2617991)Termination phase: Saturation % 184.74/27.64 % (2617991)Time elapsed: 2.274 s % 184.74/27.64 % (2617991)Peak memory usage: 183 MB % 184.74/27.64 % (2617991)Instructions burned: 6465 (million) % 184.74/27.64 % (2617997)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2569603109:cts=off:cond=on:i=7540:bs=on:fsd=on_2790 on theBenchmark for (2790ds/7540Mi) % 184.74/27.64 [W927 17:43:56.876836759 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 184.74/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 184.74/27.64 [W927 17:43:56.876857769 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 184.74/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 184.74/27.64 [W927 17:43:56.876879358 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 184.74/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 184.74/27.64 [W927 17:43:56.876886828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 184.74/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 184.74/27.64 [W927 17:43:56.876901235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.876907508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.876920915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.876926518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.876939478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.876979792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.877006082 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 [W927 17:43:56.877012967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 214.15/31.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 214.15/31.34 % (2617995)Refutation not found, incomplete strategy % 214.15/31.34 % (2617995)------------------------------ % 214.15/31.34 % (2617995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.15/31.34 % (2617995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.15/31.34 % (2617995)CaDiCaL version: 2.1.3 % 214.15/31.34 % (2617995)Termination reason: Refutation not found, incomplete strategy % 214.15/31.34 % (2617995)Time elapsed: 0.313 s % 214.15/31.34 % (2617995)Peak memory usage: 128 MB % 214.15/31.34 % (2617995)Instructions burned: 847 (million) % 214.15/31.34 % (2617995)------------------------------ % 214.15/31.34 % (2617995)------------------------------ % 214.15/31.34 % (2617999)ott+1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=64000:tgt=ground:npcc=on:drc=off:sp=const_frequency:random_seed=3172920168:i=15570:s2at=5:gtgl=4:gtg=exists_sym_2786 on theBenchmark for (2786ds/15570Mi) % 214.15/31.34 % (2617997)Instruction limit reached! % 214.15/31.34 % (2617997)------------------------------ % 214.15/31.34 % (2617997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.15/31.34 % (2617997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.15/31.34 % (2617997)CaDiCaL version: 2.1.3 % 214.15/31.34 % (2617997)Termination reason: Instruction limit % 214.15/31.34 % (2617997)Termination phase: Saturation % 214.15/31.34 % (2617997)Time elapsed: 2.415 s % 214.15/31.34 % (2617997)Peak memory usage: 175 MB % 214.15/31.34 % (2617997)Instructions burned: 7541 (million) % 214.15/31.34 % (2618001)lrs+1011_1_anc=none:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lsd=20:bce=on:bsr=on:fd=preordered:gs=on:random_seed=2384883418:i=15957:add=on:fgj=on_2765 on theBenchmark for (2765ds/15957Mi) % 214.15/31.34 % (2617981)Instruction limit reached! % 214.15/31.34 % (2617981)------------------------------ % 214.15/31.34 % (2617981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.15/31.34 % (2617981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.57/34.29 % (2617981)CaDiCaL version: 2.1.3 % 234.57/34.29 % (2617981)Termination reason: Instruction limit % 234.57/34.29 % (2617981)Termination phase: Saturation % 234.57/34.29 % (2617981)Time elapsed: 7.782 s % 234.57/34.29 % (2617981)Peak memory usage: 279 MB % 234.57/34.29 % (2617981)Instructions burned: 21997 (million) % 234.57/34.29 % (2618003)lrs+1010_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=32000:tgt=full:npcc=on:prc=on:drc=ordering:fde=none:sp=arity:spb=intro:urr=ec_only:s2agt=40:random_seed=1978549260:cond=on:i=8289:erml=3:bd=preordered:er=filter:proc=on_2759 on theBenchmark for (2759ds/8289Mi) % 234.57/34.29 % (2617992)Instruction limit reached! % 234.57/34.29 % (2617992)------------------------------ % 234.57/34.29 % (2617992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.57/34.29 % (2617992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.57/34.29 % (2617992)CaDiCaL version: 2.1.3 % 234.57/34.29 % (2617992)Termination reason: Instruction limit % 234.57/34.29 % (2617992)Termination phase: Saturation % 234.57/34.29 % (2617992)Time elapsed: 6.067 s % 234.57/34.29 % (2617992)Peak memory usage: 257 MB % 234.57/34.29 % (2617992)Instructions burned: 19193 (million) % 234.57/34.29 % (2618005)lrs+4_4_to=lpo:sil=128000:flr=on:sac=on:lwlo=on:random_seed=3461827293:i=16865:nicw=on:bs=unit_only_2751 on theBenchmark for (2751ds/16865Mi) % 234.57/34.29 % (2617999)Instruction limit reached! % 234.57/34.29 % (2617999)------------------------------ % 234.57/34.29 % (2617999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.57/34.29 % (2617999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.57/34.29 % (2617999)CaDiCaL version: 2.1.3 % 234.57/34.29 % (2617999)Termination reason: Instruction limit % 234.57/34.29 % (2617999)Termination phase: Saturation % 234.57/34.29 % (2617999)Time elapsed: 5.237 s % 234.57/34.29 % (2617999)Peak memory usage: 244 MB % 234.57/34.29 % (2617999)Instructions burned: 15571 (million) % 234.57/34.29 % (2618007)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3518130721:i=67727:sd=2:fgj=on:ss=axioms:sgt=64_2732 on theBenchmark for (2732ds/67727Mi) % 234.57/34.29 % (2618003)Instruction limit reached! % 234.57/34.29 % (2618003)------------------------------ % 234.57/34.29 % (2618003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.57/34.29 % (2618003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.57/34.29 % (2618003)CaDiCaL version: 2.1.3 % 234.57/34.29 % (2618003)Termination reason: Instruction limit % 234.57/34.29 % (2618003)Termination phase: Saturation % 234.57/34.29 % (2618003)Time elapsed: 2.885 s % 234.57/34.29 % (2618003)Peak memory usage: 204 MB % 234.57/34.29 % (2618003)Instructions burned: 8291 (million) % 234.57/34.29 [W927 17:44:02.874568870 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/34.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.57/34.29 [W927 17:44:02.874607796 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/34.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.57/34.29 [W927 17:44:02.874629256 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/34.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.57/34.29 [W927 17:44:02.874635624 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/34.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.57/34.29 [W927 17:44:02.874649034 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/34.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874655774 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874670020 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874685255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874699520 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874705229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874718960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 [W927 17:44:02.874724352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 258.94/37.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 258.94/37.71 % (2618007)Refutation not found, incomplete strategy % 258.94/37.71 % (2618007)------------------------------ % 258.94/37.71 % (2618007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.94/37.71 % (2618007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.94/37.71 % (2618007)CaDiCaL version: 2.1.3 % 258.94/37.71 % (2618007)Termination reason: Refutation not found, incomplete strategy % 258.94/37.71 % (2618007)Time elapsed: 0.314 s % 258.94/37.71 % (2618007)Peak memory usage: 127 MB % 258.94/37.71 % (2618007)Instructions burned: 844 (million) % 258.94/37.71 % (2618009)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1347116043:cond=on:i=17955:s2at=3:aac=none:fsd=on_2729 on theBenchmark for (2729ds/17955Mi) % 258.94/37.71 % (2618007)------------------------------ % 258.94/37.71 % (2618007)------------------------------ % 258.94/37.71 % (2618011)dis-1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:irw=on:npcc=on:sac=on:random_seed=2442681963:i=10108:bd=preordered_2726 on theBenchmark for (2726ds/10108Mi) % 258.94/37.71 % (2618001)Instruction limit reached! % 258.94/37.71 % (2618001)------------------------------ % 258.94/37.71 % (2618001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.94/37.71 % (2618001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.94/37.71 % (2618001)CaDiCaL version: 2.1.3 % 258.94/37.71 % (2618001)Termination reason: Instruction limit % 258.94/37.71 % (2618001)Termination phase: Saturation % 258.94/37.71 % (2618001)Time elapsed: 5.265 s % 258.94/37.71 % (2618001)Peak memory usage: 243 MB % 258.94/37.71 % (2618001)Instructions burned: 15960 (million) % 258.94/37.71 % (2618013)lrs+2_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:spb=goal:lcm=predicate:random_seed=1999621184:i=10307:kws=inv_arity_2711 on theBenchmark for (2711ds/10307Mi) % 258.94/37.71 % (2618011)Instruction limit reached! % 258.94/37.71 % (2618011)------------------------------ % 258.94/37.71 % (2618011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.94/37.71 % (2618011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2618011)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2618011)Termination reason: Instruction limit % 233.73/39.74 % (2618011)Termination phase: Saturation % 233.73/39.74 % (2618011)Time elapsed: 3.302 s % 233.73/39.74 % (2618011)Peak memory usage: 207 MB % 233.73/39.74 % (2618011)Instructions burned: 10108 (million) % 233.73/39.74 % (2618015)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1081402443:i=25534:bd=all_2691 on theBenchmark for (2691ds/25534Mi) % 233.73/39.74 % (2618005)Instruction limit reached! % 233.73/39.74 % (2618005)------------------------------ % 233.73/39.74 % (2618005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.73/39.74 % (2618005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2618005)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2618005)Termination reason: Instruction limit % 233.73/39.74 % (2618005)Termination phase: Saturation % 233.73/39.74 % (2618005)Time elapsed: 6.052 s % 233.73/39.74 % (2618005)Peak memory usage: 191 MB % 233.73/39.74 % (2618005)Instructions burned: 16865 (million) % 233.73/39.74 % (2618017)lrs+31_1_ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:random_seed=3242551288:i=12907:kws=precedence_2689 on theBenchmark for (2689ds/12907Mi) % 233.73/39.74 % (2618009)Instruction limit reached! % 233.73/39.74 % (2618009)------------------------------ % 233.73/39.74 % (2618009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.73/39.74 % (2618009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2618009)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2618009)Termination reason: Instruction limit % 233.73/39.74 % (2618009)Termination phase: Saturation % 233.73/39.74 % (2618009)Time elapsed: 5.161 s % 233.73/39.74 % (2618009)Peak memory usage: 184 MB % 233.73/39.74 % (2618009)Instructions burned: 17956 (million) % 233.73/39.74 % (2618013)Instruction limit reached! % 233.73/39.74 % (2618013)------------------------------ % 233.73/39.74 % (2618013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.73/39.74 % (2618013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2618013)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2618013)Termination reason: Instruction limit % 233.73/39.74 % (2618013)Termination phase: Saturation % 233.73/39.74 % (2618013)Time elapsed: 3.415 s % 233.73/39.74 % (2618013)Peak memory usage: 216 MB % 233.73/39.74 % (2618013)Instructions burned: 10307 (million) % 233.73/39.74 % (2618019)dis+11_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=unary_first:lcm=reverse:urr=on:gs=on:s2agt=64:br=off:random_seed=3202641883:i=14634:s2at=20:av=off:fsr=off_2676 on theBenchmark for (2676ds/14634Mi) % 233.73/39.74 % (2618020)lrs-1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=goal_then_units:urr=on:br=off:flr=on:random_seed=1985289760:i=14826:s2at=5:gtgl=2:gtg=exists_sym:fdi=4:er=filter_2675 on theBenchmark for (2675ds/14826Mi) % 233.73/39.74 % (2618020)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 233.73/39.74 % (2618020)------------------------------ % 233.73/39.74 % (2618020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.73/39.74 % (2618020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2618020)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2618020)Termination reason: Unknown % 233.73/39.74 % (2618020)Termination phase: Saturation % 233.73/39.74 % (2618020)Time elapsed: 0.571 s % 233.73/39.74 % (2618020)Peak memory usage: 155 MB % 233.73/39.74 % (2618020)Instructions burned: 1743 (million) % 233.73/39.74 % (2618023)ott+1011_16_slsqr=800179,524288:sil=16000:lsd=1:slsq=on:random_seed=2698671768:i=16431:aac=none:slsql=off:nicw=on:bs=unit_only:fsr=off_2668 on theBenchmark for (2668ds/16431Mi) % 233.73/39.74 % (2617829)Instruction limit reached! % 233.73/39.74 % (2617829)------------------------------ % 233.73/39.74 % (2617829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.73/39.74 % (2617829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/39.74 % (2617829)CaDiCaL version: 2.1.3 % 233.73/39.74 % (2617829)Termination reason: Instruction limit % 233.73/39.74 % (2617829)Termination phase: Saturation % 233.73/39.74 % (2617829)Time elapsed: 33.449 s % 233.73/39.74 % (2617829)Peak memory usage: 211 MB % 233.73/39.74 % (2617829)Instructions burned: 137899 (million) % 233.73/39.74 % (2618025)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sas=cadical:sp=arity:spb=units:lsd=1:acc=on:urr=ec_only:fd=preordered:gs=on:s2agt=16:random_seed=2288293613:i=17138:aac=none:fgj=on:bd=all:fsr=off_2663 on theBenchmark for (2663ds/17138Mi) % 275.60/40.07 % (2618017)Instruction limit reached! % 275.60/40.07 % (2618017)------------------------------ % 275.60/40.07 % (2618017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/40.07 % (2618017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/40.07 % (2618017)CaDiCaL version: 2.1.3 % 275.60/40.07 % (2618017)Termination reason: Instruction limit % 275.60/40.07 % (2618017)Termination phase: Saturation % 275.60/40.07 % (2618017)Time elapsed: 4.268 s % 275.60/40.07 % (2618017)Peak memory usage: 232 MB % 275.60/40.07 % (2618017)Instructions burned: 12907 (million) % 275.60/40.07 % (2618027)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4138090691:i=19809:bd=all_2645 on theBenchmark for (2645ds/19809Mi) % 275.60/40.07 % (2618019)Instruction limit reached! % 275.60/40.07 % (2618019)------------------------------ % 275.60/40.07 % (2618019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.60/40.07 % (2618019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.60/40.07 % (2618019)CaDiCaL version: 2.1.3 % 275.60/40.07 % (2618019)Termination reason: Instruction limit % 275.60/40.07 % (2618019)Termination phase: Saturation % 275.60/40.07 % (2618019)Time elapsed: 4.299 s % 275.60/40.07 % (2618019)Peak memory usage: 186 MB % 275.60/40.07 % (2618019)Instructions burned: 14637 (million) % 275.60/40.07 % (2618029)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:fde=none:sp=const_min:urr=on:random_seed=1251821319:st=3:i=19814:s2at=5:fgj=on:bd=preordered:ins=2:ss=axioms:sgt=8_2631 on theBenchmark for (2631ds/19814Mi) % 275.60/40.07 [W927 17:44:12.948946317 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949017424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949040710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949048111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949062936 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949069193 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949082814 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.60/40.07 [W927 17:44:12.949089057 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.60/40.07 Pass in a dtype argument to ensure consisteTerminated %------------------------------------------------------------------------------