%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SYO934_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n005.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:29:27 PM UTC 2026 % Result : CounterSatisfiable 16.90s 3.15s % Output : Saturation 16.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYO934_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n005.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 18:42:02 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 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 % 5.35/1.59 % (1022596)Detected formulas, will run a generic FOF schedule. % 5.35/1.59 % (1022601)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=2180615370:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.35/1.59 % (1022604)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=178320061:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.35/1.59 % (1022606)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3738571311:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.35/1.59 % (1022607)dis-21_1_sil=8000:lcm=predicate:random_seed=3167701159: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) % 5.35/1.59 % (1022603)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=3643920301:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.35/1.59 % (1022602)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=3624730398:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.35/1.59 % (1022605)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2466728392:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.35/1.59 % (1022607)Refutation not found, incomplete strategy % 5.35/1.59 % (1022607)------------------------------ % 5.35/1.59 % (1022607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.59 % (1022607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.59 % (1022607)CaDiCaL version: 2.1.3 % 5.35/1.59 % (1022607)Termination reason: Refutation not found, incomplete strategy % 5.35/1.59 % (1022607)Time elapsed: 0.001 s % 5.35/1.59 % (1022607)Peak memory usage: 88 MB % 5.35/1.59 % (1022604)Refutation not found, incomplete strategy % 5.35/1.59 % (1022604)------------------------------ % 5.35/1.59 % (1022604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.59 % (1022604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.59 % (1022604)CaDiCaL version: 2.1.3 % 5.35/1.59 % (1022604)Termination reason: Refutation not found, incomplete strategy % 5.35/1.59 % (1022604)Time elapsed: 0.003 s % 5.35/1.59 % (1022604)Peak memory usage: 88 MB % 5.35/1.59 % (1022604)Instructions burned: 2 (million) % 5.35/1.59 % (1022606)Refutation not found, incomplete strategy % 5.35/1.59 % (1022606)------------------------------ % 5.35/1.59 % (1022606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.59 % (1022606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.59 % (1022606)CaDiCaL version: 2.1.3 % 5.35/1.59 % (1022606)Termination reason: Refutation not found, incomplete strategy % 5.35/1.59 % (1022606)Time elapsed: 0.005 s % 5.35/1.59 % (1022606)Peak memory usage: 89 MB % 5.35/1.59 % (1022606)Instructions burned: 6 (million) % 5.35/1.59 % (1022605)Instruction limit reached! % 5.35/1.59 % (1022605)------------------------------ % 5.35/1.59 % (1022605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.35/1.59 % (1022605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.35/1.59 % (1022605)CaDiCaL version: 2.1.3 % 5.35/1.59 % (1022605)Termination reason: Instruction limit % 5.35/1.59 % (1022605)Termination phase: Saturation % 5.35/1.59 % (1022605)Time elapsed: 0.049 s % 5.35/1.59 % (1022605)Peak memory usage: 87 MB % 5.35/1.59 % (1022605)Instructions burned: 119 (million) % 5.35/1.59 [W928 18:42:03.281032407 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/1.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.35/1.59 [W928 18:42:03.281057652 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/1.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.35/1.59 [W928 18:42:03.281079654 register_special_ops.cpp:225] Warning: Creating a tensor from 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.13/2.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.13/2.11 [W928 18:42:03.281085777 register_special_ops.cpp:225] Warning: Creating a tensor from 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.13/2.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.13/2.11 [W928 18:42:03.281107630 register_special_ops.cpp:225] Warning: Creating a tensor from 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.13/2.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.13/2.11 [W928 18:42:03.281113014 register_special_ops.cpp:225] Warning: Creating a tensor from 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.13/2.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.13/2.11 % (1022615)lrs+10_1_sil=8000:sp=occurrence:random_seed=3402198046:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 10.13/2.11 % (1022606)------------------------------ % 10.13/2.11 % (1022606)------------------------------ % 10.13/2.11 % (1022607)------------------------------ % 10.13/2.11 % (1022607)------------------------------ % 10.13/2.11 % (1022604)------------------------------ % 10.13/2.11 % (1022604)------------------------------ % 10.13/2.11 % (1022601)Refutation not found, incomplete strategy % 10.13/2.11 % (1022601)------------------------------ % 10.13/2.11 % (1022601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.11 % (1022601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.11 % (1022601)CaDiCaL version: 2.1.3 % 10.13/2.11 % (1022601)Termination reason: Refutation not found, incomplete strategy % 10.13/2.11 % (1022601)Time elapsed: 0.336 s % 10.13/2.11 % (1022601)Peak memory usage: 127 MB % 10.13/2.11 % (1022601)Instructions burned: 853 (million) % 10.13/2.11 % (1022615)Instruction limit reached! % 10.13/2.11 % (1022615)------------------------------ % 10.13/2.11 % (1022615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.11 % (1022615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.11 % (1022615)CaDiCaL version: 2.1.3 % 10.13/2.11 % (1022615)Termination reason: Instruction limit % 10.13/2.11 % (1022615)Termination phase: Saturation % 10.13/2.11 % (1022615)Time elapsed: 0.110 s % 10.13/2.11 % (1022615)Peak memory usage: 88 MB % 10.13/2.11 % (1022615)Instructions burned: 285 (million) % 10.13/2.11 % (1022617)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1352240994:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 10.13/2.11 % (1022619)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=2737598201:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.13/2.11 % (1022618)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1491339438:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 10.13/2.11 % (1022618)Refutation not found, incomplete strategy % 10.13/2.11 % (1022618)------------------------------ % 10.13/2.11 % (1022618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.11 % (1022618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.11 % (1022618)CaDiCaL version: 2.1.3 % 10.13/2.11 % (1022618)Termination reason: Refutation not found, incomplete strategy % 10.13/2.11 % (1022618)Time elapsed: 0.006 s % 10.13/2.11 % (1022618)Peak memory usage: 89 MB % 10.13/2.11 % (1022618)Instructions burned: 8 (million) % 10.13/2.11 % (1022601)------------------------------ % 10.13/2.11 % (1022601)------------------------------ % 10.13/2.11 % (1022620)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=64622326:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 10.13/2.11 % (1022620)Refutation not found, incomplete strategy % 10.13/2.11 % (1022620)------------------------------ % 10.13/2.11 % (1022620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.11 % (1022620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022620)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022620)Termination reason: Refutation not found, incomplete strategy % 13.26/2.58 % (1022620)Time elapsed: 0.001 s % 13.26/2.58 % (1022620)Peak memory usage: 88 MB % 13.26/2.58 % (1022617)Instruction limit reached! % 13.26/2.58 % (1022617)------------------------------ % 13.26/2.58 % (1022617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022617)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022617)Termination reason: Instruction limit % 13.26/2.58 % (1022617)Termination phase: Saturation % 13.26/2.58 % (1022617)Time elapsed: 0.064 s % 13.26/2.58 % (1022617)Peak memory usage: 88 MB % 13.26/2.58 % (1022617)Instructions burned: 159 (million) % 13.26/2.58 % (1022619)Instruction limit reached! % 13.26/2.58 % (1022619)------------------------------ % 13.26/2.58 % (1022619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022619)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022619)Termination reason: Instruction limit % 13.26/2.58 % (1022619)Termination phase: Saturation % 13.26/2.58 % (1022619)Time elapsed: 0.104 s % 13.26/2.58 % (1022619)Peak memory usage: 88 MB % 13.26/2.58 % (1022619)Instructions burned: 249 (million) % 13.26/2.58 % (1022626)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=761982580:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 13.26/2.58 % (1022626)Refutation not found, incomplete strategy % 13.26/2.58 % (1022626)------------------------------ % 13.26/2.58 % (1022626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022626)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022626)Termination reason: Refutation not found, incomplete strategy % 13.26/2.58 % (1022626)Time elapsed: 0.0000 s % 13.26/2.58 % (1022626)Peak memory usage: 88 MB % 13.26/2.58 % (1022603)Refutation not found, incomplete strategy % 13.26/2.58 % (1022603)------------------------------ % 13.26/2.58 % (1022603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022603)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022603)Termination reason: Refutation not found, incomplete strategy % 13.26/2.58 % (1022603)Time elapsed: 0.562 s % 13.26/2.58 % (1022603)Peak memory usage: 126 MB % 13.26/2.58 % (1022603)Instructions burned: 827 (million) % 13.26/2.58 % (1022625)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2611790867:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 13.26/2.58 % (1022627)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2561336981:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 13.26/2.58 % (1022627)Refutation not found, incomplete strategy % 13.26/2.58 % (1022627)------------------------------ % 13.26/2.58 % (1022627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022627)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022627)Termination reason: Refutation not found, incomplete strategy % 13.26/2.58 % (1022627)Time elapsed: 0.001 s % 13.26/2.58 % (1022627)Peak memory usage: 87 MB % 13.26/2.58 % (1022618)------------------------------ % 13.26/2.58 % (1022618)------------------------------ % 13.26/2.58 % (1022626)------------------------------ % 13.26/2.58 % (1022626)------------------------------ % 13.26/2.58 % (1022620)------------------------------ % 13.26/2.58 % (1022620)------------------------------ % 13.26/2.58 % (1022631)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=503019654:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 13.26/2.58 % (1022631)Refutation not found, incomplete strategy % 13.26/2.58 % (1022631)------------------------------ % 13.26/2.58 % (1022631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.26/2.58 % (1022631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.26/2.58 % (1022631)CaDiCaL version: 2.1.3 % 13.26/2.58 % (1022631)Termination reason: Refutation not found, incomplete strategy % 13.26/2.58 % (1022631)Time elapsed: 0.001 s % 13.26/2.58 % (1022631)Peak memory usage: 88 MB % 13.26/2.58 % (1022632)lrs+10_1_sil=8000:sp=occurrence:random_seed=1136882968:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 14.45/2.81 % (1022603)------------------------------ % 14.45/2.81 % (1022603)------------------------------ % 14.45/2.81 % (1022633)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2308844465:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 14.45/2.81 % (1022633)Refutation not found, incomplete strategy % 14.45/2.81 % (1022633)------------------------------ % 14.45/2.81 % (1022633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.45/2.81 % (1022633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.45/2.81 % (1022633)CaDiCaL version: 2.1.3 % 14.45/2.81 % (1022633)Termination reason: Refutation not found, incomplete strategy % 14.45/2.81 % (1022633)Time elapsed: 0.001 s % 14.45/2.81 % (1022633)Peak memory usage: 88 MB % 14.45/2.81 % (1022627)------------------------------ % 14.45/2.81 % (1022627)------------------------------ % 14.45/2.81 % (1022636)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2930852509:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 14.45/2.81 % (1022632)Instruction limit reached! % 14.45/2.81 % (1022632)------------------------------ % 14.45/2.81 % (1022632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.45/2.81 % (1022632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.45/2.81 % (1022632)CaDiCaL version: 2.1.3 % 14.45/2.81 % (1022632)Termination reason: Instruction limit % 14.45/2.81 % (1022632)Termination phase: Saturation % 14.45/2.81 % (1022632)Time elapsed: 0.180 s % 14.45/2.81 % (1022632)Peak memory usage: 88 MB % 14.45/2.81 % (1022632)Instructions burned: 910 (million) % 14.45/2.81 % (1022631)------------------------------ % 14.45/2.81 % (1022631)------------------------------ % 14.45/2.81 % (1022638)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3976148246:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 14.45/2.81 % (1022638)Refutation not found, incomplete strategy % 14.45/2.81 % (1022638)------------------------------ % 14.45/2.81 % (1022638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.45/2.81 % (1022638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.45/2.81 % (1022638)CaDiCaL version: 2.1.3 % 14.45/2.81 % (1022638)Termination reason: Refutation not found, incomplete strategy % 14.45/2.81 % (1022638)Time elapsed: 0.001 s % 14.45/2.81 % (1022638)Peak memory usage: 87 MB % 14.45/2.81 % (1022640)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3944063201:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 14.45/2.81 % (1022640)Refutation not found, incomplete strategy % 14.45/2.81 % (1022640)------------------------------ % 14.45/2.81 % (1022640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.45/2.81 % (1022640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.45/2.81 % (1022640)CaDiCaL version: 2.1.3 % 14.45/2.81 % (1022640)Termination reason: Refutation not found, incomplete strategy % 14.45/2.81 % (1022640)Time elapsed: 0.0000 s % 14.45/2.81 % (1022640)Peak memory usage: 88 MB % 14.45/2.81 % (1022633)------------------------------ % 14.45/2.81 % (1022633)------------------------------ % 14.45/2.81 % (1022641)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3647564665:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi) % 14.45/2.81 % (1022640)------------------------------ % 14.45/2.81 % (1022640)------------------------------ % 14.45/2.81 % (1022644)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=1680235523:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/125Mi) % 14.45/2.81 % (1022644)Refutation not found, incomplete strategy % 14.45/2.81 % (1022644)------------------------------ % 14.45/2.81 % (1022644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.45/2.81 % (1022644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.45/2.81 % (1022644)CaDiCaL version: 2.1.3 % 14.45/2.81 % (1022644)Termination reason: Refutation not found, incomplete strategy % 14.45/2.81 % (1022644)Time elapsed: 0.001 s % 14.45/2.81 % (1022644)Peak memory usage: 88 MB % 14.45/2.81 % (1022638)------------------------------ % 14.45/2.81 % (1022638)------------------------------ % 14.45/2.81 % (1022646)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2585233175:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi) % 16.90/3.15 % (1022646)Instruction limit reached! % 16.90/3.15 % (1022646)------------------------------ % 16.90/3.15 % (1022646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022646)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022646)Termination reason: Instruction limit % 16.90/3.15 % (1022646)Termination phase: Saturation % 16.90/3.15 % (1022646)Time elapsed: 0.030 s % 16.90/3.15 % (1022646)Peak memory usage: 89 MB % 16.90/3.15 % (1022646)Instructions burned: 139 (million) % 16.90/3.15 % (1022648)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2617553595:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/141Mi) % 16.90/3.15 % (1022648)Refutation not found, incomplete strategy % 16.90/3.15 % (1022648)------------------------------ % 16.90/3.15 % (1022648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022648)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022648)Termination reason: Refutation not found, incomplete strategy % 16.90/3.15 % (1022648)Time elapsed: 0.001 s % 16.90/3.15 % (1022648)Peak memory usage: 87 MB % 16.90/3.15 % (1022650)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4074181227:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/431Mi) % 16.90/3.15 % (1022650)Refutation not found, incomplete strategy % 16.90/3.15 % (1022650)------------------------------ % 16.90/3.15 % (1022650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022650)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022650)Termination reason: Refutation not found, incomplete strategy % 16.90/3.15 % (1022650)Time elapsed: 0.0000 s % 16.90/3.15 % (1022650)Peak memory usage: 88 MB % 16.90/3.15 % (1022644)------------------------------ % 16.90/3.15 % (1022644)------------------------------ % 16.90/3.15 % (1022650)------------------------------ % 16.90/3.15 % (1022650)------------------------------ % 16.90/3.15 % (1022653)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=1413010394:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi) % 16.90/3.15 % (1022648)------------------------------ % 16.90/3.15 % (1022648)------------------------------ % 16.90/3.15 % (1022654)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=2501993961:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi) % 16.90/3.15 % (1022654)Instruction limit reached! % 16.90/3.15 % (1022654)------------------------------ % 16.90/3.15 % (1022654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022654)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022654)Termination reason: Instruction limit % 16.90/3.15 % (1022654)Termination phase: Saturation % 16.90/3.15 % (1022654)Time elapsed: 0.034 s % 16.90/3.15 % (1022654)Peak memory usage: 88 MB % 16.90/3.15 % (1022654)Instructions burned: 151 (million) % 16.90/3.15 % (1022625)Instruction limit reached! % 16.90/3.15 % (1022625)------------------------------ % 16.90/3.15 % (1022625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022625)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022625)Termination reason: Instruction limit % 16.90/3.15 % (1022625)Termination phase: Saturation % 16.90/3.15 % (1022625)Time elapsed: 1.156 s % 16.90/3.15 % (1022625)Peak memory usage: 128 MB % 16.90/3.15 % (1022625)Instructions burned: 2351 (million) % 16.90/3.15 % (1022658)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2236471425:i=667:av=off:fsr=off_2981 on theBenchmark for (2981ds/667Mi) % 16.90/3.15 % (1022658)Refutation not found, incomplete strategy % 16.90/3.15 % (1022658)------------------------------ % 16.90/3.15 % (1022658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022658)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022658)Termination reason: Refutation not found, incomplete strategy % 16.90/3.15 % (1022658)Time elapsed: 0.0000 s % 16.90/3.15 % (1022658)Peak memory usage: 87 MB % 16.90/3.15 % (1022657)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2224376821:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi) % 16.90/3.15 % (1022659)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=1248404863:s2a=on:i=185:s2at=1.8:fdi=4_2981 on theBenchmark for (2981ds/185Mi) % 16.90/3.15 % (1022659)First to succeed. % 16.90/3.15 % (1022659)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1022596" % 16.90/3.15 % (1022658)------------------------------ % 16.90/3.15 % (1022658)------------------------------ % 16.90/3.15 [W928 18:42:05.129754589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129788429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129826886 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129839296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129865976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129877132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129902942 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129914276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129939616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129950659 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129976136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 [W928 18:42:05.129987249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.90/3.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.90/3.15 % (1022663)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3515204872:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2979 on theBenchmark for (2979ds/193Mi) % 16.90/3.15 % (1022663)Instruction limit reached! % 16.90/3.15 % (1022663)------------------------------ % 16.90/3.15 % (1022663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022663)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022663)Termination reason: Instruction limit % 16.90/3.15 % (1022663)Termination phase: Saturation % 16.90/3.15 % (1022663)Time elapsed: 0.050 s % 16.90/3.15 % (1022663)Peak memory usage: 89 MB % 16.90/3.15 % (1022663)Instructions burned: 195 (million) % 16.90/3.15 % SZS status CounterSatisfiable for theBenchmark % 16.90/3.15 % SZS output start Saturation. % 16.90/3.15 % SZS output end Saturation. % 16.90/3.15 % SZS output start Definitions and Model Updates. % 16.90/3.15 % SZS output end Definitions and Model Updates. % 16.90/3.15 % (1022659)------------------------------ % 16.90/3.15 % (1022659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.90/3.15 % (1022659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.90/3.15 % (1022659)CaDiCaL version: 2.1.3 % 16.90/3.15 % (1022659)Termination reason: Satisfiable % 16.90/3.15 % (1022659)Time elapsed: 0.001 s % 16.90/3.15 % (1022659)Peak memory usage: 88 MB % 16.90/3.15 % (1022659)------------------------------ % 16.90/3.15 % (1022659)------------------------------ % 16.90/3.15 % (1022596)Success in time 2.298 s % 16.90/3.15 % Vampire exiting %------------------------------------------------------------------------------