%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN988^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 : Wed Sep 30 08:41:45 AM UTC 2026
% Result : CounterSatisfiable 2.84s 0.78s
% Output : Saturation 2.84s
% Verified :
% SZS Type : Derivation
% Derivation depth : 0
% Number of leaves : 1
% Syntax : Number of clauses : 1 ( 1 unt; 0 nHn; 1 RR)
% Number of literals : 1 ( 0 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 1 ( 1 usr; 1 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(u6,negated_conjecture,
~ sK0 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN988^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.23 % Computer : n020.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Tue Sep 29 16:20:49 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.28 Running higher-order theorem proving
% 0.24/0.29 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.75/0.49 % (1242203)Detected formulas, will run a generic FOF schedule.
% 0.75/0.49 % (1242212)lrs+10_2:3_to=lpo:sil=16000:sp=arity:random_seed=1131094723:i=114:bd=all:ss=axioms:sgt=4_2999 on theBenchmark for (2999ds/114Mi)
% 0.75/0.49 % (1242211)lrs+1011_32_sil=2000:tgt=full:alpa=true:random_seed=1399668374:st=5:i=107:sd=1:ss=included:er=filter_2999 on theBenchmark for (2999ds/107Mi)
% 0.75/0.49 % (1242211)Refutation not found, incomplete strategy
% 0.75/0.49 % (1242211)------------------------------
% 0.75/0.49 % (1242211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (1242211)CaDiCaL version: 2.1.3
% 0.75/0.49 % (1242211)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.49 % (1242211)Time elapsed: 0.006 s
% 0.75/0.49 % (1242211)Peak memory usage: 12 MB
% 0.75/0.49 % (1242211)Instructions burned: 8 (million)
% 0.75/0.49 % (1242211)------------------------------
% 0.75/0.49 % (1242211)------------------------------
% 0.75/0.49 % (1242214)dis+1011_1_slsqr=8,1:sil=2000:spb=units:fd=off:kmz=on:flr=on:sac=on:slsq=on:random_seed=1372959308:st=2:i=121:sd=30:aac=none:ep=RS:ss=axioms:sgt=10_2999 on theBenchmark for (2999ds/121Mi)
% 0.75/0.49 % (1242208)lrs+1011_1_sp=occurrence:random_seed=550517854:st=6:sd=4:ss=included_2999 on theBenchmark for (2999ds/0Mi)
% 0.75/0.49 % (1242210)lrs+10_1_sp=unary_first:urr=on:s2agt=32:random_seed=644864272:s2a=on:i=272356:sd=1:bd=all:ss=included_2999 on theBenchmark for (2999ds/272356Mi)
% 0.75/0.49 % (1242209)dis+1010_16_tgt=full:drc=ordering:sp=reverse_frequency:nwc=1:random_seed=3140811078:i=261632:kws=inv_arity_squared:ins=1:av=off:fsd=on_2999 on theBenchmark for (2999ds/261632Mi)
% 0.75/0.49 % (1242213)ott+1011_2_sil=4000:lsd=20:rnwc=on:rp=on:sac=on:newcnf=on:random_seed=33852156:i=132:kws=arity:er=filter_2999 on theBenchmark for (2999ds/132Mi)
% 0.75/0.49 % (1242214)Refutation not found, incomplete strategy
% 0.75/0.49 % (1242214)------------------------------
% 0.75/0.49 % (1242214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (1242214)CaDiCaL version: 2.1.3
% 0.75/0.49 % (1242214)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.49 % (1242214)Time elapsed: 0.001 s
% 0.75/0.49 % (1242214)Peak memory usage: 11 MB
% 0.75/0.49 % (1242213)Refutation not found, incomplete strategy
% 0.75/0.49 % (1242213)------------------------------
% 0.75/0.49 % (1242213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (1242213)CaDiCaL version: 2.1.3
% 0.75/0.49 % (1242213)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.49 % (1242213)Time elapsed: 0.001 s
% 0.75/0.49 % (1242213)Peak memory usage: 11 MB
% 0.75/0.49 % (1242214)------------------------------
% 0.75/0.49 % (1242214)------------------------------
% 0.75/0.49 % (1242213)------------------------------
% 0.75/0.49 % (1242213)------------------------------
% 0.75/0.49 % (1242208)Refutation not found, incomplete strategy
% 0.75/0.49 % (1242208)------------------------------
% 0.75/0.49 % (1242208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (1242208)CaDiCaL version: 2.1.3
% 0.75/0.49 % (1242208)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.49 % (1242208)Time elapsed: 0.009 s
% 0.75/0.49 % (1242208)Peak memory usage: 12 MB
% 0.75/0.49 % (1242208)Instructions burned: 9 (million)
% 0.75/0.49 % (1242208)------------------------------
% 0.75/0.49 % (1242208)------------------------------
% 0.75/0.49 % (1242218)lrs+10_1_sil=2000:sos=on:random_seed=197504759:i=135:sd=2:gtg=position:ss=axioms_2999 on theBenchmark for (2999ds/135Mi)
% 0.75/0.49 % (1242218)Refutation not found, incomplete strategy
% 0.75/0.49 % (1242218)------------------------------
% 0.75/0.49 % (1242218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242212)Instruction limit reached!
% 0.75/0.49 % (1242212)------------------------------
% 0.75/0.49 % (1242212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.49 % (1242212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.49 % (1242212)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242212)Termination reason: Instruction limit
% 2.51/0.68 % (1242212)Termination phase: Saturation
% 2.51/0.68 % (1242212)Time elapsed: 0.042 s
% 2.51/0.68 % (1242212)Peak memory usage: 11 MB
% 2.51/0.68 % (1242212)Instructions burned: 117 (million)
% 2.51/0.68 % (1242218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.68 % (1242218)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242218)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.68 % (1242218)Time elapsed: 0.002 s
% 2.51/0.68 % (1242218)Peak memory usage: 11 MB
% 2.51/0.68 % (1242218)------------------------------
% 2.51/0.68 % (1242218)------------------------------
% 2.51/0.68 % (1242225)dis+1010_4_sil=2000:sos=on:sac=on:random_seed=3519511841:i=140:sd=1:ss=axioms_2999 on theBenchmark for (2999ds/140Mi)
% 2.51/0.68 % (1242224)lrs+1011_1_sil=16000:random_seed=3251673951:i=269:sd=10:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/269Mi)
% 2.51/0.68 % (1242225)Refutation not found, incomplete strategy
% 2.51/0.68 % (1242225)------------------------------
% 2.51/0.68 % (1242225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.68 % (1242225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.68 % (1242225)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242225)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.68 % (1242225)Time elapsed: 0.001 s
% 2.51/0.68 % (1242225)Peak memory usage: 11 MB
% 2.51/0.68 % (1242225)------------------------------
% 2.51/0.68 % (1242225)------------------------------
% 2.51/0.68 % (1242224)Refutation not found, incomplete strategy
% 2.51/0.68 % (1242224)------------------------------
% 2.51/0.68 % (1242224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.68 % (1242224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.68 % (1242224)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242224)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.68 % (1242224)Time elapsed: 0.009 s
% 2.51/0.68 % (1242224)Peak memory usage: 12 MB
% 2.51/0.68 % (1242224)Instructions burned: 9 (million)
% 2.51/0.68 % (1242227)ott+11_4:1_slsqr=8,1:to=kbo:sil=4000:spb=goal:bsr=on:slsq=on:random_seed=3452315746:s2pl=on:st=3:s2a=on:i=124:gtgl=4:sd=1:kws=inv_arity:ep=RST:gtg=position:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/124Mi)
% 2.51/0.68 % (1242224)------------------------------
% 2.51/0.68 % (1242224)------------------------------
% 2.51/0.68 % (1242229)ott+1010_1_to=lpo:sil=32000:fde=none:sos=on:spb=goal_then_units:urr=on:random_seed=2903539115:st=2.5:cts=off:i=297:sd=4:ins=10:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/297Mi)
% 2.51/0.68 % (1242229)Refutation not found, incomplete strategy
% 2.51/0.68 % (1242229)------------------------------
% 2.51/0.68 % (1242229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.68 % (1242229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.68 % (1242229)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242229)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.68 % (1242229)Time elapsed: 0.0000 s
% 2.51/0.68 % (1242229)Peak memory usage: 12 MB
% 2.51/0.68 % (1242229)------------------------------
% 2.51/0.68 % (1242229)------------------------------
% 2.51/0.68 % (1242237)lrs+1011_32_sfv=off:sil=128000:sos=all:newcnf=on:random_seed=2450232814:cond=fast:i=114:nm=2:fsr=off:gtg=all:ss=axioms_2999 on theBenchmark for (2999ds/114Mi)
% 2.51/0.68 % (1242237)Refutation not found, incomplete strategy
% 2.51/0.68 % (1242237)------------------------------
% 2.51/0.68 % (1242237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.68 % (1242237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.51/0.68 % (1242237)CaDiCaL version: 2.1.3
% 2.51/0.68 % (1242237)Termination reason: Refutation not found, incomplete strategy
% 2.51/0.68 % (1242237)Time elapsed: 0.0000 s
% 2.51/0.68 % (1242237)Peak memory usage: 11 MB
% 2.51/0.68 % (1242237)------------------------------
% 2.51/0.68 % (1242237)------------------------------
% 2.51/0.68 % (1242233)lrs+1011_1_sil=4000:plsq=on:sp=occurrence:sos=all:erd=off:plsqr=32,1:random_seed=1727185287:st=5:i=160:sup=off:ss=included_2999 on theBenchmark for (2999ds/160Mi)
% 2.51/0.68 % (1242233)Refutation not found, incomplete strategy
% 2.51/0.68 % (1242233)------------------------------
% 2.51/0.68 % (1242233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.51/0.68 % (1242233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.74 % (1242233)CaDiCaL version: 2.1.3
% 2.84/0.74 % (1242233)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.74 % (1242233)Time elapsed: 0.001 s
% 2.84/0.74 % (1242233)Peak memory usage: 11 MB
% 2.84/0.74 % (1242233)------------------------------
% 2.84/0.74 % (1242233)------------------------------
% 2.84/0.74 % (1242235)lrs+10_16:1_sil=2000:sp=reverse_frequency:lcm=predicate:bsr=unit_only:random_seed=3975678907:avsq=on:i=433:kws=inv_frequency:bs=unit_only:gtg=exists_sym_2999 on theBenchmark for (2999ds/433Mi)
% 2.84/0.74 % (1242230)lrs-1002_1_sil=2000:random_seed=214022469:i=641:sd=20:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/641Mi)
% 2.84/0.74 % (1242239)lrs+10_64_sil=16000:sos=on:urr=on:br=off:random_seed=4055103804:st=2.2:i=120:sd=1:nm=2:gtg=all:ss=axioms_2998 on theBenchmark for (2998ds/120Mi)
% 2.84/0.74 % (1242239)Refutation not found, incomplete strategy
% 2.84/0.74 % (1242239)------------------------------
% 2.84/0.74 % (1242239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.74 % (1242239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.74 % (1242239)CaDiCaL version: 2.1.3
% 2.84/0.74 % (1242239)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.74 % (1242239)Time elapsed: 0.0000 s
% 2.84/0.74 % (1242239)Peak memory usage: 12 MB
% 2.84/0.74 % (1242239)------------------------------
% 2.84/0.74 % (1242239)------------------------------
% 2.84/0.74 % (1242241)lrs+21_1_slsqr=16,1:to=lpo:sil=4000:fs=off:acc=on:alpa=true:slsq=on:random_seed=3417585442:i=126:sd=3:aac=none:doe=on:fsr=off:sup=off:ss=included:er=filter:sgt=10_2998 on theBenchmark for (2998ds/126Mi)
% 2.84/0.74 % (1242245)dis-1011_1_sil=64000:sp=occurrence:nwc=2:sac=on:random_seed=3047987287:i=161:gtgl=2:gtg=exists_sym_2998 on theBenchmark for (2998ds/161Mi)
% 2.84/0.74 % (1242241)Refutation not found, incomplete strategy
% 2.84/0.74 % (1242241)------------------------------
% 2.84/0.74 % (1242241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.74 % (1242241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.74 % (1242241)CaDiCaL version: 2.1.3
% 2.84/0.74 % (1242241)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.75 % (1242241)Time elapsed: 0.001 s
% 2.84/0.75 % (1242241)Peak memory usage: 11 MB
% 2.84/0.75 % (1242241)------------------------------
% 2.84/0.75 % (1242241)------------------------------
% 2.84/0.75 % (1242245)Refutation not found, incomplete strategy
% 2.84/0.75 % (1242245)------------------------------
% 2.84/0.75 % (1242245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.75 % (1242245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.75 % (1242245)CaDiCaL version: 2.1.3
% 2.84/0.75 % (1242245)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.75 % (1242245)Time elapsed: 0.005 s
% 2.84/0.75 % (1242245)Peak memory usage: 12 MB
% 2.84/0.75 % (1242245)Instructions burned: 10 (million)
% 2.84/0.75 % (1242245)------------------------------
% 2.84/0.75 % (1242245)------------------------------
% 2.84/0.75 % (1242249)dis-1010_1_anc=none:sil=2000:sims=off:etr=on:sos=on:spb=units:nwc=2:random_seed=1662160787:i=698:sd=2:kws=arity:aac=none:ss=axioms:sgt=10_2998 on theBenchmark for (2998ds/698Mi)
% 2.84/0.75 % (1242249)Refutation not found, incomplete strategy
% 2.84/0.75 % (1242249)------------------------------
% 2.84/0.75 % (1242249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.75 % (1242249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.75 % (1242249)CaDiCaL version: 2.1.3
% 2.84/0.75 % (1242249)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.75 % (1242249)Time elapsed: 0.0000 s
% 2.84/0.75 % (1242249)Peak memory usage: 11 MB
% 2.84/0.75 % (1242249)------------------------------
% 2.84/0.75 % (1242249)------------------------------
% 2.84/0.75 % (1242248)lrs+11_1024_sil=2000:drc=off:gs=on:flr=on:random_seed=2972287972:s2a=on:i=137:sd=2:fgj=on:av=off:ss=axioms:sgt=4_2998 on theBenchmark for (2998ds/137Mi)
% 2.84/0.75 % (1242227)Instruction limit reached!
% 2.84/0.75 % (1242227)------------------------------
% 2.84/0.75 % (1242227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.75 % (1242227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.75 % (1242227)CaDiCaL version: 2.1.3
% 2.84/0.75 % (1242227)Termination reason: Instruction limit
% 2.84/0.78 % (1242227)Termination phase: Saturation
% 2.84/0.78 % (1242227)Time elapsed: 0.106 s
% 2.84/0.78 % (1242227)Peak memory usage: 11 MB
% 2.84/0.78 % (1242227)Instructions burned: 125 (million)
% 2.84/0.78 % (1242251)dis+10_1_sil=32000:s2agt=32:random_seed=3440744927:st=3:s2a=on:i=183:sd=1:gtg=position:ss=axioms_2998 on theBenchmark for (2998ds/183Mi)
% 2.84/0.78 % (1242253)dis+1010_2_sil=8000:plsq=on:plsqr=1,2:fd=off:random_seed=4131048319:st=1.5:s2a=on:i=119:sd=2:sup=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 2.84/0.78 % (1242253)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242253)------------------------------
% 2.84/0.78 % (1242253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242253)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242253)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242253)Time elapsed: 0.001 s
% 2.84/0.78 % (1242253)Peak memory usage: 11 MB
% 2.84/0.78 % (1242253)------------------------------
% 2.84/0.78 % (1242253)------------------------------
% 2.84/0.78 % (1242256)dis+1010_3_sil=2000:tgt=full:plsq=on:drc=off:fde=unused:sp=arity:acc=on:nwc=20:flr=on:sac=on:avsqc=2:random_seed=3644039407:s2pl=on:st=3:avsq=on:i=285:s2at=5:avsqr=52993,1048576:sd=10:gtg=exists_sym:ss=axioms_2997 on theBenchmark for (2997ds/285Mi)
% 2.84/0.78 % (1242248)Instruction limit reached!
% 2.84/0.78 % (1242248)------------------------------
% 2.84/0.78 % (1242248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242248)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242248)Termination reason: Instruction limit
% 2.84/0.78 % (1242248)Termination phase: Saturation
% 2.84/0.78 % (1242248)Time elapsed: 0.098 s
% 2.84/0.78 % (1242248)Peak memory usage: 12 MB
% 2.84/0.78 % (1242248)Instructions burned: 137 (million)
% 2.84/0.78 % (1242258)lrs+1011_1_to=lpo:sil=32000:sp=arity:spb=goal:urr=on:bsr=on:fd=preordered:nwc=0.968:br=off:newcnf=on:random_seed=762063006:s2a=on:i=130:s2at=11:bd=preordered:nm=20:ins=10:gtg=position:gsp=on_2997 on theBenchmark for (2997ds/130Mi)
% 2.84/0.78 % (1242258)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242258)------------------------------
% 2.84/0.78 % (1242258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242258)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242258)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242258)Time elapsed: 0.001 s
% 2.84/0.78 % (1242258)Peak memory usage: 12 MB
% 2.84/0.78 % (1242258)------------------------------
% 2.84/0.78 % (1242258)------------------------------
% 2.84/0.78 % (1242251)Instruction limit reached!
% 2.84/0.78 % (1242251)------------------------------
% 2.84/0.78 % (1242251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242251)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242251)Termination reason: Instruction limit
% 2.84/0.78 % (1242251)Termination phase: Saturation
% 2.84/0.78 % (1242251)Time elapsed: 0.128 s
% 2.84/0.78 % (1242251)Peak memory usage: 12 MB
% 2.84/0.78 % (1242251)Instructions burned: 184 (million)
% 2.84/0.78 % (1242260)lrs+11_128_sil=2000:spb=units:lcm=predicate:nwc=20:slsqc=4:slsq=on:random_seed=179203605:cts=off:i=178:slsql=off:nm=2:av=off:fsr=off_2996 on theBenchmark for (2996ds/178Mi)
% 2.84/0.78 % (1242230)Instruction limit reached!
% 2.84/0.78 % (1242230)------------------------------
% 2.84/0.78 % (1242230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242230)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242230)Termination reason: Instruction limit
% 2.84/0.78 % (1242230)Termination phase: Saturation
% 2.84/0.78 % (1242230)Time elapsed: 0.237 s
% 2.84/0.78 % (1242230)Peak memory usage: 12 MB
% 2.84/0.78 % (1242230)Instructions burned: 641 (million)
% 2.84/0.78 % (1242261)lrs-10_3:2_anc=all:sil=8000:plsq=on:plsqc=1:erd=off:plsqr=1,1:urr=on:rp=on:br=off:sac=on:avsqc=3:random_seed=2133962614:avsq=on:s2a=on:i=270:s2at=2:nicw=on:ss=axioms_2996 on theBenchmark for (2996ds/270Mi)
% 2.84/0.78 % (1242235)Instruction limit reached!
% 2.84/0.78 % (1242235)------------------------------
% 2.84/0.78 % (1242235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242235)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242235)Termination reason: Instruction limit
% 2.84/0.78 % (1242235)Termination phase: Saturation
% 2.84/0.78 % (1242235)Time elapsed: 0.264 s
% 2.84/0.78 % (1242235)Peak memory usage: 12 MB
% 2.84/0.78 % (1242235)Instructions burned: 434 (million)
% 2.84/0.78 % (1242263)dis-1011_1_sil=16000:tgt=full:prc=on:bsd=on:avsql=on:sp=unary_first:spb=intro:acc=on:fd=preordered:avsqc=1:random_seed=4161205839:st=4:avsq=on:i=960:avsqr=1,16:kws=precedence:bd=all:ins=10:ss=axioms_2996 on theBenchmark for (2996ds/960Mi)
% 2.84/0.78 % (1242263)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242263)------------------------------
% 2.84/0.78 % (1242263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242263)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242263)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242263)Time elapsed: 0.004 s
% 2.84/0.78 % (1242263)Peak memory usage: 12 MB
% 2.84/0.78 % (1242263)Instructions burned: 7 (million)
% 2.84/0.78 % (1242263)------------------------------
% 2.84/0.78 % (1242263)------------------------------
% 2.84/0.78 % (1242265)lrs+4_1_sfv=off:sil=16000:sos=all:random_seed=2591880771:i=183:av=off_2996 on theBenchmark for (2996ds/183Mi)
% 2.84/0.78 % (1242265)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242265)------------------------------
% 2.84/0.78 % (1242265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242265)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242265)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242265)Time elapsed: 0.0000 s
% 2.84/0.78 % (1242265)Peak memory usage: 11 MB
% 2.84/0.78 % (1242265)------------------------------
% 2.84/0.78 % (1242265)------------------------------
% 2.84/0.78 % (1242269)lrs+1010_14_sil=4000:tgt=full:plsq=on:plsqc=3:erd=off:plsqr=1,64:spb=goal_then_units:plsql=on:slsqc=3:slsq=on:random_seed=1523400283:i=274:s2at=3:sd=1:kws=arity_squared:gtg=exists_all:ss=axioms:fsd=on:sgt=16_2996 on theBenchmark for (2996ds/274Mi)
% 2.84/0.78 % (1242267)lrs+11_8_slsqr=4,1:sil=2000:erd=off:spb=goal:lsd=50:s2agt=8:slsqc=3:slsq=on:random_seed=2817860484:s2pl=on:i=137:sd=2:ep=R:nm=6:av=off:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/137Mi)
% 2.84/0.78 % (1242267)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242267)------------------------------
% 2.84/0.78 % (1242267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242267)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242267)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242267)Time elapsed: 0.001 s
% 2.84/0.78 % (1242267)Peak memory usage: 11 MB
% 2.84/0.78 % (1242267)------------------------------
% 2.84/0.78 % (1242267)------------------------------
% 2.84/0.78 % (1242256)Instruction limit reached!
% 2.84/0.78 % (1242256)------------------------------
% 2.84/0.78 % (1242256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242256)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242256)Termination reason: Instruction limit
% 2.84/0.78 % (1242256)Termination phase: Saturation
% 2.84/0.78 % (1242256)Time elapsed: 0.183 s
% 2.84/0.78 % (1242256)Peak memory usage: 12 MB
% 2.84/0.78 % (1242256)Instructions burned: 285 (million)
% 2.84/0.78 % (1242272)lrs+34_16:1_anc=all_dependent:to=lpo:sil=2000:sp=unary_first:sos=on:urr=full:fd=off:sac=on:random_seed=2637045068:i=259:aac=none:bd=preordered:ss=axioms_2995 on theBenchmark for (2995ds/259Mi)
% 2.84/0.78 % (1242272)Refutation not found, incomplete strategy
% 2.84/0.78 % (1242272)------------------------------
% 2.84/0.78 % (1242272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242272)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242272)Termination reason: Refutation not found, incomplete strategy
% 2.84/0.78 % (1242272)Time elapsed: 0.001 s
% 2.84/0.78 % (1242272)Peak memory usage: 12 MB
% 2.84/0.78 % (1242272)------------------------------
% 2.84/0.78 % (1242272)------------------------------
% 2.84/0.78 % (1242273)ott+10_1_sil=8000:drc=ordering:urr=on:br=off:random_seed=1573507577:s2a=on:cond=on:i=1197:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/1197Mi)
% 2.84/0.78 % (1242275)lrs+22_32_sil=4000:plsq=on:rp=on:newcnf=on:random_seed=1680567133:st=2.5:s2a=on:i=132:sd=5:ss=included_2995 on theBenchmark for (2995ds/132Mi)
% 2.84/0.78 % (1242275) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1242203-1242275"...
% 2.84/0.78 % (1242275)...printing done.
% 2.84/0.78 % SZS status CounterSatisfiable for theBenchmark
% 2.84/0.78 % SZS output start Saturation.
% See solution above
% 2.84/0.78 % SZS output start Definitions and Model Updates.
% 2.84/0.78 globally flip the polarity of every occurrence of predicate "sK0"
% 2.84/0.78 % SZS output end Definitions and Model Updates.
% 2.84/0.78 % (1242275)------------------------------
% 2.84/0.78 % (1242275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.84/0.78 % (1242275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/0.78 % (1242275)CaDiCaL version: 2.1.3
% 2.84/0.78 % (1242275)Termination reason: Satisfiable
% 2.84/0.78 % (1242275)Time elapsed: 0.001 s
% 2.84/0.78 % (1242275)Peak memory usage: 11 MB
% 2.84/0.78 % (1242203)Success in time 0.472 s
% 2.84/0.78 % Vampire exiting
%------------------------------------------------------------------------------