%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 10:18:22 AM UTC 2026
% Result : Theorem 206.38s 39.14s
% Output : Refutation 206.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 33 ( 16 unt; 0 def)
% Number of atoms : 105 ( 11 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 118 ( 46 ~; 41 |; 24 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 29 ( 25 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+2.ax',d1_xboole_0) ).
fof(f2714,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+54.ax',t51_card_1) ).
fof(f5658,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& m1_group_2(X1,X0) )
=> r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_latsubgr) ).
fof(f5659,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& m1_group_2(X1,X0) )
=> k1_funct_1(k1_latsubgr(X0),X1) != k1_xboole_0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_latsubgr) ).
fof(f5660,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_group_1(X1)
& m1_group_2(X1,X0) )
=> k1_funct_1(k1_latsubgr(X0),X1) != k1_xboole_0 ) ),
inference(negated_conjecture,[status(cth)],[f5659]) ).
fof(f12715,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f5658]) ).
fof(f12716,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1))
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f12715]) ).
fof(f12717,plain,
? [X0] :
( ? [X1] :
( k1_xboole_0 = k1_funct_1(k1_latsubgr(X0),X1)
& v1_group_1(X1)
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f5660]) ).
fof(f12718,plain,
? [X0] :
( ? [X1] :
( k1_xboole_0 = k1_funct_1(k1_latsubgr(X0),X1)
& v1_group_1(X1)
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f12717]) ).
fof(f12772,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f29]) ).
fof(f17674,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f2714]) ).
fof(f23197,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1)) ),
inference(cnf_transformation,[],[f12716]) ).
fof(f23198,plain,
m1_group_2(sK1667,sK1666),
inference(cnf_transformation,[],[f12718]) ).
fof(f23199,plain,
v1_group_1(sK1667),
inference(cnf_transformation,[],[f12718]) ).
fof(f23200,plain,
k1_xboole_0 = k1_funct_1(k1_latsubgr(sK1666),sK1667),
inference(cnf_transformation,[],[f12718]) ).
fof(f23201,plain,
l1_group_1(sK1666),
inference(cnf_transformation,[],[f12718]) ).
fof(f23202,plain,
v4_group_1(sK1666),
inference(cnf_transformation,[],[f12718]) ).
fof(f23203,plain,
v3_group_1(sK1666),
inference(cnf_transformation,[],[f12718]) ).
fof(f23204,plain,
~ v3_struct_0(sK1666),
inference(cnf_transformation,[],[f12718]) ).
fof(f23241,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f12772,f17674]) ).
fof(f25987,plain,
np__0 = k1_funct_1(k1_latsubgr(sK1666),sK1667),
inference(definition_unfolding,[],[f23200,f17674]) ).
fof(f26001,plain,
! [X1] : ~ r2_hidden(X1,np__0),
inference(equality_resolution,[],[f23241]) ).
fof(f34948,plain,
! [X0,X1] :
( ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| v1_group_1(X1)
| r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1)) ),
inference(consistent_polarity_flipping,[],[f23197]) ).
fof(f34949,plain,
v3_struct_0(sK1666),
inference(consistent_polarity_flipping,[],[f23204]) ).
fof(f34950,plain,
~ v1_group_1(sK1667),
inference(consistent_polarity_flipping,[],[f23199]) ).
fof(f201619,plain,
! [X0] :
( ~ v4_group_1(sK1666)
| ~ l1_group_1(sK1666)
| ~ v3_struct_0(sK1666)
| ~ m1_group_2(X0,sK1666)
| v1_group_1(X0)
| r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),X0)) ),
inference(resolution,[],[f34948,f23203]) ).
fof(f201622,plain,
! [X0] :
( ~ l1_group_1(sK1666)
| ~ v3_struct_0(sK1666)
| ~ m1_group_2(X0,sK1666)
| v1_group_1(X0)
| r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),X0)) ),
inference(forward_subsumption_resolution,[],[f201619,f23202]) ).
fof(f201632,plain,
! [X0] :
( ~ v3_struct_0(sK1666)
| ~ m1_group_2(X0,sK1666)
| v1_group_1(X0)
| r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),X0)) ),
inference(forward_subsumption_resolution,[],[f201622,f23201]) ).
fof(f201642,plain,
! [X0] :
( ~ m1_group_2(X0,sK1666)
| v1_group_1(X0)
| r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),X0)) ),
inference(forward_subsumption_resolution,[],[f201632,f34949]) ).
fof(f626168,plain,
( v1_group_1(sK1667)
| r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),sK1667)) ),
inference(resolution,[],[f201642,f23198]) ).
fof(f626169,plain,
r2_hidden(k2_group_1(sK1666),k1_funct_1(k1_latsubgr(sK1666),sK1667)),
inference(forward_subsumption_resolution,[],[f626168,f34950]) ).
fof(f626199,plain,
r2_hidden(k2_group_1(sK1666),np__0),
inference(forward_demodulation,[],[f626169,f25987]) ).
fof(f626225,plain,
$false,
inference(forward_subsumption_resolution,[],[f626199,f26001]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 10:24:42 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.29/3.93 % (2617052)Will run a generic schedule for satisfiability detection.
% 23.29/3.93 % (2617061)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2903270648:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 23.29/3.93 % (2617058)% WARNING: option uhcvi not known.
% 23.29/3.93 % (2617058)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2155543358:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 23.29/3.93 % (2617057)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=865983692_2997 on theBenchmark for (2997ds/0Mi)
% 23.29/3.93 % (2617059)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1016133438:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 23.29/3.93 % (2617060)dis+10_1_sil=32000:sp=arity:random_seed=142024528:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 23.29/3.93 % (2617062)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3433796368:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 23.29/3.93 % (2617063)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1694661551:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 23.29/3.93 % (2617061)Instruction limit reached!
% 23.29/3.93 % (2617061)------------------------------
% 23.29/3.93 % (2617061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.29/3.93 % (2617061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/3.93 % (2617061)CaDiCaL version: 2.1.3
% 23.29/3.93 % (2617061)Termination reason: Instruction limit
% 23.29/3.93 % (2617061)Termination phase: NewCNF
% 23.29/3.93 % (2617061)Time elapsed: 0.052 s
% 23.29/3.93 % (2617061)Peak memory usage: 26 MB
% 23.29/3.93 % (2617061)Instructions burned: 116 (million)
% 23.29/3.93 % (2617071)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=746189080:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 23.29/3.93 % (2617060)Instruction limit reached!
% 23.29/3.93 % (2617060)------------------------------
% 23.29/3.93 % (2617060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.29/3.93 % (2617060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/3.93 % (2617060)CaDiCaL version: 2.1.3
% 23.29/3.93 % (2617060)Termination reason: Instruction limit
% 23.29/3.93 % (2617060)Termination phase: Preprocessing 3
% 23.29/3.93 % (2617060)Time elapsed: 0.076 s
% 23.29/3.93 % (2617060)Peak memory usage: 25 MB
% 23.29/3.93 % (2617060)Instructions burned: 104 (million)
% 23.29/3.93 % (2617062)Instruction limit reached!
% 23.29/3.93 % (2617062)------------------------------
% 23.29/3.93 % (2617062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.29/3.93 % (2617062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/3.93 % (2617062)CaDiCaL version: 2.1.3
% 23.29/3.93 % (2617062)Termination reason: Instruction limit
% 23.29/3.93 % (2617062)Termination phase: Preprocessing 3
% 23.29/3.93 % (2617062)Time elapsed: 0.092 s
% 23.29/3.93 % (2617062)Peak memory usage: 25 MB
% 23.29/3.93 % (2617062)Instructions burned: 131 (million)
% 23.29/3.93 % (2617073)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1506493491:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 23.29/3.93 % (2617063)Instruction limit reached!
% 23.29/3.93 % (2617063)------------------------------
% 23.29/3.93 % (2617063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.29/3.93 % (2617063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.29/3.93 % (2617063)CaDiCaL version: 2.1.3
% 23.29/3.93 % (2617063)Termination reason: Instruction limit
% 23.29/3.93 % (2617063)Termination phase: Preprocessing 3
% 23.29/3.93 % (2617063)Time elapsed: 0.109 s
% 23.29/3.93 % (2617063)Peak memory usage: 27 MB
% 23.29/3.93 % (2617063)Instructions burned: 159 (million)
% 23.29/3.93 % (2617074)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=3925674304:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 23.29/3.93 % (2617076)ott-21_1_sil=16000:fs=off:random_seed=516823765:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 23.29/3.93 % (2617073)Instruction limit reached!
% 23.29/3.93 % (2617073)------------------------------
% 23.29/3.93 % (2617073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.29/3.93 % (2617073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617073)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617073)Termination reason: Instruction limit
% 55.21/8.48 % (2617073)Termination phase: Preprocessing 3
% 55.21/8.48 % (2617073)Time elapsed: 0.091 s
% 55.21/8.48 % (2617073)Peak memory usage: 25 MB
% 55.21/8.48 % (2617073)Instructions burned: 131 (million)
% 55.21/8.48 % (2617079)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=486368133:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 55.21/8.48 % (2617076)Instruction limit reached!
% 55.21/8.48 % (2617076)------------------------------
% 55.21/8.48 % (2617076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617076)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617076)Termination reason: Instruction limit
% 55.21/8.48 % (2617076)Termination phase: Preprocessing 3
% 55.21/8.48 % (2617076)Time elapsed: 0.119 s
% 55.21/8.48 % (2617076)Peak memory usage: 27 MB
% 55.21/8.48 % (2617076)Instructions burned: 181 (million)
% 55.21/8.48 % (2617071)Instruction limit reached!
% 55.21/8.48 % (2617071)------------------------------
% 55.21/8.48 % (2617071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617071)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617071)Termination reason: Instruction limit
% 55.21/8.48 % (2617071)Termination phase: Finite model building preprocessing
% 55.21/8.48 % (2617071)Time elapsed: 0.213 s
% 55.21/8.48 % (2617071)Peak memory usage: 39 MB
% 55.21/8.48 % (2617071)Instructions burned: 718 (million)
% 55.21/8.48 % (2617081)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1931012866:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 55.21/8.48 % (2617083)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3115276312:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 55.21/8.48 % (2617074)Instruction limit reached!
% 55.21/8.48 % (2617074)------------------------------
% 55.21/8.48 % (2617074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617074)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617074)Termination reason: Instruction limit
% 55.21/8.48 % (2617074)Termination phase: Property scanning
% 55.21/8.48 % (2617074)Time elapsed: 0.334 s
% 55.21/8.48 % (2617074)Peak memory usage: 33 MB
% 55.21/8.48 % (2617074)Instructions burned: 684 (million)
% 55.21/8.48 % (2617079)Instruction limit reached!
% 55.21/8.48 % (2617079)------------------------------
% 55.21/8.48 % (2617079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617079)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617079)Termination reason: Instruction limit
% 55.21/8.48 % (2617079)Termination phase: Property scanning
% 55.21/8.48 % (2617079)Time elapsed: 0.246 s
% 55.21/8.48 % (2617079)Peak memory usage: 32 MB
% 55.21/8.48 % (2617079)Instructions burned: 479 (million)
% 55.21/8.48 % (2617085)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3974470099:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 55.21/8.48 % (2617086)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=800462013:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 55.21/8.48 % (2617083)Instruction limit reached!
% 55.21/8.48 % (2617083)------------------------------
% 55.21/8.48 % (2617083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.21/8.48 % (2617083)CaDiCaL version: 2.1.3
% 55.21/8.48 % (2617083)Termination reason: Instruction limit
% 55.21/8.48 % (2617083)Termination phase: Saturation
% 55.21/8.48 % (2617083)Time elapsed: 0.324 s
% 55.21/8.48 % (2617083)Peak memory usage: 42 MB
% 55.21/8.48 % (2617083)Instructions burned: 1180 (million)
% 55.21/8.48 % (2617089)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3010764890:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 55.21/8.48 % (2617081)Instruction limit reached!
% 55.21/8.48 % (2617081)------------------------------
% 55.21/8.48 % (2617081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.21/8.48 % (2617081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617081)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617081)Termination reason: Instruction limit
% 122.59/17.98 % (2617081)Termination phase: Finite model building preprocessing
% 122.59/17.98 % (2617081)Time elapsed: 0.381 s
% 122.59/17.98 % (2617081)Peak memory usage: 37 MB
% 122.59/17.98 % (2617081)Instructions burned: 866 (million)
% 122.59/17.98 % (2617091)fmb+10_1_sil=64000:random_seed=3870287790:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 122.59/17.98 % (2617086)Instruction limit reached!
% 122.59/17.98 % (2617086)------------------------------
% 122.59/17.98 % (2617086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617086)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617086)Termination reason: Instruction limit
% 122.59/17.98 % (2617086)Termination phase: Saturation
% 122.59/17.98 % (2617086)Time elapsed: 0.344 s
% 122.59/17.98 % (2617086)Peak memory usage: 34 MB
% 122.59/17.98 % (2617086)Instructions burned: 692 (million)
% 122.59/17.98 % (2617093)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2946120322:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 122.59/17.98 % (2617089)Instruction limit reached!
% 122.59/17.98 % (2617089)------------------------------
% 122.59/17.98 % (2617089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617089)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617089)Termination reason: Instruction limit
% 122.59/17.98 % (2617089)Termination phase: Saturation
% 122.59/17.98 % (2617089)Time elapsed: 0.232 s
% 122.59/17.98 % (2617089)Peak memory usage: 37 MB
% 122.59/17.98 % (2617089)Instructions burned: 879 (million)
% 122.59/17.98 % (2617095)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2927943594:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 122.59/17.98 % (2617085)Instruction limit reached!
% 122.59/17.98 % (2617085)------------------------------
% 122.59/17.98 % (2617085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617085)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617085)Termination reason: Instruction limit
% 122.59/17.98 % (2617085)Termination phase: Finite model building preprocessing
% 122.59/17.98 % (2617085)Time elapsed: 0.402 s
% 122.59/17.98 % (2617085)Peak memory usage: 37 MB
% 122.59/17.98 % (2617085)Instructions burned: 889 (million)
% 122.59/17.98 % (2617097)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4281164755:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 122.59/17.98 % (2617095)Instruction limit reached!
% 122.59/17.98 % (2617095)------------------------------
% 122.59/17.98 % (2617095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617095)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617095)Termination reason: Instruction limit
% 122.59/17.98 % (2617095)Termination phase: Finite model building preprocessing
% 122.59/17.98 % (2617095)Time elapsed: 0.229 s
% 122.59/17.98 % (2617095)Peak memory usage: 38 MB
% 122.59/17.98 % (2617095)Instructions burned: 922 (million)
% 122.59/17.98 % (2617099)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3508599213:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 122.59/17.98 % (2617099)Instruction limit reached!
% 122.59/17.98 % (2617099)------------------------------
% 122.59/17.98 % (2617099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617099)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617099)Termination reason: Instruction limit
% 122.59/17.98 % (2617099)Termination phase: Saturation
% 122.59/17.98 % (2617099)Time elapsed: 0.384 s
% 122.59/17.98 % (2617099)Peak memory usage: 38 MB
% 122.59/17.98 % (2617099)Instructions burned: 1473 (million)
% 122.59/17.98 % (2617101)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3835421141:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 122.59/17.98 % (2617101)Instruction limit reached!
% 122.59/17.98 % (2617101)------------------------------
% 122.59/17.98 % (2617101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.59/17.98 % (2617101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.59/17.98 % (2617101)CaDiCaL version: 2.1.3
% 122.59/17.98 % (2617101)Termination reason: Instruction limit
% 226.40/32.67 % (2617101)Termination phase: Finite model building preprocessing
% 226.40/32.67 % (2617101)Time elapsed: 1.745 s
% 226.40/32.67 % (2617101)Peak memory usage: 72 MB
% 226.40/32.67 % (2617101)Instructions burned: 6326 (million)
% 226.40/32.67 % (2617103)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2925279335:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 226.40/32.67 % (2617103)Instruction limit reached!
% 226.40/32.67 % (2617103)------------------------------
% 226.40/32.67 % (2617103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617103)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617103)Termination reason: Instruction limit
% 226.40/32.67 % (2617103)Termination phase: Finite model building preprocessing
% 226.40/32.67 % (2617103)Time elapsed: 0.425 s
% 226.40/32.67 % (2617103)Peak memory usage: 50 MB
% 226.40/32.67 % (2617103)Instructions burned: 2182 (million)
% 226.40/32.67 % (2617105)ott-2_1_sil=16000:newcnf=on:random_seed=2298587828:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2960 on theBenchmark for (2960ds/869Mi)
% 226.40/32.67 % (2617097)Instruction limit reached!
% 226.40/32.67 % (2617097)------------------------------
% 226.40/32.67 % (2617097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617097)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617097)Termination reason: Instruction limit
% 226.40/32.67 % (2617097)Termination phase: Saturation
% 226.40/32.67 % (2617097)Time elapsed: 2.907 s
% 226.40/32.67 % (2617097)Peak memory usage: 75 MB
% 226.40/32.67 % (2617097)Instructions burned: 5131 (million)
% 226.40/32.67 % (2617107)ott+10_1_sil=32000:tgt=ground:random_seed=3234347899:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi)
% 226.40/32.67 % (2617105)Instruction limit reached!
% 226.40/32.67 % (2617105)------------------------------
% 226.40/32.67 % (2617105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617105)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617105)Termination reason: Instruction limit
% 226.40/32.67 % (2617105)Termination phase: Saturation
% 226.40/32.67 % (2617105)Time elapsed: 0.227 s
% 226.40/32.67 % (2617105)Peak memory usage: 36 MB
% 226.40/32.67 % (2617105)Instructions burned: 869 (million)
% 226.40/32.67 % (2617109)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2208085101:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 226.40/32.67 % (2617093)Instruction limit reached!
% 226.40/32.67 % (2617093)------------------------------
% 226.40/32.67 % (2617093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617093)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617093)Termination reason: Instruction limit
% 226.40/32.67 % (2617093)Termination phase: Finite model building preprocessing
% 226.40/32.67 % (2617093)Time elapsed: 5.024 s
% 226.40/32.67 % (2617093)Peak memory usage: 74 MB
% 226.40/32.67 % (2617093)Instructions burned: 9516 (million)
% 226.40/32.67 % (2617111)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3385756864:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi)
% 226.40/32.67 % (2617107)Instruction limit reached!
% 226.40/32.67 % (2617107)------------------------------
% 226.40/32.67 % (2617107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617107)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617107)Termination reason: Instruction limit
% 226.40/32.67 % (2617107)Termination phase: Saturation
% 226.40/32.67 % (2617107)Time elapsed: 2.989 s
% 226.40/32.67 % (2617107)Peak memory usage: 92 MB
% 226.40/32.67 % (2617107)Instructions burned: 5114 (million)
% 226.40/32.67 % (2617113)dis+21_1_sil=32000:sas=cadical:random_seed=4134389686:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 226.40/32.67 % (2617111)Instruction limit reached!
% 226.40/32.67 % (2617111)------------------------------
% 226.40/32.67 % (2617111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.40/32.67 % (2617111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.40/32.67 % (2617111)CaDiCaL version: 2.1.3
% 226.40/32.67 % (2617111)Termination reason: Instruction limit
% 226.40/32.67 % (2617111)Termination phase: Saturation
% 226.40/32.67 % (2617111)Time elapsed: 1.903 s
% 206.38/39.13 % (2617111)Peak memory usage: 60 MB
% 206.38/39.13 % (2617111)Instructions burned: 3512 (million)
% 206.38/39.13 % (2617115)ott+11_1_sil=16000:gs=on:random_seed=340083834:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2919 on theBenchmark for (2919ds/2251Mi)
% 206.38/39.13 % (2617113)Instruction limit reached!
% 206.38/39.13 % (2617113)------------------------------
% 206.38/39.13 % (2617113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.13 % (2617113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.13 % (2617113)CaDiCaL version: 2.1.3
% 206.38/39.13 % (2617113)Termination reason: Instruction limit
% 206.38/39.13 % (2617113)Termination phase: Saturation
% 206.38/39.13 % (2617113)Time elapsed: 2.030 s
% 206.38/39.13 % (2617113)Peak memory usage: 69 MB
% 206.38/39.13 % (2617113)Instructions burned: 3775 (million)
% 206.38/39.13 % (2617117)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1797874418:fmbsr=1.6:i=67534_2908 on theBenchmark for (2908ds/67534Mi)
% 206.38/39.13 % (2617115)Instruction limit reached!
% 206.38/39.13 % (2617115)------------------------------
% 206.38/39.13 % (2617115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617115)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617115)Termination reason: Instruction limit
% 206.38/39.14 % (2617115)Termination phase: Saturation
% 206.38/39.14 % (2617115)Time elapsed: 1.098 s
% 206.38/39.14 % (2617115)Peak memory usage: 49 MB
% 206.38/39.14 % (2617115)Instructions burned: 2252 (million)
% 206.38/39.14 % (2617119)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3749216333:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2908 on theBenchmark for (2908ds/4591Mi)
% 206.38/39.14 % (2617119)Instruction limit reached!
% 206.38/39.14 % (2617119)------------------------------
% 206.38/39.14 % (2617119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617119)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617119)Termination reason: Instruction limit
% 206.38/39.14 % (2617119)Termination phase: Saturation
% 206.38/39.14 % (2617119)Time elapsed: 2.712 s
% 206.38/39.14 % (2617119)Peak memory usage: 108 MB
% 206.38/39.14 % (2617119)Instructions burned: 4592 (million)
% 206.38/39.14 % (2617121)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=689688682:i=29340_2880 on theBenchmark for (2880ds/29340Mi)
% 206.38/39.14 % (2617091)Instruction limit reached!
% 206.38/39.14 % (2617091)------------------------------
% 206.38/39.14 % (2617091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617091)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617091)Termination reason: Instruction limit
% 206.38/39.14 % (2617091)Termination phase: Finite model building preprocessing
% 206.38/39.14 % (2617091)Time elapsed: 11.919 s
% 206.38/39.14 % (2617091)Peak memory usage: 89 MB
% 206.38/39.14 % (2617091)Instructions burned: 22062 (million)
% 206.38/39.14 % (2617123)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=668338702:i=5211_2871 on theBenchmark for (2871ds/5211Mi)
% 206.38/39.14 % (2617123)Instruction limit reached!
% 206.38/39.14 % (2617123)------------------------------
% 206.38/39.14 % (2617123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617123)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617123)Termination reason: Instruction limit
% 206.38/39.14 % (2617123)Termination phase: Saturation
% 206.38/39.14 % (2617123)Time elapsed: 1.749 s
% 206.38/39.14 % (2617123)Peak memory usage: 53 MB
% 206.38/39.14 % (2617123)Instructions burned: 5212 (million)
% 206.38/39.14 % (2617125)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4074383517:i=5497:nm=2_2853 on theBenchmark for (2853ds/5497Mi)
% 206.38/39.14 % (2617125)Instruction limit reached!
% 206.38/39.14 % (2617125)------------------------------
% 206.38/39.14 % (2617125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617125)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617125)Termination reason: Instruction limit
% 206.38/39.14 % (2617125)Termination phase: Finite model building preprocessing
% 206.38/39.14 % (2617125)Time elapsed: 2.900 s
% 206.38/39.14 % (2617125)Peak memory usage: 67 MB
% 206.38/39.14 % (2617125)Instructions burned: 5498 (million)
% 206.38/39.14 % (2617127)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=362346292:fmbsr=2:i=46332_2824 on theBenchmark for (2824ds/46332Mi)
% 206.38/39.14 % (2617109)Instruction limit reached!
% 206.38/39.14 % (2617109)------------------------------
% 206.38/39.14 % (2617109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617109)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617109)Termination reason: Instruction limit
% 206.38/39.14 % (2617109)Termination phase: Finite model building preprocessing
% 206.38/39.14 % (2617109)Time elapsed: 15.808 s
% 206.38/39.14 % (2617109)Peak memory usage: 148 MB
% 206.38/39.14 % (2617109)Instructions burned: 54284 (million)
% 206.38/39.14 % (2617129)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3295259669:i=14071_2799 on theBenchmark for (2799ds/14071Mi)
% 206.38/39.14 % (2617129)Instruction limit reached!
% 206.38/39.14 % (2617129)------------------------------
% 206.38/39.14 % (2617129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617129)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617129)Termination reason: Instruction limit
% 206.38/39.14 % (2617129)Termination phase: Finite model building preprocessing
% 206.38/39.14 % (2617129)Time elapsed: 3.991 s
% 206.38/39.14 % (2617129)Peak memory usage: 82 MB
% 206.38/39.14 % (2617129)Instructions burned: 14072 (million)
% 206.38/39.14 % (2617131)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4194274483:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi)
% 206.38/39.14 % (2617121)Instruction limit reached!
% 206.38/39.14 % (2617121)------------------------------
% 206.38/39.14 % (2617121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617121)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617121)Termination reason: Instruction limit
% 206.38/39.14 % (2617121)Termination phase: Saturation
% 206.38/39.14 % (2617121)Time elapsed: 14.860 s
% 206.38/39.14 % (2617121)Peak memory usage: 734 MB
% 206.38/39.14 % (2617121)Instructions burned: 29341 (million)
% 206.38/39.14 % (2617133)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=963038611:i=8173:av=off_2731 on theBenchmark for (2731ds/8173Mi)
% 206.38/39.14 % (2617131)Instruction limit reached!
% 206.38/39.14 % (2617131)------------------------------
% 206.38/39.14 % (2617131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617131)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617131)Termination reason: Instruction limit
% 206.38/39.14 % (2617131)Termination phase: Saturation
% 206.38/39.14 % (2617131)Time elapsed: 5.530 s
% 206.38/39.14 % (2617131)Peak memory usage: 209 MB
% 206.38/39.14 % (2617131)Instructions burned: 22574 (million)
% 206.38/39.14 % (2617135)dis+10_16:1_sil=16000:random_seed=3970792047:i=9155:fsr=off_2704 on theBenchmark for (2704ds/9155Mi)
% 206.38/39.14 % (2617133)Instruction limit reached!
% 206.38/39.14 % (2617133)------------------------------
% 206.38/39.14 % (2617133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617133)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617133)Termination reason: Instruction limit
% 206.38/39.14 % (2617133)Termination phase: Saturation
% 206.38/39.14 % (2617133)Time elapsed: 4.755 s
% 206.38/39.14 % (2617133)Peak memory usage: 222 MB
% 206.38/39.14 % (2617133)Instructions burned: 8175 (million)
% 206.38/39.14 % (2617137)ott-3_8_sil=64000:random_seed=2192066315:i=20139:bs=on_2683 on theBenchmark for (2683ds/20139Mi)
% 206.38/39.14 % (2617135)Instruction limit reached!
% 206.38/39.14 % (2617135)------------------------------
% 206.38/39.14 % (2617135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617135)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617135)Termination reason: Instruction limit
% 206.38/39.14 % (2617135)Termination phase: Saturation
% 206.38/39.14 % (2617135)Time elapsed: 2.627 s
% 206.38/39.14 % (2617135)Peak memory usage: 101 MB
% 206.38/39.14 % (2617135)Instructions burned: 9156 (million)
% 206.38/39.14 % (2617139)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1456467964:fmbsr=2:i=32576_2677 on theBenchmark for (2677ds/32576Mi)
% 206.38/39.14 % (2617059)Instruction limit reached!
% 206.38/39.14 % (2617059)------------------------------
% 206.38/39.14 % (2617059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617059)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617059)Termination reason: Instruction limit
% 206.38/39.14 % (2617059)Termination phase: Saturation
% 206.38/39.14 % (2617059)Time elapsed: 37.162 s
% 206.38/39.14 % (2617059)Peak memory usage: 309 MB
% 206.38/39.14 % (2617059)Instructions burned: 88025 (million)
% 206.38/39.14 % (2617141)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2203414257:i=11404_2625 on theBenchmark for (2625ds/11404Mi)
% 206.38/39.14 % (2617058) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2617052-2617058"...
% 206.38/39.14 % (2617058)...printing done.
% 206.38/39.14 % (2617058)Refutation found. Thanks to Tanya!
% 206.38/39.14 % SZS status Theorem for theBenchmark
% 206.38/39.14 % SZS output start Proof for theBenchmark
% See solution above
% 206.38/39.14 % (2617058)------------------------------
% 206.38/39.14 % (2617058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 206.38/39.14 % (2617058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.38/39.14 % (2617058)CaDiCaL version: 2.1.3
% 206.38/39.14 % (2617058)Termination reason: Refutation
% 206.38/39.14 % (2617058)Time elapsed: 38.368 s
% 206.38/39.14 % (2617058)Peak memory usage: 376 MB
% 206.38/39.14 % (2617058)Instructions burned: 71659 (million)
% 206.38/39.14 % (2617052)Success in time 38.702 s
% 206.38/39.14 % Vampire exiting
%------------------------------------------------------------------------------