%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SYN989_8 : TPTP v9.3.1. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.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 02:06:20 PM UTC 2026 % Result : Satisfiable 17.97s 3.23s % Output : Saturation 17.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN989_8 : TPTP v9.3.1. Released v8.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.20 % Computer : n006.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Mon Sep 28 17:20:11 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.24 Running first-order theorem proving % 0.10/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 6.56/1.66 % (4130575)Detected formulas, will run a generic FOF schedule. % 6.56/1.66 % (4130600)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=64109376:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.56/1.66 % (4130600)Refutation not found, incomplete strategy % 6.56/1.66 % (4130600)------------------------------ % 6.56/1.66 % (4130600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.56/1.66 % (4130600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.56/1.66 % (4130600)CaDiCaL version: 2.1.3 % 6.56/1.66 % (4130600)Termination reason: Refutation not found, incomplete strategy % 6.56/1.66 % (4130600)Time elapsed: 0.0000 s % 6.56/1.66 % (4130600)Peak memory usage: 87 MB % 6.56/1.66 % (4130596)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=1261358101:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.56/1.66 % (4130598)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=1657757149:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.56/1.66 % (4130597)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=2922750965:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.56/1.66 % (4130602)dis-21_1_sil=8000:lcm=predicate:random_seed=1930050850: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) % 6.56/1.66 % (4130599)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2204569479:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.56/1.66 % (4130601)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3351493806:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.56/1.66 % (4130599)Refutation not found, incomplete strategy % 6.56/1.66 % (4130599)------------------------------ % 6.56/1.66 % (4130599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.56/1.66 % (4130599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.56/1.66 % (4130599)CaDiCaL version: 2.1.3 % 6.56/1.66 % (4130599)Termination reason: Refutation not found, incomplete strategy % 6.56/1.66 % (4130599)Time elapsed: 0.001 s % 6.56/1.66 % (4130599)Peak memory usage: 87 MB % 6.56/1.66 % (4130602)Refutation not found, incomplete strategy % 6.56/1.66 % (4130602)------------------------------ % 6.56/1.66 % (4130602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.56/1.66 % (4130602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.56/1.66 % (4130602)CaDiCaL version: 2.1.3 % 6.56/1.66 % (4130602)Termination reason: Refutation not found, incomplete strategy % 6.56/1.66 % (4130602)Time elapsed: 0.001 s % 6.56/1.66 % (4130602)Peak memory usage: 88 MB % 6.56/1.66 % (4130601)Refutation not found, incomplete strategy % 6.56/1.66 % (4130601)------------------------------ % 6.56/1.66 % (4130601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.56/1.66 % (4130601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.56/1.66 % (4130601)CaDiCaL version: 2.1.3 % 6.56/1.66 % (4130601)Termination reason: Refutation not found, incomplete strategy % 6.56/1.66 % (4130601)Time elapsed: 0.005 s % 6.56/1.66 % (4130601)Peak memory usage: 88 MB % 6.56/1.66 % (4130601)Instructions burned: 6 (million) % 6.56/1.66 % (4130600)------------------------------ % 6.56/1.66 % (4130600)------------------------------ % 6.56/1.66 % (4130602)------------------------------ % 6.56/1.66 % (4130602)------------------------------ % 6.56/1.66 % (4130599)------------------------------ % 6.56/1.66 % (4130599)------------------------------ % 6.56/1.66 % (4130601)------------------------------ % 6.56/1.66 % (4130601)------------------------------ % 6.56/1.66 % (4130610)lrs+10_1_sil=8000:sp=occurrence:random_seed=2251076626:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.56/1.66 % (4130610)Refutation not found, incomplete strategy % 6.56/1.66 % (4130610)------------------------------ % 6.56/1.66 % (4130610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.56/1.66 % (4130610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.56/1.66 % (4130610)CaDiCaL version: 2.1.3 % 6.56/1.66 % (4130610)Termination reason: Refutation not found, incomplete strategy % 10.70/2.17 % (4130610)Time elapsed: 0.0000 s % 10.70/2.17 % (4130610)Peak memory usage: 87 MB % 10.70/2.17 [W928 17:20:12.134232427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 [W928 17:20:12.134266570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 [W928 17:20:12.134302944 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 [W928 17:20:12.134315657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 [W928 17:20:12.134342087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 [W928 17:20:12.134353670 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.70/2.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.70/2.17 % (4130610)------------------------------ % 10.70/2.17 % (4130610)------------------------------ % 10.70/2.17 % (4130614)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=869534290:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.70/2.17 % (4130613)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3894477786:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 10.70/2.17 % (4130612)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3207055462:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 10.70/2.17 % (4130613)Refutation not found, incomplete strategy % 10.70/2.17 % (4130613)------------------------------ % 10.70/2.17 % (4130613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.70/2.17 % (4130612)Refutation not found, incomplete strategy % 10.70/2.17 % (4130612)------------------------------ % 10.70/2.17 % (4130612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.70/2.17 % (4130613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.70/2.17 % (4130612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.70/2.17 % (4130613)CaDiCaL version: 2.1.3 % 10.70/2.17 % (4130613)Termination reason: Refutation not found, incomplete strategy % 10.70/2.17 % (4130613)Time elapsed: 0.001 s % 10.70/2.17 % (4130612)CaDiCaL version: 2.1.3 % 10.70/2.17 % (4130613)Peak memory usage: 87 MB % 10.70/2.17 % (4130612)Termination reason: Refutation not found, incomplete strategy % 10.70/2.17 % (4130612)Time elapsed: 0.001 s % 10.70/2.17 % (4130612)Peak memory usage: 87 MB % 10.70/2.17 % (4130614)Instruction limit reached! % 10.70/2.17 % (4130614)------------------------------ % 10.70/2.17 % (4130614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.70/2.17 % (4130614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.70/2.17 % (4130614)CaDiCaL version: 2.1.3 % 10.70/2.17 % (4130614)Termination reason: Instruction limit % 10.70/2.17 % (4130614)Termination phase: Saturation % 10.70/2.17 % (4130614)Time elapsed: 0.105 s % 10.70/2.17 % (4130614)Peak memory usage: 88 MB % 10.70/2.17 % (4130614)Instructions burned: 248 (million) % 10.70/2.17 % (4130618)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1715691248:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 11.04/2.28 % (4130618)Refutation not found, incomplete strategy % 11.04/2.28 % (4130618)------------------------------ % 11.04/2.28 % (4130618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130618)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130618)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130618)Time elapsed: 0.0000 s % 11.04/2.28 % (4130618)Peak memory usage: 87 MB % 11.04/2.28 % (4130598)Refutation not found, incomplete strategy % 11.04/2.28 % (4130598)------------------------------ % 11.04/2.28 % (4130598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130598)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130598)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130598)Time elapsed: 0.560 s % 11.04/2.28 % (4130598)Peak memory usage: 125 MB % 11.04/2.28 % (4130598)Instructions burned: 826 (million) % 11.04/2.28 % (4130596)Refutation not found, incomplete strategy % 11.04/2.28 % (4130596)------------------------------ % 11.04/2.28 % (4130596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130596)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130596)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130596)Time elapsed: 0.577 s % 11.04/2.28 % (4130596)Peak memory usage: 125 MB % 11.04/2.28 % (4130596)Instructions burned: 853 (million) % 11.04/2.28 % (4130613)------------------------------ % 11.04/2.28 % (4130613)------------------------------ % 11.04/2.28 % (4130612)------------------------------ % 11.04/2.28 % (4130612)------------------------------ % 11.04/2.28 % (4130618)------------------------------ % 11.04/2.28 % (4130618)------------------------------ % 11.04/2.28 % (4130619)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2503337820:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 11.04/2.28 % (4130621)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1342946794:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 11.04/2.28 % (4130621)Refutation not found, incomplete strategy % 11.04/2.28 % (4130621)------------------------------ % 11.04/2.28 % (4130621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130621)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130621)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130621)Time elapsed: 0.001 s % 11.04/2.28 % (4130621)Peak memory usage: 88 MB % 11.04/2.28 % (4130598)------------------------------ % 11.04/2.28 % (4130598)------------------------------ % 11.04/2.28 % (4130622)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3417317739:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 11.04/2.28 % (4130622)Refutation not found, incomplete strategy % 11.04/2.28 % (4130622)------------------------------ % 11.04/2.28 % (4130622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130622)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130622)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130622)Time elapsed: 0.001 s % 11.04/2.28 % (4130622)Peak memory usage: 87 MB % 11.04/2.28 % (4130624)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1530585378:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 11.04/2.28 % (4130624)Refutation not found, incomplete strategy % 11.04/2.28 % (4130624)------------------------------ % 11.04/2.28 % (4130624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.04/2.28 % (4130624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/2.28 % (4130624)CaDiCaL version: 2.1.3 % 11.04/2.28 % (4130624)Termination reason: Refutation not found, incomplete strategy % 11.04/2.28 % (4130624)Time elapsed: 0.0000 s % 11.04/2.28 % (4130624)Peak memory usage: 87 MB % 11.04/2.28 % (4130596)------------------------------ % 11.04/2.28 % (4130596)------------------------------ % 13.04/2.62 % (4130624)------------------------------ % 13.04/2.62 % (4130624)------------------------------ % 13.04/2.62 % (4130629)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3149432824:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 13.04/2.62 % (4130628)lrs+10_1_sil=8000:sp=occurrence:random_seed=3284054891:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 13.04/2.62 % (4130628)Refutation not found, incomplete strategy % 13.04/2.62 % (4130628)------------------------------ % 13.04/2.62 % (4130628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.62 % (4130628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.62 % (4130628)CaDiCaL version: 2.1.3 % 13.04/2.62 % (4130628)Termination reason: Refutation not found, incomplete strategy % 13.04/2.62 % (4130628)Time elapsed: 0.001 s % 13.04/2.62 % (4130628)Peak memory usage: 87 MB % 13.04/2.62 % (4130629)Refutation not found, incomplete strategy % 13.04/2.62 % (4130629)------------------------------ % 13.04/2.62 % (4130629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.62 % (4130629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.62 % (4130629)CaDiCaL version: 2.1.3 % 13.04/2.62 % (4130629)Termination reason: Refutation not found, incomplete strategy % 13.04/2.62 % (4130629)Time elapsed: 0.001 s % 13.04/2.62 % (4130629)Peak memory usage: 88 MB % 13.04/2.62 % (4130621)------------------------------ % 13.04/2.62 % (4130621)------------------------------ % 13.04/2.62 % (4130622)------------------------------ % 13.04/2.62 % (4130622)------------------------------ % 13.04/2.62 % (4130630)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=644730873:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 13.04/2.62 % (4130633)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2748414262:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 13.04/2.62 % (4130633)Refutation not found, incomplete strategy % 13.04/2.62 % (4130633)------------------------------ % 13.04/2.62 % (4130633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.62 % (4130633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.62 % (4130633)CaDiCaL version: 2.1.3 % 13.04/2.62 % (4130633)Termination reason: Refutation not found, incomplete strategy % 13.04/2.62 % (4130633)Time elapsed: 0.001 s % 13.04/2.62 % (4130633)Peak memory usage: 87 MB % 13.04/2.62 % (4130634)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3603237787:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 13.04/2.62 % (4130634)Refutation not found, incomplete strategy % 13.04/2.62 % (4130634)------------------------------ % 13.04/2.62 % (4130634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.04/2.62 % (4130634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.04/2.62 % (4130634)CaDiCaL version: 2.1.3 % 13.04/2.62 % (4130634)Termination reason: Refutation not found, incomplete strategy % 13.04/2.62 % (4130634)Time elapsed: 0.001 s % 13.04/2.62 % (4130634)Peak memory usage: 87 MB % 13.04/2.62 % (4130629)------------------------------ % 13.04/2.62 % (4130629)------------------------------ % 13.04/2.62 % (4130628)------------------------------ % 13.04/2.62 % (4130628)------------------------------ % 13.04/2.62 [W928 17:20:13.075020611 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.04/2.62 [W928 17:20:13.075048087 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.04/2.62 [W928 17:20:13.075068821 register_special_ops.cpp:225] Warning: Creating a tensor from 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.04/2.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.04/2.62 [W928 17:20:13.075075043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075089737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075099934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075114417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075157983 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075178873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075185113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075199143 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 [W928 17:20:13.075204824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.07/2.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.07/2.80 % (4130639)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=2799967330:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 12.07/2.80 % (4130638)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1289998909:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 12.07/2.80 % (4130639)Refutation not found, incomplete strategy % 12.07/2.80 % (4130639)------------------------------ % 12.07/2.80 % (4130639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.07/2.80 % (4130639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.07/2.80 % (4130639)CaDiCaL version: 2.1.3 % 12.07/2.80 % (4130639)Termination reason: Refutation not found, incomplete strategy % 12.07/2.80 % (4130639)Time elapsed: 0.001 s % 12.07/2.80 % (4130639)Peak memory usage: 87 MB % 12.07/2.80 % (4130630)Refutation not found, incomplete strategy % 12.07/2.80 % (4130630)------------------------------ % 12.07/2.80 % (4130630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.07/2.80 % (4130630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.07/2.80 % (4130630)CaDiCaL version: 2.1.3 % 12.07/2.80 % (4130630)Termination reason: Refutation not found, incomplete strategy % 12.07/2.80 % (4130630)Time elapsed: 0.320 s % 12.07/2.80 % (4130630)Peak memory usage: 126 MB % 17.11/3.03 % (4130630)Instructions burned: 825 (million) % 17.11/3.03 % (4130633)------------------------------ % 17.11/3.03 % (4130633)------------------------------ % 17.11/3.03 % (4130634)------------------------------ % 17.11/3.03 % (4130634)------------------------------ % 17.11/3.03 % (4130642)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3473387893:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi) % 17.11/3.03 % (4130643)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=483063192:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 17.11/3.03 % (4130643)Refutation not found, incomplete strategy % 17.11/3.03 % (4130643)------------------------------ % 17.11/3.03 % (4130643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.03 % (4130643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.03 % (4130643)CaDiCaL version: 2.1.3 % 17.11/3.03 % (4130643)Termination reason: Refutation not found, incomplete strategy % 17.11/3.03 % (4130643)Time elapsed: 0.001 s % 17.11/3.03 % (4130643)Peak memory usage: 87 MB % 17.11/3.03 % (4130639)------------------------------ % 17.11/3.03 % (4130639)------------------------------ % 17.11/3.03 % (4130642)Instruction limit reached! % 17.11/3.03 % (4130642)------------------------------ % 17.11/3.03 % (4130642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.03 % (4130642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.03 % (4130642)CaDiCaL version: 2.1.3 % 17.11/3.03 % (4130642)Termination reason: Instruction limit % 17.11/3.03 % (4130642)Termination phase: Saturation % 17.11/3.03 % (4130642)Time elapsed: 0.056 s % 17.11/3.03 % (4130642)Peak memory usage: 88 MB % 17.11/3.03 % (4130642)Instructions burned: 134 (million) % 17.11/3.03 % (4130630)------------------------------ % 17.11/3.03 % (4130630)------------------------------ % 17.11/3.03 [W928 17:20:14.529443501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529479371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529517714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529530124 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529556938 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529568298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529595081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.11/3.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.11/3.03 [W928 17:20:14.529606404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.529632241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.529642574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.529667258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.529688418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 % (4130646)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=195041818:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi) % 17.97/3.23 % (4130646)Refutation not found, incomplete strategy % 17.97/3.23 % (4130646)------------------------------ % 17.97/3.23 % (4130646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130646)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130646)Termination reason: Refutation not found, incomplete strategy % 17.97/3.23 % (4130646)Time elapsed: 0.001 s % 17.97/3.23 % (4130646)Peak memory usage: 87 MB % 17.97/3.23 % (4130648)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=3436711888:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi) % 17.97/3.23 % (4130647)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=3451863632:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 17.97/3.23 % (4130648)Instruction limit reached! % 17.97/3.23 % (4130648)------------------------------ % 17.97/3.23 % (4130648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130648)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130648)Termination reason: Instruction limit % 17.97/3.23 % (4130648)Termination phase: Saturation % 17.97/3.23 % (4130648)Time elapsed: 0.034 s % 17.97/3.23 % (4130648)Peak memory usage: 88 MB % 17.97/3.23 % (4130648)Instructions burned: 154 (million) % 17.97/3.23 % (4130619)Instruction limit reached! % 17.97/3.23 % (4130619)------------------------------ % 17.97/3.23 % (4130619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130619)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130619)Termination reason: Instruction limit % 17.97/3.23 % (4130619)Termination phase: Saturation % 17.97/3.23 % (4130619)Time elapsed: 1.161 s % 17.97/3.23 % (4130619)Peak memory usage: 127 MB % 17.97/3.23 % (4130619)Instructions burned: 2350 (million) % 17.97/3.23 % (4130643)------------------------------ % 17.97/3.23 % (4130643)------------------------------ % 17.97/3.23 % (4130652)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2670366307:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi) % 17.97/3.23 % (4130638)Refutation not found, incomplete strategy % 17.97/3.23 % (4130638)------------------------------ % 17.97/3.23 % (4130638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130638)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130638)Termination reason: Refutation not found, incomplete strategy % 17.97/3.23 % (4130638)Time elapsed: 0.557 s % 17.97/3.23 % (4130638)Peak memory usage: 126 MB % 17.97/3.23 % (4130638)Instructions burned: 824 (million) % 17.97/3.23 % (4130653)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3512211665:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi) % 17.97/3.23 % (4130653)Refutation not found, incomplete strategy % 17.97/3.23 % (4130653)------------------------------ % 17.97/3.23 % (4130653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130653)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130653)Termination reason: Refutation not found, incomplete strategy % 17.97/3.23 % (4130653)Time elapsed: 0.001 s % 17.97/3.23 % (4130653)Peak memory usage: 87 MB % 17.97/3.23 % (4130646)------------------------------ % 17.97/3.23 % (4130646)------------------------------ % 17.97/3.23 % (4130654)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=3758803380:s2a=on:i=185:s2at=1.8:fdi=4_2979 on theBenchmark for (2979ds/185Mi) % 17.97/3.23 % (4130654)First to succeed. % 17.97/3.23 % (4130654)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4130575" % 17.97/3.23 [W928 17:20:14.942799743 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942846473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942885237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942898167 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942923683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942935980 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942973654 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.942991950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.943040664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.943053900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.943084594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 [W928 17:20:14.943150050 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.97/3.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.97/3.23 % (4130658)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3078741300:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/193Mi) % 17.97/3.23 % (4130638)------------------------------ % 17.97/3.23 % (4130638)------------------------------ % 17.97/3.23 % (4130658)Refutation not found, incomplete strategy % 17.97/3.23 % (4130658)------------------------------ % 17.97/3.23 % (4130658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130658)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130658)Termination reason: Refutation not found, incomplete strategy % 17.97/3.23 % (4130658)Time elapsed: 0.001 s % 17.97/3.23 % (4130658)Peak memory usage: 87 MB % 17.97/3.23 % (4130653)------------------------------ % 17.97/3.23 % (4130653)------------------------------ % 17.97/3.23 % SZS status Satisfiable for theBenchmark % 17.97/3.23 % SZS output start Saturation. % 17.97/3.23 % SZS output end Saturation. % 17.97/3.23 % SZS output start Definitions and Model Updates. % 17.97/3.23 % SZS output end Definitions and Model Updates. % 17.97/3.23 % (4130654)------------------------------ % 17.97/3.23 % (4130654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.97/3.23 % (4130654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.97/3.23 % (4130654)CaDiCaL version: 2.1.3 % 17.97/3.23 % (4130654)Termination reason: Satisfiable % 17.97/3.23 % (4130654)Time elapsed: 0.001 s % 17.97/3.23 % (4130654)Peak memory usage: 88 MB % 17.97/3.23 % (4130654)------------------------------ % 17.97/3.23 % (4130654)------------------------------ % 17.97/3.23 % (4130575)Success in time 2.465 s % 17.97/3.23 % Vampire exiting %------------------------------------------------------------------------------