%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM286-3 : TPTP v9.3.1. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:12:05 PM UTC 2026 % Result : Timeout 289.56s 41.72s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM286-3 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.36 % Computer : n003.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sun Sep 27 19:29:56 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.40 Running first-order theorem proving % 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.79/2.24 % (876485)Input is clausal, will run a generic CNF schedule. % 9.79/2.24 % (876491)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1709905209:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.79/2.24 % (876494)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1596617699:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.79/2.24 % (876496)dis-21_1_sil=8000:lcm=predicate:random_seed=353464258: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) % 9.79/2.24 % (876490)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=316745624:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.79/2.24 % (876495)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3372320141:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.79/2.24 % (876493)lrs+10_1_sil=8000:sp=occurrence:random_seed=2881049552:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.79/2.24 % (876492)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3198208711:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.79/2.24 % (876493)Refutation not found, incomplete strategy % 9.79/2.24 % (876493)------------------------------ % 9.79/2.24 % (876493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.24 % (876493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.24 % (876494)Refutation not found, incomplete strategy % 9.79/2.24 % (876494)------------------------------ % 9.79/2.24 % (876494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.24 % (876493)CaDiCaL version: 2.1.3 % 9.79/2.24 % (876494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.24 % (876493)Termination reason: Refutation not found, incomplete strategy % 9.79/2.24 % (876493)Time elapsed: 0.001 s % 9.79/2.24 % (876493)Peak memory usage: 86 MB % 9.79/2.24 % (876494)CaDiCaL version: 2.1.3 % 9.79/2.24 % (876494)Termination reason: Refutation not found, incomplete strategy % 9.79/2.24 % (876494)Time elapsed: 0.001 s % 9.79/2.24 % (876494)Peak memory usage: 86 MB % 9.79/2.24 % (876494)Instructions burned: 1 (million) % 9.79/2.24 % (876496)Refutation not found, incomplete strategy % 9.79/2.24 % (876496)------------------------------ % 9.79/2.24 % (876496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.24 % (876496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.24 % (876496)CaDiCaL version: 2.1.3 % 9.79/2.24 % (876496)Termination reason: Refutation not found, incomplete strategy % 9.79/2.24 % (876496)Time elapsed: 0.001 s % 9.79/2.24 % (876496)Peak memory usage: 86 MB % 9.79/2.24 % (876496)Instructions burned: 1 (million) % 9.79/2.24 % (876495)Instruction limit reached! % 9.79/2.24 % (876495)------------------------------ % 9.79/2.24 % (876495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.24 % (876495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.24 % (876495)CaDiCaL version: 2.1.3 % 9.79/2.24 % (876495)Termination reason: Instruction limit % 9.79/2.24 % (876495)Termination phase: Saturation % 9.79/2.24 % (876495)Time elapsed: 0.125 s % 9.79/2.24 % (876495)Peak memory usage: 90 MB % 9.79/2.24 % (876495)Instructions burned: 182 (million) % 9.79/2.24 % (876496)------------------------------ % 9.79/2.24 % (876496)------------------------------ % 9.79/2.24 % (876493)------------------------------ % 9.79/2.24 % (876493)------------------------------ % 9.79/2.24 % (876494)------------------------------ % 9.79/2.24 % (876494)------------------------------ % 9.79/2.24 % (876504)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=3683979860:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi) % 9.79/2.24 % (876504)Refutation not found, incomplete strategy % 9.79/2.24 % (876504)------------------------------ % 9.79/2.24 % (876504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.79/2.24 % (876504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.79/2.24 % (876504)CaDiCaL version: 2.1.3 % 9.79/2.24 % (876504)Termination reason: Refutation not found, incomplete strategy % 13.10/2.83 % (876504)Time elapsed: 0.001 s % 13.10/2.83 % (876504)Peak memory usage: 86 MB % 13.10/2.83 % (876507)lrs+10_64_to=lpo:sil=8000:random_seed=3675178078:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 13.10/2.83 % (876505)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2295043966:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi) % 13.10/2.83 % (876506)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2159386099:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 13.10/2.83 % (876506)Refutation not found, incomplete strategy % 13.10/2.83 % (876506)------------------------------ % 13.10/2.83 % (876506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.83 % (876506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.83 % (876506)CaDiCaL version: 2.1.3 % 13.10/2.83 % (876506)Termination reason: Refutation not found, incomplete strategy % 13.10/2.83 % (876506)Time elapsed: 0.001 s % 13.10/2.83 % (876506)Peak memory usage: 86 MB % 13.10/2.83 % (876506)Instructions burned: 1 (million) % 13.10/2.83 % (876505)Refutation not found, incomplete strategy % 13.10/2.83 % (876505)------------------------------ % 13.10/2.83 % (876505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.83 % (876505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.83 % (876505)CaDiCaL version: 2.1.3 % 13.10/2.83 % (876505)Termination reason: Refutation not found, incomplete strategy % 13.10/2.83 % (876505)Time elapsed: 0.002 s % 13.10/2.83 % (876505)Peak memory usage: 86 MB % 13.10/2.83 % (876505)Instructions burned: 1 (million) % 13.10/2.83 % (876507)Instruction limit reached! % 13.10/2.83 % (876507)------------------------------ % 13.10/2.83 % (876507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.83 % (876507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.83 % (876507)CaDiCaL version: 2.1.3 % 13.10/2.83 % (876507)Termination reason: Instruction limit % 13.10/2.83 % (876507)Termination phase: Saturation % 13.10/2.83 % (876507)Time elapsed: 0.071 s % 13.10/2.83 % (876507)Peak memory usage: 90 MB % 13.10/2.83 % (876507)Instructions burned: 126 (million) % 13.10/2.83 % (876504)------------------------------ % 13.10/2.83 % (876504)------------------------------ % 13.10/2.83 % (876512)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3736826001:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi) % 13.10/2.83 % (876506)------------------------------ % 13.10/2.83 % (876506)------------------------------ % 13.10/2.83 % (876505)------------------------------ % 13.10/2.83 % (876505)------------------------------ % 13.10/2.83 % (876513)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3795848021:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi) % 13.10/2.83 % (876512)Instruction limit reached! % 13.10/2.83 % (876512)------------------------------ % 13.10/2.83 % (876512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.83 % (876512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.83 % (876512)CaDiCaL version: 2.1.3 % 13.10/2.83 % (876512)Termination reason: Instruction limit % 13.10/2.83 % (876512)Termination phase: Saturation % 13.10/2.83 % (876512)Time elapsed: 0.132 s % 13.10/2.83 % (876512)Peak memory usage: 91 MB % 13.10/2.83 % (876512)Instructions burned: 195 (million) % 13.10/2.83 % (876513)Instruction limit reached! % 13.10/2.83 % (876513)------------------------------ % 13.10/2.83 % (876513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.10/2.83 % (876513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.10/2.83 % (876513)CaDiCaL version: 2.1.3 % 13.10/2.83 % (876513)Termination reason: Instruction limit % 13.10/2.83 % (876513)Termination phase: Saturation % 13.10/2.83 % (876513)Time elapsed: 0.095 s % 13.10/2.83 % (876513)Peak memory usage: 91 MB % 13.10/2.83 % (876513)Instructions burned: 158 (million) % 13.10/2.83 % (876516)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=366350428:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi) % 13.10/2.83 % (876517)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=2747843054:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi) % 13.10/2.83 % (876517)Refutation not found, incomplete strategy % 19.79/3.74 % (876517)------------------------------ % 19.79/3.74 % (876517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.74 % (876517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.74 % (876517)CaDiCaL version: 2.1.3 % 19.79/3.74 % (876517)Termination reason: Refutation not found, incomplete strategy % 19.79/3.74 % (876517)Time elapsed: 0.001 s % 19.79/3.74 % (876517)Peak memory usage: 86 MB % 19.79/3.74 % (876517)Instructions burned: 1 (million) % 19.79/3.74 % (876519)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1614217641:i=107_2990 on theBenchmark for (2990ds/107Mi) % 19.79/3.74 % (876519)Refutation not found, incomplete strategy % 19.79/3.74 % (876519)------------------------------ % 19.79/3.74 % (876519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.74 % (876519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.74 % (876519)CaDiCaL version: 2.1.3 % 19.79/3.74 % (876519)Termination reason: Refutation not found, incomplete strategy % 19.79/3.74 % (876519)Time elapsed: 0.007 s % 19.79/3.74 % (876519)Peak memory usage: 88 MB % 19.79/3.74 % (876519)Instructions burned: 12 (million) % 19.79/3.74 % (876520)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4013250316:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi) % 19.79/3.74 % (876520)Refutation not found, incomplete strategy % 19.79/3.74 % (876520)------------------------------ % 19.79/3.74 % (876520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.74 % (876520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.74 % (876520)CaDiCaL version: 2.1.3 % 19.79/3.74 % (876520)Termination reason: Refutation not found, incomplete strategy % 19.79/3.74 % (876520)Time elapsed: 0.003 s % 19.79/3.74 % (876520)Peak memory usage: 87 MB % 19.79/3.74 % (876520)Instructions burned: 4 (million) % 19.79/3.74 % (876517)------------------------------ % 19.79/3.74 % (876517)------------------------------ % 19.79/3.74 % (876519)------------------------------ % 19.79/3.74 % (876519)------------------------------ % 19.79/3.74 % (876520)------------------------------ % 19.79/3.74 % (876520)------------------------------ % 19.79/3.74 [W927 19:29:58.715573353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715618744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715657641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715671064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715697031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715708698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.79/3.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.79/3.74 [W927 19:29:58.715736562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 [W927 19:29:58.715747805 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 [W927 19:29:58.715779546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 [W927 19:29:58.715850510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 [W927 19:29:58.715887834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 [W927 19:29:58.715899004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 36.00/5.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.00/5.95 % (876525)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1153425581:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi) % 36.00/5.95 % (876526)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1592769109:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi) % 36.00/5.95 % (876526)Refutation not found, incomplete strategy % 36.00/5.95 % (876526)------------------------------ % 36.00/5.95 % (876526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.00/5.95 % (876526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.00/5.95 % (876526)CaDiCaL version: 2.1.3 % 36.00/5.95 % (876526)Termination reason: Refutation not found, incomplete strategy % 36.00/5.95 % (876526)Time elapsed: 0.001 s % 36.00/5.95 % (876526)Peak memory usage: 86 MB % 36.00/5.95 % (876527)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2704924201:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi) % 36.00/5.95 % (876516)Refutation not found, incomplete strategy % 36.00/5.95 % (876516)------------------------------ % 36.00/5.95 % (876516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.00/5.95 % (876516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.00/5.95 % (876516)CaDiCaL version: 2.1.3 % 36.00/5.95 % (876516)Termination reason: Refutation not found, incomplete strategy % 36.00/5.95 % (876516)Time elapsed: 0.574 s % 36.00/5.95 % (876516)Peak memory usage: 125 MB % 36.00/5.95 % (876516)Instructions burned: 828 (million) % 36.00/5.95 % (876526)------------------------------ % 36.00/5.95 % (876526)------------------------------ % 36.00/5.95 % (876516)------------------------------ % 36.00/5.95 % (876516)------------------------------ % 36.00/5.95 % (876527)Instruction limit reached! % 36.00/5.95 % (876527)------------------------------ % 36.00/5.95 % (876527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.00/5.95 % (876527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.00/5.95 % (876527)CaDiCaL version: 2.1.3 % 36.00/5.95 % (876527)Termination reason: Instruction limit % 36.00/5.95 % (876527)Termination phase: Saturation % 36.00/5.95 % (876527)Time elapsed: 0.307 s % 36.00/5.95 % (876527)Peak memory usage: 94 MB % 36.00/5.95 % (876527)Instructions burned: 500 (million) % 36.00/5.95 % (876531)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3446718445:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi) % 36.00/5.95 % (876532)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2497700887:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi) % 39.66/6.50 % (876531)Instruction limit reached! % 39.66/6.50 % (876531)------------------------------ % 39.66/6.50 % (876531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.66/6.50 % (876531)CaDiCaL version: 2.1.3 % 39.66/6.50 % (876531)Termination reason: Instruction limit % 39.66/6.50 % (876531)Termination phase: Saturation % 39.66/6.50 % (876531)Time elapsed: 0.112 s % 39.66/6.50 % (876531)Peak memory usage: 90 MB % 39.66/6.50 % (876531)Instructions burned: 192 (million) % 39.66/6.50 % (876533)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1002512047:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi) % 39.66/6.50 % (876533)Instruction limit reached! % 39.66/6.50 % (876533)------------------------------ % 39.66/6.50 % (876533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.66/6.50 % (876533)CaDiCaL version: 2.1.3 % 39.66/6.50 % (876533)Termination reason: Instruction limit % 39.66/6.50 % (876533)Termination phase: Saturation % 39.66/6.50 % (876533)Time elapsed: 0.102 s % 39.66/6.50 % (876533)Peak memory usage: 90 MB % 39.66/6.50 % (876533)Instructions burned: 156 (million) % 39.66/6.50 % (876532)Instruction limit reached! % 39.66/6.50 % (876532)------------------------------ % 39.66/6.50 % (876532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.66/6.50 % (876532)CaDiCaL version: 2.1.3 % 39.66/6.50 % (876532)Termination reason: Instruction limit % 39.66/6.50 % (876532)Termination phase: Saturation % 39.66/6.50 % (876532)Time elapsed: 0.162 s % 39.66/6.50 % (876532)Peak memory usage: 92 MB % 39.66/6.50 % (876532)Instructions burned: 265 (million) % 39.66/6.50 % (876537)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=2191950613:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi) % 39.66/6.50 % (876538)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1505704867:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi) % 39.66/6.50 % (876538)Refutation not found, incomplete strategy % 39.66/6.50 % (876538)------------------------------ % 39.66/6.50 % (876538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.66/6.50 % (876538)CaDiCaL version: 2.1.3 % 39.66/6.50 % (876538)Termination reason: Refutation not found, incomplete strategy % 39.66/6.50 % (876538)Time elapsed: 0.001 s % 39.66/6.50 % (876538)Peak memory usage: 86 MB % 39.66/6.50 % (876539)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3000381952:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi) % 39.66/6.50 % (876539)Instruction limit reached! % 39.66/6.50 % (876539)------------------------------ % 39.66/6.50 % (876539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.66/6.50 % (876539)CaDiCaL version: 2.1.3 % 39.66/6.50 % (876539)Termination reason: Instruction limit % 39.66/6.50 % (876539)Termination phase: Saturation % 39.66/6.50 % (876539)Time elapsed: 0.104 s % 39.66/6.50 % (876539)Peak memory usage: 91 MB % 39.66/6.50 % (876539)Instructions burned: 181 (million) % 39.66/6.50 % (876538)------------------------------ % 39.66/6.50 % (876538)------------------------------ % 39.66/6.50 % (876543)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=637737073:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 39.66/6.50 % (876544)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=1528850069:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi) % 39.66/6.50 % (876544)Instruction limit reached! % 39.66/6.50 % (876544)------------------------------ % 39.66/6.50 % (876544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.66/6.50 % (876544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876544)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876544)Termination reason: Instruction limit % 54.74/8.64 % (876544)Termination phase: Saturation % 54.74/8.64 % (876544)Time elapsed: 0.205 s % 54.74/8.64 % (876544)Peak memory usage: 90 MB % 54.74/8.64 % (876544)Instructions burned: 412 (million) % 54.74/8.64 % (876547)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=1315302135:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi) % 54.74/8.64 % (876537)Instruction limit reached! % 54.74/8.64 % (876537)------------------------------ % 54.74/8.64 % (876537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.74/8.64 % (876537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876537)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876537)Termination reason: Instruction limit % 54.74/8.64 % (876537)Termination phase: Saturation % 54.74/8.64 % (876537)Time elapsed: 2.004 s % 54.74/8.64 % (876537)Peak memory usage: 149 MB % 54.74/8.64 % (876537)Instructions burned: 3256 (million) % 54.74/8.64 % (876549)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=3032623596:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi) % 54.74/8.64 % (876549)Refutation not found, incomplete strategy % 54.74/8.64 % (876549)------------------------------ % 54.74/8.64 % (876549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.74/8.64 % (876549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876549)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876549)Termination reason: Refutation not found, incomplete strategy % 54.74/8.64 % (876549)Time elapsed: 0.001 s % 54.74/8.64 % (876549)Peak memory usage: 87 MB % 54.74/8.64 % (876549)Instructions burned: 1 (million) % 54.74/8.64 % (876525)Instruction limit reached! % 54.74/8.64 % (876525)------------------------------ % 54.74/8.64 % (876525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.74/8.64 % (876525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876525)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876525)Termination reason: Instruction limit % 54.74/8.64 % (876525)Termination phase: Saturation % 54.74/8.64 % (876525)Time elapsed: 3.149 s % 54.74/8.64 % (876525)Peak memory usage: 158 MB % 54.74/8.64 % (876525)Instructions burned: 5208 (million) % 54.74/8.64 % (876549)------------------------------ % 54.74/8.64 % (876549)------------------------------ % 54.74/8.64 % (876551)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1676687648:st=4:i=720:sd=3:fsr=off:ss=axioms_2954 on theBenchmark for (2954ds/720Mi) % 54.74/8.64 % (876551)Refutation not found, incomplete strategy % 54.74/8.64 % (876551)------------------------------ % 54.74/8.64 % (876551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.74/8.64 % (876551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876551)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876551)Termination reason: Refutation not found, incomplete strategy % 54.74/8.64 % (876551)Time elapsed: 0.001 s % 54.74/8.64 % (876551)Peak memory usage: 86 MB % 54.74/8.64 % (876551)Instructions burned: 1 (million) % 54.74/8.64 % (876552)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4180110218:i=598:bs=on:bd=preordered:av=off:ss=axioms_2953 on theBenchmark for (2953ds/598Mi) % 54.74/8.64 % (876552)Refutation not found, incomplete strategy % 54.74/8.64 % (876552)------------------------------ % 54.74/8.64 % (876552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.74/8.64 % (876552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.74/8.64 % (876552)CaDiCaL version: 2.1.3 % 54.74/8.64 % (876552)Termination reason: Refutation not found, incomplete strategy % 54.74/8.64 % (876552)Time elapsed: 0.001 s % 54.74/8.64 % (876552)Peak memory usage: 86 MB % 54.74/8.64 % (876551)------------------------------ % 54.74/8.64 % (876551)------------------------------ % 54.74/8.64 % (876552)------------------------------ % 54.74/8.64 % (876552)------------------------------ % 54.74/8.64 % (876555)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3886613890:i=2989:sd=3:ss=axioms:sgt=60_2950 on theBenchmark for (2950ds/2989Mi) % 55.96/9.02 % (876556)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=1945781723:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi) % 55.96/9.02 [W927 19:30:02.804549710 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804593450 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804635151 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804647401 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804673281 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804684368 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804709592 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804719965 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804743635 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804753826 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804778363 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 [W927 19:30:02.804788549 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.96/9.02 % (876555)Refutation not found, incomplete strategy % 55.96/9.02 % (876555)------------------------------ % 63.58/9.98 % (876555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876555)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876555)Termination reason: Refutation not found, incomplete strategy % 63.58/9.98 % (876555)Time elapsed: 0.542 s % 63.58/9.98 % (876555)Peak memory usage: 126 MB % 63.58/9.98 % (876555)Instructions burned: 828 (million) % 63.58/9.98 % (876555)------------------------------ % 63.58/9.98 % (876555)------------------------------ % 63.58/9.98 % (876559)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=3770357491:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi) % 63.58/9.98 % (876556)Instruction limit reached! % 63.58/9.98 % (876556)------------------------------ % 63.58/9.98 % (876556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876556)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876556)Termination reason: Instruction limit % 63.58/9.98 % (876556)Termination phase: Saturation % 63.58/9.98 % (876556)Time elapsed: 1.258 s % 63.58/9.98 % (876556)Peak memory usage: 138 MB % 63.58/9.98 % (876556)Instructions burned: 1999 (million) % 63.58/9.98 % (876561)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1305036066:i=1098:nicw=on_2935 on theBenchmark for (2935ds/1098Mi) % 63.58/9.98 % (876561)Instruction limit reached! % 63.58/9.98 % (876561)------------------------------ % 63.58/9.98 % (876561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876561)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876561)Termination reason: Instruction limit % 63.58/9.98 % (876561)Termination phase: Saturation % 63.58/9.98 % (876561)Time elapsed: 0.654 s % 63.58/9.98 % (876561)Peak memory usage: 108 MB % 63.58/9.98 % (876561)Instructions burned: 1099 (million) % 63.58/9.98 % (876559)Instruction limit reached! % 63.58/9.98 % (876559)------------------------------ % 63.58/9.98 % (876559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876559)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876559)Termination reason: Instruction limit % 63.58/9.98 % (876559)Termination phase: Saturation % 63.58/9.98 % (876559)Time elapsed: 1.304 s % 63.58/9.98 % (876559)Peak memory usage: 138 MB % 63.58/9.98 % (876559)Instructions burned: 2088 (million) % 63.58/9.98 % (876563)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=258928770:i=433:bd=preordered_2927 on theBenchmark for (2927ds/433Mi) % 63.58/9.98 % (876563)Refutation not found, incomplete strategy % 63.58/9.98 % (876563)------------------------------ % 63.58/9.98 % (876563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876563)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876563)Termination reason: Refutation not found, incomplete strategy % 63.58/9.98 % (876563)Time elapsed: 0.013 s % 63.58/9.98 % (876563)Peak memory usage: 88 MB % 63.58/9.98 % (876563)Instructions burned: 22 (million) % 63.58/9.98 % (876564)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3945325542:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2926 on theBenchmark for (2926ds/2942Mi) % 63.58/9.98 % (876547)Instruction limit reached! % 63.58/9.98 % (876547)------------------------------ % 63.58/9.98 % (876547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.58/9.98 % (876547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.58/9.98 % (876547)CaDiCaL version: 2.1.3 % 63.58/9.98 % (876547)Termination reason: Instruction limit % 63.58/9.98 % (876547)Termination phase: Saturation % 63.58/9.98 % (876547)Time elapsed: 4.570 s % 63.58/9.98 % (876547)Peak memory usage: 229 MB % 63.58/9.98 % (876547)Instructions burned: 8480 (million) % 63.58/9.98 % (876563)------------------------------ % 63.58/9.98 % (876563)------------------------------ % 63.58/9.98 % (876567)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1709806169:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2923 on theBenchmark for (2923ds/6922Mi) % 69.80/10.81 % (876568)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=1558478388:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2923 on theBenchmark for (2923ds/596Mi) % 69.80/10.81 % (876568)Instruction limit reached! % 69.80/10.81 % (876568)------------------------------ % 69.80/10.81 % (876568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.80/10.81 % (876568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.81 % (876568)CaDiCaL version: 2.1.3 % 69.80/10.81 % (876568)Termination reason: Instruction limit % 69.80/10.81 % (876568)Termination phase: Saturation % 69.80/10.81 % (876568)Time elapsed: 0.318 s % 69.80/10.81 % (876568)Peak memory usage: 98 MB % 69.80/10.81 % (876568)Instructions burned: 597 (million) % 69.80/10.81 [W927 19:30:05.494502582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494549170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494588760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494599927 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494625504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494635737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494661231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494671488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494694918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494705058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 69.80/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.80/10.81 [W927 19:30:05.494728725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:05.494738739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 % (876571)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=2760674007:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2918 on theBenchmark for (2918ds/4123Mi) % 70.22/10.99 % (876567)Refutation not found, incomplete strategy % 70.22/10.99 % (876567)------------------------------ % 70.22/10.99 % (876567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.22/10.99 % (876567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.22/10.99 % (876567)CaDiCaL version: 2.1.3 % 70.22/10.99 % (876567)Termination reason: Refutation not found, incomplete strategy % 70.22/10.99 % (876567)Time elapsed: 0.552 s % 70.22/10.99 % (876567)Peak memory usage: 126 MB % 70.22/10.99 % (876567)Instructions burned: 830 (million) % 70.22/10.99 % (876567)------------------------------ % 70.22/10.99 % (876567)------------------------------ % 70.22/10.99 % (876543)Instruction limit reached! % 70.22/10.99 % (876543)------------------------------ % 70.22/10.99 % (876543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.22/10.99 % (876543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.22/10.99 % (876543)CaDiCaL version: 2.1.3 % 70.22/10.99 % (876543)Termination reason: Instruction limit % 70.22/10.99 % (876543)Termination phase: Saturation % 70.22/10.99 % (876543)Time elapsed: 6.001 s % 70.22/10.99 % (876543)Peak memory usage: 198 MB % 70.22/10.99 % (876543)Instructions burned: 10307 (million) % 70.22/10.99 % (876573)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2483471344:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2914 on theBenchmark for (2914ds/16411Mi) % 70.22/10.99 % (876574)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2100642832:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi) % 70.22/10.99 [W927 19:30:06.452204727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:06.452239690 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:06.452280601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:06.452293571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:06.452321241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.22/10.99 [W927 19:30:06.452332835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.22/10.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452359295 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452371129 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452395795 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452406189 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452430623 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 [W927 19:30:06.452440813 register_special_ops.cpp:225] Warning: Creating a tensor from 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.69/11.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.69/11.23 % (876573)Refutation not found, incomplete strategy % 73.69/11.23 % (876573)------------------------------ % 73.69/11.23 % (876573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.69/11.23 % (876573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.69/11.23 % (876573)CaDiCaL version: 2.1.3 % 73.69/11.23 % (876573)Termination reason: Refutation not found, incomplete strategy % 73.69/11.23 % (876573)Time elapsed: 0.547 s % 73.69/11.23 % (876573)Peak memory usage: 125 MB % 73.69/11.23 % (876573)Instructions burned: 828 (million) % 73.69/11.23 % (876564)Instruction limit reached! % 73.69/11.23 % (876564)------------------------------ % 73.69/11.23 % (876564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.69/11.23 % (876564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.69/11.23 % (876564)CaDiCaL version: 2.1.3 % 73.69/11.23 % (876564)Termination reason: Instruction limit % 73.69/11.23 % (876564)Termination phase: Saturation % 73.69/11.23 % (876564)Time elapsed: 1.887 s % 73.69/11.23 % (876564)Peak memory usage: 147 MB % 73.69/11.23 % (876564)Instructions burned: 2942 (million) % 73.69/11.23 % (876573)------------------------------ % 73.69/11.23 % (876573)------------------------------ % 73.69/11.23 % (876577)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=3072483284:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2905 on theBenchmark for (2905ds/1722Mi) % 73.69/11.23 % (876578)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=4056957871:cts=off:cond=on:i=9530:bs=on:fsd=on_2904 on theBenchmark for (2904ds/9530Mi) % 73.69/11.23 % (876574)Instruction limit reached! % 73.69/11.23 % (876574)------------------------------ % 73.69/11.23 % (876574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.69/11.23 % (876574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.69/11.23 % (876574)CaDiCaL version: 2.1.3 % 73.69/11.23 % (876574)Termination reason: Instruction limit % 73.69/11.23 % (876574)Termination phase: Saturation % 73.69/11.23 % (876574)Time elapsed: 1.038 s % 73.69/11.23 % (876574)Peak memory usage: 136 MB % 73.69/11.23 % (876574)Instructions burned: 1671 (million) % 73.69/11.23 % (876581)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1736472353:st=2:i=4495:sd=10:ss=included_2902 on theBenchmark for (2902ds/4495Mi) % 89.55/13.59 [W927 19:30:07.288364837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288443662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288492622 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288504319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288530696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288541596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288566437 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288577610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288601267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288612224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288636374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 [W927 19:30:07.288647571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.55/13.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.55/13.59 % (876577)Refutation not found, incomplete strategy % 89.55/13.59 % (876577)------------------------------ % 89.55/13.59 % (876577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.55/13.59 % (876577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.57/13.76 % (876577)CaDiCaL version: 2.1.3 % 90.57/13.76 % (876577)Termination reason: Refutation not found, incomplete strategy % 90.57/13.76 % (876577)Time elapsed: 0.556 s % 90.57/13.76 % (876577)Peak memory usage: 126 MB % 90.57/13.76 % (876577)Instructions burned: 830 (million) % 90.57/13.76 [W927 19:30:07.660503754 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660546724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660584225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660606958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660634535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660644825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660669236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660683059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660706903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660717119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660741436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 [W927 19:30:07.660752213 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 90.57/13.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 90.57/13.76 % (876577)------------------------------ % 95.97/14.41 % (876577)------------------------------ % 95.97/14.41 % (876581)Refutation not found, incomplete strategy % 95.97/14.41 % (876581)------------------------------ % 95.97/14.41 % (876581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.97/14.41 % (876581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.97/14.41 % (876581)CaDiCaL version: 2.1.3 % 95.97/14.41 % (876581)Termination reason: Refutation not found, incomplete strategy % 95.97/14.41 % (876581)Time elapsed: 0.555 s % 95.97/14.41 % (876581)Peak memory usage: 126 MB % 95.97/14.41 % (876581)Instructions burned: 828 (million) % 95.97/14.41 % (876583)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=2150446826:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2896 on theBenchmark for (2896ds/4920Mi) % 95.97/14.41 % (876571)Instruction limit reached! % 95.97/14.41 % (876571)------------------------------ % 95.97/14.41 % (876571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.97/14.41 % (876571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.97/14.41 % (876571)CaDiCaL version: 2.1.3 % 95.97/14.41 % (876571)Termination reason: Instruction limit % 95.97/14.41 % (876571)Termination phase: Saturation % 95.97/14.41 % (876571)Time elapsed: 2.460 s % 95.97/14.41 % (876571)Peak memory usage: 162 MB % 95.97/14.41 % (876571)Instructions burned: 4123 (million) % 95.97/14.41 % (876581)------------------------------ % 95.97/14.41 % (876581)------------------------------ % 95.97/14.41 % (876586)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=3762392092:i=4629:av=off:gsp=on_2892 on theBenchmark for (2892ds/4629Mi) % 95.97/14.41 % (876585)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=3826229803:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2892 on theBenchmark for (2892ds/2083Mi) % 95.97/14.41 % (876586)Refutation not found, incomplete strategy % 95.97/14.41 % (876586)------------------------------ % 95.97/14.41 % (876586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.97/14.41 % (876586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.97/14.41 % (876586)CaDiCaL version: 2.1.3 % 95.97/14.41 % (876586)Termination reason: Refutation not found, incomplete strategy % 95.97/14.41 % (876586)Time elapsed: 0.573 s % 95.97/14.41 % (876586)Peak memory usage: 130 MB % 95.97/14.41 % (876586)Instructions burned: 872 (million) % 95.97/14.41 % (876586)------------------------------ % 95.97/14.41 % (876586)------------------------------ % 95.97/14.41 % (876589)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1096188173:i=1258:av=off_2882 on theBenchmark for (2882ds/1258Mi) % 95.97/14.41 % (876585)Instruction limit reached! % 95.97/14.41 % (876585)------------------------------ % 95.97/14.41 % (876585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.97/14.41 % (876585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.97/14.41 % (876585)CaDiCaL version: 2.1.3 % 95.97/14.41 % (876585)Termination reason: Instruction limit % 95.97/14.41 % (876585)Termination phase: Saturation % 95.97/14.41 % (876585)Time elapsed: 1.269 s % 95.97/14.41 % (876585)Peak memory usage: 138 MB % 95.97/14.41 % (876585)Instructions burned: 2085 (million) % 95.97/14.41 % (876591)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3757116452:i=7343:av=off:ss=included_2877 on theBenchmark for (2877ds/7343Mi) % 95.97/14.41 % (876589)Instruction limit reached! % 95.97/14.41 % (876589)------------------------------ % 95.97/14.41 % (876589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.97/14.41 % (876589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.97/14.41 % (876589)CaDiCaL version: 2.1.3 % 95.97/14.41 % (876589)Termination reason: Instruction limit % 95.97/14.41 % (876589)Termination phase: Saturation % 95.97/14.41 % (876589)Time elapsed: 0.706 s % 95.97/14.41 % (876589)Peak memory usage: 99 MB % 95.97/14.41 % (876589)Instructions burned: 1259 (million) % 95.97/14.41 [W927 19:30:09.070483019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.97/14.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070519526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070557566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070569503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070612967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070624257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070649377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070660427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070686014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070697061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070721868 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 [W927 19:30:09.070732948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.48/14.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.48/14.56 % (876593)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2024999290:i=1325:sd=2:ss=axioms:sgt=16_2873 on theBenchmark for (2873ds/1325Mi) % 96.48/14.56 % (876593)Refutation not found, incomplete strategy % 96.48/14.56 % (876593)------------------------------ % 96.48/14.56 % (876593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.48/14.56 % (876593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.48/14.56 % (876593)CaDiCaL version: 2.1.3 % 96.48/14.56 % (876593)Termination reason: Refutation not found, incomplete strategy % 96.48/14.56 % (876593)Time elapsed: 0.001 s % 96.48/14.56 % (876593)Peak memory usage: 86 MB % 96.48/14.56 % (876591)Refutation not found, incomplete strategy % 105.80/15.87 % (876591)------------------------------ % 105.80/15.87 % (876591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.80/15.87 % (876591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.80/15.87 % (876591)CaDiCaL version: 2.1.3 % 105.80/15.87 % (876591)Termination reason: Refutation not found, incomplete strategy % 105.80/15.87 % (876591)Time elapsed: 0.542 s % 105.80/15.87 % (876591)Peak memory usage: 125 MB % 105.80/15.87 % (876591)Instructions burned: 825 (million) % 105.80/15.87 % (876593)------------------------------ % 105.80/15.87 % (876593)------------------------------ % 105.80/15.87 % (876591)------------------------------ % 105.80/15.87 % (876591)------------------------------ % 105.80/15.87 % (876595)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=2688608797:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2869 on theBenchmark for (2869ds/2646Mi) % 105.80/15.87 % (876596)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3748775412:i=1489:sd=2:ep=R:ss=axioms_2868 on theBenchmark for (2868ds/1489Mi) % 105.80/15.87 % (876583)Instruction limit reached! % 105.80/15.87 % (876583)------------------------------ % 105.80/15.87 % (876583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.80/15.87 % (876583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.80/15.87 % (876583)CaDiCaL version: 2.1.3 % 105.80/15.87 % (876583)Termination reason: Instruction limit % 105.80/15.87 % (876583)Termination phase: Saturation % 105.80/15.87 % (876583)Time elapsed: 2.924 s % 105.80/15.87 % (876583)Peak memory usage: 157 MB % 105.80/15.87 % (876583)Instructions burned: 4922 (million) % 105.80/15.87 [W927 19:30:10.890440336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890475656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890513503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890524630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890549860 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890561657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890587054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.80/15.87 [W927 19:30:10.890598831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.80/15.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.890623675 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.890634165 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.890657948 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.890668345 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 % (876599)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=2352894843:i=1503_2865 on theBenchmark for (2865ds/1503Mi) % 108.65/16.19 [W927 19:30:10.039659147 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039707204 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039748184 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039762351 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039789158 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039800965 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039826879 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039838462 register_special_ops.cpp:225] Warning: Creating a tensor from 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.65/16.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.65/16.19 [W927 19:30:10.039863439 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.76/16.73 [W927 19:30:10.039874939 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.76/16.73 [W927 19:30:10.039906086 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.76/16.73 [W927 19:30:10.039916863 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.76/16.73 % (876595)Refutation not found, incomplete strategy % 111.76/16.73 % (876595)------------------------------ % 111.76/16.73 % (876595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.76/16.73 % (876595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.76/16.73 % (876595)CaDiCaL version: 2.1.3 % 111.76/16.73 % (876595)Termination reason: Refutation not found, incomplete strategy % 111.76/16.73 % (876595)Time elapsed: 0.544 s % 111.76/16.73 % (876595)Peak memory usage: 126 MB % 111.76/16.73 % (876595)Instructions burned: 826 (million) % 111.76/16.73 % (876596)Refutation not found, incomplete strategy % 111.76/16.73 % (876596)------------------------------ % 111.76/16.73 % (876596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.76/16.73 % (876596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.76/16.73 % (876596)CaDiCaL version: 2.1.3 % 111.76/16.73 % (876596)Termination reason: Refutation not found, incomplete strategy % 111.76/16.73 % (876596)Time elapsed: 0.546 s % 111.76/16.73 % (876596)Peak memory usage: 126 MB % 111.76/16.73 % (876596)Instructions burned: 824 (million) % 111.76/16.73 % (876595)------------------------------ % 111.76/16.73 % (876595)------------------------------ % 111.76/16.73 % (876596)------------------------------ % 111.76/16.73 % (876596)------------------------------ % 111.76/16.73 % (876601)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1840205489:i=13942:kws=frequency_2860 on theBenchmark for (2860ds/13942Mi) % 111.76/16.73 % (876599)Refutation not found, incomplete strategy % 111.76/16.73 % (876599)------------------------------ % 111.76/16.73 % (876599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.76/16.73 % (876599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.76/16.73 % (876599)CaDiCaL version: 2.1.3 % 111.76/16.73 % (876599)Termination reason: Refutation not found, incomplete strategy % 111.76/16.73 % (876599)Time elapsed: 0.579 s % 111.76/16.73 % (876599)Peak memory usage: 128 MB % 111.76/16.73 % (876599)Instructions burned: 860 (million) % 111.76/16.73 % (876602)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=295677155:i=3604:fsr=off:er=filter_2858 on theBenchmark for (2858ds/3604Mi) % 111.76/16.73 % (876599)------------------------------ % 111.76/16.73 % (876599)------------------------------ % 111.76/16.73 % (876605)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=423217772:i=1876:sd=1:ss=included:sgt=32_2855 on theBenchmark for (2855ds/1876Mi) % 111.76/16.73 [W927 19:30:12.347811534 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.76/16.73 [W927 19:30:12.347845878 register_special_ops.cpp:225] Warning: Creating a tensor from 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.76/16.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347883725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347895159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347920682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347931106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347955753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347966133 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347989400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.347999820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.348036357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 [W927 19:30:12.348046884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.92/17.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.92/17.71 % (876605)Refutation not found, incomplete strategy % 118.92/17.71 % (876605)------------------------------ % 118.92/17.71 % (876605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.92/17.71 % (876605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.92/17.71 % (876605)CaDiCaL version: 2.1.3 % 118.92/17.71 % (876605)Termination reason: Refutation not found, incomplete strategy % 118.92/17.71 % (876605)Time elapsed: 0.551 s % 118.92/17.71 % (876605)Peak memory usage: 125 MB % 118.92/17.71 % (876605)Instructions burned: 828 (million) % 118.92/17.71 % (876578)Instruction limit reached! % 118.92/17.71 % (876578)------------------------------ % 118.92/17.71 % (876578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.92/17.71 % (876578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.92/17.71 % (876578)CaDiCaL version: 2.1.3 % 118.92/17.71 % (876578)Termination reason: Instruction limit % 118.92/17.71 % (876578)Termination phase: Saturation % 118.92/17.71 % (876578)Time elapsed: 5.623 s % 136.96/20.19 % (876578)Peak memory usage: 180 MB % 136.96/20.19 % (876578)Instructions burned: 9530 (million) % 136.96/20.19 % (876605)------------------------------ % 136.96/20.19 % (876605)------------------------------ % 136.96/20.19 % (876607)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1536849449:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2846 on theBenchmark for (2846ds/1932Mi) % 136.96/20.19 % (876608)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=687140599:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2845 on theBenchmark for (2845ds/1980Mi) % 136.96/20.19 [W927 19:30:12.207274844 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207308908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207347255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207359915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207387469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207399409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207425676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207437466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207463019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207474790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.96/20.19 [W927 19:30:12.207499777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.96/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:12.207510627 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 % (876607)Refutation not found, incomplete strategy % 145.27/21.30 % (876607)------------------------------ % 145.27/21.30 % (876607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.27/21.30 % (876607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.27/21.30 % (876607)CaDiCaL version: 2.1.3 % 145.27/21.30 % (876607)Termination reason: Refutation not found, incomplete strategy % 145.27/21.30 % (876607)Time elapsed: 0.541 s % 145.27/21.30 % (876607)Peak memory usage: 125 MB % 145.27/21.30 % (876607)Instructions burned: 824 (million) % 145.27/21.30 % (876607)------------------------------ % 145.27/21.30 % (876607)------------------------------ % 145.27/21.30 % (876611)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=3216164524:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2836 on theBenchmark for (2836ds/3902Mi) % 145.27/21.30 % (876602)Instruction limit reached! % 145.27/21.30 % (876602)------------------------------ % 145.27/21.30 % (876602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.27/21.30 % (876602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.27/21.30 % (876602)CaDiCaL version: 2.1.3 % 145.27/21.30 % (876602)Termination reason: Instruction limit % 145.27/21.30 % (876602)Termination phase: Saturation % 145.27/21.30 % (876602)Time elapsed: 2.182 s % 145.27/21.30 % (876602)Peak memory usage: 154 MB % 145.27/21.30 % (876602)Instructions burned: 3604 (million) % 145.27/21.30 % (876613)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=112167630:avsq=on:i=3916:aac=none:amm=off_2834 on theBenchmark for (2834ds/3916Mi) % 145.27/21.30 % (876608)Instruction limit reached! % 145.27/21.30 % (876608)------------------------------ % 145.27/21.30 % (876608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.27/21.30 % (876608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.27/21.30 % (876608)CaDiCaL version: 2.1.3 % 145.27/21.30 % (876608)Termination reason: Instruction limit % 145.27/21.30 % (876608)Termination phase: Saturation % 145.27/21.30 % (876608)Time elapsed: 1.243 s % 145.27/21.30 % (876608)Peak memory usage: 138 MB % 145.27/21.30 % (876608)Instructions burned: 1982 (million) % 145.27/21.30 [W927 19:30:13.182257231 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:13.182284562 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:13.182321979 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:13.182334022 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:13.182360493 register_special_ops.cpp:225] Warning: Creating a tensor from 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.27/21.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.27/21.30 [W927 19:30:13.182371539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182397333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182407343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182446040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182456570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182480201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 [W927 19:30:13.182490027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.39/23.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.39/23.39 % (876615)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2817495699:cond=on:i=3940:av=off:er=known_2831 on theBenchmark for (2831ds/3940Mi) % 159.39/23.39 % (876611)Refutation not found, incomplete strategy % 159.39/23.39 % (876611)------------------------------ % 159.39/23.39 % (876611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.39 % (876611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.39 % (876611)CaDiCaL version: 2.1.3 % 159.39/23.39 % (876611)Termination reason: Refutation not found, incomplete strategy % 159.39/23.39 % (876611)Time elapsed: 0.553 s % 159.39/23.39 % (876611)Peak memory usage: 126 MB % 159.39/23.39 % (876611)Instructions burned: 828 (million) % 159.39/23.39 % (876611)------------------------------ % 159.39/23.39 % (876611)------------------------------ % 159.39/23.39 % (876617)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1425783228:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2827 on theBenchmark for (2827ds/3980Mi) % 159.39/23.39 % (876613)Instruction limit reached! % 159.39/23.39 % (876613)------------------------------ % 159.39/23.39 % (876613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.39 % (876613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.39 % (876613)CaDiCaL version: 2.1.3 % 159.39/23.39 % (876613)Termination reason: Instruction limit % 159.39/23.39 % (876613)Termination phase: Saturation % 159.39/23.39 % (876613)Time elapsed: 2.490 s % 159.39/23.39 % (876613)Peak memory usage: 116 MB % 159.39/23.39 % (876613)Instructions burned: 3916 (million) % 159.39/23.39 % (876619)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=3797448555:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2808 on theBenchmark for (2808ds/2087Mi) % 159.39/23.39 % (876615)Instruction limit reached! % 159.39/23.39 % (876615)------------------------------ % 159.39/23.39 % (876615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.39 % (876615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.86 % (876615)CaDiCaL version: 2.1.3 % 161.97/23.86 % (876615)Termination reason: Instruction limit % 161.97/23.86 % (876615)Termination phase: Saturation % 161.97/23.86 % (876615)Time elapsed: 2.326 s % 161.97/23.86 % (876615)Peak memory usage: 153 MB % 161.97/23.86 % (876615)Instructions burned: 3941 (million) % 161.97/23.86 % (876621)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=3931711870:cts=off:cond=on:i=4272:bs=on:fsd=on_2806 on theBenchmark for (2806ds/4272Mi) % 161.97/23.86 % (876617)Instruction limit reached! % 161.97/23.86 % (876617)------------------------------ % 161.97/23.86 % (876617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.97/23.86 % (876617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.86 % (876617)CaDiCaL version: 2.1.3 % 161.97/23.86 % (876617)Termination reason: Instruction limit % 161.97/23.86 % (876617)Termination phase: Saturation % 161.97/23.86 % (876617)Time elapsed: 2.437 s % 161.97/23.86 % (876617)Peak memory usage: 158 MB % 161.97/23.86 % (876617)Instructions burned: 3982 (million) % 161.97/23.86 % (876623)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1008302739:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2801 on theBenchmark for (2801ds/2197Mi) % 161.97/23.86 [W927 19:30:17.774651651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774695378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774736635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774748335 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774773802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774784776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774809689 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774820679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774844563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 161.97/23.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 161.97/23.86 [W927 19:30:17.774855556 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.60 [W927 19:30:17.774879417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.60 [W927 19:30:17.774890287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.60 % (876623)Refutation not found, incomplete strategy % 181.84/26.60 % (876623)------------------------------ % 181.84/26.60 % (876623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.84/26.60 % (876623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.84/26.60 % (876623)CaDiCaL version: 2.1.3 % 181.84/26.60 % (876623)Termination reason: Refutation not found, incomplete strategy % 181.84/26.60 % (876623)Time elapsed: 0.546 s % 181.84/26.60 % (876623)Peak memory usage: 125 MB % 181.84/26.60 % (876623)Instructions burned: 829 (million) % 181.84/26.60 % (876619)Instruction limit reached! % 181.84/26.60 % (876619)------------------------------ % 181.84/26.60 % (876619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.84/26.60 % (876619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.84/26.60 % (876619)CaDiCaL version: 2.1.3 % 181.84/26.60 % (876619)Termination reason: Instruction limit % 181.84/26.60 % (876619)Termination phase: Saturation % 181.84/26.60 % (876619)Time elapsed: 1.289 s % 181.84/26.60 % (876619)Peak memory usage: 140 MB % 181.84/26.60 % (876619)Instructions burned: 2087 (million) % 181.84/26.60 % (876625)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2338281638:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2793 on theBenchmark for (2793ds/6508Mi) % 181.84/26.60 % (876623)------------------------------ % 181.84/26.60 % (876623)------------------------------ % 181.84/26.60 % (876627)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2849313696:i=2330:fgj=on:av=off:fsr=off_2791 on theBenchmark for (2791ds/2330Mi) % 181.84/26.60 % (876621)Instruction limit reached! % 181.84/26.60 % (876621)------------------------------ % 181.84/26.60 % (876621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.84/26.60 % (876621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.84/26.60 % (876621)CaDiCaL version: 2.1.3 % 181.84/26.60 % (876621)Termination reason: Instruction limit % 181.84/26.60 % (876621)Termination phase: Saturation % 181.84/26.60 % (876621)Time elapsed: 2.574 s % 181.84/26.60 % (876621)Peak memory usage: 160 MB % 181.84/26.60 % (876621)Instructions burned: 4272 (million) % 181.84/26.60 % (876629)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=628210527:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2778 on theBenchmark for (2778ds/7592Mi) % 181.84/26.60 % (876601)Instruction limit reached! % 181.84/26.60 % (876601)------------------------------ % 181.84/26.60 % (876601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.84/26.60 % (876601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.84/26.60 % (876601)CaDiCaL version: 2.1.3 % 181.84/26.60 % (876601)Termination reason: Instruction limit % 181.84/26.60 % (876601)Termination phase: Saturation % 181.84/26.60 % (876601)Time elapsed: 8.205 s % 181.84/26.60 % (876601)Peak memory usage: 242 MB % 181.84/26.60 % (876601)Instructions burned: 13943 (million) % 181.84/26.60 % (876627)Instruction limit reached! % 181.84/26.60 % (876627)------------------------------ % 181.84/26.60 % (876627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.84/26.60 % (876627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.84/26.60 % (876627)CaDiCaL version: 2.1.3 % 181.84/26.60 % (876627)Termination reason: Instruction limit % 181.84/26.60 % (876627)Termination phase: Saturation % 181.84/26.60 % (876627)Time elapsed: 1.414 s % 181.84/26.60 % (876627)Peak memory usage: 141 MB % 181.84/26.60 % (876627)Instructions burned: 2330 (million) % 181.84/26.60 % (876631)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=1063931224:i=2693:kws=precedence:ins=1:av=off_2776 on theBenchmark for (2776ds/2693Mi) % 181.84/26.67 % (876632)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2764425297:i=28651:sd=4:ss=included:sgt=64_2775 on theBenchmark for (2775ds/28651Mi) % 181.84/26.67 [W927 19:30:20.335390585 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335435592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335472449 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335485686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335512703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335525453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335552560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335564570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335590267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335602161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335627554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 181.84/26.67 [W927 19:30:20.335639398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 181.84/26.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 182.88/26.84 % (876632)Refutation not found, incomplete strategy % 182.88/26.84 % (876632)------------------------------ % 182.88/26.84 % (876632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.88/26.84 % (876632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.88/26.84 % (876632)CaDiCaL version: 2.1.3 % 182.88/26.84 % (876632)Termination reason: Refutation not found, incomplete strategy % 182.88/26.84 % (876632)Time elapsed: 0.552 s % 182.88/26.84 % (876632)Peak memory usage: 125 MB % 182.88/26.84 % (876632)Instructions burned: 828 (million) % 182.88/26.84 % (876632)------------------------------ % 182.88/26.84 % (876632)------------------------------ % 182.88/26.84 % (876635)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=797771947:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2765 on theBenchmark for (2765ds/2700Mi) % 182.88/26.84 % (876631)Instruction limit reached! % 182.88/26.84 % (876631)------------------------------ % 182.88/26.84 % (876631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.88/26.84 % (876631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.88/26.84 % (876631)CaDiCaL version: 2.1.3 % 182.88/26.84 % (876631)Termination reason: Instruction limit % 182.88/26.84 % (876631)Termination phase: Saturation % 182.88/26.84 % (876631)Time elapsed: 1.643 s % 182.88/26.84 % (876631)Peak memory usage: 146 MB % 182.88/26.84 % (876631)Instructions burned: 2694 (million) % 182.88/26.84 % (876637)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=2208614293:i=3196:nm=4_2758 on theBenchmark for (2758ds/3196Mi) % 182.88/26.84 % (876625)Instruction limit reached! % 182.88/26.84 % (876625)------------------------------ % 182.88/26.84 % (876625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.88/26.84 % (876625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.88/26.84 % (876625)CaDiCaL version: 2.1.3 % 182.88/26.84 % (876625)Termination reason: Instruction limit % 182.88/26.84 % (876625)Termination phase: Saturation % 182.88/26.84 % (876625)Time elapsed: 3.643 s % 182.88/26.84 % (876625)Peak memory usage: 141 MB % 182.88/26.84 % (876625)Instructions burned: 6508 (million) % 182.88/26.84 % (876639)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3811163814:cts=off:i=3254:av=off_2755 on theBenchmark for (2755ds/3254Mi) % 182.88/26.84 % (876637)Refutation not found, incomplete strategy % 182.88/26.84 % (876637)------------------------------ % 182.88/26.84 % (876637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.88/26.84 % (876637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.88/26.84 % (876637)CaDiCaL version: 2.1.3 % 182.88/26.84 % (876637)Termination reason: Refutation not found, incomplete strategy % 182.88/26.84 % (876637)Time elapsed: 0.579 s % 182.88/26.84 % (876637)Peak memory usage: 130 MB % 182.88/26.84 % (876637)Instructions burned: 876 (million) % 182.88/26.84 % (876637)------------------------------ % 182.88/26.84 % (876637)------------------------------ % 182.88/26.84 % (876635)Instruction limit reached! % 182.88/26.84 % (876635)------------------------------ % 182.88/26.84 % (876635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.88/26.84 % (876635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.88/26.84 % (876635)CaDiCaL version: 2.1.3 % 182.88/26.84 % (876635)Termination reason: Instruction limit % 182.88/26.84 % (876635)Termination phase: Saturation % 182.88/26.84 % (876635)Time elapsed: 1.655 s % 182.88/26.84 % (876635)Peak memory usage: 147 MB % 182.88/26.84 % (876635)Instructions burned: 2700 (million) % 182.88/26.84 % (876641)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=4197154149:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2748 on theBenchmark for (2748ds/3264Mi) % 182.88/26.84 % (876642)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=1836922340:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2747 on theBenchmark for (2747ds/9708Mi) % 182.88/26.84 [W927 19:30:22.074138147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 182.88/26.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074181805 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074221262 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074232572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074257269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074267386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074291986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074302179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074326066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074336087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074360410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.074370430 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.145532958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 188.75/27.64 [W927 19:30:22.145567615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 188.75/27.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145606115 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145635096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145662523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145672593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145697393 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145707350 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145731507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145741510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145765267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 [W927 19:30:22.145775251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.54/33.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.54/33.10 % (876641)Refutation not found, incomplete strategy % 228.54/33.10 % (876641)------------------------------ % 228.54/33.10 % (876641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.54/33.10 % (876641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.54/33.10 % (876641)CaDiCaL version: 2.1.3 % 228.54/33.10 % (876641)Termination reason: Refutation not found, incomplete strategy % 228.54/33.10 % (876641)Time elapsed: 0.552 s % 228.54/33.10 % (876641)Peak memory usage: 126 MB % 228.54/33.10 % (876641)Instructions burned: 827 (million) % 228.54/33.10 % (876642)Refutation not found, incomplete strategy % 228.54/33.10 % (876642)------------------------------ % 228.54/33.10 % (876642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.54/33.10 % (876642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.54/33.10 % (876642)CaDiCaL version: 2.1.3 % 228.54/33.10 % (876642)Termination reason: Refutation not found, incomplete strategy % 228.54/33.10 % (876642)Time elapsed: 0.554 s % 231.76/33.66 % (876642)Peak memory usage: 126 MB % 231.76/33.66 % (876642)Instructions burned: 829 (million) % 231.76/33.66 % (876629)Instruction limit reached! % 231.76/33.66 % (876629)------------------------------ % 231.76/33.66 % (876629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.76/33.66 % (876629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.76/33.66 % (876629)CaDiCaL version: 2.1.3 % 231.76/33.66 % (876629)Termination reason: Instruction limit % 231.76/33.66 % (876629)Termination phase: Saturation % 231.76/33.66 % (876629)Time elapsed: 3.813 s % 231.76/33.66 % (876629)Peak memory usage: 151 MB % 231.76/33.66 % (876629)Instructions burned: 7593 (million) % 231.76/33.66 % (876641)------------------------------ % 231.76/33.66 % (876641)------------------------------ % 231.76/33.66 % (876642)------------------------------ % 231.76/33.66 % (876642)------------------------------ % 231.76/33.66 % (876645)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2036094188:i=21997:s2at=5:gtg=all_2739 on theBenchmark for (2739ds/21997Mi) % 231.76/33.66 % (876646)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3276961612:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2738 on theBenchmark for (2738ds/7551Mi) % 231.76/33.66 % (876648)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1389117836:i=8924:sd=1:ss=included_2737 on theBenchmark for (2737ds/8924Mi) % 231.76/33.66 % (876639)Instruction limit reached! % 231.76/33.66 % (876639)------------------------------ % 231.76/33.66 % (876639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.76/33.66 % (876639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.76/33.66 % (876639)CaDiCaL version: 2.1.3 % 231.76/33.66 % (876639)Termination reason: Instruction limit % 231.76/33.66 % (876639)Termination phase: Saturation % 231.76/33.66 % (876639)Time elapsed: 1.961 s % 231.76/33.66 % (876639)Peak memory usage: 149 MB % 231.76/33.66 % (876639)Instructions burned: 3254 (million) % 231.76/33.66 % (876651)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=2950509010:i=9638:kws=frequency:bd=preordered_2734 on theBenchmark for (2734ds/9638Mi) % 231.76/33.66 [W927 19:30:23.118728621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118778398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118818738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118832392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118858505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118870799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.76/33.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.76/33.66 [W927 19:30:23.118896916 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 [W927 19:30:23.118917946 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 [W927 19:30:23.118945470 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 [W927 19:30:23.118956137 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 [W927 19:30:23.118985630 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 [W927 19:30:23.118996307 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/39.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.04/39.68 % (876648)Refutation not found, incomplete strategy % 275.04/39.68 % (876648)------------------------------ % 275.04/39.68 % (876648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.04/39.68 % (876648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.04/39.68 % (876648)CaDiCaL version: 2.1.3 % 275.04/39.68 % (876648)Termination reason: Refutation not found, incomplete strategy % 275.04/39.68 % (876648)Time elapsed: 0.553 s % 275.04/39.68 % (876648)Peak memory usage: 126 MB % 275.04/39.68 % (876648)Instructions burned: 829 (million) % 275.04/39.68 % (876648)------------------------------ % 275.04/39.68 % (876648)------------------------------ % 275.04/39.68 % (876653)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=1880425936:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2727 on theBenchmark for (2727ds/5177Mi) % 275.04/39.68 % (876653)Refutation not found, incomplete strategy % 275.04/39.68 % (876653)------------------------------ % 275.04/39.68 % (876653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.04/39.68 % (876653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.04/39.68 % (876653)CaDiCaL version: 2.1.3 % 275.04/39.68 % (876653)Termination reason: Refutation not found, incomplete strategy % 275.04/39.68 % (876653)Time elapsed: 0.573 s % 275.04/39.68 % (876653)Peak memory usage: 128 MB % 275.04/39.68 % (876653)Instructions burned: 872 (million) % 275.04/39.68 % (876653)------------------------------ % 275.04/39.68 % (876653)------------------------------ % 275.04/39.68 % (876655)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=3434695194:i=6464:aac=none:ins=10_2717 on theBenchmark for (2717ds/6464Mi) % 275.04/39.68 % (876646)Instruction limit reached! % 275.04/39.68 % (876646)------------------------------ % 275.04/39.68 % (876646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.04/39.68 % (876646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.04/39.68 % (876646)CaDiCaL version: 2.1.3 % 275.04/39.68 % (876646)Termination reason: Instruction limit % 275.04/39.68 % (876646)Termination phase: Saturation % 275.04/39.68 % (876646)Time elapsed: 3.862 s % 275.04/39.68 % (876646)Peak memory usage: 143 MB % 275.04/39.68 % (876646)Instructions burned: 7554 (million) % 275.04/39.68 % (876657)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=651622914:i=19192:av=off_2697 on theBenchmark for (2697ds/19192Mi) % 275.04/39.68 % (876655)Instruction limit reached! % 275.04/39.68 % (876655)------------------------------ % 289.56/41.72 % (876655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.56/41.72 % (876655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.56/41.72 % (876655)CaDiCaL version: 2.1.3 % 289.56/41.72 % (876655)Termination reason: Instruction limit % 289.56/41.72 % (876655)Termination phase: Saturation % 289.56/41.72 % (876655)Time elapsed: 3.871 s % 289.56/41.72 % (876655)Peak memory usage: 178 MB % 289.56/41.72 % (876655)Instructions burned: 6465 (million) % 289.56/41.72 % (876651)Instruction limit reached! % 289.56/41.72 % (876651)------------------------------ % 289.56/41.72 % (876651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.56/41.72 % (876651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.56/41.72 % (876651)CaDiCaL version: 2.1.3 % 289.56/41.72 % (876651)Termination reason: Instruction limit % 289.56/41.72 % (876651)Termination phase: Saturation % 289.56/41.72 % (876651)Time elapsed: 5.667 s % 289.56/41.72 % (876651)Peak memory usage: 177 MB % 289.56/41.72 % (876651)Instructions burned: 9639 (million) % 289.56/41.72 % (876659)lrs+10_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=8000:npcc=on:prc=on:fde=unused:sp=const_min:random_seed=3627297296:i=7136:fgj=on:bd=preordered:ins=3:ss=included_2677 on theBenchmark for (2677ds/7136Mi) % 289.56/41.72 % (876660)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=2375528644:cts=off:cond=on:i=7540:bs=on:fsd=on_2675 on theBenchmark for (2675ds/7540Mi) % 289.56/41.72 [W927 19:30:29.136562790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136606444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136644197 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136658228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136685621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136698178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136724332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136736598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 289.56/41.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.56/41.72 [W927 19:30:29.136762795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.22/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.22/43.17 [W927 19:30:29.136775932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.22/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.22/43.17 [W927 19:30:29.136800803 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.22/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.22/43.17 [W927 19:30:29.136823456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.22/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.22/43.17 % (876659)Refutation not found, incomplete strategy % 300.22/43.17 % (876659)------------------------------ % 300.22/43.17 % (876659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.22/43.17 % (876659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.17 % (876659)CaDiCaL version: 2.1.3 % 300.22/43.17 % (876659)Termination reason: Refutation not found, incomplete strategy % 300.22/43.17 % (876659)Time elapsed: 0.554 s % 300.22/43.17 % (876659)Peak memory usage: 126 MB % 300.22/43.17 % (876659)Instructions burned: 829 (million) % 300.22/43.17 % (876659)------------------------------ % 300.22/43.17 % (876659)------------------------------ % 300.22/43.17 % (876663)ott+1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=64000:tgt=ground:npcc=on:drc=off:sp=const_frequency:random_seed=2933433088:i=15570:s2at=5:gtgl=4:gtg=exists_sym_2667 on theBenchmark for (2667ds/15570Mi) % 300.22/43.17 % (876491)Instruction limit reached! % 300.22/43.17 % (876491)------------------------------ % 300.22/43.17 % (876491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.22/43.17 % (876491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.17 % (876491)CaDiCaL version: 2.1.3 % 300.22/43.17 % (876491)Termination reason: Instruction limit % 300.22/43.17 % (876491)Termination phase: Saturation % 300.22/43.17 % (876491)Time elapsed: 35.343 s % 300.22/43.17 % (876491)Peak memory usage: 1210 MB % 300.22/43.17 % (876491)Instructions burned: 132376 (million) % 300.22/43.17 % (876665)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=1924508036:i=15957:add=on:fgj=on_2644 on theBenchmark for (2644ds/15957Mi) % 300.22/43.17 % (876660)Instruction limit reached! % 300.22/43.17 % (876660)------------------------------ % 300.22/43.17 % (876660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.22/43.17 % (876660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.17 % (876660)CaDiCaL version: 2.1.3 % 300.22/43.17 % (876660)Termination reason: Instruction limit % 300.22/43.17 % (876660)Termination phase: Saturation % 300.22/43.17 % (876660)Time elapsed: 4.484 s % 300.22/43.17 % (876660)Peak memory usage: 182 MB % 300.22/43.17 % (876660)Instructions burned: 7542 (million) % 300.22/43.17 % (876667)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=3022580298:cond=on:i=8289:erml=3:bd=preordered:er=filter:proc=on_2629 on theBenchmark for (2629ds/8289Mi) % 300.22/43.17 % (876645)Instruction limit reached! % 300.22/43.17 % (876645)------------------------------ % 300.22/43.17 % (876645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.22/43.17 % (876645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.22/43.17 % (876645)CaDiCaL version: 2.1.3 % 300.22/43.17 % (876645)Termination reason: Instruction limit % 300.22/43.17 % (876645)Termination phase: Saturation % 300.22/43.17 % (876645)Time elapsed: 12.385 s % 300.22/43.17 % (876645)Peak memory usage: 324 MB % 300.22/43.17 % (876645)Instructions burned: 21997 (million) % 300.22/43.17 % (876669)lrs+4_4_to=lpo:sil=128000:flr=on:sac=on:lwlo=on:random_seed=2951791868:i=16865:nicw=on:b % 300.22/43.17 Terminated %------------------------------------------------------------------------------