%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW205+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 01:39:37 PM UTC 2026
% Result : Theorem 186.75s 32.56s
% Output : Refutation 186.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 23 ( 17 unt; 0 def)
% Number of atoms : 38 ( 4 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 32 ( 17 ~; 9 |; 3 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-5 aty)
% Number of variables : 49 ( 47 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_ORe,hAPP(v_s,X0))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_th) ).
fof(f46,axiom,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__norm__def) ).
fof(f210,axiom,
! [X0,X1,X2,X3] :
( class_RealVector_Oreal__normed__vector(X3)
=> ( ! [X4] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X2,X4)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X3,hAPP(X1,X4)),X0) )
=> c_SEQ_OBseq(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_BseqI2_H) ).
fof(f1131,axiom,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__RealVector_Oreal__normed__vector) ).
fof(f1271,axiom,
! [X0,X1,X2,X3,X4,X5] : hAPP(c_COMBB(X5,X4,X3,X2,X1),X0) = hAPP(X2,hAPP(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBB__1) ).
fof(f1274,conjecture,
c_SEQ_OBseq(tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1275,negated_conjecture,
~ c_SEQ_OBseq(tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____))),
inference(negated_conjecture,[status(cth)],[f1274]) ).
fof(f1283,plain,
~ c_SEQ_OBseq(tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____))),
inference(flattening,[],[f1275]) ).
fof(f1489,plain,
! [X0,X1,X2,X3] :
( c_SEQ_OBseq(X3,X1)
| ? [X4] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X3,hAPP(X1,X4)),X0)
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X2,X4) )
| ~ class_RealVector_Oreal__normed__vector(X3) ),
inference(ennf_transformation,[],[f210]) ).
fof(f1490,plain,
! [X0,X1,X2,X3] :
( c_SEQ_OBseq(X3,X1)
| ? [X4] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X3,hAPP(X1,X4)),X0)
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X2,X4) )
| ~ class_RealVector_Oreal__normed__vector(X3) ),
inference(flattening,[],[f1489]) ).
fof(f2419,plain,
! [X0,X1,X2,X3] :
( c_SEQ_OBseq(X3,X1)
| ( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X3,hAPP(X1,sK15(X0,X1,X2,X3))),X0)
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X2,sK15(X0,X1,X2,X3)) )
| ~ class_RealVector_Oreal__normed__vector(X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X4,sK15(X0,X1,X2,X3))],[f1490]) ).
fof(f2729,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_ORe,hAPP(v_s,X0))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(cnf_transformation,[],[f15]) ).
fof(f2769,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f46]) ).
fof(f2992,plain,
! [X2,X3,X0,X1] :
( c_SEQ_OBseq(X3,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X3,hAPP(X1,sK15(X0,X1,X2,X3))),X0)
| ~ class_RealVector_Oreal__normed__vector(X3) ),
inference(cnf_transformation,[],[f2419]) ).
fof(f4240,plain,
class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1131]) ).
fof(f4380,plain,
! [X2,X3,X0,X1,X4,X5] : hAPP(X2,hAPP(X1,X0)) = hAPP(c_COMBB(X5,X4,X3,X2,X1),X0),
inference(cnf_transformation,[],[f1271]) ).
fof(f4383,plain,
~ c_SEQ_OBseq(tc_RealDef_Oreal,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____))),
inference(cnf_transformation,[],[f1283]) ).
fof(f22467,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),sK15(X0,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),X1,tc_RealDef_Oreal))),X0)
| ~ class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ),
inference(resolution,[],[f2992,f4383]) ).
fof(f22471,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),sK15(X0,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),X1,tc_RealDef_Oreal))),X0),
inference(forward_subsumption_resolution,[],[f22467,f4240]) ).
fof(f22472,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),sK15(X0,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),X1,tc_RealDef_Oreal))),X0),
inference(forward_demodulation,[],[f22471,f2769]) ).
fof(f22473,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_ORe,hAPP(c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____),sK15(X0,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),X1,tc_RealDef_Oreal)))),X0),
inference(forward_demodulation,[],[f22472,f4380]) ).
fof(f22474,plain,
! [X0,X1] : ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_ORe,hAPP(v_s,hAPP(v_f____,sK15(X0,c_COMBB(tc_Complex_Ocomplex,tc_RealDef_Oreal,tc_Nat_Onat,c_Complex_ORe,c_COMBB(tc_Nat_Onat,tc_Complex_Ocomplex,tc_Nat_Onat,v_s,v_f____)),X1,tc_RealDef_Oreal))))),X0),
inference(forward_demodulation,[],[f22473,f4380]) ).
fof(f94035,plain,
$false,
inference(resolution,[],[f22474,f2729]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW205+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n005.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 13:18:08 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.77/1.82 % (777897)Will run a generic schedule for satisfiability detection.
% 9.77/1.82 % (777906)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3432441105:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.77/1.82 % (777903)% WARNING: option uhcvi not known.
% 9.77/1.82 % (777902)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3590193833_2999 on theBenchmark for (2999ds/0Mi)
% 9.77/1.82 % (777903)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3897262026:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.77/1.82 % (777904)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1218365030:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.77/1.82 % (777905)dis+10_1_sil=32000:sp=arity:random_seed=3927931537:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.77/1.82 % (777907)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1272263472:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.77/1.82 % (777908)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=40470060:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.77/1.82 % (777906)Instruction limit reached!
% 9.77/1.82 % (777906)------------------------------
% 9.77/1.82 % (777906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.77/1.82 % (777906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/1.82 % (777906)CaDiCaL version: 2.1.3
% 9.77/1.82 % (777906)Termination reason: Instruction limit
% 9.77/1.82 % (777906)Termination phase: Saturation
% 9.77/1.82 % (777906)Time elapsed: 0.030 s
% 9.77/1.82 % (777906)Peak memory usage: 14 MB
% 9.77/1.82 % (777906)Instructions burned: 116 (million)
% 9.77/1.82 % (777916)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3665874841:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 9.77/1.82 % (777905)Instruction limit reached!
% 9.77/1.82 % (777905)------------------------------
% 9.77/1.82 % (777905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.77/1.82 % (777905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/1.82 % (777905)CaDiCaL version: 2.1.3
% 9.77/1.82 % (777905)Termination reason: Instruction limit
% 9.77/1.82 % (777905)Termination phase: Saturation
% 9.77/1.82 % (777905)Time elapsed: 0.052 s
% 9.77/1.82 % (777905)Peak memory usage: 14 MB
% 9.77/1.82 % (777905)Instructions burned: 104 (million)
% 9.77/1.82 % (777907)Instruction limit reached!
% 9.77/1.82 % (777907)------------------------------
% 9.77/1.82 % (777907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.77/1.82 % (777907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/1.82 % (777907)CaDiCaL version: 2.1.3
% 9.77/1.82 % (777907)Termination reason: Instruction limit
% 9.77/1.82 % (777907)Termination phase: Saturation
% 9.77/1.82 % (777907)Time elapsed: 0.072 s
% 9.77/1.82 % (777907)Peak memory usage: 15 MB
% 9.77/1.82 % (777907)Instructions burned: 131 (million)
% 9.77/1.82 % (777918)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=600473225:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 9.77/1.82 % (777908)Instruction limit reached!
% 9.77/1.82 % (777908)------------------------------
% 9.77/1.82 % (777908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.77/1.82 % (777908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/1.82 % (777908)CaDiCaL version: 2.1.3
% 9.77/1.82 % (777908)Termination reason: Instruction limit
% 9.77/1.82 % (777908)Termination phase: Saturation
% 9.77/1.82 % (777908)Time elapsed: 0.089 s
% 9.77/1.82 % (777908)Peak memory usage: 16 MB
% 9.77/1.82 % (777908)Instructions burned: 160 (million)
% 9.77/1.82 % (777920)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1174884277:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.77/1.82 % (777921)ott-21_1_sil=16000:fs=off:random_seed=1983179250:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.77/1.82 % (777918)Instruction limit reached!
% 9.77/1.82 % (777918)------------------------------
% 9.77/1.82 % (777918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.77/1.82 % (777918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.77/1.82 % (777918)CaDiCaL version: 2.1.3
% 9.77/1.82 % (777918)Termination reason: Instruction limit
% 35.73/5.31 % (777918)Termination phase: Saturation
% 35.73/5.31 % (777918)Time elapsed: 0.061 s
% 35.73/5.31 % (777918)Peak memory usage: 15 MB
% 35.73/5.31 % (777918)Instructions burned: 131 (million)
% 35.73/5.31 % (777924)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4019089874:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 35.73/5.31 % (777921)Instruction limit reached!
% 35.73/5.31 % (777921)------------------------------
% 35.73/5.31 % (777921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777921)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777921)Termination reason: Instruction limit
% 35.73/5.31 % (777921)Termination phase: Saturation
% 35.73/5.31 % (777921)Time elapsed: 0.092 s
% 35.73/5.31 % (777921)Peak memory usage: 14 MB
% 35.73/5.31 % (777921)Instructions burned: 182 (million)
% 35.73/5.31 % (777916)Instruction limit reached!
% 35.73/5.31 % (777916)------------------------------
% 35.73/5.31 % (777916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777916)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777916)Termination reason: Instruction limit
% 35.73/5.31 % (777916)Termination phase: Finite model building preprocessing
% 35.73/5.31 % (777916)Time elapsed: 0.183 s
% 35.73/5.31 % (777916)Peak memory usage: 22 MB
% 35.73/5.31 % (777916)Instructions burned: 716 (million)
% 35.73/5.31 % (777926)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2165987282:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.73/5.31 % (777927)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2625203525:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 35.73/5.31 % TRYING [1]
% 35.73/5.31 % TRYING [2]
% 35.73/5.31 % (777924)Instruction limit reached!
% 35.73/5.31 % (777924)------------------------------
% 35.73/5.31 % (777924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777924)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777924)Termination reason: Instruction limit
% 35.73/5.31 % (777924)Termination phase: Saturation
% 35.73/5.31 % (777924)Time elapsed: 0.288 s
% 35.73/5.31 % (777924)Peak memory usage: 16 MB
% 35.73/5.31 % (777924)Instructions burned: 478 (million)
% 35.73/5.31 % (777930)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1980270067:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 35.73/5.31 % (777920)Instruction limit reached!
% 35.73/5.31 % (777920)------------------------------
% 35.73/5.31 % (777920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777920)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777920)Termination reason: Instruction limit
% 35.73/5.31 % (777920)Termination phase: Saturation
% 35.73/5.31 % (777920)Time elapsed: 0.419 s
% 35.73/5.31 % (777920)Peak memory usage: 20 MB
% 35.73/5.31 % (777920)Instructions burned: 684 (million)
% 35.73/5.31 % (777932)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3508058859:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 35.73/5.31 % TRYING [1]
% 35.73/5.31 % TRYING [3]
% 35.73/5.31 % (777927)Instruction limit reached!
% 35.73/5.31 % (777927)------------------------------
% 35.73/5.31 % (777927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777927)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777927)Termination reason: Instruction limit
% 35.73/5.31 % (777927)Termination phase: Saturation
% 35.73/5.31 % (777927)Time elapsed: 0.394 s
% 35.73/5.31 % (777927)Peak memory usage: 24 MB
% 35.73/5.31 % (777927)Instructions burned: 1181 (million)
% 35.73/5.31 % (777934)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3123172250:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 35.73/5.31 % (777926)Instruction limit reached!
% 35.73/5.31 % (777926)------------------------------
% 35.73/5.31 % (777926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.73/5.31 % (777926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.73/5.31 % (777926)CaDiCaL version: 2.1.3
% 35.73/5.31 % (777926)Termination reason: Instruction limit
% 96.43/13.99 % (777926)Termination phase: Finite model building constraint generation
% 96.43/13.99 % (777926)Time elapsed: 0.423 s
% 96.43/13.99 % (777926)Peak memory usage: 32 MB
% 96.43/13.99 % (777926)Instructions burned: 868 (million)
% 96.43/13.99 % (777936)fmb+10_1_sil=64000:random_seed=4051643933:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 96.43/13.99 % (777930)Cannot represent all propositional literals internally
% 96.43/13.99 % (777930)Refutation not found, incomplete strategy
% 96.43/13.99 % (777930)------------------------------
% 96.43/13.99 % (777930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.43/13.99 % (777930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.43/13.99 % (777930)CaDiCaL version: 2.1.3
% 96.43/13.99 % (777930)Termination reason: Refutation not found, incomplete strategy
% 96.43/13.99 % (777930)Time elapsed: 0.369 s
% 96.43/13.99 % (777930)Peak memory usage: 25 MB
% 96.43/13.99 % (777930)Instructions burned: 762 (million)
% 96.43/13.99 % (777930)------------------------------
% 96.43/13.99 % (777930)------------------------------
% 96.43/13.99 % (777938)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3119130003:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 96.43/13.99 % (777934)Instruction limit reached!
% 96.43/13.99 % (777934)------------------------------
% 96.43/13.99 % (777934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.43/13.99 % (777934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.43/13.99 % (777934)CaDiCaL version: 2.1.3
% 96.43/13.99 % (777934)Termination reason: Instruction limit
% 96.43/13.99 % (777934)Termination phase: Saturation
% 96.43/13.99 % (777934)Time elapsed: 0.235 s
% 96.43/13.99 % (777934)Peak memory usage: 21 MB
% 96.43/13.99 % (777934)Instructions burned: 879 (million)
% 96.43/13.99 % (777940)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3113111041:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 96.43/13.99 % (777932)Instruction limit reached!
% 96.43/13.99 % (777932)------------------------------
% 96.43/13.99 % (777932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.43/13.99 % (777932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.43/13.99 % (777932)CaDiCaL version: 2.1.3
% 96.43/13.99 % (777932)Termination reason: Instruction limit
% 96.43/13.99 % (777932)Termination phase: Saturation
% 96.43/13.99 % (777932)Time elapsed: 0.452 s
% 96.43/13.99 % (777932)Peak memory usage: 22 MB
% 96.43/13.99 % (777932)Instructions burned: 693 (million)
% 96.43/13.99 % (777942)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4272100770:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 96.43/13.99 % TRYING [1]
% 96.43/13.99 % TRYING [8]
% 96.43/13.99 % TRYING [2]
% 96.43/13.99 % (777940)Instruction limit reached!
% 96.43/13.99 % (777940)------------------------------
% 96.43/13.99 % (777940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.43/13.99 % (777940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.43/13.99 % (777940)CaDiCaL version: 2.1.3
% 96.43/13.99 % (777940)Termination reason: Instruction limit
% 96.43/13.99 % (777940)Termination phase: Finite model building constraint generation
% 96.43/13.99 % (777940)Time elapsed: 0.230 s
% 96.43/13.99 % (777940)Peak memory usage: 35 MB
% 96.43/13.99 % (777940)Instructions burned: 924 (million)
% 96.43/13.99 % (777944)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=946528732:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 96.43/13.99 % (777938)Cannot represent all propositional literals internally
% 96.43/13.99 % (777938)Refutation not found, incomplete strategy
% 96.43/13.99 % (777938)------------------------------
% 96.43/13.99 % (777938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 96.43/13.99 % (777938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.43/13.99 % (777938)CaDiCaL version: 2.1.3
% 96.43/13.99 % (777938)Termination reason: Refutation not found, incomplete strategy
% 96.43/13.99 % (777938)Time elapsed: 0.370 s
% 96.43/13.99 % (777938)Peak memory usage: 25 MB
% 96.43/13.99 % (777938)Instructions burned: 753 (million)
% 96.43/13.99 % (777938)------------------------------
% 96.43/13.99 % (777938)------------------------------
% 96.43/13.99 % (777946)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3882797413:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 96.43/13.99 % (777944)Instruction limit reached!
% 96.43/13.99 % (777944)------------------------------
% 96.43/13.99 % (777944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777944)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777944)Termination reason: Instruction limit
% 171.78/24.55 % (777944)Termination phase: Saturation
% 171.78/24.55 % (777944)Time elapsed: 0.386 s
% 171.78/24.55 % (777944)Peak memory usage: 27 MB
% 171.78/24.55 % (777944)Instructions burned: 1476 (million)
% 171.78/24.55 % (777948)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3034776080:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 171.78/24.55 % (777946)Cannot represent all propositional literals internally
% 171.78/24.55 % (777946)Refutation not found, incomplete strategy
% 171.78/24.55 % (777946)------------------------------
% 171.78/24.55 % (777946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777946)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777946)Termination reason: Refutation not found, incomplete strategy
% 171.78/24.55 % (777946)Time elapsed: 0.384 s
% 171.78/24.55 % (777946)Peak memory usage: 25 MB
% 171.78/24.55 % (777946)Instructions burned: 788 (million)
% 171.78/24.55 % (777946)------------------------------
% 171.78/24.55 % (777946)------------------------------
% 171.78/24.55 % (777950)ott-2_1_sil=16000:newcnf=on:random_seed=2147857824:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi)
% 171.78/24.55 % TRYING [4]
% 171.78/24.55 % TRYING [3]
% 171.78/24.55 % (777948)Instruction limit reached!
% 171.78/24.55 % (777948)------------------------------
% 171.78/24.55 % (777948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777948)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777948)Termination reason: Instruction limit
% 171.78/24.55 % (777948)Termination phase: Finite model building preprocessing
% 171.78/24.55 % (777948)Time elapsed: 0.567 s
% 171.78/24.55 % (777948)Peak memory usage: 35 MB
% 171.78/24.55 % (777948)Instructions burned: 2175 (million)
% 171.78/24.55 % (777952)ott+10_1_sil=32000:tgt=ground:random_seed=1713288914:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi)
% 171.78/24.55 % (777950)Instruction limit reached!
% 171.78/24.55 % (777950)------------------------------
% 171.78/24.55 % (777950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777950)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777950)Termination reason: Instruction limit
% 171.78/24.55 % (777950)Termination phase: Saturation
% 171.78/24.55 % (777950)Time elapsed: 0.497 s
% 171.78/24.55 % (777950)Peak memory usage: 20 MB
% 171.78/24.55 % (777950)Instructions burned: 870 (million)
% 171.78/24.55 % (777954)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2821069429:i=54282_2977 on theBenchmark for (2977ds/54282Mi)
% 171.78/24.55 % TRYING [1]
% 171.78/24.55 % TRYING [2]
% 171.78/24.55 % TRYING [3]
% 171.78/24.55 % (777952)Instruction limit reached!
% 171.78/24.55 % (777952)------------------------------
% 171.78/24.55 % (777952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777952)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777952)Termination reason: Instruction limit
% 171.78/24.55 % (777952)Termination phase: Saturation
% 171.78/24.55 % (777952)Time elapsed: 1.774 s
% 171.78/24.55 % (777952)Peak memory usage: 44 MB
% 171.78/24.55 % (777952)Instructions burned: 5114 (million)
% 171.78/24.55 % (777956)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2036826826:i=3512:aac=none_2960 on theBenchmark for (2960ds/3512Mi)
% 171.78/24.55 % (777942)Instruction limit reached!
% 171.78/24.55 % (777942)------------------------------
% 171.78/24.55 % (777942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 171.78/24.55 % (777942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.78/24.55 % (777942)CaDiCaL version: 2.1.3
% 171.78/24.55 % (777942)Termination reason: Instruction limit
% 171.78/24.55 % (777942)Termination phase: Saturation
% 171.78/24.55 % (777942)Time elapsed: 2.948 s
% 171.78/24.55 % (777942)Peak memory usage: 39 MB
% 171.78/24.55 % (777942)Instructions burned: 5131 (million)
% 171.78/24.55 % (777958)dis+21_1_sil=32000:sas=cadical:random_seed=977230263:i=3773:amm=off_2959 on theBenchmark for (2959ds/3773Mi)
% 171.78/24.55 % TRYING [4]
% 171.78/24.55 % (777956)Instruction limit reached!
% 171.78/24.55 % (777956)------------------------------
% 171.78/24.55 % (777956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777956)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777956)Termination reason: Instruction limit
% 186.75/32.55 % (777956)Termination phase: Saturation
% 186.75/32.55 % (777956)Time elapsed: 1.109 s
% 186.75/32.55 % (777956)Peak memory usage: 35 MB
% 186.75/32.55 % (777956)Instructions burned: 3515 (million)
% 186.75/32.55 % (777960)ott+11_1_sil=16000:gs=on:random_seed=1140386224:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2949 on theBenchmark for (2949ds/2251Mi)
% 186.75/32.55 % TRYING [4]
% 186.75/32.55 % (777960)Instruction limit reached!
% 186.75/32.55 % (777960)------------------------------
% 186.75/32.55 % (777960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777960)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777960)Termination reason: Instruction limit
% 186.75/32.55 % (777960)Termination phase: Saturation
% 186.75/32.55 % (777960)Time elapsed: 0.810 s
% 186.75/32.55 % (777960)Peak memory usage: 83 MB
% 186.75/32.55 % (777960)Instructions burned: 2252 (million)
% 186.75/32.55 % (777962)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3250962349:fmbsr=1.6:i=67534_2940 on theBenchmark for (2940ds/67534Mi)
% 186.75/32.55 % (777958)Instruction limit reached!
% 186.75/32.55 % (777958)------------------------------
% 186.75/32.55 % (777958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777958)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777958)Termination reason: Instruction limit
% 186.75/32.55 % (777958)Termination phase: Saturation
% 186.75/32.55 % (777958)Time elapsed: 2.215 s
% 186.75/32.55 % (777958)Peak memory usage: 35 MB
% 186.75/32.55 % (777958)Instructions burned: 3774 (million)
% 186.75/32.55 % (777964)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3164194977:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2937 on theBenchmark for (2937ds/4591Mi)
% 186.75/32.55 % TRYING [5]
% 186.75/32.55 % (777964)Instruction limit reached!
% 186.75/32.55 % (777964)------------------------------
% 186.75/32.55 % (777964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777964)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777964)Termination reason: Instruction limit
% 186.75/32.55 % (777964)Termination phase: Saturation
% 186.75/32.55 % (777964)Time elapsed: 1.836 s
% 186.75/32.55 % (777964)Peak memory usage: 34 MB
% 186.75/32.55 % (777964)Instructions burned: 4594 (million)
% 186.75/32.55 % (777966)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3347893571:i=29340_2918 on theBenchmark for (2918ds/29340Mi)
% 186.75/32.55 % TRYING [7]
% 186.75/32.55 % TRYING [5]
% 186.75/32.55 % (777936)Instruction limit reached!
% 186.75/32.55 % (777936)------------------------------
% 186.75/32.55 % (777936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777936)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777936)Termination reason: Instruction limit
% 186.75/32.55 % (777936)Termination phase: Finite model building SAT solving
% 186.75/32.55 % (777936)Time elapsed: 9.869 s
% 186.75/32.55 % (777936)Peak memory usage: 608 MB
% 186.75/32.55 % (777936)Instructions burned: 22061 (million)
% 186.75/32.55 % (777968)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3911290918:i=5211_2893 on theBenchmark for (2893ds/5211Mi)
% 186.75/32.55 % (777968)Instruction limit reached!
% 186.75/32.55 % (777968)------------------------------
% 186.75/32.55 % (777968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777968)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777968)Termination reason: Instruction limit
% 186.75/32.55 % (777968)Termination phase: Saturation
% 186.75/32.55 % (777968)Time elapsed: 2.651 s
% 186.75/32.55 % (777968)Peak memory usage: 45 MB
% 186.75/32.55 % (777968)Instructions burned: 5214 (million)
% 186.75/32.55 % (777970)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3650342798:i=5497:nm=2_2866 on theBenchmark for (2866ds/5497Mi)
% 186.75/32.55 % (777970)Cannot represent all propositional literals internally
% 186.75/32.55 % (777970)Refutation not found, incomplete strategy
% 186.75/32.55 % (777970)------------------------------
% 186.75/32.55 % (777970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777970)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777970)Termination reason: Refutation not found, incomplete strategy
% 186.75/32.55 % (777970)Time elapsed: 0.371 s
% 186.75/32.55 % (777970)Peak memory usage: 25 MB
% 186.75/32.55 % (777970)Instructions burned: 755 (million)
% 186.75/32.55 % (777970)------------------------------
% 186.75/32.55 % (777970)------------------------------
% 186.75/32.55 % (777972)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3205282920:fmbsr=2:i=46332_2862 on theBenchmark for (2862ds/46332Mi)
% 186.75/32.55 % (777972)Cannot represent all propositional literals internally
% 186.75/32.55 % (777972)Refutation not found, incomplete strategy
% 186.75/32.55 % (777972)------------------------------
% 186.75/32.55 % (777972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777972)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777972)Termination reason: Refutation not found, incomplete strategy
% 186.75/32.55 % (777972)Time elapsed: 0.368 s
% 186.75/32.55 % (777972)Peak memory usage: 23 MB
% 186.75/32.55 % (777972)Instructions burned: 771 (million)
% 186.75/32.55 % (777972)------------------------------
% 186.75/32.55 % (777972)------------------------------
% 186.75/32.55 % (777974)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1163251119:i=14071_2858 on theBenchmark for (2858ds/14071Mi)
% 186.75/32.55 % TRYING [12]
% 186.75/32.55 % (777962)Instruction limit reached!
% 186.75/32.55 % (777962)------------------------------
% 186.75/32.55 % (777962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777962)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777962)Termination reason: Instruction limit
% 186.75/32.55 % (777962)Termination phase: Finite model building constraint generation
% 186.75/32.55 % (777962)Time elapsed: 12.887 s
% 186.75/32.55 % (777962)Peak memory usage: 3900 MB
% 186.75/32.55 % (777962)Instructions burned: 67539 (million)
% 186.75/32.55 % (777976)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2067925573:i=22565:add=on:rawr=on_2808 on theBenchmark for (2808ds/22565Mi)
% 186.75/32.55 % (777974)Instruction limit reached!
% 186.75/32.55 % (777974)------------------------------
% 186.75/32.55 % (777974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777974)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777974)Termination reason: Instruction limit
% 186.75/32.55 % (777974)Termination phase: Finite model building constraint generation
% 186.75/32.55 % (777974)Time elapsed: 5.262 s
% 186.75/32.55 % (777974)Peak memory usage: 909 MB
% 186.75/32.55 % (777974)Instructions burned: 14074 (million)
% 186.75/32.55 % (777978)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4064330439:i=8173:av=off_2804 on theBenchmark for (2804ds/8173Mi)
% 186.75/32.55 % (777966)Instruction limit reached!
% 186.75/32.55 % (777966)------------------------------
% 186.75/32.55 % (777966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777966)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777966)Termination reason: Instruction limit
% 186.75/32.55 % (777966)Termination phase: Saturation
% 186.75/32.55 % (777966)Time elapsed: 14.598 s
% 186.75/32.55 % (777966)Peak memory usage: 123 MB
% 186.75/32.55 % (777966)Instructions burned: 29341 (million)
% 186.75/32.55 % (777981)dis+10_16:1_sil=16000:random_seed=7083015:i=9155:fsr=off_2772 on theBenchmark for (2772ds/9155Mi)
% 186.75/32.55 % (777954)Instruction limit reached!
% 186.75/32.55 % (777954)------------------------------
% 186.75/32.55 % (777954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.55 % (777954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.55 % (777954)CaDiCaL version: 2.1.3
% 186.75/32.55 % (777954)Termination reason: Instruction limit
% 186.75/32.55 % (777954)Termination phase: Finite model building constraint generation
% 186.75/32.55 % (777954)Time elapsed: 21.584 s
% 186.75/32.55 % (777954)Peak memory usage: 2348 MB
% 186.75/32.55 % (777954)Instructions burned: 54284 (million)
% 186.75/32.55 % (777984)ott-3_8_sil=64000:random_seed=3531497031:i=20139:bs=on_2758 on theBenchmark for (2758ds/20139Mi)
% 186.75/32.55 % (777976)Instruction limit reached!
% 186.75/32.56 % (777976)------------------------------
% 186.75/32.56 % (777976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.56 % (777976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.56 % (777976)CaDiCaL version: 2.1.3
% 186.75/32.56 % (777976)Termination reason: Instruction limit
% 186.75/32.56 % (777976)Termination phase: Saturation
% 186.75/32.56 % (777976)Time elapsed: 5.147 s
% 186.75/32.56 % (777976)Peak memory usage: 94 MB
% 186.75/32.56 % (777976)Instructions burned: 22567 (million)
% 186.75/32.56 % (777986)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3084829650:fmbsr=2:i=32576_2756 on theBenchmark for (2756ds/32576Mi)
% 186.75/32.56 % TRYING [9]
% 186.75/32.56 % (777978)Instruction limit reached!
% 186.75/32.56 % (777978)------------------------------
% 186.75/32.56 % (777978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.56 % (777978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.56 % (777978)CaDiCaL version: 2.1.3
% 186.75/32.56 % (777978)Termination reason: Instruction limit
% 186.75/32.56 % (777978)Termination phase: Saturation
% 186.75/32.56 % (777978)Time elapsed: 5.273 s
% 186.75/32.56 % (777978)Peak memory usage: 97 MB
% 186.75/32.56 % (777978)Instructions burned: 8173 (million)
% 186.75/32.56 % (777988)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3510718931:i=11404_2751 on theBenchmark for (2751ds/11404Mi)
% 186.75/32.56 % (777981)Instruction limit reached!
% 186.75/32.56 % (777981)------------------------------
% 186.75/32.56 % (777981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.56 % (777981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.56 % (777981)CaDiCaL version: 2.1.3
% 186.75/32.56 % (777981)Termination reason: Instruction limit
% 186.75/32.56 % (777981)Termination phase: Saturation
% 186.75/32.56 % (777981)Time elapsed: 4.759 s
% 186.75/32.56 % (777981)Peak memory usage: 79 MB
% 186.75/32.56 % (777981)Instructions burned: 9155 (million)
% 186.75/32.56 % (777990)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3601985361:i=14134_2724 on theBenchmark for (2724ds/14134Mi)
% 186.75/32.56 % (777986)Instruction limit reached!
% 186.75/32.56 % (777986)------------------------------
% 186.75/32.56 % (777986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.56 % (777986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.56 % (777986)CaDiCaL version: 2.1.3
% 186.75/32.56 % (777986)Termination reason: Instruction limit
% 186.75/32.56 % (777986)Termination phase: Finite model building constraint generation
% 186.75/32.56 % (777986)Time elapsed: 6.531 s
% 186.75/32.56 % (777986)Peak memory usage: 2042 MB
% 186.75/32.56 % (777986)Instructions burned: 32577 (million)
% 186.75/32.56 % (777992)dis+33_16_sil=32000:sac=on:random_seed=2765212766:i=15851:nm=0_2689 on theBenchmark for (2689ds/15851Mi)
% 186.75/32.56 % (777990) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-777897-777990"...
% 186.75/32.56 % (777990)...printing done.
% 186.75/32.56 % (777990)Refutation found. Thanks to Tanya!
% 186.75/32.56 % SZS status Theorem for theBenchmark
% 186.75/32.56 % SZS output start Proof for theBenchmark
% See solution above
% 186.75/32.56 % (777990)------------------------------
% 186.75/32.56 % (777990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 186.75/32.56 % (777990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.75/32.56 % (777990)CaDiCaL version: 2.1.3
% 186.75/32.56 % (777990)Termination reason: Refutation
% 186.75/32.56 % (777990)Time elapsed: 4.289 s
% 186.75/32.56 % (777990)Peak memory usage: 54 MB
% 186.75/32.56 % (777990)Instructions burned: 6525 (million)
% 186.75/32.56 % (777897)Success in time 32.329 s
% 186.75/32.56 % Vampire exiting
%------------------------------------------------------------------------------