%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM350+1 : TPTP v9.3.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n001.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:14 PM UTC 2026 % Result : Timeout 300.33s 43.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM350+1 : TPTP v9.3.1. Released v3.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.38 % Computer : n001.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 19:42:31 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.41 Running first-order theorem proving % 0.11/0.41 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 % 3.67/1.41 % (3908481)Detected formulas, will run a generic FOF schedule. % 3.67/1.41 % (3908491)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3610880022:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 3.67/1.41 % (3908489)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3347940420:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 3.67/1.41 % (3908488)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1045196219:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 3.67/1.41 % (3908486)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=1412687653:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 3.67/1.41 % (3908487)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1818091834:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 3.67/1.41 % (3908490)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1109743254:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 3.67/1.41 % (3908489)Refutation not found, incomplete strategy % 3.67/1.41 % (3908489)------------------------------ % 3.67/1.41 % (3908489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.67/1.41 % (3908489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.41 % (3908489)CaDiCaL version: 2.1.3 % 3.67/1.41 % (3908489)Termination reason: Refutation not found, incomplete strategy % 3.67/1.41 % (3908489)Time elapsed: 0.002 s % 3.67/1.41 % (3908489)Peak memory usage: 86 MB % 3.67/1.41 % (3908489)Instructions burned: 1 (million) % 3.67/1.41 % (3908490)Refutation not found, incomplete strategy % 3.67/1.41 % (3908490)------------------------------ % 3.67/1.41 % (3908490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.67/1.41 % (3908490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.41 % (3908490)CaDiCaL version: 2.1.3 % 3.67/1.41 % (3908490)Termination reason: Refutation not found, incomplete strategy % 3.67/1.41 % (3908490)Time elapsed: 0.002 s % 3.67/1.41 % (3908490)Peak memory usage: 88 MB % 3.67/1.41 % (3908490)Instructions burned: 1 (million) % 3.67/1.41 % (3908491)Instruction limit reached! % 3.67/1.41 % (3908491)------------------------------ % 3.67/1.41 % (3908491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.67/1.41 % (3908491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.41 % (3908491)CaDiCaL version: 2.1.3 % 3.67/1.41 % (3908491)Termination reason: Instruction limit % 3.67/1.41 % (3908491)Termination phase: Saturation % 3.67/1.41 % (3908491)Time elapsed: 0.047 s % 3.67/1.41 % (3908491)Peak memory usage: 90 MB % 3.67/1.41 % (3908491)Instructions burned: 140 (million) % 3.67/1.41 % (3908492)dis-21_1_sil=8000:lcm=predicate:random_seed=2471273497:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 3.67/1.41 % (3908492)Instruction limit reached! % 3.67/1.41 % (3908492)------------------------------ % 3.67/1.41 % (3908492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.67/1.41 % (3908492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.41 % (3908492)CaDiCaL version: 2.1.3 % 3.67/1.41 % (3908492)Termination reason: Instruction limit % 3.67/1.41 % (3908492)Termination phase: Saturation % 3.67/1.41 % (3908492)Time elapsed: 0.074 s % 3.67/1.41 % (3908492)Peak memory usage: 89 MB % 3.67/1.41 % (3908492)Instructions burned: 129 (million) % 3.67/1.41 % (3908500)lrs+10_1_sil=8000:sp=occurrence:random_seed=2401493248:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 3.67/1.41 % (3908500)Refutation not found, incomplete strategy % 3.67/1.41 % (3908500)------------------------------ % 3.67/1.41 % (3908500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.67/1.41 % (3908500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.67/1.41 % (3908500)CaDiCaL version: 2.1.3 % 3.67/1.41 % (3908500)Termination reason: Refutation not found, incomplete strategy % 3.67/1.41 % (3908500)Time elapsed: 0.002 s % 3.67/1.41 % (3908500)Peak memory usage: 88 MB % 3.67/1.41 % (3908500)Instructions burned: 1 (million) % 3.67/1.41 % (3908501)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2822657533:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.58/1.75 % (3908489)------------------------------ % 5.58/1.75 % (3908489)------------------------------ % 5.58/1.75 % (3908490)------------------------------ % 5.58/1.75 % (3908490)------------------------------ % 5.58/1.75 % (3908501)Refutation not found, incomplete strategy % 5.58/1.75 % (3908501)------------------------------ % 5.58/1.75 % (3908501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.58/1.75 % (3908501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.58/1.75 % (3908501)CaDiCaL version: 2.1.3 % 5.58/1.75 % (3908501)Termination reason: Refutation not found, incomplete strategy % 5.58/1.75 % (3908501)Time elapsed: 0.003 s % 5.58/1.75 % (3908501)Peak memory usage: 87 MB % 5.58/1.75 % (3908501)Instructions burned: 5 (million) % 5.58/1.75 % (3908500)------------------------------ % 5.58/1.75 % (3908500)------------------------------ % 5.58/1.75 [W927 19:42:32.624965820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.624966950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625018060 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625018720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625058934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625059880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625071594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625073917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625097301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625100147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.58/1.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.58/1.75 [W927 19:42:32.625110391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625111211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625136354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625136691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625150454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625150534 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625174404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625175585 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625186425 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625195551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625210818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625220518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625221618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.27/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.27/2.18 [W927 19:42:32.625230988 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.85/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.85/2.84 % (3908504)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3638509754:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 12.85/2.84 % (3908505)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2456662880:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 12.85/2.84 % (3908504)Refutation not found, incomplete strategy % 12.85/2.84 % (3908504)------------------------------ % 12.85/2.84 % (3908504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.85/2.84 % (3908504)CaDiCaL version: 2.1.3 % 12.85/2.84 % (3908504)Termination reason: Refutation not found, incomplete strategy % 12.85/2.84 % (3908504)Time elapsed: 0.002 s % 12.85/2.84 % (3908504)Peak memory usage: 87 MB % 12.85/2.84 % (3908504)Instructions burned: 1 (million) % 12.85/2.84 % (3908506)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=222157602:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 12.85/2.84 % (3908506)Refutation not found, incomplete strategy % 12.85/2.84 % (3908506)------------------------------ % 12.85/2.84 % (3908506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.85/2.84 % (3908506)CaDiCaL version: 2.1.3 % 12.85/2.84 % (3908506)Termination reason: Refutation not found, incomplete strategy % 12.85/2.84 % (3908506)Time elapsed: 0.003 s % 12.85/2.84 % (3908506)Peak memory usage: 88 MB % 12.85/2.84 % (3908506)Instructions burned: 7 (million) % 12.85/2.84 % (3908501)------------------------------ % 12.85/2.84 % (3908501)------------------------------ % 12.85/2.84 % (3908505)Instruction limit reached! % 12.85/2.84 % (3908505)------------------------------ % 12.85/2.84 % (3908505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.85/2.84 % (3908505)CaDiCaL version: 2.1.3 % 12.85/2.84 % (3908505)Termination reason: Instruction limit % 12.85/2.84 % (3908505)Termination phase: Saturation % 12.85/2.84 % (3908505)Time elapsed: 0.124 s % 12.85/2.84 % (3908505)Peak memory usage: 93 MB % 12.85/2.84 % (3908505)Instructions burned: 249 (million) % 12.85/2.84 % (3908488)Refutation not found, incomplete strategy % 12.85/2.84 % (3908488)------------------------------ % 12.85/2.84 % (3908488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908487)Refutation not found, incomplete strategy % 12.85/2.84 % (3908487)------------------------------ % 12.85/2.84 % (3908487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.85/2.84 % (3908488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.85/2.84 % (3908487)CaDiCaL version: 2.1.3 % 12.85/2.84 % (3908488)CaDiCaL version: 2.1.3 % 12.85/2.84 % (3908488)Termination reason: Refutation not found, incomplete strategy % 12.85/2.84 % (3908488)Time elapsed: 0.561 s % 12.85/2.84 % (3908487)Termination reason: Refutation not found, incomplete strategy % 12.85/2.84 % (3908487)Time elapsed: 0.561 s % 12.85/2.84 % (3908487)Peak memory usage: 126 MB % 12.85/2.84 % (3908488)Peak memory usage: 126 MB % 12.85/2.84 % (3908487)Instructions burned: 834 (million) % 12.85/2.84 % (3908488)Instructions burned: 835 (million) % 12.85/2.84 % (3908506)------------------------------ % 12.85/2.84 % (3908506)------------------------------ % 12.85/2.84 % (3908510)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2927926057:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 12.85/2.84 % (3908504)------------------------------ % 12.85/2.84 % (3908504)------------------------------ % 12.85/2.84 % (3908511)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2407709036:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 12.85/2.84 % (3908511)Refutation not found, incomplete strategy % 12.85/2.84 % (3908511)------------------------------ % 12.85/2.84 % (3908511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.85/2.84 % (3908511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908511)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908511)Termination reason: Refutation not found, incomplete strategy % 19.93/3.85 % (3908511)Time elapsed: 0.002 s % 19.93/3.85 % (3908511)Peak memory usage: 88 MB % 19.93/3.85 % (3908511)Instructions burned: 1 (million) % 19.93/3.85 % (3908512)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1516823537:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 19.93/3.85 % (3908512)Instruction limit reached! % 19.93/3.85 % (3908512)------------------------------ % 19.93/3.85 % (3908512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (3908512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908512)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908512)Termination reason: Instruction limit % 19.93/3.85 % (3908512)Termination phase: Saturation % 19.93/3.85 % (3908512)Time elapsed: 0.031 s % 19.93/3.85 % (3908512)Peak memory usage: 88 MB % 19.93/3.85 % (3908512)Instructions burned: 132 (million) % 19.93/3.85 % (3908487)------------------------------ % 19.93/3.85 % (3908487)------------------------------ % 19.93/3.85 % (3908488)------------------------------ % 19.93/3.85 % (3908488)------------------------------ % 19.93/3.85 % (3908514)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=237490724:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 19.93/3.85 % (3908517)lrs+10_1_sil=8000:sp=occurrence:random_seed=789775140:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 19.93/3.85 % (3908514)Instruction limit reached! % 19.93/3.85 % (3908514)------------------------------ % 19.93/3.85 % (3908514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (3908514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908514)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908514)Termination reason: Instruction limit % 19.93/3.85 % (3908514)Termination phase: Saturation % 19.93/3.85 % (3908514)Time elapsed: 0.060 s % 19.93/3.85 % (3908514)Peak memory usage: 90 MB % 19.93/3.85 % (3908514)Instructions burned: 115 (million) % 19.93/3.85 % (3908511)------------------------------ % 19.93/3.85 % (3908511)------------------------------ % 19.93/3.85 % (3908519)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2029688432:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 19.93/3.85 % (3908518)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=213776603:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 19.93/3.85 % (3908518)Refutation not found, incomplete strategy % 19.93/3.85 % (3908518)------------------------------ % 19.93/3.85 % (3908518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (3908518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908518)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908518)Termination reason: Refutation not found, incomplete strategy % 19.93/3.85 % (3908518)Time elapsed: 0.002 s % 19.93/3.85 % (3908518)Peak memory usage: 87 MB % 19.93/3.85 % (3908518)Instructions burned: 1 (million) % 19.93/3.85 % (3908522)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=186206879:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 19.93/3.85 % (3908522)Refutation not found, incomplete strategy % 19.93/3.85 % (3908522)------------------------------ % 19.93/3.85 % (3908522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (3908522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908522)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908522)Termination reason: Refutation not found, incomplete strategy % 19.93/3.85 % (3908522)Time elapsed: 0.002 s % 19.93/3.85 % (3908522)Peak memory usage: 88 MB % 19.93/3.85 % (3908522)Instructions burned: 2 (million) % 19.93/3.85 % (3908523)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1829723735:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 19.93/3.85 % (3908517)Instruction limit reached! % 19.93/3.85 % (3908517)------------------------------ % 19.93/3.85 % (3908517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.93/3.85 % (3908517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.93/3.85 % (3908517)CaDiCaL version: 2.1.3 % 19.93/3.85 % (3908517)Termination reason: Instruction limit % 25.11/4.44 % (3908517)Termination phase: Saturation % 25.11/4.44 % (3908517)Time elapsed: 0.272 s % 25.11/4.44 % (3908517)Peak memory usage: 99 MB % 25.11/4.44 % (3908517)Instructions burned: 909 (million) % 25.11/4.44 % (3908523)Refutation not found, incomplete strategy % 25.11/4.44 % (3908523)------------------------------ % 25.11/4.44 % (3908523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.11/4.44 % (3908523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.11/4.44 % (3908523)CaDiCaL version: 2.1.3 % 25.11/4.44 % (3908523)Termination reason: Refutation not found, incomplete strategy % 25.11/4.44 % (3908523)Time elapsed: 0.005 s % 25.11/4.44 % (3908523)Peak memory usage: 88 MB % 25.11/4.44 % (3908523)Instructions burned: 9 (million) % 25.11/4.44 % (3908518)------------------------------ % 25.11/4.44 % (3908518)------------------------------ % 25.11/4.44 % (3908528)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1529088558:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 25.11/4.44 % (3908522)------------------------------ % 25.11/4.44 % (3908522)------------------------------ % 25.11/4.44 % (3908523)------------------------------ % 25.11/4.44 % (3908523)------------------------------ % 25.11/4.44 % (3908529)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=642425541:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 25.11/4.44 % (3908529)Refutation not found, incomplete strategy % 25.11/4.44 % (3908529)------------------------------ % 25.11/4.44 % (3908529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.11/4.44 % (3908529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.11/4.44 % (3908529)CaDiCaL version: 2.1.3 % 25.11/4.44 % (3908529)Termination reason: Refutation not found, incomplete strategy % 25.11/4.44 % (3908529)Time elapsed: 0.004 s % 25.11/4.44 % (3908529)Peak memory usage: 88 MB % 25.11/4.44 % (3908529)Instructions burned: 7 (million) % 25.11/4.44 % (3908531)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2604609283:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi) % 25.11/4.44 % (3908531)Instruction limit reached! % 25.11/4.44 % (3908531)------------------------------ % 25.11/4.44 % (3908531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.11/4.44 % (3908531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.11/4.44 % (3908531)CaDiCaL version: 2.1.3 % 25.11/4.44 % (3908531)Termination reason: Instruction limit % 25.11/4.44 % (3908531)Termination phase: Saturation % 25.11/4.44 % (3908531)Time elapsed: 0.071 s % 25.11/4.44 % (3908531)Peak memory usage: 91 MB % 25.11/4.44 % (3908531)Instructions burned: 135 (million) % 25.11/4.44 % (3908533)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2287719199:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 25.11/4.44 % (3908533)Refutation not found, incomplete strategy % 25.11/4.44 % (3908533)------------------------------ % 25.11/4.44 % (3908533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.11/4.44 % (3908533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.11/4.44 % (3908533)CaDiCaL version: 2.1.3 % 25.11/4.44 % (3908533)Termination reason: Refutation not found, incomplete strategy % 25.11/4.44 % (3908533)Time elapsed: 0.002 s % 25.11/4.44 % (3908533)Peak memory usage: 87 MB % 25.11/4.44 % (3908533)Instructions burned: 1 (million) % 25.11/4.44 % (3908529)------------------------------ % 25.11/4.44 % (3908529)------------------------------ % 25.11/4.44 % (3908535)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1419242264:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 25.11/4.44 % (3908535)Refutation not found, incomplete strategy % 25.11/4.44 % (3908535)------------------------------ % 25.11/4.44 % (3908535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.11/4.44 % (3908535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.11/4.44 % (3908535)CaDiCaL version: 2.1.3 % 25.11/4.44 % (3908535)Termination reason: Refutation not found, incomplete strategy % 25.11/4.44 % (3908535)Time elapsed: 0.002 s % 25.11/4.44 % (3908535)Peak memory usage: 87 MB % 25.11/4.44 % (3908535)Instructions burned: 1 (million) % 25.11/4.44 % (3908537)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=520119865:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 32.25/5.47 % (3908533)------------------------------ % 32.25/5.47 % (3908533)------------------------------ % 32.25/5.47 % (3908535)------------------------------ % 32.25/5.47 % (3908535)------------------------------ % 32.25/5.47 % (3908540)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1142371768:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi) % 32.25/5.47 % (3908540)Instruction limit reached! % 32.25/5.47 % (3908540)------------------------------ % 32.25/5.47 % (3908540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.47 % (3908540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.47 % (3908540)CaDiCaL version: 2.1.3 % 32.25/5.47 % (3908540)Termination reason: Instruction limit % 32.25/5.47 % (3908540)Termination phase: Saturation % 32.25/5.47 % (3908540)Time elapsed: 0.082 s % 32.25/5.47 % (3908540)Peak memory usage: 91 MB % 32.25/5.47 % (3908540)Instructions burned: 152 (million) % 32.25/5.47 % (3908541)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1405460442:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi) % 32.25/5.47 % (3908510)Instruction limit reached! % 32.25/5.47 % (3908510)------------------------------ % 32.25/5.47 % (3908510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.47 % (3908510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.47 % (3908510)CaDiCaL version: 2.1.3 % 32.25/5.47 % (3908510)Termination reason: Instruction limit % 32.25/5.47 % (3908510)Termination phase: Saturation % 32.25/5.47 % (3908510)Time elapsed: 1.538 s % 32.25/5.47 % (3908510)Peak memory usage: 142 MB % 32.25/5.47 % (3908510)Instructions burned: 2351 (million) % 32.25/5.47 % (3908543)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=909368597:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi) % 32.25/5.47 % (3908545)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1144863586:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi) % 32.25/5.47 % (3908545)Instruction limit reached! % 32.25/5.47 % (3908545)------------------------------ % 32.25/5.47 % (3908545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.47 % (3908545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.47 % (3908545)CaDiCaL version: 2.1.3 % 32.25/5.47 % (3908545)Termination reason: Instruction limit % 32.25/5.47 % (3908545)Termination phase: Saturation % 32.25/5.47 % (3908545)Time elapsed: 0.085 s % 32.25/5.47 % (3908545)Peak memory usage: 90 MB % 32.25/5.47 % (3908545)Instructions burned: 186 (million) % 32.25/5.47 % (3908548)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3304801241:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/193Mi) % 32.25/5.47 % (3908548)Refutation not found, incomplete strategy % 32.25/5.47 % (3908548)------------------------------ % 32.25/5.47 % (3908548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.47 % (3908548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.47 % (3908548)CaDiCaL version: 2.1.3 % 32.25/5.47 % (3908548)Termination reason: Refutation not found, incomplete strategy % 32.25/5.47 % (3908548)Time elapsed: 0.003 s % 32.25/5.47 % (3908548)Peak memory usage: 88 MB % 32.25/5.47 % (3908548)Instructions burned: 3 (million) % 32.25/5.47 % (3908543)Instruction limit reached! % 32.25/5.47 % (3908543)------------------------------ % 32.25/5.47 % (3908543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.25/5.47 % (3908543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.25/5.47 % (3908543)CaDiCaL version: 2.1.3 % 32.25/5.47 % (3908543)Termination reason: Instruction limit % 32.25/5.47 % (3908543)Termination phase: Saturation % 32.25/5.47 % (3908543)Time elapsed: 0.389 s % 32.25/5.47 % (3908543)Peak memory usage: 121 MB % 32.25/5.47 % (3908543)Instructions burned: 668 (million) % 32.25/5.47 % (3908550)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1443265580:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi) % 41.22/6.88 % (3908550)Refutation not found, incomplete strategy % 41.22/6.88 % (3908550)------------------------------ % 41.22/6.88 % (3908550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.22/6.88 % (3908550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.88 % (3908550)CaDiCaL version: 2.1.3 % 41.22/6.88 % (3908550)Termination reason: Refutation not found, incomplete strategy % 41.22/6.88 % (3908550)Time elapsed: 0.005 s % 41.22/6.88 % (3908550)Peak memory usage: 88 MB % 41.22/6.88 % (3908550)Instructions burned: 8 (million) % 41.22/6.88 % (3908548)------------------------------ % 41.22/6.88 % (3908548)------------------------------ % 41.22/6.88 % (3908552)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3488359388:i=12111:sd=1:ss=included_2969 on theBenchmark for (2969ds/12111Mi) % 41.22/6.88 % (3908550)------------------------------ % 41.22/6.88 % (3908550)------------------------------ % 41.22/6.88 % (3908554)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1373554671:i=319:kws=precedence:fsr=off_2967 on theBenchmark for (2967ds/319Mi) % 41.22/6.88 % (3908554)Instruction limit reached! % 41.22/6.88 % (3908554)------------------------------ % 41.22/6.88 % (3908554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.22/6.88 % (3908554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.22/6.88 % (3908554)CaDiCaL version: 2.1.3 % 41.22/6.88 % (3908554)Termination reason: Instruction limit % 41.22/6.88 % (3908554)Termination phase: Saturation % 41.22/6.88 % (3908554)Time elapsed: 0.146 s % 41.22/6.88 % (3908554)Peak memory usage: 92 MB % 41.22/6.88 % (3908554)Instructions burned: 322 (million) % 41.22/6.88 [W927 19:42:35.655662601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655697702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655735212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655746585 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655771845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655783792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655808999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655820816 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.22/6.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.22/6.88 [W927 19:42:35.655845686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.73/9.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.73/9.67 [W927 19:42:35.655857489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.73/9.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.73/9.67 [W927 19:42:35.655889486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.73/9.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.73/9.67 [W927 19:42:35.655911753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.73/9.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.73/9.67 % (3908556)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2837873510:i=2064:ep=RST_2964 on theBenchmark for (2964ds/2064Mi) % 61.73/9.67 % (3908556)Refutation not found, incomplete strategy % 61.73/9.67 % (3908556)------------------------------ % 61.73/9.67 % (3908556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.67 % (3908556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.67 % (3908556)CaDiCaL version: 2.1.3 % 61.73/9.67 % (3908556)Termination reason: Refutation not found, incomplete strategy % 61.73/9.67 % (3908556)Time elapsed: 0.008 s % 61.73/9.67 % (3908556)Peak memory usage: 88 MB % 61.73/9.67 % (3908556)Instructions burned: 16 (million) % 61.73/9.67 % (3908552)Refutation not found, incomplete strategy % 61.73/9.67 % (3908552)------------------------------ % 61.73/9.67 % (3908552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.67 % (3908552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.67 % (3908552)CaDiCaL version: 2.1.3 % 61.73/9.67 % (3908552)Termination reason: Refutation not found, incomplete strategy % 61.73/9.67 % (3908552)Time elapsed: 0.546 s % 61.73/9.67 % (3908552)Peak memory usage: 126 MB % 61.73/9.67 % (3908552)Instructions burned: 830 (million) % 61.73/9.67 % (3908556)------------------------------ % 61.73/9.67 % (3908556)------------------------------ % 61.73/9.67 % (3908552)------------------------------ % 61.73/9.67 % (3908552)------------------------------ % 61.73/9.67 % (3908558)dis-1011_128_sil=32000:random_seed=3701937348:i=3706:ep=RST:av=off_2960 on theBenchmark for (2960ds/3706Mi) % 61.73/9.67 % (3908559)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=316375215:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2959 on theBenchmark for (2959ds/757Mi) % 61.73/9.67 % (3908519)Instruction limit reached! % 61.73/9.67 % (3908519)------------------------------ % 61.73/9.67 % (3908519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.67 % (3908519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.67 % (3908519)CaDiCaL version: 2.1.3 % 61.73/9.67 % (3908519)Termination reason: Instruction limit % 61.73/9.67 % (3908519)Termination phase: Saturation % 61.73/9.67 % (3908519)Time elapsed: 3.099 s % 61.73/9.67 % (3908519)Peak memory usage: 165 MB % 61.73/9.67 % (3908519)Instructions burned: 5202 (million) % 61.73/9.67 % (3908562)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2910687099:i=13913:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/13913Mi) % 61.73/9.67 % (3908559)Instruction limit reached! % 61.73/9.67 % (3908559)------------------------------ % 61.73/9.67 % (3908559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.67 % (3908559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.67 % (3908559)CaDiCaL version: 2.1.3 % 61.73/9.67 % (3908559)Termination reason: Instruction limit % 61.73/9.67 % (3908559)Termination phase: Saturation % 61.73/9.67 % (3908559)Time elapsed: 0.455 s % 61.73/9.67 % (3908559)Peak memory usage: 130 MB % 61.73/9.67 % (3908559)Instructions burned: 757 (million) % 68.83/10.84 % (3908564)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4277972666:i=9925:aac=none_2953 on theBenchmark for (2953ds/9925Mi) % 68.83/10.84 % (3908562)Refutation not found, incomplete strategy % 68.83/10.84 % (3908562)------------------------------ % 68.83/10.84 % (3908562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.83/10.84 % (3908562)CaDiCaL version: 2.1.3 % 68.83/10.84 % (3908562)Termination reason: Refutation not found, incomplete strategy % 68.83/10.84 % (3908562)Time elapsed: 0.573 s % 68.83/10.84 % (3908562)Peak memory usage: 128 MB % 68.83/10.84 % (3908562)Instructions burned: 865 (million) % 68.83/10.84 % (3908537)Instruction limit reached! % 68.83/10.84 % (3908537)------------------------------ % 68.83/10.84 % (3908537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.83/10.84 % (3908537)CaDiCaL version: 2.1.3 % 68.83/10.84 % (3908537)Termination reason: Instruction limit % 68.83/10.84 % (3908537)Termination phase: Saturation % 68.83/10.84 % (3908537)Time elapsed: 3.230 s % 68.83/10.84 % (3908537)Peak memory usage: 144 MB % 68.83/10.84 % (3908537)Instructions burned: 6060 (million) % 68.83/10.84 % (3908562)------------------------------ % 68.83/10.84 % (3908562)------------------------------ % 68.83/10.84 % (3908528)Instruction limit reached! % 68.83/10.84 % (3908528)------------------------------ % 68.83/10.84 % (3908528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.83/10.84 % (3908528)CaDiCaL version: 2.1.3 % 68.83/10.84 % (3908528)Termination reason: Instruction limit % 68.83/10.84 % (3908528)Termination phase: Saturation % 68.83/10.84 % (3908528)Time elapsed: 3.871 s % 68.83/10.84 % (3908528)Peak memory usage: 236 MB % 68.83/10.84 % (3908528)Instructions burned: 13195 (million) % 68.83/10.84 % (3908566)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4121408084:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2947 on theBenchmark for (2947ds/2479Mi) % 68.83/10.84 % (3908566)Refutation not found, incomplete strategy % 68.83/10.84 % (3908566)------------------------------ % 68.83/10.84 % (3908566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.83/10.84 % (3908566)CaDiCaL version: 2.1.3 % 68.83/10.84 % (3908566)Termination reason: Refutation not found, incomplete strategy % 68.83/10.84 % (3908566)Time elapsed: 0.003 s % 68.83/10.84 % (3908566)Peak memory usage: 88 MB % 68.83/10.84 % (3908566)Instructions burned: 3 (million) % 68.83/10.84 % (3908567)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1078849270:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2947 on theBenchmark for (2947ds/440Mi) % 68.83/10.84 % (3908568)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4262237379:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2946 on theBenchmark for (2946ds/11145Mi) % 68.83/10.84 % (3908566)------------------------------ % 68.83/10.84 % (3908566)------------------------------ % 68.83/10.84 % (3908567)Instruction limit reached! % 68.83/10.84 % (3908567)------------------------------ % 68.83/10.84 % (3908567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.83/10.84 % (3908567)CaDiCaL version: 2.1.3 % 68.83/10.84 % (3908567)Termination reason: Instruction limit % 68.83/10.84 % (3908567)Termination phase: Saturation % 68.83/10.84 % (3908567)Time elapsed: 0.237 s % 68.83/10.84 % (3908567)Peak memory usage: 94 MB % 68.83/10.84 % (3908567)Instructions burned: 440 (million) % 68.83/10.84 % (3908572)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1034043386:cts=off:i=3034:av=off:er=known:fsd=on_2943 on theBenchmark for (2943ds/3034Mi) % 68.83/10.84 % (3908573)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=728798285:st=2:s2a=on:i=524:s2at=2:ss=axioms_2943 on theBenchmark for (2943ds/524Mi) % 68.83/10.84 % (3908573)Instruction limit reached! % 68.83/10.84 % (3908573)------------------------------ % 68.83/10.84 % (3908573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.83/10.84 % (3908573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908573)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908573)Termination reason: Instruction limit % 75.21/11.90 % (3908573)Termination phase: Saturation % 75.21/11.90 % (3908573)Time elapsed: 0.237 s % 75.21/11.90 % (3908573)Peak memory usage: 92 MB % 75.21/11.90 % (3908573)Instructions burned: 524 (million) % 75.21/11.90 % (3908558)Instruction limit reached! % 75.21/11.90 % (3908558)------------------------------ % 75.21/11.90 % (3908558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.21/11.90 % (3908558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908558)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908558)Termination reason: Instruction limit % 75.21/11.90 % (3908558)Termination phase: Saturation % 75.21/11.90 % (3908558)Time elapsed: 2.033 s % 75.21/11.90 % (3908558)Peak memory usage: 104 MB % 75.21/11.90 % (3908558)Instructions burned: 3707 (million) % 75.21/11.90 % (3908576)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4143082860:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2939 on theBenchmark for (2939ds/1016Mi) % 75.21/11.90 % (3908576)Refutation not found, incomplete strategy % 75.21/11.90 % (3908576)------------------------------ % 75.21/11.90 % (3908576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.21/11.90 % (3908576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908576)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908576)Termination reason: Refutation not found, incomplete strategy % 75.21/11.90 % (3908576)Time elapsed: 0.002 s % 75.21/11.90 % (3908576)Peak memory usage: 87 MB % 75.21/11.90 % (3908576)Instructions burned: 1 (million) % 75.21/11.90 % (3908577)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2303132351:i=14123:bd=preordered:ins=4_2938 on theBenchmark for (2938ds/14123Mi) % 75.21/11.90 % (3908576)------------------------------ % 75.21/11.90 % (3908576)------------------------------ % 75.21/11.90 % (3908580)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2787485471:i=5781:kws=precedence:bd=all:rawr=on_2935 on theBenchmark for (2935ds/5781Mi) % 75.21/11.90 % (3908572)Instruction limit reached! % 75.21/11.90 % (3908572)------------------------------ % 75.21/11.90 % (3908572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.21/11.90 % (3908572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908572)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908572)Termination reason: Instruction limit % 75.21/11.90 % (3908572)Termination phase: Saturation % 75.21/11.90 % (3908572)Time elapsed: 1.716 s % 75.21/11.90 % (3908572)Peak memory usage: 151 MB % 75.21/11.90 % (3908572)Instructions burned: 3035 (million) % 75.21/11.90 % (3908582)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=729875097:i=2448:gtgl=5:bd=preordered:gtg=all_2925 on theBenchmark for (2925ds/2448Mi) % 75.21/11.90 % (3908568)Instruction limit reached! % 75.21/11.90 % (3908568)------------------------------ % 75.21/11.90 % (3908568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.21/11.90 % (3908568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908568)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908568)Termination reason: Instruction limit % 75.21/11.90 % (3908568)Termination phase: Saturation % 75.21/11.90 % (3908568)Time elapsed: 2.793 s % 75.21/11.90 % (3908568)Peak memory usage: 145 MB % 75.21/11.90 % (3908568)Instructions burned: 11149 (million) % 75.21/11.90 % (3908584)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3566132591:i=3223:kws=precedence:fgj=on:av=off_2917 on theBenchmark for (2917ds/3223Mi) % 75.21/11.90 % (3908582)Instruction limit reached! % 75.21/11.90 % (3908582)------------------------------ % 75.21/11.90 % (3908582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.21/11.90 % (3908582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.21/11.90 % (3908582)CaDiCaL version: 2.1.3 % 75.21/11.90 % (3908582)Termination reason: Instruction limit % 75.21/11.90 % (3908582)Termination phase: Saturation % 75.21/11.90 % (3908582)Time elapsed: 1.023 s % 75.21/11.90 % (3908582)Peak memory usage: 150 MB % 75.21/11.90 % (3908582)Instructions burned: 2451 (million) % 75.21/11.90 % (3908586)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2764234180:st=5.6:i=2033:sd=3:ss=axioms_2913 on theBenchmark for (2913ds/2033Mi) % 83.90/12.86 % (3908580)Instruction limit reached! % 83.90/12.86 % (3908580)------------------------------ % 83.90/12.86 % (3908580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908580)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908580)Termination reason: Instruction limit % 83.90/12.86 % (3908580)Termination phase: Saturation % 83.90/12.86 % (3908580)Time elapsed: 2.528 s % 83.90/12.86 % (3908580)Peak memory usage: 134 MB % 83.90/12.86 % (3908580)Instructions burned: 5783 (million) % 83.90/12.86 % (3908586)Refutation not found, incomplete strategy % 83.90/12.86 % (3908586)------------------------------ % 83.90/12.86 % (3908586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908586)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908586)Termination reason: Refutation not found, incomplete strategy % 83.90/12.86 % (3908586)Time elapsed: 0.342 s % 83.90/12.86 % (3908586)Peak memory usage: 129 MB % 83.90/12.86 % (3908586)Instructions burned: 880 (million) % 83.90/12.86 % (3908541)Instruction limit reached! % 83.90/12.86 % (3908541)------------------------------ % 83.90/12.86 % (3908541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908541)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908541)Termination reason: Instruction limit % 83.90/12.86 % (3908541)Termination phase: Saturation % 83.90/12.86 % (3908541)Time elapsed: 6.994 s % 83.90/12.86 % (3908541)Peak memory usage: 167 MB % 83.90/12.86 % (3908541)Instructions burned: 14156 (million) % 83.90/12.86 % (3908586)------------------------------ % 83.90/12.86 % (3908586)------------------------------ % 83.90/12.86 % (3908564)Instruction limit reached! % 83.90/12.86 % (3908564)------------------------------ % 83.90/12.86 % (3908564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908564)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908564)Termination reason: Instruction limit % 83.90/12.86 % (3908564)Termination phase: Saturation % 83.90/12.86 % (3908564)Time elapsed: 4.554 s % 83.90/12.86 % (3908564)Peak memory usage: 151 MB % 83.90/12.86 % (3908564)Instructions burned: 9926 (million) % 83.90/12.86 % (3908588)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3417513985:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2908 on theBenchmark for (2908ds/2055Mi) % 83.90/12.86 % (3908590)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3536753266:i=4835:sd=13:ss=axioms:sgt=23_2906 on theBenchmark for (2906ds/4835Mi) % 83.90/12.86 % (3908591)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1385721315:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2906 on theBenchmark for (2906ds/797Mi) % 83.90/12.86 % (3908589)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3003801302:i=21611:sd=3:ss=axioms_2906 on theBenchmark for (2906ds/21611Mi) % 83.90/12.86 % (3908591)Instruction limit reached! % 83.90/12.86 % (3908591)------------------------------ % 83.90/12.86 % (3908591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908591)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908591)Termination reason: Instruction limit % 83.90/12.86 % (3908591)Termination phase: Saturation % 83.90/12.86 % (3908591)Time elapsed: 0.424 s % 83.90/12.86 % (3908591)Peak memory usage: 102 MB % 83.90/12.86 % (3908591)Instructions burned: 798 (million) % 83.90/12.86 % (3908588)Refutation not found, incomplete strategy % 83.90/12.86 % (3908588)------------------------------ % 83.90/12.86 % (3908588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.90/12.86 % (3908588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.90/12.86 % (3908588)CaDiCaL version: 2.1.3 % 83.90/12.86 % (3908588)Termination reason: Refutation not found, incomplete strategy % 83.90/12.86 % (3908588)Time elapsed: 0.590 s % 83.90/12.86 % (3908588)Peak memory usage: 129 MB % 83.90/12.86 % (3908588)Instructions burned: 869 (million) % 94.51/14.21 % (3908589)Refutation not found, incomplete strategy % 94.51/14.21 % (3908589)------------------------------ % 94.51/14.21 % (3908589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.21 % (3908589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.21 % (3908589)CaDiCaL version: 2.1.3 % 94.51/14.21 % (3908589)Termination reason: Refutation not found, incomplete strategy % 94.51/14.21 % (3908589)Time elapsed: 0.583 s % 94.51/14.21 % (3908589)Peak memory usage: 128 MB % 94.51/14.21 % (3908589)Instructions burned: 870 (million) % 94.51/14.21 % (3908596)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1444139165:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2900 on theBenchmark for (2900ds/2326Mi) % 94.51/14.21 % (3908596)Refutation not found, incomplete strategy % 94.51/14.21 % (3908596)------------------------------ % 94.51/14.21 % (3908596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.21 % (3908596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.21 % (3908596)CaDiCaL version: 2.1.3 % 94.51/14.21 % (3908596)Termination reason: Refutation not found, incomplete strategy % 94.51/14.21 % (3908596)Time elapsed: 0.013 s % 94.51/14.21 % (3908596)Peak memory usage: 89 MB % 94.51/14.21 % (3908596)Instructions burned: 25 (million) % 94.51/14.21 % (3908588)------------------------------ % 94.51/14.21 % (3908588)------------------------------ % 94.51/14.21 % (3908589)------------------------------ % 94.51/14.21 % (3908589)------------------------------ % 94.51/14.21 % (3908596)------------------------------ % 94.51/14.21 % (3908596)------------------------------ % 94.51/14.21 % (3908598)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2913100501:i=6038:nm=6_2897 on theBenchmark for (2897ds/6038Mi) % 94.51/14.21 % (3908599)lrs+10_1_sil=32000:sp=occurrence:random_seed=2376679745:st=2:i=33334:sd=3:ss=included:sgt=32_2896 on theBenchmark for (2896ds/33334Mi) % 94.51/14.21 % (3908601)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2834305123:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2895 on theBenchmark for (2895ds/1008Mi) % 94.51/14.21 % (3908584)Instruction limit reached! % 94.51/14.21 % (3908584)------------------------------ % 94.51/14.21 % (3908584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.21 % (3908584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.21 % (3908584)CaDiCaL version: 2.1.3 % 94.51/14.21 % (3908584)Termination reason: Instruction limit % 94.51/14.21 % (3908584)Termination phase: Saturation % 94.51/14.21 % (3908584)Time elapsed: 2.171 s % 94.51/14.21 % (3908584)Peak memory usage: 147 MB % 94.51/14.21 % (3908584)Instructions burned: 3224 (million) % 94.51/14.21 % (3908590)Instruction limit reached! % 94.51/14.21 % (3908590)------------------------------ % 94.51/14.21 % (3908590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.21 % (3908590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.21 % (3908590)CaDiCaL version: 2.1.3 % 94.51/14.21 % (3908590)Termination reason: Instruction limit % 94.51/14.21 % (3908590)Termination phase: Saturation % 94.51/14.21 % (3908590)Time elapsed: 1.197 s % 94.51/14.21 % (3908590)Peak memory usage: 135 MB % 94.51/14.21 % (3908590)Instructions burned: 4840 (million) % 94.51/14.21 % (3908604)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3423860788:i=8327:s2at=5:bd=preordered_2893 on theBenchmark for (2893ds/8327Mi) % 94.51/14.21 % (3908605)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3885542888:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2892 on theBenchmark for (2892ds/1083Mi) % 94.51/14.21 % (3908598)Refutation not found, incomplete strategy % 94.51/14.21 % (3908598)------------------------------ % 94.51/14.21 % (3908598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.51/14.21 % (3908598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.51/14.21 % (3908598)CaDiCaL version: 2.1.3 % 94.51/14.21 % (3908598)Termination reason: Refutation not found, incomplete strategy % 94.51/14.21 % (3908598)Time elapsed: 0.625 s % 94.51/14.21 % (3908598)Peak memory usage: 130 MB % 94.51/14.21 % (3908598)Instructions burned: 946 (million) % 106.11/15.96 % (3908601)Instruction limit reached! % 106.11/15.96 % (3908601)------------------------------ % 106.11/15.96 % (3908601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.11/15.96 % (3908601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.11/15.96 % (3908601)CaDiCaL version: 2.1.3 % 106.11/15.96 % (3908601)Termination reason: Instruction limit % 106.11/15.96 % (3908601)Termination phase: Saturation % 106.11/15.96 % (3908601)Time elapsed: 0.473 s % 106.11/15.96 % (3908601)Peak memory usage: 94 MB % 106.11/15.96 % (3908601)Instructions burned: 1008 (million) % 106.11/15.96 % (3908605)Instruction limit reached! % 106.11/15.96 % (3908605)------------------------------ % 106.11/15.96 % (3908605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.11/15.96 % (3908605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.11/15.96 % (3908605)CaDiCaL version: 2.1.3 % 106.11/15.96 % (3908605)Termination reason: Instruction limit % 106.11/15.96 % (3908605)Termination phase: Saturation % 106.11/15.96 % (3908605)Time elapsed: 0.264 s % 106.11/15.96 % (3908605)Peak memory usage: 100 MB % 106.11/15.96 % (3908605)Instructions burned: 1087 (million) % 106.11/15.96 % (3908608)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2116239418:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2889 on theBenchmark for (2889ds/1084Mi) % 106.11/15.96 % (3908608)Refutation not found, incomplete strategy % 106.11/15.96 % (3908608)------------------------------ % 106.11/15.96 % (3908608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.11/15.96 % (3908608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.11/15.96 % (3908608)CaDiCaL version: 2.1.3 % 106.11/15.96 % (3908608)Termination reason: Refutation not found, incomplete strategy % 106.11/15.96 % (3908608)Time elapsed: 0.002 s % 106.11/15.96 % (3908608)Peak memory usage: 86 MB % 106.11/15.96 % (3908608)Instructions burned: 1 (million) % 106.11/15.96 % (3908609)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4004398110:i=6995:s2at=5:gtg=all_2888 on theBenchmark for (2888ds/6995Mi) % 106.11/15.96 % (3908598)------------------------------ % 106.11/15.96 % (3908598)------------------------------ % 106.11/15.96 % (3908612)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=581122609:st=2:i=6225:sd=15:ss=axioms_2887 on theBenchmark for (2887ds/6225Mi) % 106.11/15.96 % (3908608)------------------------------ % 106.11/15.96 % (3908608)------------------------------ % 106.11/15.96 % (3908612)Refutation not found, incomplete strategy % 106.11/15.96 % (3908612)------------------------------ % 106.11/15.96 % (3908612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.11/15.96 % (3908612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.11/15.96 % (3908612)CaDiCaL version: 2.1.3 % 106.11/15.96 % (3908612)Termination reason: Refutation not found, incomplete strategy % 106.11/15.96 % (3908612)Time elapsed: 0.005 s % 106.11/15.96 % (3908612)Peak memory usage: 88 MB % 106.11/15.96 % (3908612)Instructions burned: 7 (million) % 106.11/15.96 % (3908614)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2500783334:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2885 on theBenchmark for (2885ds/3372Mi) % 106.11/15.96 % (3908612)------------------------------ % 106.11/15.96 % (3908612)------------------------------ % 106.11/15.96 % (3908616)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=88789350:st=2.3:i=26457:sd=10:ss=included:sgt=8_2882 on theBenchmark for (2882ds/26457Mi) % 106.11/15.96 [W927 19:42:44.070985700 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.11/15.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.11/15.96 [W927 19:42:44.071037547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.11/15.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.11/15.96 [W927 19:42:44.071076500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071088291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071119674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071130414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071154198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071164958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071188241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071199151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071223085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 [W927 19:42:44.071233945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.85/18.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.85/18.12 % (3908614)Refutation not found, incomplete strategy % 121.85/18.12 % (3908614)------------------------------ % 121.85/18.12 % (3908614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.85/18.12 % (3908614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.85/18.12 % (3908614)CaDiCaL version: 2.1.3 % 121.85/18.12 % (3908614)Termination reason: Refutation not found, incomplete strategy % 121.85/18.12 % (3908614)Time elapsed: 0.553 s % 121.85/18.12 % (3908614)Peak memory usage: 127 MB % 121.85/18.12 % (3908614)Instructions burned: 837 (million) % 121.85/18.12 % (3908614)------------------------------ % 121.85/18.12 % (3908614)------------------------------ % 121.85/18.12 % (3908618)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=2842642108:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2875 on theBenchmark for (2875ds/13494Mi) % 121.85/18.12 % (3908609)Instruction limit reached! % 121.85/18.12 % (3908609)------------------------------ % 121.85/18.12 % (3908609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.85/18.12 % (3908609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.85/18.12 % (3908609)CaDiCaL version: 2.1.3 % 151.67/22.36 % (3908609)Termination reason: Instruction limit % 151.67/22.36 % (3908609)Termination phase: Saturation % 151.67/22.36 % (3908609)Time elapsed: 2.137 s % 151.67/22.36 % (3908609)Peak memory usage: 207 MB % 151.67/22.36 % (3908609)Instructions burned: 6997 (million) % 151.67/22.36 % (3908716)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1942040082:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2866 on theBenchmark for (2866ds/2503Mi) % 151.67/22.36 % (3908716)Instruction limit reached! % 151.67/22.36 % (3908716)------------------------------ % 151.67/22.36 % (3908716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.67/22.36 % (3908716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.67/22.36 % (3908716)CaDiCaL version: 2.1.3 % 151.67/22.36 % (3908716)Termination reason: Instruction limit % 151.67/22.36 % (3908716)Termination phase: Saturation % 151.67/22.36 % (3908716)Time elapsed: 1.053 s % 151.67/22.36 % (3908716)Peak memory usage: 144 MB % 151.67/22.36 % (3908716)Instructions burned: 2505 (million) % 151.67/22.36 % (3908884)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=343993601:i=2559:sd=1:ep=RSTC:ss=axioms_2854 on theBenchmark for (2854ds/2559Mi) % 151.67/22.36 [W927 19:42:47.175769530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175811773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175846958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175857064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175883958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175893552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175917704 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175927257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175951700 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.67/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.67/22.36 [W927 19:42:47.175963060 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.00/22.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.00/22.96 [W927 19:42:47.175986797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.00/22.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.00/22.96 [W927 19:42:47.175996692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.00/22.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.00/22.96 % (3908884)Refutation not found, incomplete strategy % 155.00/22.96 % (3908884)------------------------------ % 155.00/22.96 % (3908884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.00/22.96 % (3908884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.00/22.96 % (3908884)CaDiCaL version: 2.1.3 % 155.00/22.96 % (3908884)Termination reason: Refutation not found, incomplete strategy % 155.00/22.96 % (3908884)Time elapsed: 0.491 s % 155.00/22.96 % (3908884)Peak memory usage: 127 MB % 155.00/22.96 % (3908884)Instructions burned: 834 (million) % 155.00/22.96 % (3908884)------------------------------ % 155.00/22.96 % (3908884)------------------------------ % 155.00/22.96 % (3908906)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4092143052:i=30753:av=off:ss=included_2844 on theBenchmark for (2844ds/30753Mi) % 155.00/22.96 % (3908577)Instruction limit reached! % 155.00/22.96 % (3908577)------------------------------ % 155.00/22.96 % (3908577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.00/22.96 % (3908577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.00/22.96 % (3908577)CaDiCaL version: 2.1.3 % 155.00/22.96 % (3908577)Termination reason: Instruction limit % 155.00/22.96 % (3908577)Termination phase: Saturation % 155.00/22.96 % (3908577)Time elapsed: 9.830 s % 155.00/22.96 % (3908577)Peak memory usage: 240 MB % 155.00/22.96 % (3908577)Instructions burned: 14123 (million) % 155.00/22.96 % (3908906)Refutation not found, incomplete strategy % 155.00/22.96 % (3908906)------------------------------ % 155.00/22.96 % (3908906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.00/22.96 % (3908906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.00/22.96 % (3908906)CaDiCaL version: 2.1.3 % 155.00/22.96 % (3908906)Termination reason: Refutation not found, incomplete strategy % 155.00/22.96 % (3908906)Time elapsed: 0.507 s % 155.00/22.96 % (3908906)Peak memory usage: 128 MB % 155.00/22.96 % (3908906)Instructions burned: 900 (million) % 155.00/22.96 % (3908604)Instruction limit reached! % 155.00/22.96 % (3908604)------------------------------ % 155.00/22.96 % (3908604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.00/22.96 % (3908604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.00/22.96 % (3908604)CaDiCaL version: 2.1.3 % 155.00/22.96 % (3908604)Termination reason: Instruction limit % 155.00/22.96 % (3908604)Termination phase: Saturation % 155.00/22.96 % (3908604)Time elapsed: 5.666 s % 155.00/22.96 % (3908604)Peak memory usage: 207 MB % 155.00/22.96 % (3908604)Instructions burned: 8328 (million) % 155.00/22.96 % (3908913)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=771392761:i=26473:ep=RSTC_2838 on theBenchmark for (2838ds/26473Mi) % 155.00/22.96 % (3908906)------------------------------ % 155.00/22.96 % (3908906)------------------------------ % 155.00/22.96 % (3908917)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=458909245:cts=off:i=2759:kws=inv_arity:fgj=on_2835 on theBenchmark for (2835ds/2759Mi) % 155.00/22.96 % (3908919)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=1018199442:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2834 on theBenchmark for (2834ds/5665Mi) % 155.00/22.96 % (3908919)Refutation not found, incomplete strategy % 155.00/22.96 % (3908919)------------------------------ % 155.00/22.96 % (3908919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908919)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908919)Termination reason: Refutation not found, incomplete strategy % 175.94/25.70 % (3908919)Time elapsed: 0.493 s % 175.94/25.70 % (3908919)Peak memory usage: 129 MB % 175.94/25.70 % (3908919)Instructions burned: 860 (million) % 175.94/25.70 % (3908919)------------------------------ % 175.94/25.70 % (3908919)------------------------------ % 175.94/25.70 % (3908917)Refutation not found, incomplete strategy % 175.94/25.70 % (3908917)------------------------------ % 175.94/25.70 % (3908917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908917)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908917)Termination reason: Refutation not found, incomplete strategy % 175.94/25.70 % (3908917)Time elapsed: 0.954 s % 175.94/25.70 % (3908917)Peak memory usage: 130 MB % 175.94/25.70 % (3908917)Instructions burned: 913 (million) % 175.94/25.70 % (3908924)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=156439983:i=1532:ep=RS:ss=axioms_2823 on theBenchmark for (2823ds/1532Mi) % 175.94/25.70 % (3908917)------------------------------ % 175.94/25.70 % (3908917)------------------------------ % 175.94/25.70 % (3908926)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1251338850:i=1565:sd=2:ss=axioms:sgt=32_2819 on theBenchmark for (2819ds/1565Mi) % 175.94/25.70 % (3908924)Refutation not found, incomplete strategy % 175.94/25.70 % (3908924)------------------------------ % 175.94/25.70 % (3908924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908924)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908924)Termination reason: Refutation not found, incomplete strategy % 175.94/25.70 % (3908924)Time elapsed: 0.916 s % 175.94/25.70 % (3908924)Peak memory usage: 128 MB % 175.94/25.70 % (3908924)Instructions burned: 863 (million) % 175.94/25.70 % (3908924)------------------------------ % 175.94/25.70 % (3908924)------------------------------ % 175.94/25.70 % (3908932)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=2852928789:i=1572:fgj=on:gsp=on_2807 on theBenchmark for (2807ds/1572Mi) % 175.94/25.70 % (3908926)Instruction limit reached! % 175.94/25.70 % (3908926)------------------------------ % 175.94/25.70 % (3908926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908926)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908926)Termination reason: Instruction limit % 175.94/25.70 % (3908926)Termination phase: Saturation % 175.94/25.70 % (3908926)Time elapsed: 1.714 s % 175.94/25.70 % (3908926)Peak memory usage: 132 MB % 175.94/25.70 % (3908926)Instructions burned: 1565 (million) % 175.94/25.70 % (3908936)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2549168299:i=6052:sd=4:ss=axioms:sgt=24_2799 on theBenchmark for (2799ds/6052Mi) % 175.94/25.70 % (3908932)Instruction limit reached! % 175.94/25.70 % (3908932)------------------------------ % 175.94/25.70 % (3908932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908932)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908932)Termination reason: Instruction limit % 175.94/25.70 % (3908932)Termination phase: Saturation % 175.94/25.70 % (3908932)Time elapsed: 1.666 s % 175.94/25.70 % (3908932)Peak memory usage: 135 MB % 175.94/25.70 % (3908932)Instructions burned: 1572 (million) % 175.94/25.70 % (3908936)Refutation not found, incomplete strategy % 175.94/25.70 % (3908936)------------------------------ % 175.94/25.70 % (3908936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.94/25.70 % (3908936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.94/25.70 % (3908936)CaDiCaL version: 2.1.3 % 175.94/25.70 % (3908936)Termination reason: Refutation not found, incomplete strategy % 175.94/25.70 % (3908936)Time elapsed: 0.932 s % 175.94/25.70 % (3908936)Peak memory usage: 128 MB % 175.94/25.70 % (3908936)Instructions burned: 880 (million) % 175.94/25.70 % (3908942)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=1583775274:i=3500:sd=1:bd=preordered:sup=off:ss=included_2787 on theBenchmark for (2787ds/3500Mi) % 196.94/28.79 % (3908936)------------------------------ % 196.94/28.79 % (3908936)------------------------------ % 196.94/28.79 % (3908944)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=2712199751:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2782 on theBenchmark for (2782ds/1842Mi) % 196.94/28.79 [W927 19:42:54.176581342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176628186 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176685909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176705360 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176748150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176765717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176807424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176825247 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176867214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176884954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176926978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.94/28.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.94/28.79 [W927 19:42:54.176944698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 % (3908942)Refutation not found, incomplete strategy % 216.89/31.56 % (3908942)------------------------------ % 216.89/31.56 % (3908942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.89/31.56 % (3908942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.89/31.56 % (3908942)CaDiCaL version: 2.1.3 % 216.89/31.56 % (3908942)Termination reason: Refutation not found, incomplete strategy % 216.89/31.56 % (3908942)Time elapsed: 0.885 s % 216.89/31.56 % (3908942)Peak memory usage: 126 MB % 216.89/31.56 % (3908942)Instructions burned: 834 (million) % 216.89/31.56 % (3908942)------------------------------ % 216.89/31.56 % (3908942)------------------------------ % 216.89/31.56 % (3908946)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=908469005:i=66096:add=on_2771 on theBenchmark for (2771ds/66096Mi) % 216.89/31.56 % (3908618)Instruction limit reached! % 216.89/31.56 % (3908618)------------------------------ % 216.89/31.56 % (3908618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.89/31.56 % (3908618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.89/31.56 % (3908618)CaDiCaL version: 2.1.3 % 216.89/31.56 % (3908618)Termination reason: Instruction limit % 216.89/31.56 % (3908618)Termination phase: Saturation % 216.89/31.56 % (3908618)Time elapsed: 11.348 s % 216.89/31.56 % (3908618)Peak memory usage: 259 MB % 216.89/31.56 % (3908618)Instructions burned: 13495 (million) % 216.89/31.56 % (3908944)Instruction limit reached! % 216.89/31.56 % (3908944)------------------------------ % 216.89/31.56 % (3908944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.89/31.56 % (3908944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.89/31.56 % (3908944)CaDiCaL version: 2.1.3 % 216.89/31.56 % (3908944)Termination reason: Instruction limit % 216.89/31.56 % (3908944)Termination phase: Saturation % 216.89/31.56 % (3908944)Time elapsed: 2.029 s % 216.89/31.56 % (3908944)Peak memory usage: 137 MB % 216.89/31.56 % (3908944)Instructions burned: 1842 (million) % 216.89/31.56 % (3908950)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3247339849:i=1884:sd=1:nm=60:ss=axioms_2760 on theBenchmark for (2760ds/1884Mi) % 216.89/31.56 % (3908951)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1126334175:cts=off:i=5469:bs=on:fsr=off_2760 on theBenchmark for (2760ds/5469Mi) % 216.89/31.56 [W927 19:42:56.911758376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 [W927 19:42:56.911816320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 [W927 19:42:56.911872040 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 [W927 19:42:56.911888980 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 [W927 19:42:56.911929037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.89/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.89/31.56 [W927 19:42:56.911945394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.911985357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.912013214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.912055065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.912071771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.912111402 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 [W927 19:42:56.912127872 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 251.55/36.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 251.55/36.42 % (3908950)Refutation not found, incomplete strategy % 251.55/36.42 % (3908950)------------------------------ % 251.55/36.42 % (3908950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.55/36.42 % (3908950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.55/36.42 % (3908950)CaDiCaL version: 2.1.3 % 251.55/36.42 % (3908950)Termination reason: Refutation not found, incomplete strategy % 251.55/36.42 % (3908950)Time elapsed: 0.872 s % 251.55/36.42 % (3908950)Peak memory usage: 127 MB % 251.55/36.42 % (3908950)Instructions burned: 834 (million) % 251.55/36.42 % (3908950)------------------------------ % 251.55/36.42 % (3908950)------------------------------ % 251.55/36.42 % (3908958)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=2940123443:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2744 on theBenchmark for (2744ds/2037Mi) % 251.55/36.42 % (3908616)Instruction limit reached! % 251.55/36.42 % (3908616)------------------------------ % 251.55/36.42 % (3908616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.55/36.42 % (3908616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.55/36.42 % (3908616)CaDiCaL version: 2.1.3 % 251.55/36.42 % (3908616)Termination reason: Instruction limit % 251.55/36.42 % (3908616)Termination phase: Saturation % 251.55/36.42 % (3908616)Time elapsed: 15.658 s % 251.55/36.42 % (3908616)Peak memory usage: 367 MB % 251.55/36.42 % (3908616)Instructions burned: 26458 (million) % 251.55/36.42 % (3908962)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4038996038:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2724 on theBenchmark for (2724ds/2110Mi) % 251.55/36.42 % (3908958)Instruction limit reached! % 251.55/36.42 % (3908958)------------------------------ % 251.55/36.42 % (3908958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 251.55/36.42 % (3908958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.55/36.42 % (3908958)CaDiCaL version: 2.1.3 % 251.55/36.42 % (3908958)Termination reason: Instruction limit % 251.55/36.42 % (3908958)Termination phase: Saturation % 251.55/36.42 % (3908958)Time elapsed: 2.068 s % 251.55/36.42 % (3908958)Peak memory usage: 143 MB % 251.55/36.42 % (3908958)Instructions burned: 2037 (million) % 252.27/36.57 % (3908964)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=3593404454:i=2430:add=off:aac=none:nm=16_2720 on theBenchmark for (2720ds/2430Mi) % 252.27/36.57 % (3908951)Instruction limit reached! % 252.27/36.57 % (3908951)------------------------------ % 252.27/36.57 % (3908951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908951)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908951)Termination reason: Instruction limit % 252.27/36.57 % (3908951)Termination phase: Saturation % 252.27/36.57 % (3908951)Time elapsed: 4.626 s % 252.27/36.57 % (3908951)Peak memory usage: 98 MB % 252.27/36.57 % (3908951)Instructions burned: 5470 (million) % 252.27/36.57 % (3908599)Refutation not found, non-redundant clauses discarded % 252.27/36.57 % (3908599)------------------------------ % 252.27/36.57 % (3908599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908599)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908599)Termination reason: Refutation not found, non-redundant clauses discarded % 252.27/36.57 % (3908599)Time elapsed: 18.498 s % 252.27/36.57 % (3908599)Peak memory usage: 316 MB % 252.27/36.57 % (3908599)Instructions burned: 29107 (million) % 252.27/36.57 % (3908968)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=4012753806:cond=fast:i=4891_2710 on theBenchmark for (2710ds/4891Mi) % 252.27/36.57 % (3908599)------------------------------ % 252.27/36.57 % (3908599)------------------------------ % 252.27/36.57 % (3908962)Instruction limit reached! % 252.27/36.57 % (3908962)------------------------------ % 252.27/36.57 % (3908962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908962)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908962)Termination reason: Instruction limit % 252.27/36.57 % (3908962)Termination phase: Saturation % 252.27/36.57 % (3908962)Time elapsed: 1.663 s % 252.27/36.57 % (3908962)Peak memory usage: 142 MB % 252.27/36.57 % (3908962)Instructions burned: 2111 (million) % 252.27/36.57 % (3908970)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=726285189:st=2:i=14845:sd=2:ss=included:fsd=on_2705 on theBenchmark for (2705ds/14845Mi) % 252.27/36.57 % (3908971)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1575266229:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2705 on theBenchmark for (2705ds/7534Mi) % 252.27/36.57 % (3908964)Instruction limit reached! % 252.27/36.57 % (3908964)------------------------------ % 252.27/36.57 % (3908964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908964)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908964)Termination reason: Instruction limit % 252.27/36.57 % (3908964)Termination phase: Saturation % 252.27/36.57 % (3908964)Time elapsed: 2.291 s % 252.27/36.57 % (3908964)Peak memory usage: 142 MB % 252.27/36.57 % (3908964)Instructions burned: 2430 (million) % 252.27/36.57 % (3908970)Refutation not found, incomplete strategy % 252.27/36.57 % (3908970)------------------------------ % 252.27/36.57 % (3908970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908970)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908970)Termination reason: Refutation not found, incomplete strategy % 252.27/36.57 % (3908970)Time elapsed: 0.925 s % 252.27/36.57 % (3908970)Peak memory usage: 129 MB % 252.27/36.57 % (3908970)Instructions burned: 900 (million) % 252.27/36.57 % (3908971)Refutation not found, incomplete strategy % 252.27/36.57 % (3908971)------------------------------ % 252.27/36.57 % (3908971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.27/36.57 % (3908971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.27/36.57 % (3908971)CaDiCaL version: 2.1.3 % 252.27/36.57 % (3908971)Termination reason: Refutation not found, incomplete strategy % 252.27/36.57 % (3908971)Time elapsed: 0.917 s % 252.27/36.57 % (3908971)Peak memory usage: 128 MB % 276.17/40.03 % (3908971)Instructions burned: 874 (million) % 276.17/40.03 % (3908976)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=4066479353:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2694 on theBenchmark for (2694ds/10353Mi) % 276.17/40.03 % (3908970)------------------------------ % 276.17/40.03 % (3908970)------------------------------ % 276.17/40.03 % (3908971)------------------------------ % 276.17/40.03 % (3908971)------------------------------ % 276.17/40.03 % (3908978)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2720481498:i=7860_2689 on theBenchmark for (2689ds/7860Mi) % 276.17/40.03 % (3908978)Refutation not found, incomplete strategy % 276.17/40.03 % (3908978)------------------------------ % 276.17/40.03 % (3908978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.17/40.03 % (3908978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.17/40.03 % (3908978)CaDiCaL version: 2.1.3 % 276.17/40.03 % (3908978)Termination reason: Refutation not found, incomplete strategy % 276.17/40.03 % (3908978)Time elapsed: 0.022 s % 276.17/40.03 % (3908978)Peak memory usage: 88 MB % 276.17/40.03 % (3908978)Instructions burned: 22 (million) % 276.17/40.03 % (3908979)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=2241835712:i=7896:sd=2:bs=on:ss=included:sgt=20_2688 on theBenchmark for (2688ds/7896Mi) % 276.17/40.03 % (3908978)------------------------------ % 276.17/40.03 % (3908978)------------------------------ % 276.17/40.03 % (3908968)Instruction limit reached! % 276.17/40.03 % (3908968)------------------------------ % 276.17/40.03 % (3908968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.17/40.03 % (3908968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.17/40.03 % (3908968)CaDiCaL version: 2.1.3 % 276.17/40.03 % (3908968)Termination reason: Instruction limit % 276.17/40.03 % (3908968)Termination phase: Saturation % 276.17/40.03 % (3908968)Time elapsed: 2.753 s % 276.17/40.03 % (3908968)Peak memory usage: 161 MB % 276.17/40.03 % (3908968)Instructions burned: 4892 (million) % 276.17/40.03 % (3908982)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2738335143:i=5812:gtgl=2:gtg=all_2682 on theBenchmark for (2682ds/5812Mi) % 276.17/40.03 % (3908983)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=1126546191:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2680 on theBenchmark for (2680ds/2965Mi) % 276.17/40.03 % (3908983)Refutation not found, incomplete strategy % 276.17/40.03 % (3908983)------------------------------ % 276.17/40.03 % (3908983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.17/40.03 % (3908983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.17/40.03 % (3908983)CaDiCaL version: 2.1.3 % 276.17/40.03 % (3908983)Termination reason: Refutation not found, incomplete strategy % 276.17/40.03 % (3908983)Time elapsed: 0.520 s % 276.17/40.03 % (3908983)Peak memory usage: 132 MB % 276.17/40.03 % (3908983)Instructions burned: 946 (million) % 276.17/40.03 % (3908983)------------------------------ % 276.17/40.03 % (3908983)------------------------------ % 276.17/40.03 % (3908988)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=889218552:i=2967:kws=precedence:bd=preordered:av=off_2670 on theBenchmark for (2670ds/2967Mi) % 276.17/40.03 % (3908982)Instruction limit reached! % 276.17/40.03 % (3908982)------------------------------ % 276.17/40.03 % (3908982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.17/40.03 % (3908982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.17/40.03 % (3908982)CaDiCaL version: 2.1.3 % 276.17/40.03 % (3908982)Termination reason: Instruction limit % 276.17/40.03 % (3908982)Termination phase: Saturation % 276.17/40.03 % (3908982)Time elapsed: 2.987 s % 276.17/40.03 % (3908982)Peak memory usage: 230 MB % 276.17/40.03 % (3908982)Instructions burned: 5812 (million) % 276.17/40.03 % (3908990)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3437194628:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2649 on theBenchmark for (2649ds/3022Mi) % 276.17/40.03 [W927 19:43:07.632964599 register_special_opsTerminated %------------------------------------------------------------------------------