%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM368+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 : n017.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:15 PM UTC 2026 % Result : Timeout 300.10s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM368+1 : TPTP v9.3.1. Released v3.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.36 % Computer : n017.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sun Sep 27 19:35:50 UTC 2026 % 0.11/0.36 % CPUTime : % 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.11/0.40 Running first-order theorem proving % 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.62/1.41 % (2892522)Detected formulas, will run a generic FOF schedule. % 3.62/1.41 % (2892530)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4060325443:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 3.62/1.41 % (2892530)Refutation not found, incomplete strategy % 3.62/1.41 % (2892530)------------------------------ % 3.62/1.41 % (2892530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.62/1.41 % (2892530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.62/1.41 % (2892530)CaDiCaL version: 2.1.3 % 3.62/1.41 % (2892530)Termination reason: Refutation not found, incomplete strategy % 3.62/1.41 % (2892530)Time elapsed: 0.001 s % 3.62/1.41 % (2892530)Peak memory usage: 87 MB % 3.62/1.41 % (2892530)Instructions burned: 1 (million) % 3.62/1.41 % (2892529)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=1876563969:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 3.62/1.41 % (2892528)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=1795570239:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 3.62/1.41 % (2892527)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=2496338957:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 3.62/1.41 % (2892531)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2961552013:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 3.62/1.41 % (2892533)dis-21_1_sil=8000:lcm=predicate:random_seed=614253463: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.62/1.41 % (2892531)Refutation not found, incomplete strategy % 3.62/1.41 % (2892531)------------------------------ % 3.62/1.41 % (2892531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.62/1.41 % (2892531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.62/1.41 % (2892531)CaDiCaL version: 2.1.3 % 3.62/1.41 % (2892531)Termination reason: Refutation not found, incomplete strategy % 3.62/1.41 % (2892531)Time elapsed: 0.002 s % 3.62/1.41 % (2892531)Peak memory usage: 87 MB % 3.62/1.41 % (2892531)Instructions burned: 2 (million) % 3.62/1.41 % (2892532)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2418007530:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 3.62/1.41 % (2892533)Instruction limit reached! % 3.62/1.41 % (2892533)------------------------------ % 3.62/1.41 % (2892533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.62/1.41 % (2892533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.62/1.41 % (2892533)CaDiCaL version: 2.1.3 % 3.62/1.41 % (2892533)Termination reason: Instruction limit % 3.62/1.41 % (2892533)Termination phase: Saturation % 3.62/1.41 % (2892533)Time elapsed: 0.057 s % 3.62/1.41 % (2892533)Peak memory usage: 88 MB % 3.62/1.41 % (2892533)Instructions burned: 131 (million) % 3.62/1.41 % (2892530)------------------------------ % 3.62/1.41 % (2892530)------------------------------ % 3.62/1.41 % (2892532)Instruction limit reached! % 3.62/1.41 % (2892532)------------------------------ % 3.62/1.41 % (2892532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.62/1.41 % (2892532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.62/1.41 % (2892532)CaDiCaL version: 2.1.3 % 3.62/1.41 % (2892532)Termination reason: Instruction limit % 3.62/1.41 % (2892532)Termination phase: Saturation % 3.62/1.41 % (2892532)Time elapsed: 0.084 s % 3.62/1.41 % (2892532)Peak memory usage: 90 MB % 3.62/1.41 % (2892532)Instructions burned: 139 (million) % 3.62/1.41 % (2892542)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3858501068:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 3.62/1.41 % (2892542)Refutation not found, incomplete strategy % 3.62/1.41 % (2892542)------------------------------ % 3.62/1.41 % (2892542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.62/1.41 % (2892542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.62/1.41 % (2892542)CaDiCaL version: 2.1.3 % 3.62/1.41 % (2892542)Termination reason: Refutation not found, incomplete strategy % 3.62/1.41 % (2892542)Time elapsed: 0.002 s % 5.96/1.71 % (2892542)Peak memory usage: 87 MB % 5.96/1.71 % (2892542)Instructions burned: 5 (million) % 5.96/1.71 % (2892541)lrs+10_1_sil=8000:sp=occurrence:random_seed=2893086206:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 5.96/1.71 % (2892541)Refutation not found, incomplete strategy % 5.96/1.71 % (2892541)------------------------------ % 5.96/1.71 % (2892541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.96/1.71 % (2892541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.71 % (2892541)CaDiCaL version: 2.1.3 % 5.96/1.71 % (2892541)Termination reason: Refutation not found, incomplete strategy % 5.96/1.71 % (2892541)Time elapsed: 0.002 s % 5.96/1.71 % (2892541)Peak memory usage: 88 MB % 5.96/1.71 % (2892541)Instructions burned: 1 (million) % 5.96/1.71 % (2892531)------------------------------ % 5.96/1.71 % (2892531)------------------------------ % 5.96/1.71 % (2892543)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3220937067:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 5.96/1.71 % (2892543)Refutation not found, incomplete strategy % 5.96/1.71 % (2892543)------------------------------ % 5.96/1.71 % (2892543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.96/1.71 % (2892543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.96/1.71 % (2892543)CaDiCaL version: 2.1.3 % 5.96/1.71 % (2892543)Termination reason: Refutation not found, incomplete strategy % 5.96/1.71 % (2892543)Time elapsed: 0.002 s % 5.96/1.71 % (2892543)Peak memory usage: 87 MB % 5.96/1.71 % (2892543)Instructions burned: 1 (million) % 5.96/1.71 % (2892542)------------------------------ % 5.96/1.71 % (2892542)------------------------------ % 5.96/1.71 [W927 19:35:51.654087573 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654123880 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654163790 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654177223 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654204124 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654215887 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654241530 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654253104 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/1.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.96/1.71 [W927 19:35:51.654277077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.654288584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.654319471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.654341644 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.654994152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655039592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655078486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655092503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655118623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655130510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655155940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655167783 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655193177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.73/2.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.73/2.13 [W927 19:35:51.655205017 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.02/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.02/2.84 [W927 19:35:51.655229994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.02/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.02/2.84 [W927 19:35:51.655296687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.02/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.02/2.84 % (2892546)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=1876406195:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 13.02/2.84 % (2892541)------------------------------ % 13.02/2.84 % (2892541)------------------------------ % 13.02/2.84 % (2892548)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=833248578:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 13.02/2.84 % (2892548)Refutation not found, incomplete strategy % 13.02/2.84 % (2892548)------------------------------ % 13.02/2.84 % (2892548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.84 % (2892548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.84 % (2892548)CaDiCaL version: 2.1.3 % 13.02/2.84 % (2892548)Termination reason: Refutation not found, incomplete strategy % 13.02/2.84 % (2892548)Time elapsed: 0.002 s % 13.02/2.84 % (2892548)Peak memory usage: 88 MB % 13.02/2.84 % (2892548)Instructions burned: 3 (million) % 13.02/2.84 % (2892543)------------------------------ % 13.02/2.84 % (2892543)------------------------------ % 13.02/2.84 % (2892529)Refutation not found, incomplete strategy % 13.02/2.84 % (2892529)------------------------------ % 13.02/2.84 % (2892529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.84 % (2892529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.84 % (2892529)CaDiCaL version: 2.1.3 % 13.02/2.84 % (2892529)Termination reason: Refutation not found, incomplete strategy % 13.02/2.84 % (2892529)Time elapsed: 0.568 s % 13.02/2.84 % (2892529)Peak memory usage: 126 MB % 13.02/2.84 % (2892529)Instructions burned: 835 (million) % 13.02/2.84 % (2892528)Refutation not found, incomplete strategy % 13.02/2.84 % (2892528)------------------------------ % 13.02/2.84 % (2892528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.84 % (2892528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.84 % (2892528)CaDiCaL version: 2.1.3 % 13.02/2.84 % (2892528)Termination reason: Refutation not found, incomplete strategy % 13.02/2.84 % (2892528)Time elapsed: 0.569 s % 13.02/2.84 % (2892528)Peak memory usage: 126 MB % 13.02/2.84 % (2892528)Instructions burned: 835 (million) % 13.02/2.84 % (2892546)Instruction limit reached! % 13.02/2.84 % (2892546)------------------------------ % 13.02/2.84 % (2892546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.84 % (2892546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.84 % (2892546)CaDiCaL version: 2.1.3 % 13.02/2.84 % (2892546)Termination reason: Instruction limit % 13.02/2.84 % (2892546)Termination phase: Saturation % 13.02/2.84 % (2892546)Time elapsed: 0.134 s % 13.02/2.84 % (2892546)Peak memory usage: 90 MB % 13.02/2.84 % (2892546)Instructions burned: 249 (million) % 13.02/2.84 % (2892550)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=328034494:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 13.02/2.84 % (2892548)------------------------------ % 13.02/2.84 % (2892548)------------------------------ % 13.02/2.84 % (2892552)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2365935391:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 13.02/2.84 % (2892552)Refutation not found, incomplete strategy % 13.02/2.84 % (2892552)------------------------------ % 13.02/2.84 % (2892552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.84 % (2892552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.02/3.39 % (2892552)CaDiCaL version: 2.1.3 % 17.02/3.39 % (2892552)Termination reason: Refutation not found, incomplete strategy % 17.02/3.39 % (2892552)Time elapsed: 0.002 s % 17.02/3.39 % (2892552)Peak memory usage: 89 MB % 17.02/3.39 % (2892552)Instructions burned: 2 (million) % 17.02/3.39 % (2892553)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=155925951:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 17.02/3.39 % (2892555)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=876806309:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 17.02/3.39 % (2892555)Refutation not found, incomplete strategy % 17.02/3.39 % (2892555)------------------------------ % 17.02/3.39 % (2892555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.02/3.39 % (2892555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.02/3.39 % (2892555)CaDiCaL version: 2.1.3 % 17.02/3.39 % (2892555)Termination reason: Refutation not found, incomplete strategy % 17.02/3.39 % (2892555)Time elapsed: 0.003 s % 17.02/3.39 % (2892555)Peak memory usage: 87 MB % 17.02/3.39 % (2892555)Instructions burned: 10 (million) % 17.02/3.39 % (2892553)Instruction limit reached! % 17.02/3.39 % (2892553)------------------------------ % 17.02/3.39 % (2892553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.02/3.39 % (2892553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.02/3.39 % (2892553)CaDiCaL version: 2.1.3 % 17.02/3.39 % (2892553)Termination reason: Instruction limit % 17.02/3.39 % (2892553)Termination phase: Saturation % 17.02/3.39 % (2892553)Time elapsed: 0.057 s % 17.02/3.39 % (2892553)Peak memory usage: 88 MB % 17.02/3.39 % (2892553)Instructions burned: 128 (million) % 17.02/3.39 % (2892528)------------------------------ % 17.02/3.39 % (2892528)------------------------------ % 17.02/3.39 % (2892529)------------------------------ % 17.02/3.39 % (2892529)------------------------------ % 17.02/3.39 % (2892555)------------------------------ % 17.02/3.39 % (2892555)------------------------------ % 17.02/3.39 % (2892552)------------------------------ % 17.02/3.39 % (2892552)------------------------------ % 17.02/3.39 % (2892559)lrs+10_1_sil=8000:sp=occurrence:random_seed=756268802:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 17.02/3.39 % (2892560)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=831968680:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 17.02/3.39 % (2892561)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2830424894:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 17.02/3.39 % (2892560)Refutation not found, incomplete strategy % 17.02/3.39 % (2892560)------------------------------ % 17.02/3.39 % (2892560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.02/3.39 % (2892560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.02/3.39 % (2892560)CaDiCaL version: 2.1.3 % 17.02/3.39 % (2892560)Termination reason: Refutation not found, incomplete strategy % 17.02/3.39 % (2892560)Time elapsed: 0.002 s % 17.02/3.39 % (2892560)Peak memory usage: 87 MB % 17.02/3.39 % (2892560)Instructions burned: 1 (million) % 17.02/3.39 % (2892562)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=665615209:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 17.02/3.39 % (2892562)Refutation not found, incomplete strategy % 17.02/3.39 % (2892562)------------------------------ % 17.02/3.39 % (2892562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.02/3.39 % (2892562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.02/3.39 % (2892562)CaDiCaL version: 2.1.3 % 17.02/3.39 % (2892562)Termination reason: Refutation not found, incomplete strategy % 17.02/3.39 % (2892562)Time elapsed: 0.001 s % 17.02/3.39 % (2892562)Peak memory usage: 89 MB % 17.02/3.39 % (2892562)Instructions burned: 2 (million) % 17.02/3.39 % (2892563)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1348275068:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 17.02/3.39 % (2892563)Refutation not found, incomplete strategy % 17.02/3.39 % (2892563)------------------------------ % 17.02/3.39 % (2892563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.02/3.39 % (2892563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892563)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892563)Termination reason: Refutation not found, incomplete strategy % 19.18/3.76 % (2892563)Time elapsed: 0.006 s % 19.18/3.76 % (2892563)Peak memory usage: 88 MB % 19.18/3.76 % (2892563)Instructions burned: 9 (million) % 19.18/3.76 % (2892562)------------------------------ % 19.18/3.76 % (2892562)------------------------------ % 19.18/3.76 % (2892560)------------------------------ % 19.18/3.76 % (2892560)------------------------------ % 19.18/3.76 % (2892569)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1862456366:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 19.18/3.76 % (2892563)------------------------------ % 19.18/3.76 % (2892563)------------------------------ % 19.18/3.76 % (2892570)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=3199485641:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 19.18/3.76 % (2892570)Refutation not found, incomplete strategy % 19.18/3.76 % (2892570)------------------------------ % 19.18/3.76 % (2892570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.18/3.76 % (2892570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892570)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892570)Termination reason: Refutation not found, incomplete strategy % 19.18/3.76 % (2892570)Time elapsed: 0.005 s % 19.18/3.76 % (2892570)Peak memory usage: 89 MB % 19.18/3.76 % (2892570)Instructions burned: 7 (million) % 19.18/3.76 % (2892559)Instruction limit reached! % 19.18/3.76 % (2892559)------------------------------ % 19.18/3.76 % (2892559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.18/3.76 % (2892559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892559)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892559)Termination reason: Instruction limit % 19.18/3.76 % (2892559)Termination phase: Saturation % 19.18/3.76 % (2892559)Time elapsed: 0.499 s % 19.18/3.76 % (2892559)Peak memory usage: 99 MB % 19.18/3.76 % (2892559)Instructions burned: 907 (million) % 19.18/3.76 % (2892572)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1424304803:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 19.18/3.76 % (2892572)Instruction limit reached! % 19.18/3.76 % (2892572)------------------------------ % 19.18/3.76 % (2892572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.18/3.76 % (2892572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892572)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892572)Termination reason: Instruction limit % 19.18/3.76 % (2892572)Termination phase: Saturation % 19.18/3.76 % (2892572)Time elapsed: 0.070 s % 19.18/3.76 % (2892572)Peak memory usage: 91 MB % 19.18/3.76 % (2892572)Instructions burned: 135 (million) % 19.18/3.76 % (2892574)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=765543913:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 19.18/3.76 % (2892574)Refutation not found, incomplete strategy % 19.18/3.76 % (2892574)------------------------------ % 19.18/3.76 % (2892574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.18/3.76 % (2892574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892574)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892574)Termination reason: Refutation not found, incomplete strategy % 19.18/3.76 % (2892574)Time elapsed: 0.002 s % 19.18/3.76 % (2892574)Peak memory usage: 87 MB % 19.18/3.76 % (2892574)Instructions burned: 1 (million) % 19.18/3.76 % (2892570)------------------------------ % 19.18/3.76 % (2892570)------------------------------ % 19.18/3.76 % (2892576)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4190764910:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 19.18/3.76 % (2892576)Refutation not found, incomplete strategy % 19.18/3.76 % (2892576)------------------------------ % 19.18/3.76 % (2892576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.18/3.76 % (2892576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.18/3.76 % (2892576)CaDiCaL version: 2.1.3 % 19.18/3.76 % (2892576)Termination reason: Refutation not found, incomplete strategy % 19.18/3.76 % (2892576)Time elapsed: 0.001 s % 19.18/3.76 % (2892576)Peak memory usage: 87 MB % 19.18/3.76 % (2892576)Instructions burned: 1 (million) % 19.18/3.76 % (2892578)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=30530399:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 23.93/4.22 % (2892574)------------------------------ % 23.93/4.22 % (2892574)------------------------------ % 23.93/4.22 % (2892569)Refutation not found, incomplete strategy % 23.93/4.22 % (2892569)------------------------------ % 23.93/4.22 % (2892569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.93/4.22 % (2892569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.93/4.22 % (2892569)CaDiCaL version: 2.1.3 % 23.93/4.22 % (2892569)Termination reason: Refutation not found, incomplete strategy % 23.93/4.22 % (2892569)Time elapsed: 0.668 s % 23.93/4.22 % (2892569)Peak memory usage: 135 MB % 23.93/4.22 % (2892569)Instructions burned: 1599 (million) % 23.93/4.22 % (2892576)------------------------------ % 23.93/4.22 % (2892576)------------------------------ % 23.93/4.22 % (2892581)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=178564927:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi) % 23.93/4.22 % (2892581)Instruction limit reached! % 23.93/4.22 % (2892581)------------------------------ % 23.93/4.22 % (2892581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.93/4.22 % (2892581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.93/4.22 % (2892581)CaDiCaL version: 2.1.3 % 23.93/4.22 % (2892581)Termination reason: Instruction limit % 23.93/4.22 % (2892581)Termination phase: Saturation % 23.93/4.22 % (2892581)Time elapsed: 0.084 s % 23.93/4.22 % (2892581)Peak memory usage: 92 MB % 23.93/4.22 % (2892581)Instructions burned: 151 (million) % 23.93/4.22 % (2892550)Instruction limit reached! % 23.93/4.22 % (2892550)------------------------------ % 23.93/4.22 % (2892550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.93/4.22 % (2892550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.93/4.22 % (2892550)CaDiCaL version: 2.1.3 % 23.93/4.22 % (2892550)Termination reason: Instruction limit % 23.93/4.22 % (2892550)Termination phase: Saturation % 23.93/4.22 % (2892550)Time elapsed: 1.491 s % 23.93/4.22 % (2892550)Peak memory usage: 142 MB % 23.93/4.22 % (2892550)Instructions burned: 2352 (million) % 23.93/4.22 % (2892569)------------------------------ % 23.93/4.22 % (2892569)------------------------------ % 23.93/4.22 % (2892582)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1165900604:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi) % 23.93/4.22 % (2892584)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3230139372:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi) % 23.93/4.22 % (2892586)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1672957105:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi) % 23.93/4.22 % (2892586)Refutation not found, incomplete strategy % 23.93/4.22 % (2892586)------------------------------ % 23.93/4.22 % (2892586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.93/4.22 % (2892586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.93/4.22 % (2892586)CaDiCaL version: 2.1.3 % 23.93/4.22 % (2892586)Termination reason: Refutation not found, incomplete strategy % 23.93/4.22 % (2892586)Time elapsed: 0.001 s % 23.93/4.22 % (2892586)Peak memory usage: 88 MB % 23.93/4.22 % (2892586)Instructions burned: 3 (million) % 23.93/4.22 % (2892584)Refutation not found, incomplete strategy % 23.93/4.22 % (2892584)------------------------------ % 23.93/4.22 % (2892584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.93/4.22 % (2892584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.93/4.22 % (2892584)CaDiCaL version: 2.1.3 % 23.93/4.22 % (2892584)Termination reason: Refutation not found, incomplete strategy % 23.93/4.22 % (2892584)Time elapsed: 0.011 s % 23.93/4.22 % (2892584)Peak memory usage: 88 MB % 23.93/4.22 % (2892584)Instructions burned: 21 (million) % 23.93/4.22 % (2892585)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=2036352456:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi) % 23.93/4.22 % (2892585)Instruction limit reached! % 38.15/6.23 % (2892585)------------------------------ % 38.15/6.23 % (2892585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.15/6.23 % (2892585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.15/6.23 % (2892585)CaDiCaL version: 2.1.3 % 38.15/6.23 % (2892585)Termination reason: Instruction limit % 38.15/6.23 % (2892585)Termination phase: Saturation % 38.15/6.23 % (2892585)Time elapsed: 0.085 s % 38.15/6.23 % (2892585)Peak memory usage: 91 MB % 38.15/6.23 % (2892585)Instructions burned: 186 (million) % 38.15/6.23 % (2892586)------------------------------ % 38.15/6.23 % (2892586)------------------------------ % 38.15/6.23 % (2892584)------------------------------ % 38.15/6.23 % (2892584)------------------------------ % 38.15/6.23 % (2892591)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2345980714:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2974 on theBenchmark for (2974ds/4850Mi) % 38.15/6.23 % (2892592)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=350706831:i=12111:sd=1:ss=included_2974 on theBenchmark for (2974ds/12111Mi) % 38.15/6.23 % (2892591)Refutation not found, incomplete strategy % 38.15/6.23 % (2892591)------------------------------ % 38.15/6.23 % (2892591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.15/6.23 % (2892591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.15/6.23 % (2892591)CaDiCaL version: 2.1.3 % 38.15/6.23 % (2892591)Termination reason: Refutation not found, incomplete strategy % 38.15/6.23 % (2892591)Time elapsed: 0.005 s % 38.15/6.23 % (2892591)Peak memory usage: 88 MB % 38.15/6.23 % (2892591)Instructions burned: 8 (million) % 38.15/6.23 % (2892593)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3537643647:i=319:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/319Mi) % 38.15/6.23 [W927 19:35:53.009828333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009850363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009871253 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009877722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009892145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009898711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009911979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.15/6.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.15/6.23 [W927 19:35:53.009918787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.95/8.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.95/8.02 [W927 19:35:53.009931424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.95/8.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.95/8.02 [W927 19:35:53.009938070 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.95/8.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.95/8.02 [W927 19:35:53.009950824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.95/8.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.95/8.02 [W927 19:35:53.009956671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.95/8.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.95/8.02 % (2892591)------------------------------ % 48.95/8.02 % (2892591)------------------------------ % 48.95/8.02 % (2892593)Instruction limit reached! % 48.95/8.02 % (2892593)------------------------------ % 48.95/8.02 % (2892593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/8.02 % (2892593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/8.02 % (2892593)CaDiCaL version: 2.1.3 % 48.95/8.02 % (2892593)Termination reason: Instruction limit % 48.95/8.02 % (2892593)Termination phase: Saturation % 48.95/8.02 % (2892593)Time elapsed: 0.145 s % 48.95/8.02 % (2892593)Peak memory usage: 93 MB % 48.95/8.02 % (2892593)Instructions burned: 320 (million) % 48.95/8.02 % (2892592)Refutation not found, incomplete strategy % 48.95/8.02 % (2892592)------------------------------ % 48.95/8.02 % (2892592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/8.02 % (2892592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/8.02 % (2892592)CaDiCaL version: 2.1.3 % 48.95/8.02 % (2892592)Termination reason: Refutation not found, incomplete strategy % 48.95/8.02 % (2892592)Time elapsed: 0.324 s % 48.95/8.02 % (2892592)Peak memory usage: 127 MB % 48.95/8.02 % (2892592)Instructions burned: 836 (million) % 48.95/8.02 % (2892597)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=740302183:i=2064:ep=RST_2970 on theBenchmark for (2970ds/2064Mi) % 48.95/8.02 % (2892597)Refutation not found, incomplete strategy % 48.95/8.02 % (2892597)------------------------------ % 48.95/8.02 % (2892597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/8.02 % (2892597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/8.02 % (2892597)CaDiCaL version: 2.1.3 % 48.95/8.02 % (2892597)Termination reason: Refutation not found, incomplete strategy % 48.95/8.02 % (2892597)Time elapsed: 0.008 s % 48.95/8.02 % (2892597)Peak memory usage: 88 MB % 48.95/8.02 % (2892597)Instructions burned: 16 (million) % 48.95/8.02 % (2892598)dis-1011_128_sil=32000:random_seed=763182323:i=3706:ep=RST:av=off_2969 on theBenchmark for (2969ds/3706Mi) % 48.95/8.02 % (2892592)------------------------------ % 48.95/8.02 % (2892592)------------------------------ % 48.95/8.02 % (2892601)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4053037302:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2967 on theBenchmark for (2967ds/757Mi) % 48.95/8.02 % (2892601)Refutation not found, incomplete strategy % 48.95/8.02 % (2892601)------------------------------ % 48.95/8.02 % (2892601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.95/8.02 % (2892601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.95/8.02 % (2892601)CaDiCaL version: 2.1.3 % 48.95/8.02 % (2892601)Termination reason: Refutation not found, incomplete strategy % 48.95/8.02 % (2892601)Time elapsed: 0.001 s % 48.95/8.02 % (2892601)Peak memory usage: 89 MB % 48.95/8.02 % (2892601)Instructions burned: 2 (million) % 48.95/8.02 % (2892597)------------------------------ % 65.91/10.19 % (2892597)------------------------------ % 65.91/10.19 % (2892601)------------------------------ % 65.91/10.19 % (2892601)------------------------------ % 65.91/10.19 % (2892603)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=704752603:i=13913:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/13913Mi) % 65.91/10.19 % (2892604)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4131337402:i=9925:aac=none_2965 on theBenchmark for (2965ds/9925Mi) % 65.91/10.19 % (2892603)Refutation not found, incomplete strategy % 65.91/10.19 % (2892603)------------------------------ % 65.91/10.19 % (2892603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.91/10.19 % (2892603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.91/10.19 % (2892603)CaDiCaL version: 2.1.3 % 65.91/10.19 % (2892603)Termination reason: Refutation not found, incomplete strategy % 65.91/10.19 % (2892603)Time elapsed: 0.571 s % 65.91/10.19 % (2892603)Peak memory usage: 128 MB % 65.91/10.19 % (2892603)Instructions burned: 862 (million) % 65.91/10.19 % (2892561)Instruction limit reached! % 65.91/10.19 % (2892561)------------------------------ % 65.91/10.19 % (2892561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.91/10.19 % (2892561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.91/10.19 % (2892561)CaDiCaL version: 2.1.3 % 65.91/10.19 % (2892561)Termination reason: Instruction limit % 65.91/10.19 % (2892561)Termination phase: Saturation % 65.91/10.19 % (2892561)Time elapsed: 3.177 s % 65.91/10.19 % (2892561)Peak memory usage: 164 MB % 65.91/10.19 % (2892561)Instructions burned: 5203 (million) % 65.91/10.19 % (2892603)------------------------------ % 65.91/10.19 % (2892603)------------------------------ % 65.91/10.19 % (2892607)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4129586739:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2956 on theBenchmark for (2956ds/2479Mi) % 65.91/10.19 % (2892607)Refutation not found, incomplete strategy % 65.91/10.19 % (2892607)------------------------------ % 65.91/10.19 % (2892607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.91/10.19 % (2892607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.91/10.19 % (2892607)CaDiCaL version: 2.1.3 % 65.91/10.19 % (2892607)Termination reason: Refutation not found, incomplete strategy % 65.91/10.19 % (2892607)Time elapsed: 0.003 s % 65.91/10.19 % (2892607)Peak memory usage: 88 MB % 65.91/10.19 % (2892607)Instructions burned: 3 (million) % 65.91/10.19 % (2892608)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2355944114:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2956 on theBenchmark for (2956ds/440Mi) % 65.91/10.19 % (2892607)------------------------------ % 65.91/10.19 % (2892607)------------------------------ % 65.91/10.19 % (2892608)Instruction limit reached! % 65.91/10.19 % (2892608)------------------------------ % 65.91/10.19 % (2892608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.91/10.19 % (2892608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.91/10.19 % (2892608)CaDiCaL version: 2.1.3 % 65.91/10.19 % (2892608)Termination reason: Instruction limit % 65.91/10.19 % (2892608)Termination phase: Saturation % 65.91/10.19 % (2892608)Time elapsed: 0.232 s % 65.91/10.19 % (2892608)Peak memory usage: 94 MB % 65.91/10.19 % (2892608)Instructions burned: 441 (million) % 65.91/10.19 % (2892611)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4015695681:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2952 on theBenchmark for (2952ds/11145Mi) % 65.91/10.19 % (2892612)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=972211382:cts=off:i=3034:av=off:er=known:fsd=on_2952 on theBenchmark for (2952ds/3034Mi) % 65.91/10.19 % (2892598)Instruction limit reached! % 65.91/10.19 % (2892598)------------------------------ % 65.91/10.19 % (2892598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.91/10.19 % (2892598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.91/10.19 % (2892598)CaDiCaL version: 2.1.3 % 65.91/10.19 % (2892598)Termination reason: Instruction limit % 65.91/10.19 % (2892598)Termination phase: Saturation % 65.91/10.19 % (2892598)Time elapsed: 2.046 s % 65.91/10.19 % (2892598)Peak memory usage: 104 MB % 65.91/10.19 % (2892598)Instructions burned: 3708 (million) % 65.91/10.19 % (2892615)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3948215432:st=2:s2a=on:i=524:s2at=2:ss=axioms_2947 on theBenchmark for (2947ds/524Mi) % 72.36/11.07 % (2892578)Instruction limit reached! % 72.36/11.07 % (2892578)------------------------------ % 72.36/11.07 % (2892578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892578)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892578)Termination reason: Instruction limit % 72.36/11.07 % (2892578)Termination phase: Saturation % 72.36/11.07 % (2892578)Time elapsed: 3.522 s % 72.36/11.07 % (2892578)Peak memory usage: 153 MB % 72.36/11.07 % (2892578)Instructions burned: 6062 (million) % 72.36/11.07 % (2892615)Instruction limit reached! % 72.36/11.07 % (2892615)------------------------------ % 72.36/11.07 % (2892615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892615)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892615)Termination reason: Instruction limit % 72.36/11.07 % (2892615)Termination phase: Saturation % 72.36/11.07 % (2892615)Time elapsed: 0.242 s % 72.36/11.07 % (2892615)Peak memory usage: 93 MB % 72.36/11.07 % (2892615)Instructions burned: 524 (million) % 72.36/11.07 % (2892617)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2139932656:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2944 on theBenchmark for (2944ds/1016Mi) % 72.36/11.07 % (2892617)Refutation not found, incomplete strategy % 72.36/11.07 % (2892617)------------------------------ % 72.36/11.07 % (2892617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892617)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892617)Termination reason: Refutation not found, incomplete strategy % 72.36/11.07 % (2892617)Time elapsed: 0.002 s % 72.36/11.07 % (2892617)Peak memory usage: 87 MB % 72.36/11.07 % (2892617)Instructions burned: 1 (million) % 72.36/11.07 % (2892618)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3497747009:i=14123:bd=preordered:ins=4_2943 on theBenchmark for (2943ds/14123Mi) % 72.36/11.07 % (2892617)------------------------------ % 72.36/11.07 % (2892617)------------------------------ % 72.36/11.07 % (2892621)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=548374259:i=5781:kws=precedence:bd=all:rawr=on_2940 on theBenchmark for (2940ds/5781Mi) % 72.36/11.07 % (2892604)Instruction limit reached! % 72.36/11.07 % (2892604)------------------------------ % 72.36/11.07 % (2892604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892604)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892604)Termination reason: Instruction limit % 72.36/11.07 % (2892604)Termination phase: Saturation % 72.36/11.07 % (2892604)Time elapsed: 2.611 s % 72.36/11.07 % (2892604)Peak memory usage: 157 MB % 72.36/11.07 % (2892604)Instructions burned: 9927 (million) % 72.36/11.07 % (2892623)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=1587078033:i=2448:gtgl=5:bd=preordered:gtg=all_2937 on theBenchmark for (2937ds/2448Mi) % 72.36/11.07 % (2892612)Instruction limit reached! % 72.36/11.07 % (2892612)------------------------------ % 72.36/11.07 % (2892612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892612)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892612)Termination reason: Instruction limit % 72.36/11.07 % (2892612)Termination phase: Saturation % 72.36/11.07 % (2892612)Time elapsed: 1.667 s % 72.36/11.07 % (2892612)Peak memory usage: 137 MB % 72.36/11.07 % (2892612)Instructions burned: 3035 (million) % 72.36/11.07 % (2892625)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3155770734:i=3223:kws=precedence:fgj=on:av=off_2934 on theBenchmark for (2934ds/3223Mi) % 72.36/11.07 % (2892623)Instruction limit reached! % 72.36/11.07 % (2892623)------------------------------ % 72.36/11.07 % (2892623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.36/11.07 % (2892623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.36/11.07 % (2892623)CaDiCaL version: 2.1.3 % 72.36/11.07 % (2892623)Termination reason: Instruction limit % 77.50/11.96 % (2892623)Termination phase: Saturation % 77.50/11.96 % (2892623)Time elapsed: 0.820 s % 77.50/11.96 % (2892623)Peak memory usage: 150 MB % 77.50/11.96 % (2892623)Instructions burned: 2452 (million) % 77.50/11.96 % (2892627)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=214748093:st=5.6:i=2033:sd=3:ss=axioms_2928 on theBenchmark for (2928ds/2033Mi) % 77.50/11.96 % (2892627)Refutation not found, incomplete strategy % 77.50/11.96 % (2892627)------------------------------ % 77.50/11.96 % (2892627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.50/11.96 % (2892627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.50/11.96 % (2892627)CaDiCaL version: 2.1.3 % 77.50/11.96 % (2892627)Termination reason: Refutation not found, incomplete strategy % 77.50/11.96 % (2892627)Time elapsed: 0.373 s % 77.50/11.96 % (2892627)Peak memory usage: 129 MB % 77.50/11.96 % (2892627)Instructions burned: 919 (million) % 77.50/11.96 % (2892627)------------------------------ % 77.50/11.96 % (2892627)------------------------------ % 77.50/11.96 % (2892629)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=805822240:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2921 on theBenchmark for (2921ds/2055Mi) % 77.50/11.97 % (2892629)Refutation not found, incomplete strategy % 77.50/11.97 % (2892629)------------------------------ % 77.50/11.97 % (2892629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.50/11.97 % (2892629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.50/11.97 % (2892629)CaDiCaL version: 2.1.3 % 77.50/11.97 % (2892629)Termination reason: Refutation not found, incomplete strategy % 77.50/11.97 % (2892629)Time elapsed: 0.355 s % 77.50/11.97 % (2892629)Peak memory usage: 129 MB % 77.50/11.97 % (2892629)Instructions burned: 910 (million) % 77.50/11.97 % (2892629)------------------------------ % 77.50/11.97 % (2892629)------------------------------ % 77.50/11.97 % (2892621)Instruction limit reached! % 77.50/11.97 % (2892621)------------------------------ % 77.50/11.97 % (2892621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.50/11.97 % (2892621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.50/11.97 % (2892621)CaDiCaL version: 2.1.3 % 77.50/11.97 % (2892621)Termination reason: Instruction limit % 77.50/11.97 % (2892621)Termination phase: Saturation % 77.50/11.97 % (2892621)Time elapsed: 2.422 s % 77.50/11.97 % (2892621)Peak memory usage: 132 MB % 77.50/11.97 % (2892621)Instructions burned: 5783 (million) % 77.50/11.97 % (2892631)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=173223785:i=21611:sd=3:ss=axioms_2915 on theBenchmark for (2915ds/21611Mi) % 77.50/11.97 % (2892632)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3558859902:i=4835:sd=13:ss=axioms:sgt=23_2914 on theBenchmark for (2914ds/4835Mi) % 77.50/11.97 % (2892631)Refutation not found, incomplete strategy % 77.50/11.97 % (2892631)------------------------------ % 77.50/11.97 % (2892631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.50/11.97 % (2892631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.50/11.97 % (2892631)CaDiCaL version: 2.1.3 % 77.50/11.97 % (2892631)Termination reason: Refutation not found, incomplete strategy % 77.50/11.97 % (2892631)Time elapsed: 0.346 s % 77.50/11.97 % (2892631)Peak memory usage: 129 MB % 77.50/11.97 % (2892631)Instructions burned: 871 (million) % 77.50/11.97 % (2892631)------------------------------ % 77.50/11.97 % (2892631)------------------------------ % 77.50/11.97 % (2892625)Instruction limit reached! % 77.50/11.97 % (2892625)------------------------------ % 77.50/11.97 % (2892625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.50/11.97 % (2892625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.50/11.97 % (2892625)CaDiCaL version: 2.1.3 % 77.50/11.97 % (2892625)Termination reason: Instruction limit % 77.50/11.97 % (2892625)Termination phase: Saturation % 77.50/11.97 % (2892625)Time elapsed: 2.418 s % 77.50/11.97 % (2892625)Peak memory usage: 147 MB % 77.50/11.97 % (2892625)Instructions burned: 3223 (million) % 77.50/11.97 % (2892635)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=1285471064:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2908 on theBenchmark for (2908ds/797Mi) % 77.50/11.97 % (2892636)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3047093159:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2908 on theBenchmark for (2908ds/2326Mi) % 79.46/12.06 % (2892636)Refutation not found, incomplete strategy % 79.46/12.06 % (2892636)------------------------------ % 79.46/12.06 % (2892636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.46/12.06 % (2892636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.46/12.06 % (2892636)CaDiCaL version: 2.1.3 % 79.46/12.06 % (2892636)Termination reason: Refutation not found, incomplete strategy % 79.46/12.06 % (2892636)Time elapsed: 0.013 s % 79.46/12.06 % (2892636)Peak memory usage: 89 MB % 79.46/12.06 % (2892636)Instructions burned: 24 (million) % 79.46/12.06 % (2892582)Instruction limit reached! % 79.46/12.06 % (2892582)------------------------------ % 79.46/12.06 % (2892582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.46/12.06 % (2892582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.46/12.06 % (2892582)CaDiCaL version: 2.1.3 % 79.46/12.06 % (2892582)Termination reason: Instruction limit % 79.46/12.07 % (2892582)Termination phase: Saturation % 79.46/12.07 % (2892582)Time elapsed: 7.082 s % 79.46/12.07 % (2892582)Peak memory usage: 179 MB % 79.46/12.07 % (2892582)Instructions burned: 14157 (million) % 79.46/12.07 % (2892635)Instruction limit reached! % 79.46/12.07 % (2892635)------------------------------ % 79.46/12.07 % (2892635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.46/12.07 % (2892635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.46/12.07 % (2892635)CaDiCaL version: 2.1.3 % 79.46/12.07 % (2892635)Termination reason: Instruction limit % 79.46/12.07 % (2892635)Termination phase: Saturation % 79.46/12.07 % (2892635)Time elapsed: 0.229 s % 79.46/12.07 % (2892635)Peak memory usage: 99 MB % 79.46/12.07 % (2892635)Instructions burned: 799 (million) % 79.46/12.07 % (2892639)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2968820992:i=6038:nm=6_2905 on theBenchmark for (2905ds/6038Mi) % 79.46/12.07 % (2892640)lrs+10_1_sil=32000:sp=occurrence:random_seed=3079429782:st=2:i=33334:sd=3:ss=included:sgt=32_2905 on theBenchmark for (2905ds/33334Mi) % 79.46/12.07 % (2892636)------------------------------ % 79.46/12.07 % (2892636)------------------------------ % 79.46/12.07 % (2892640)Refutation not found, incomplete strategy % 79.46/12.07 % (2892640)------------------------------ % 79.46/12.07 % (2892640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.46/12.07 % (2892640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.46/12.07 % (2892640)CaDiCaL version: 2.1.3 % 79.46/12.07 % (2892640)Termination reason: Refutation not found, incomplete strategy % 79.46/12.07 % (2892640)Time elapsed: 0.090 s % 79.46/12.07 % (2892640)Peak memory usage: 92 MB % 79.46/12.07 % (2892640)Instructions burned: 314 (million) % 79.46/12.07 % (2892643)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1161693106:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2903 on theBenchmark for (2903ds/1008Mi) % 79.46/12.07 % (2892640)------------------------------ % 79.46/12.07 % (2892640)------------------------------ % 79.46/12.07 % (2892645)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=687334631:i=8327:s2at=5:bd=preordered_2901 on theBenchmark for (2901ds/8327Mi) % 79.46/12.07 % (2892611)Instruction limit reached! % 79.46/12.07 % (2892611)------------------------------ % 79.46/12.07 % (2892611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.46/12.07 % (2892611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.46/12.07 % (2892611)CaDiCaL version: 2.1.3 % 79.46/12.07 % (2892611)Termination reason: Instruction limit % 79.46/12.07 % (2892611)Termination phase: Saturation % 79.46/12.07 % (2892611)Time elapsed: 5.106 s % 79.46/12.07 % (2892611)Peak memory usage: 144 MB % 79.46/12.07 % (2892611)Instructions burned: 11146 (million) % 79.46/12.07 % (2892647)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=4046809577:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2899 on theBenchmark for (2899ds/1083Mi) % 79.46/12.07 % (2892639)Refutation not found, incomplete strategy % 79.46/12.07 % (2892639)------------------------------ % 79.46/12.07 % (2892639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892639)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892639)Termination reason: Refutation not found, incomplete strategy % 90.31/13.69 % (2892639)Time elapsed: 0.636 s % 90.31/13.69 % (2892639)Peak memory usage: 132 MB % 90.31/13.69 % (2892639)Instructions burned: 947 (million) % 90.31/13.69 % (2892643)Instruction limit reached! % 90.31/13.69 % (2892643)------------------------------ % 90.31/13.69 % (2892643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892643)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892643)Termination reason: Instruction limit % 90.31/13.69 % (2892643)Termination phase: Saturation % 90.31/13.69 % (2892643)Time elapsed: 0.486 s % 90.31/13.69 % (2892643)Peak memory usage: 94 MB % 90.31/13.69 % (2892643)Instructions burned: 1008 (million) % 90.31/13.69 % (2892649)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3927208773:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2897 on theBenchmark for (2897ds/1084Mi) % 90.31/13.69 % (2892649)Refutation not found, incomplete strategy % 90.31/13.69 % (2892649)------------------------------ % 90.31/13.69 % (2892649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892649)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892649)Termination reason: Refutation not found, incomplete strategy % 90.31/13.69 % (2892649)Time elapsed: 0.001 s % 90.31/13.69 % (2892649)Peak memory usage: 86 MB % 90.31/13.69 % (2892649)Instructions burned: 1 (million) % 90.31/13.69 % (2892639)------------------------------ % 90.31/13.69 % (2892639)------------------------------ % 90.31/13.69 % (2892647)Instruction limit reached! % 90.31/13.69 % (2892647)------------------------------ % 90.31/13.69 % (2892647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892647)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892647)Termination reason: Instruction limit % 90.31/13.69 % (2892647)Termination phase: Saturation % 90.31/13.69 % (2892647)Time elapsed: 0.464 s % 90.31/13.69 % (2892647)Peak memory usage: 99 MB % 90.31/13.69 % (2892647)Instructions burned: 1085 (million) % 90.31/13.69 % (2892651)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3035298536:i=6995:s2at=5:gtg=all_2895 on theBenchmark for (2895ds/6995Mi) % 90.31/13.69 % (2892649)------------------------------ % 90.31/13.69 % (2892649)------------------------------ % 90.31/13.69 % (2892652)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1814217655:st=2:i=6225:sd=15:ss=axioms_2893 on theBenchmark for (2893ds/6225Mi) % 90.31/13.69 % (2892652)Refutation not found, incomplete strategy % 90.31/13.69 % (2892652)------------------------------ % 90.31/13.69 % (2892652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892652)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892652)Termination reason: Refutation not found, incomplete strategy % 90.31/13.69 % (2892652)Time elapsed: 0.005 s % 90.31/13.69 % (2892652)Peak memory usage: 88 MB % 90.31/13.69 % (2892652)Instructions burned: 7 (million) % 90.31/13.69 % (2892654)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1700466666:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2893 on theBenchmark for (2893ds/3372Mi) % 90.31/13.69 % (2892632)Instruction limit reached! % 90.31/13.69 % (2892632)------------------------------ % 90.31/13.69 % (2892632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.31/13.69 % (2892632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.31/13.69 % (2892632)CaDiCaL version: 2.1.3 % 90.31/13.69 % (2892632)Termination reason: Instruction limit % 90.31/13.69 % (2892632)Termination phase: Saturation % 90.31/13.69 % (2892632)Time elapsed: 2.246 s % 90.31/13.69 % (2892632)Peak memory usage: 133 MB % 90.31/13.69 % (2892632)Instructions burned: 4837 (million) % 90.31/13.69 % (2892652)------------------------------ % 90.31/13.69 % (2892652)------------------------------ % 90.31/13.69 % (2892657)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2377074935:st=2.3:i=26457:sd=10:ss=included:sgt=8_2890 on theBenchmark for (2890ds/26457Mi) % 101.42/15.19 % (2892658)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=3295844116:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2889 on theBenchmark for (2889ds/13494Mi) % 101.42/15.19 [W927 19:36:02.312759867 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312795624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312835545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312848105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312880711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312892155 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312918245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312929515 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312955315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312965462 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.312990089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.42/15.19 [W927 19:36:02.313019599 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.42/15.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 % (2892654)Refutation not found, incomplete strategy % 110.96/16.61 % (2892654)------------------------------ % 110.96/16.61 % (2892654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.96/16.61 % (2892654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.96/16.61 % (2892654)CaDiCaL version: 2.1.3 % 110.96/16.61 % (2892654)Termination reason: Refutation not found, incomplete strategy % 110.96/16.61 % (2892654)Time elapsed: 0.556 s % 110.96/16.61 % (2892654)Peak memory usage: 127 MB % 110.96/16.61 % (2892654)Instructions burned: 837 (million) % 110.96/16.61 % (2892654)------------------------------ % 110.96/16.61 % (2892654)------------------------------ % 110.96/16.61 % (2892661)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=3633716800:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2883 on theBenchmark for (2883ds/2503Mi) % 110.96/16.61 % (2892645)Instruction limit reached! % 110.96/16.61 % (2892645)------------------------------ % 110.96/16.61 % (2892645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.96/16.61 % (2892645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.96/16.61 % (2892645)CaDiCaL version: 2.1.3 % 110.96/16.61 % (2892645)Termination reason: Instruction limit % 110.96/16.61 % (2892645)Termination phase: Saturation % 110.96/16.61 % (2892645)Time elapsed: 2.524 s % 110.96/16.61 % (2892645)Peak memory usage: 207 MB % 110.96/16.61 % (2892645)Instructions burned: 8331 (million) % 110.96/16.61 % (2892663)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=49957518:i=2559:sd=1:ep=RSTC:ss=axioms_2875 on theBenchmark for (2875ds/2559Mi) % 110.96/16.61 [W927 19:36:03.936861494 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936883925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936904594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936911191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936927480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936933841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936946629 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936952837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.96/16.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.96/16.61 [W927 19:36:03.936965333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.20/16.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.20/16.92 [W927 19:36:03.936971537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.20/16.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.20/16.92 [W927 19:36:03.936994680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.20/16.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.20/16.92 [W927 19:36:03.937000053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.20/16.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.20/16.92 % (2892663)Refutation not found, incomplete strategy % 112.20/16.92 % (2892663)------------------------------ % 112.20/16.92 % (2892663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.20/16.92 % (2892663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.92 % (2892663)CaDiCaL version: 2.1.3 % 112.20/16.92 % (2892663)Termination reason: Refutation not found, incomplete strategy % 112.20/16.92 % (2892663)Time elapsed: 0.299 s % 112.20/16.92 % (2892663)Peak memory usage: 126 MB % 112.20/16.92 % (2892663)Instructions burned: 830 (million) % 112.20/16.92 % (2892663)------------------------------ % 112.20/16.92 % (2892663)------------------------------ % 112.20/16.92 % (2892665)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2694531520:i=30753:av=off:ss=included_2869 on theBenchmark for (2869ds/30753Mi) % 112.20/16.92 % (2892665)Refutation not found, incomplete strategy % 112.20/16.92 % (2892665)------------------------------ % 112.20/16.92 % (2892665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.20/16.92 % (2892665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.92 % (2892665)CaDiCaL version: 2.1.3 % 112.20/16.92 % (2892665)Termination reason: Refutation not found, incomplete strategy % 112.20/16.92 % (2892665)Time elapsed: 0.352 s % 112.20/16.92 % (2892665)Peak memory usage: 128 MB % 112.20/16.92 % (2892665)Instructions burned: 901 (million) % 112.20/16.92 % (2892661)Instruction limit reached! % 112.20/16.92 % (2892661)------------------------------ % 112.20/16.92 % (2892661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.20/16.92 % (2892661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.92 % (2892661)CaDiCaL version: 2.1.3 % 112.20/16.92 % (2892661)Termination reason: Instruction limit % 112.20/16.92 % (2892661)Termination phase: Saturation % 112.20/16.92 % (2892661)Time elapsed: 1.818 s % 112.20/16.92 % (2892661)Peak memory usage: 143 MB % 112.20/16.92 % (2892661)Instructions burned: 2503 (million) % 112.20/16.92 % (2892665)------------------------------ % 112.20/16.92 % (2892665)------------------------------ % 112.20/16.92 % (2892667)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1411630388:i=26473:ep=RSTC_2863 on theBenchmark for (2863ds/26473Mi) % 112.20/16.92 % (2892668)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=1843700453:cts=off:i=2759:kws=inv_arity:fgj=on_2862 on theBenchmark for (2862ds/2759Mi) % 112.20/16.92 % (2892668)Refutation not found, incomplete strategy % 112.20/16.92 % (2892668)------------------------------ % 112.20/16.92 % (2892668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.20/16.92 % (2892668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.20/16.92 % (2892668)CaDiCaL version: 2.1.3 % 112.20/16.92 % (2892668)Termination reason: Refutation not found, incomplete strategy % 112.20/16.92 % (2892668)Time elapsed: 0.354 s % 112.20/16.92 % (2892668)Peak memory usage: 132 MB % 112.20/16.92 % (2892668)Instructions burned: 944 (million) % 112.20/16.92 % (2892668)------------------------------ % 112.20/16.92 % (2892668)------------------------------ % 119.13/18.00 % (2892671)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=4008422790:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2856 on theBenchmark for (2856ds/5665Mi) % 119.13/18.00 % (2892651)Instruction limit reached! % 119.13/18.00 % (2892651)------------------------------ % 119.13/18.00 % (2892651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.13/18.00 % (2892651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.13/18.00 % (2892651)CaDiCaL version: 2.1.3 % 119.13/18.00 % (2892651)Termination reason: Instruction limit % 119.13/18.00 % (2892651)Termination phase: Saturation % 119.13/18.00 % (2892651)Time elapsed: 3.894 s % 119.13/18.00 % (2892651)Peak memory usage: 188 MB % 119.13/18.00 % (2892651)Instructions burned: 6996 (million) % 119.13/18.00 % (2892673)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=1958560770:i=1532:ep=RS:ss=axioms_2854 on theBenchmark for (2854ds/1532Mi) % 119.13/18.00 % (2892671)Refutation not found, incomplete strategy % 119.13/18.00 % (2892671)------------------------------ % 119.13/18.00 % (2892671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.13/18.00 % (2892671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.13/18.00 % (2892671)CaDiCaL version: 2.1.3 % 119.13/18.00 % (2892671)Termination reason: Refutation not found, incomplete strategy % 119.13/18.00 % (2892671)Time elapsed: 0.373 s % 119.13/18.00 % (2892671)Peak memory usage: 129 MB % 119.13/18.00 % (2892671)Instructions burned: 912 (million) % 119.13/18.00 % (2892671)------------------------------ % 119.13/18.00 % (2892671)------------------------------ % 119.13/18.00 % (2892618)Instruction limit reached! % 119.13/18.00 % (2892618)------------------------------ % 119.13/18.00 % (2892618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.13/18.00 % (2892618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.13/18.00 % (2892618)CaDiCaL version: 2.1.3 % 119.13/18.00 % (2892618)Termination reason: Instruction limit % 119.13/18.00 % (2892618)Termination phase: Saturation % 119.13/18.00 % (2892618)Time elapsed: 9.351 s % 119.13/18.00 % (2892618)Peak memory usage: 240 MB % 119.13/18.00 % (2892618)Instructions burned: 14123 (million) % 119.13/18.00 % (2892675)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3612872990:i=1565:sd=2:ss=axioms:sgt=32_2849 on theBenchmark for (2849ds/1565Mi) % 119.13/18.00 % (2892676)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=2240090954:i=1572:fgj=on:gsp=on_2848 on theBenchmark for (2848ds/1572Mi) % 119.13/18.00 % (2892673)Refutation not found, incomplete strategy % 119.13/18.00 % (2892673)------------------------------ % 119.13/18.00 % (2892673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.13/18.00 % (2892673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.13/18.00 % (2892673)CaDiCaL version: 2.1.3 % 119.13/18.00 % (2892673)Termination reason: Refutation not found, incomplete strategy % 119.13/18.00 % (2892673)Time elapsed: 0.600 s % 119.13/18.00 % (2892673)Peak memory usage: 129 MB % 119.13/18.00 % (2892673)Instructions burned: 897 (million) % 119.13/18.00 % (2892675)Refutation not found, incomplete strategy % 119.13/18.00 % (2892675)------------------------------ % 119.13/18.00 % (2892675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.13/18.00 % (2892675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.13/18.00 % (2892675)CaDiCaL version: 2.1.3 % 119.13/18.00 % (2892675)Termination reason: Refutation not found, incomplete strategy % 119.13/18.00 % (2892675)Time elapsed: 0.324 s % 119.13/18.00 % (2892675)Peak memory usage: 129 MB % 119.13/18.00 % (2892675)Instructions burned: 872 (million) % 119.13/18.00 % (2892673)------------------------------ % 119.13/18.00 % (2892673)------------------------------ % 119.13/18.00 % (2892675)------------------------------ % 119.13/18.00 % (2892675)------------------------------ % 119.13/18.00 % (2892679)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3808386672:i=6052:sd=4:ss=axioms:sgt=24_2844 on theBenchmark for (2844ds/6052Mi) % 119.13/18.00 % (2892680)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=2723707832:i=3500:sd=1:bd=preordered:sup=off:ss=included_2843 on theBenchmark for (2843ds/3500Mi) % 133.78/19.80 [W927 19:36:06.064761792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064798794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064819995 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064825932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064838925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064844291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064857414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064864414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064877199 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064883469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064896306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 [W927 19:36:06.064902564 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.78/19.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.78/19.80 % (2892680)Refutation not found, incomplete strategy % 133.78/19.80 % (2892680)------------------------------ % 133.78/19.80 % (2892680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.78/19.80 % (2892680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.15/22.36 % (2892680)CaDiCaL version: 2.1.3 % 152.15/22.36 % (2892680)Termination reason: Refutation not found, incomplete strategy % 152.15/22.36 % (2892680)Time elapsed: 0.307 s % 152.15/22.36 % (2892680)Peak memory usage: 126 MB % 152.15/22.36 % (2892680)Instructions burned: 834 (million) % 152.15/22.36 % (2892680)------------------------------ % 152.15/22.36 % (2892680)------------------------------ % 152.15/22.36 % (2892683)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=1330441114:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2837 on theBenchmark for (2837ds/1842Mi) % 152.15/22.36 % (2892679)Refutation not found, incomplete strategy % 152.15/22.36 % (2892679)------------------------------ % 152.15/22.36 % (2892679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.15/22.36 % (2892679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.15/22.36 % (2892679)CaDiCaL version: 2.1.3 % 152.15/22.36 % (2892679)Termination reason: Refutation not found, incomplete strategy % 152.15/22.36 % (2892679)Time elapsed: 0.613 s % 152.15/22.36 % (2892679)Peak memory usage: 129 MB % 152.15/22.36 % (2892679)Instructions burned: 919 (million) % 152.15/22.36 % (2892676)Instruction limit reached! % 152.15/22.36 % (2892676)------------------------------ % 152.15/22.36 % (2892676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.15/22.36 % (2892676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.15/22.36 % (2892676)CaDiCaL version: 2.1.3 % 152.15/22.36 % (2892676)Termination reason: Instruction limit % 152.15/22.36 % (2892676)Termination phase: Saturation % 152.15/22.36 % (2892676)Time elapsed: 1.075 s % 152.15/22.36 % (2892676)Peak memory usage: 136 MB % 152.15/22.36 % (2892676)Instructions burned: 1572 (million) % 152.15/22.36 % (2892685)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=794810675:i=66096:add=on_2835 on theBenchmark for (2835ds/66096Mi) % 152.15/22.36 % (2892679)------------------------------ % 152.15/22.36 % (2892679)------------------------------ % 152.15/22.36 % (2892687)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3491240745:i=1884:sd=1:nm=60:ss=axioms_2833 on theBenchmark for (2833ds/1884Mi) % 152.15/22.36 % (2892683)Instruction limit reached! % 152.15/22.36 % (2892683)------------------------------ % 152.15/22.36 % (2892683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.15/22.36 % (2892683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.15/22.36 % (2892683)CaDiCaL version: 2.1.3 % 152.15/22.36 % (2892683)Termination reason: Instruction limit % 152.15/22.36 % (2892683)Termination phase: Saturation % 152.15/22.36 % (2892683)Time elapsed: 0.719 s % 152.15/22.36 % (2892683)Peak memory usage: 135 MB % 152.15/22.36 % (2892683)Instructions burned: 1844 (million) % 152.15/22.36 [W927 19:36:08.246342739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.15/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.15/22.36 [W927 19:36:08.246381540 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.15/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.15/22.36 [W927 19:36:08.246421723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.15/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.15/22.36 [W927 19:36:08.246434820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.15/22.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.15/22.36 [W927 19:36:08.246461867 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246472927 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246504954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246525251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246550951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246561088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246585171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 [W927 19:36:08.246595171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 186.60/27.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 186.60/27.18 % (2892689)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3789949137:cts=off:i=5469:bs=on:fsr=off_2829 on theBenchmark for (2829ds/5469Mi) % 186.60/27.18 % (2892687)Refutation not found, incomplete strategy % 186.60/27.18 % (2892687)------------------------------ % 186.60/27.18 % (2892687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.60/27.18 % (2892687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.60/27.18 % (2892687)CaDiCaL version: 2.1.3 % 186.60/27.18 % (2892687)Termination reason: Refutation not found, incomplete strategy % 186.60/27.18 % (2892687)Time elapsed: 0.549 s % 186.60/27.18 % (2892687)Peak memory usage: 127 MB % 186.60/27.18 % (2892687)Instructions burned: 833 (million) % 186.60/27.18 % (2892687)------------------------------ % 186.60/27.18 % (2892687)------------------------------ % 186.60/27.18 % (2892691)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=1983792471:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2824 on theBenchmark for (2824ds/2037Mi) % 186.60/27.18 % (2892691)Instruction limit reached! % 186.60/27.18 % (2892691)------------------------------ % 186.60/27.18 % (2892691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.60/27.18 % (2892691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.60/27.18 % (2892691)CaDiCaL version: 2.1.3 % 186.60/27.18 % (2892691)Termination reason: Instruction limit % 186.60/27.18 % (2892691)Termination phase: Saturation % 186.60/27.18 % (2892691)Time elapsed: 1.182 s % 186.60/27.18 % (2892691)Peak memory usage: 143 MB % 186.60/27.18 % (2892691)Instructions burned: 2038 (million) % 186.60/27.18 % (2892658)Instruction limit reached! % 186.60/27.18 % (2892658)------------------------------ % 186.60/27.18 % (2892658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.60/27.18 % (2892658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.06/27.72 % (2892658)CaDiCaL version: 2.1.3 % 190.06/27.72 % (2892658)Termination reason: Instruction limit % 190.06/27.72 % (2892658)Termination phase: Saturation % 190.06/27.72 % (2892658)Time elapsed: 7.768 s % 190.06/27.72 % (2892658)Peak memory usage: 241 MB % 190.06/27.72 % (2892658)Instructions burned: 13494 (million) % 190.06/27.72 % (2892693)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3421003038:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2810 on theBenchmark for (2810ds/2110Mi) % 190.06/27.72 % (2892694)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=2685114588:i=2430:add=off:aac=none:nm=16_2810 on theBenchmark for (2810ds/2430Mi) % 190.06/27.72 % (2892689)Instruction limit reached! % 190.06/27.72 % (2892689)------------------------------ % 190.06/27.72 % (2892689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.06/27.72 % (2892689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.06/27.72 % (2892689)CaDiCaL version: 2.1.3 % 190.06/27.72 % (2892689)Termination reason: Instruction limit % 190.06/27.72 % (2892689)Termination phase: Saturation % 190.06/27.72 % (2892689)Time elapsed: 2.650 s % 190.06/27.72 % (2892689)Peak memory usage: 98 MB % 190.06/27.72 % (2892689)Instructions burned: 5470 (million) % 190.06/27.72 % (2892697)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=906806662:cond=fast:i=4891_2801 on theBenchmark for (2801ds/4891Mi) % 190.06/27.72 % (2892693)Instruction limit reached! % 190.06/27.72 % (2892693)------------------------------ % 190.06/27.72 % (2892693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.06/27.72 % (2892693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.06/27.72 % (2892693)CaDiCaL version: 2.1.3 % 190.06/27.72 % (2892693)Termination reason: Instruction limit % 190.06/27.72 % (2892693)Termination phase: Saturation % 190.06/27.72 % (2892693)Time elapsed: 1.202 s % 190.06/27.72 % (2892693)Peak memory usage: 138 MB % 190.06/27.72 % (2892693)Instructions burned: 2111 (million) % 190.06/27.72 % (2892699)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=203129963:st=2:i=14845:sd=2:ss=included:fsd=on_2797 on theBenchmark for (2797ds/14845Mi) % 190.06/27.72 % (2892694)Instruction limit reached! % 190.06/27.72 % (2892694)------------------------------ % 190.06/27.72 % (2892694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.06/27.72 % (2892694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.06/27.72 % (2892694)CaDiCaL version: 2.1.3 % 190.06/27.72 % (2892694)Termination reason: Instruction limit % 190.06/27.72 % (2892694)Termination phase: Saturation % 190.06/27.72 % (2892694)Time elapsed: 1.625 s % 190.06/27.72 % (2892694)Peak memory usage: 142 MB % 190.06/27.72 % (2892694)Instructions burned: 2430 (million) % 190.06/27.72 % (2892701)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3376126111:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2792 on theBenchmark for (2792ds/7534Mi) % 190.06/27.72 % (2892699)Refutation not found, incomplete strategy % 190.06/27.72 % (2892699)------------------------------ % 190.06/27.72 % (2892699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.06/27.72 % (2892699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.06/27.72 % (2892699)CaDiCaL version: 2.1.3 % 190.06/27.72 % (2892699)Termination reason: Refutation not found, incomplete strategy % 190.06/27.72 % (2892699)Time elapsed: 0.592 s % 190.06/27.72 % (2892699)Peak memory usage: 129 MB % 190.06/27.72 % (2892699)Instructions burned: 904 (million) % 190.06/27.72 % (2892699)------------------------------ % 190.06/27.72 % (2892699)------------------------------ % 190.06/27.72 % (2892703)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=1264403767:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2787 on theBenchmark for (2787ds/10353Mi) % 190.06/27.72 % (2892701)Refutation not found, incomplete strategy % 190.06/27.72 % (2892701)------------------------------ % 190.06/27.72 % (2892701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.06/27.72 % (2892701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892701)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892701)Termination reason: Refutation not found, incomplete strategy % 197.43/28.98 % (2892701)Time elapsed: 0.572 s % 197.43/28.98 % (2892701)Peak memory usage: 128 MB % 197.43/28.98 % (2892701)Instructions burned: 870 (million) % 197.43/28.98 % (2892701)------------------------------ % 197.43/28.98 % (2892701)------------------------------ % 197.43/28.98 % (2892705)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1029257088:i=7860_2782 on theBenchmark for (2782ds/7860Mi) % 197.43/28.98 % (2892705)Refutation not found, incomplete strategy % 197.43/28.98 % (2892705)------------------------------ % 197.43/28.98 % (2892705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.43/28.98 % (2892705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892705)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892705)Termination reason: Refutation not found, incomplete strategy % 197.43/28.98 % (2892705)Time elapsed: 0.011 s % 197.43/28.98 % (2892705)Peak memory usage: 88 MB % 197.43/28.98 % (2892705)Instructions burned: 22 (million) % 197.43/28.98 % (2892705)------------------------------ % 197.43/28.98 % (2892705)------------------------------ % 197.43/28.98 % (2892707)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=1530610997:i=7896:sd=2:bs=on:ss=included:sgt=20_2778 on theBenchmark for (2778ds/7896Mi) % 197.43/28.98 % (2892707)Refutation not found, incomplete strategy % 197.43/28.98 % (2892707)------------------------------ % 197.43/28.98 % (2892707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.43/28.98 % (2892707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892707)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892707)Termination reason: Refutation not found, incomplete strategy % 197.43/28.98 % (2892707)Time elapsed: 0.572 s % 197.43/28.98 % (2892707)Peak memory usage: 129 MB % 197.43/28.98 % (2892707)Instructions burned: 865 (million) % 197.43/28.98 % (2892707)------------------------------ % 197.43/28.98 % (2892707)------------------------------ % 197.43/28.98 % (2892709)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3830457317:i=5812:gtgl=2:gtg=all_2768 on theBenchmark for (2768ds/5812Mi) % 197.43/28.98 % (2892697)Instruction limit reached! % 197.43/28.98 % (2892697)------------------------------ % 197.43/28.98 % (2892697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.43/28.98 % (2892697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892697)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892697)Termination reason: Instruction limit % 197.43/28.98 % (2892697)Termination phase: Saturation % 197.43/28.98 % (2892697)Time elapsed: 3.437 s % 197.43/28.98 % (2892697)Peak memory usage: 162 MB % 197.43/28.98 % (2892697)Instructions burned: 4891 (million) % 197.43/28.98 % (2892711)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=1324614650:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2764 on theBenchmark for (2764ds/2965Mi) % 197.43/28.98 % (2892711)Refutation not found, incomplete strategy % 197.43/28.98 % (2892711)------------------------------ % 197.43/28.98 % (2892711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.43/28.98 % (2892711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892711)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892711)Termination reason: Refutation not found, incomplete strategy % 197.43/28.98 % (2892711)Time elapsed: 0.621 s % 197.43/28.98 % (2892711)Peak memory usage: 132 MB % 197.43/28.98 % (2892711)Instructions burned: 952 (million) % 197.43/28.98 % (2892711)------------------------------ % 197.43/28.98 % (2892711)------------------------------ % 197.43/28.98 % (2892713)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=879295036:i=2967:kws=precedence:bd=preordered:av=off_2754 on theBenchmark for (2754ds/2967Mi) % 197.43/28.98 % (2892713)Instruction limit reached! % 197.43/28.98 % (2892713)------------------------------ % 197.43/28.98 % (2892713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.43/28.98 % (2892713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.43/28.98 % (2892713)CaDiCaL version: 2.1.3 % 197.43/28.98 % (2892713)Termination reason: Instruction limit % 197.43/28.98 % (2892713)Termination phase: Saturation % 227.42/32.90 % (2892713)Time elapsed: 1.638 s % 227.42/32.90 % (2892713)Peak memory usage: 150 MB % 227.42/32.90 % (2892713)Instructions burned: 2967 (million) % 227.42/32.90 % (2892715)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=3908779590:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2736 on theBenchmark for (2736ds/3022Mi) % 227.42/32.90 [W927 19:36:17.971876663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.971911559 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.971949943 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.971961710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.971986673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.971999277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972036344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972048694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972073964 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972085794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972111311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 227.42/32.90 [W927 19:36:17.972122981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 227.42/32.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.97/39.90 % (2892715)Refutation not found, incomplete strategy % 276.97/39.90 % (2892715)------------------------------ % 276.97/39.90 % (2892715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892715)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892715)Termination reason: Refutation not found, incomplete strategy % 276.97/39.90 % (2892715)Time elapsed: 0.552 s % 276.97/39.90 % (2892715)Peak memory usage: 127 MB % 276.97/39.90 % (2892715)Instructions burned: 833 (million) % 276.97/39.90 % (2892657)Instruction limit reached! % 276.97/39.90 % (2892657)------------------------------ % 276.97/39.90 % (2892657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892657)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892657)Termination reason: Instruction limit % 276.97/39.90 % (2892657)Termination phase: Saturation % 276.97/39.90 % (2892657)Time elapsed: 15.960 s % 276.97/39.90 % (2892657)Peak memory usage: 322 MB % 276.97/39.90 % (2892657)Instructions burned: 26457 (million) % 276.97/39.90 % (2892717)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=2730574421:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2728 on theBenchmark for (2728ds/3207Mi) % 276.97/39.90 % (2892715)------------------------------ % 276.97/39.90 % (2892715)------------------------------ % 276.97/39.90 % (2892667)Instruction limit reached! % 276.97/39.90 % (2892667)------------------------------ % 276.97/39.90 % (2892667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892667)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892667)Termination reason: Instruction limit % 276.97/39.90 % (2892667)Termination phase: Saturation % 276.97/39.90 % (2892667)Time elapsed: 13.614 s % 276.97/39.90 % (2892667)Peak memory usage: 172 MB % 276.97/39.90 % (2892667)Instructions burned: 26474 (million) % 276.97/39.90 % (2892719)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3653995189:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2726 on theBenchmark for (2726ds/3289Mi) % 276.97/39.90 % (2892720)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=4178601133:i=38569:sd=3:ss=axioms:sgt=32_2725 on theBenchmark for (2725ds/38569Mi) % 276.97/39.90 % (2892709)Instruction limit reached! % 276.97/39.90 % (2892709)------------------------------ % 276.97/39.90 % (2892709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892709)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892709)Termination reason: Instruction limit % 276.97/39.90 % (2892709)Termination phase: Saturation % 276.97/39.90 % (2892709)Time elapsed: 4.385 s % 276.97/39.90 % (2892709)Peak memory usage: 177 MB % 276.97/39.90 % (2892709)Instructions burned: 5812 (million) % 276.97/39.90 % (2892717)Refutation not found, incomplete strategy % 276.97/39.90 % (2892717)------------------------------ % 276.97/39.90 % (2892717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892717)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892717)Termination reason: Refutation not found, incomplete strategy % 276.97/39.90 % (2892717)Time elapsed: 0.607 s % 276.97/39.90 % (2892717)Peak memory usage: 129 MB % 276.97/39.90 % (2892717)Instructions burned: 901 (million) % 276.97/39.90 % (2892723)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1306263818:cts=off:i=3394_2722 on theBenchmark for (2722ds/3394Mi) % 276.97/39.90 % (2892719)Refutation not found, incomplete strategy % 276.97/39.90 % (2892719)------------------------------ % 276.97/39.90 % (2892719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.97/39.90 % (2892719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.97/39.90 % (2892719)CaDiCaL version: 2.1.3 % 276.97/39.90 % (2892719)Termination reason: Refutation not found, incomplete strategy % 276.97/39.90 % (2892719)Time elapsed: 0.586 s % 276.97/39.90 % (2892719)Peak memory usage: 129 MB % 276.97/39.90 % (2892719)Instructions burned: 882 (million) % 276.97/39.90 % (2892717)--------Terminated %------------------------------------------------------------------------------