%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEO088+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 09:53:33 AM UTC 2026
% Result : Theorem 181.23s 31.72s
% Output : Refutation 181.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 5
% Syntax : Number of formulae : 73 ( 16 unt; 2 def)
% Number of atoms : 252 ( 0 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 277 ( 98 ~; 115 |; 53 &)
% ( 7 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 97 ( 0 sgn 83 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( part_of(X1,X0)
<=> ! [X2] :
( incident_c(X2,X1)
=> incident_c(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',part_of_defn) ).
fof(f3,axiom,
! [X0,X1] :
( end_point(X0,X1)
<=> ( incident_c(X0,X1)
& ! [X2,X3] :
( ( part_of(X2,X1)
& part_of(X3,X1)
& incident_c(X0,X2)
& incident_c(X0,X3) )
=> ( part_of(X2,X3)
| part_of(X3,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax',end_point_defn) ).
fof(f17,conjecture,
! [X0,X1,X2] :
( ( part_of(X1,X0)
& end_point(X2,X0)
& incident_c(X2,X1) )
=> end_point(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_2_10) ).
fof(f18,negated_conjecture,
~ ! [X0,X1,X2] :
( ( part_of(X1,X0)
& end_point(X2,X0)
& incident_c(X2,X1) )
=> end_point(X2,X1) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f21,plain,
! [X0,X1] :
( part_of(X1,X0)
<=> ! [X2] :
( incident_c(X2,X0)
| ~ incident_c(X2,X1) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f22,plain,
! [X0,X1] :
( end_point(X0,X1)
<=> ( incident_c(X0,X1)
& ! [X2,X3] :
( part_of(X2,X3)
| part_of(X3,X2)
| ~ part_of(X2,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X3) ) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f23,plain,
! [X0,X1] :
( end_point(X0,X1)
<=> ( incident_c(X0,X1)
& ! [X2,X3] :
( part_of(X2,X3)
| part_of(X3,X2)
| ~ part_of(X2,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X3) ) ) ),
inference(flattening,[],[f22]) ).
fof(f40,plain,
? [X0,X1,X2] :
( ~ end_point(X2,X1)
& part_of(X1,X0)
& end_point(X2,X0)
& incident_c(X2,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f41,plain,
? [X0,X1,X2] :
( ~ end_point(X2,X1)
& part_of(X1,X0)
& end_point(X2,X0)
& incident_c(X2,X1) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( ( part_of(X1,X0)
| ? [X2] :
( ~ incident_c(X2,X0)
& incident_c(X2,X1) ) )
& ( ! [X2] :
( incident_c(X2,X0)
| ~ incident_c(X2,X1) )
| ~ part_of(X1,X0) ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f43,plain,
! [X0,X1] :
( ( part_of(X1,X0)
| ? [X2] :
( ~ incident_c(X2,X0)
& incident_c(X2,X1) ) )
& ( ! [X3] :
( incident_c(X3,X0)
| ~ incident_c(X3,X1) )
| ~ part_of(X1,X0) ) ),
inference(rectify,[],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( ( part_of(X1,X0)
| ( ~ incident_c(sK0(X0,X1),X0)
& incident_c(sK0(X0,X1),X1) ) )
& ( ! [X3] :
( incident_c(X3,X0)
| ~ incident_c(X3,X1) )
| ~ part_of(X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f43]) ).
fof(f49,plain,
! [X0,X1] :
( ( end_point(X0,X1)
| ~ incident_c(X0,X1)
| ? [X2,X3] :
( ~ part_of(X2,X3)
& ~ part_of(X3,X2)
& part_of(X2,X1)
& part_of(X3,X1)
& incident_c(X0,X2)
& incident_c(X0,X3) ) )
& ( ( incident_c(X0,X1)
& ! [X2,X3] :
( part_of(X2,X3)
| part_of(X3,X2)
| ~ part_of(X2,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X3) ) )
| ~ end_point(X0,X1) ) ),
inference(nnf_transformation,[],[f23]) ).
fof(f50,plain,
! [X0,X1] :
( ( end_point(X0,X1)
| ~ incident_c(X0,X1)
| ? [X2,X3] :
( ~ part_of(X2,X3)
& ~ part_of(X3,X2)
& part_of(X2,X1)
& part_of(X3,X1)
& incident_c(X0,X2)
& incident_c(X0,X3) ) )
& ( ( incident_c(X0,X1)
& ! [X2,X3] :
( part_of(X2,X3)
| part_of(X3,X2)
| ~ part_of(X2,X1)
| ~ part_of(X3,X1)
| ~ incident_c(X0,X2)
| ~ incident_c(X0,X3) ) )
| ~ end_point(X0,X1) ) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( ( end_point(X0,X1)
| ~ incident_c(X0,X1)
| ? [X2,X3] :
( ~ part_of(X2,X3)
& ~ part_of(X3,X2)
& part_of(X2,X1)
& part_of(X3,X1)
& incident_c(X0,X2)
& incident_c(X0,X3) ) )
& ( ( incident_c(X0,X1)
& ! [X4,X5] :
( part_of(X4,X5)
| part_of(X5,X4)
| ~ part_of(X4,X1)
| ~ part_of(X5,X1)
| ~ incident_c(X0,X4)
| ~ incident_c(X0,X5) ) )
| ~ end_point(X0,X1) ) ),
inference(rectify,[],[f50]) ).
fof(f52,plain,
! [X0,X1] :
( ( end_point(X0,X1)
| ~ incident_c(X0,X1)
| ( ~ part_of(sK2(X0,X1),sK3(X0,X1))
& ~ part_of(sK3(X0,X1),sK2(X0,X1))
& part_of(sK2(X0,X1),X1)
& part_of(sK3(X0,X1),X1)
& incident_c(X0,sK2(X0,X1))
& incident_c(X0,sK3(X0,X1)) ) )
& ( ( incident_c(X0,X1)
& ! [X4,X5] :
( part_of(X4,X5)
| part_of(X5,X4)
| ~ part_of(X4,X1)
| ~ part_of(X5,X1)
| ~ incident_c(X0,X4)
| ~ incident_c(X0,X5) ) )
| ~ end_point(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X2,sK2(X0,X1)),skolemize(X3,sK3(X0,X1))],[f51]) ).
fof(f68,plain,
( ~ end_point(sK15,sK14)
& part_of(sK14,sK13)
& end_point(sK15,sK13)
& incident_c(sK15,sK14) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15)],[f41]) ).
fof(f69,plain,
! [X3,X0,X1] :
( ~ part_of(X1,X0)
| ~ incident_c(X3,X1)
| incident_c(X3,X0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f70,plain,
! [X0,X1] :
( incident_c(sK0(X0,X1),X1)
| part_of(X1,X0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f71,plain,
! [X0,X1] :
( ~ incident_c(sK0(X0,X1),X0)
| part_of(X1,X0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f78,plain,
! [X0,X1,X4,X5] :
( ~ end_point(X0,X1)
| part_of(X5,X4)
| ~ part_of(X4,X1)
| ~ part_of(X5,X1)
| ~ incident_c(X0,X4)
| ~ incident_c(X0,X5)
| part_of(X4,X5) ),
inference(cnf_transformation,[],[f52]) ).
fof(f80,plain,
! [X0,X1] :
( ~ incident_c(X0,X1)
| end_point(X0,X1)
| incident_c(X0,sK3(X0,X1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f81,plain,
! [X0,X1] :
( ~ incident_c(X0,X1)
| end_point(X0,X1)
| incident_c(X0,sK2(X0,X1)) ),
inference(cnf_transformation,[],[f52]) ).
fof(f82,plain,
! [X0,X1] :
( ~ incident_c(X0,X1)
| end_point(X0,X1)
| part_of(sK3(X0,X1),X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f83,plain,
! [X0,X1] :
( ~ incident_c(X0,X1)
| end_point(X0,X1)
| part_of(sK2(X0,X1),X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f84,plain,
! [X0,X1] :
( ~ part_of(sK3(X0,X1),sK2(X0,X1))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f85,plain,
! [X0,X1] :
( ~ part_of(sK2(X0,X1),sK3(X0,X1))
| ~ incident_c(X0,X1)
| end_point(X0,X1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f110,plain,
incident_c(sK15,sK14),
inference(cnf_transformation,[],[f68]) ).
fof(f111,plain,
end_point(sK15,sK13),
inference(cnf_transformation,[],[f68]) ).
fof(f112,plain,
part_of(sK14,sK13),
inference(cnf_transformation,[],[f68]) ).
fof(f113,plain,
~ end_point(sK15,sK14),
inference(cnf_transformation,[],[f68]) ).
fof(f234,plain,
! [X0] :
( ~ incident_c(X0,sK14)
| incident_c(X0,sK13) ),
inference(resolution,[],[f69,f112]) ).
fof(f436,plain,
( end_point(sK15,sK14)
| incident_c(sK15,sK3(sK15,sK14)) ),
inference(resolution,[],[f80,f110]) ).
fof(f454,plain,
incident_c(sK15,sK3(sK15,sK14)),
inference(forward_subsumption_resolution,[],[f436,f113]) ).
fof(f562,plain,
( end_point(sK15,sK14)
| incident_c(sK15,sK2(sK15,sK14)) ),
inference(resolution,[],[f81,f110]) ).
fof(f563,plain,
incident_c(sK15,sK2(sK15,sK14)),
inference(forward_subsumption_resolution,[],[f562,f113]) ).
fof(f713,plain,
( end_point(sK15,sK14)
| part_of(sK3(sK15,sK14),sK14) ),
inference(resolution,[],[f82,f110]) ).
fof(f714,plain,
part_of(sK3(sK15,sK14),sK14),
inference(forward_subsumption_resolution,[],[f713,f113]) ).
fof(f716,plain,
! [X0] :
( ~ incident_c(X0,sK3(sK15,sK14))
| incident_c(X0,sK14) ),
inference(resolution,[],[f714,f69]) ).
fof(f718,plain,
! [X0] :
( incident_c(sK0(X0,sK3(sK15,sK14)),sK14)
| part_of(sK3(sK15,sK14),X0) ),
inference(resolution,[],[f716,f70]) ).
fof(f889,plain,
( end_point(sK15,sK14)
| part_of(sK2(sK15,sK14),sK14) ),
inference(resolution,[],[f83,f110]) ).
fof(f890,plain,
part_of(sK2(sK15,sK14),sK14),
inference(forward_subsumption_resolution,[],[f889,f113]) ).
fof(f911,plain,
! [X0] :
( ~ incident_c(X0,sK2(sK15,sK14))
| incident_c(X0,sK14) ),
inference(resolution,[],[f890,f69]) ).
fof(f922,plain,
! [X0] :
( incident_c(sK0(X0,sK2(sK15,sK14)),sK14)
| part_of(sK2(sK15,sK14),X0) ),
inference(resolution,[],[f911,f70]) ).
fof(f3616,plain,
! [X0,X1] :
( ~ incident_c(sK15,X0)
| ~ part_of(X1,sK13)
| ~ part_of(X0,sK13)
| ~ incident_c(sK15,X1)
| part_of(X0,X1)
| part_of(X1,X0) ),
inference(resolution,[],[f78,f111]) ).
fof(f4956,plain,
! [X0] :
( ~ part_of(X0,sK13)
| ~ part_of(sK2(sK15,sK14),sK13)
| ~ incident_c(sK15,X0)
| part_of(sK2(sK15,sK14),X0)
| part_of(X0,sK2(sK15,sK14)) ),
inference(resolution,[],[f3616,f563]) ).
fof(f8477,plain,
! [X0] :
( incident_c(sK0(X0,sK3(sK15,sK14)),sK13)
| part_of(sK3(sK15,sK14),X0) ),
inference(resolution,[],[f718,f234]) ).
fof(f8491,plain,
! [X0] :
( incident_c(sK0(X0,sK2(sK15,sK14)),sK13)
| part_of(sK2(sK15,sK14),X0) ),
inference(resolution,[],[f922,f234]) ).
fof(f11739,plain,
( part_of(sK3(sK15,sK14),sK13)
| part_of(sK3(sK15,sK14),sK13) ),
inference(resolution,[],[f8477,f71]) ).
fof(f11753,plain,
part_of(sK3(sK15,sK14),sK13),
inference(duplicate_literal_removal,[],[f11739]) ).
fof(f11781,plain,
( part_of(sK2(sK15,sK14),sK13)
| part_of(sK2(sK15,sK14),sK13) ),
inference(resolution,[],[f8491,f71]) ).
fof(f11795,plain,
part_of(sK2(sK15,sK14),sK13),
inference(duplicate_literal_removal,[],[f11781]) ).
fof(f34692,plain,
! [X0] :
( ~ incident_c(sK15,X0)
| ~ part_of(X0,sK13)
| part_of(sK2(sK15,sK14),X0)
| part_of(X0,sK2(sK15,sK14)) ),
inference(forward_subsumption_resolution,[],[f4956,f11795]) ).
fof(f35418,plain,
( ~ part_of(sK3(sK15,sK14),sK13)
| part_of(sK2(sK15,sK14),sK3(sK15,sK14))
| part_of(sK3(sK15,sK14),sK2(sK15,sK14)) ),
inference(resolution,[],[f34692,f454]) ).
fof(f35430,plain,
( part_of(sK2(sK15,sK14),sK3(sK15,sK14))
| part_of(sK3(sK15,sK14),sK2(sK15,sK14)) ),
inference(forward_subsumption_resolution,[],[f35418,f11753]) ).
fof(f191929,definition,
( spl16_286
<=> part_of(sK3(sK15,sK14),sK2(sK15,sK14)) ),
introduced(definition,[new_symbols(definition,[spl16_286])],[avatar_definition]) ).
fof(f191931,plain,
( part_of(sK3(sK15,sK14),sK2(sK15,sK14))
| ~ spl16_286 ),
inference(avatar_component_clause,[],[f191929]) ).
fof(f191933,definition,
( spl16_287
<=> part_of(sK2(sK15,sK14),sK3(sK15,sK14)) ),
introduced(definition,[new_symbols(definition,[spl16_287])],[avatar_definition]) ).
fof(f191935,plain,
( part_of(sK2(sK15,sK14),sK3(sK15,sK14))
| ~ spl16_287 ),
inference(avatar_component_clause,[],[f191933]) ).
fof(f191936,plain,
( spl16_286
| spl16_287 ),
inference(avatar_split_clause,[],[f35430,f191933,f191929]) ).
fof(f191937,plain,
( ~ incident_c(sK15,sK14)
| end_point(sK15,sK14)
| ~ spl16_286 ),
inference(resolution,[],[f191931,f84]) ).
fof(f191940,plain,
( end_point(sK15,sK14)
| ~ spl16_286 ),
inference(forward_subsumption_resolution,[],[f191937,f110]) ).
fof(f191941,plain,
( $false
| ~ spl16_286 ),
inference(forward_subsumption_resolution,[],[f191940,f113]) ).
fof(f191942,plain,
~ spl16_286,
inference(avatar_contradiction_clause,[],[f191941]) ).
fof(f191945,plain,
( ~ incident_c(sK15,sK14)
| end_point(sK15,sK14)
| ~ spl16_287 ),
inference(resolution,[],[f191935,f85]) ).
fof(f191948,plain,
( end_point(sK15,sK14)
| ~ spl16_287 ),
inference(forward_subsumption_resolution,[],[f191945,f110]) ).
fof(f191949,plain,
( $false
| ~ spl16_287 ),
inference(forward_subsumption_resolution,[],[f191948,f113]) ).
fof(f191950,plain,
~ spl16_287,
inference(avatar_contradiction_clause,[],[f191949]) ).
cnf(s226,plain,
( spl16_286
| spl16_287 ),
inference(sat_conversion,[],[f191936]) ).
cnf(s227,plain,
~ spl16_286,
inference(sat_conversion,[],[f191942]) ).
cnf(s228,plain,
~ spl16_287,
inference(sat_conversion,[],[f191950]) ).
cnf(s229,plain,
$false,
inference(rat,[],[s226,s228,s227]) ).
fof(f191951,plain,
$false,
inference(avatar_sat_refutation,[],[s229]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO088+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.05/0.32 % Computer : n012.cluster.edu
% 0.05/0.32 % Model : x86_64 x86_64
% 0.05/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.32 % Memory : 8046.5625MB
% 0.05/0.32 % OS : Linux 6.8.0-71-generic
% 0.05/0.32 % CPULimit : 300
% 0.05/0.32 % WCLimit : 300
% 0.05/0.32 % DateTime : Sun Sep 27 06:54:21 UTC 2026
% 0.02/0.32 % CPUTime :
% 0.02/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.02/0.34 Running first-order model finding
% 0.02/0.34 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
% 8.94/1.78 % (2021298)Will run a generic schedule for satisfiability detection.
% 8.94/1.78 % (2021304)% WARNING: option uhcvi not known.
% 8.94/1.78 % (2021305)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=414529597:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.94/1.78 % (2021306)dis+10_1_sil=32000:sp=arity:random_seed=2559547626:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.94/1.78 % (2021303)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3927888995_2999 on theBenchmark for (2999ds/0Mi)
% 8.94/1.78 % (2021304)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=377714578:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.94/1.78 % (2021307)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1840867853:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.94/1.78 % (2021308)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1623545712:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.94/1.78 % (2021309)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2416861073:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.94/1.78 % TRYING [1]
% 8.94/1.78 % TRYING [2]
% 8.94/1.78 % TRYING [3]
% 8.94/1.78 % TRYING [4]
% 8.94/1.78 % TRYING [5]
% 8.94/1.78 % (2021307)Instruction limit reached!
% 8.94/1.78 % (2021307)------------------------------
% 8.94/1.78 % (2021307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.94/1.78 % (2021307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/1.78 % (2021307)CaDiCaL version: 2.1.3
% 8.94/1.78 % (2021307)Termination reason: Instruction limit
% 8.94/1.78 % (2021307)Termination phase: Saturation
% 8.94/1.78 % (2021307)Time elapsed: 0.029 s
% 8.94/1.78 % (2021307)Peak memory usage: 12 MB
% 8.94/1.78 % (2021307)Instructions burned: 119 (million)
% 8.94/1.78 % (2021306)Instruction limit reached!
% 8.94/1.78 % (2021306)------------------------------
% 8.94/1.78 % (2021306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.94/1.78 % (2021306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/1.78 % (2021306)CaDiCaL version: 2.1.3
% 8.94/1.78 % (2021306)Termination reason: Instruction limit
% 8.94/1.78 % (2021306)Termination phase: Saturation
% 8.94/1.78 % (2021306)Time elapsed: 0.034 s
% 8.94/1.78 % (2021306)Peak memory usage: 12 MB
% 8.94/1.78 % (2021306)Instructions burned: 107 (million)
% 8.94/1.78 % (2021317)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1088279172:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.94/1.78 % (2021308)Instruction limit reached!
% 8.94/1.78 % (2021308)------------------------------
% 8.94/1.78 % (2021308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.94/1.78 % (2021308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/1.78 % (2021308)CaDiCaL version: 2.1.3
% 8.94/1.78 % (2021308)Termination reason: Instruction limit
% 8.94/1.78 % (2021308)Termination phase: Saturation
% 8.94/1.78 % (2021308)Time elapsed: 0.043 s
% 8.94/1.78 % (2021308)Peak memory usage: 13 MB
% 8.94/1.78 % (2021308)Instructions burned: 131 (million)
% 8.94/1.78 % TRYING [1]
% 8.94/1.78 % TRYING [2]
% 8.94/1.78 % TRYING [3]
% 8.94/1.78 % (2021318)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=352491451:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.94/1.78 % (2021309)Instruction limit reached!
% 8.94/1.78 % (2021309)------------------------------
% 8.94/1.78 % (2021309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.94/1.78 % (2021309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/1.78 % (2021309)CaDiCaL version: 2.1.3
% 8.94/1.78 % (2021309)Termination reason: Instruction limit
% 8.94/1.78 % (2021309)Termination phase: Saturation
% 8.94/1.78 % (2021309)Time elapsed: 0.045 s
% 8.94/1.78 % (2021309)Peak memory usage: 13 MB
% 8.94/1.78 % (2021309)Instructions burned: 160 (million)
% 8.94/1.78 % TRYING [4]
% 8.94/1.78 % (2021320)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=354586822:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 8.94/1.78 % (2021322)ott-21_1_sil=16000:fs=off:random_seed=3517471339:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 8.94/1.78 % TRYING [5]
% 8.94/1.78 % TRYING [6]
% 8.94/1.78 % (2021318)Instruction limit reached!
% 8.94/1.78 % (2021318)------------------------------
% 8.94/1.78 % (2021318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021318)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021318)Termination reason: Instruction limit
% 29.86/4.63 % (2021318)Termination phase: Saturation
% 29.86/4.63 % (2021318)Time elapsed: 0.045 s
% 29.86/4.63 % (2021318)Peak memory usage: 13 MB
% 29.86/4.63 % (2021318)Instructions burned: 133 (million)
% 29.86/4.63 % (2021325)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1158311906:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 29.86/4.63 % (2021322)Instruction limit reached!
% 29.86/4.63 % (2021322)------------------------------
% 29.86/4.63 % (2021322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021322)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021322)Termination reason: Instruction limit
% 29.86/4.63 % (2021322)Termination phase: Saturation
% 29.86/4.63 % (2021322)Time elapsed: 0.054 s
% 29.86/4.63 % (2021322)Peak memory usage: 13 MB
% 29.86/4.63 % (2021322)Instructions burned: 182 (million)
% 29.86/4.63 % (2021327)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1907807753:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 29.86/4.63 % TRYING [1]
% 29.86/4.63 % TRYING [2]
% 29.86/4.63 % TRYING [3]
% 29.86/4.63 % TRYING [4]
% 29.86/4.63 % TRYING [5]
% 29.86/4.63 % TRYING [7]
% 29.86/4.63 % TRYING [6]
% 29.86/4.63 % TRYING [6]
% 29.86/4.63 % (2021317)Instruction limit reached!
% 29.86/4.63 % (2021317)------------------------------
% 29.86/4.63 % (2021317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021317)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021317)Termination reason: Instruction limit
% 29.86/4.63 % (2021317)Termination phase: Finite model building constraint generation
% 29.86/4.63 % (2021317)Time elapsed: 0.208 s
% 29.86/4.63 % (2021317)Peak memory usage: 18 MB
% 29.86/4.63 % (2021317)Instructions burned: 716 (million)
% 29.86/4.63 % TRYING [7]
% 29.86/4.63 % (2021329)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2757716034:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 29.86/4.63 % (2021320)Instruction limit reached!
% 29.86/4.63 % (2021320)------------------------------
% 29.86/4.63 % (2021320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021320)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021320)Termination reason: Instruction limit
% 29.86/4.63 % (2021320)Termination phase: Saturation
% 29.86/4.63 % (2021320)Time elapsed: 0.215 s
% 29.86/4.63 % (2021320)Peak memory usage: 18 MB
% 29.86/4.63 % (2021320)Instructions burned: 686 (million)
% 29.86/4.63 % (2021325)Instruction limit reached!
% 29.86/4.63 % (2021325)------------------------------
% 29.86/4.63 % (2021325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021325)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021325)Termination reason: Instruction limit
% 29.86/4.63 % (2021325)Termination phase: Saturation
% 29.86/4.63 % (2021325)Time elapsed: 0.175 s
% 29.86/4.63 % (2021325)Peak memory usage: 14 MB
% 29.86/4.63 % (2021325)Instructions burned: 480 (million)
% 29.86/4.63 % (2021331)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3472722758:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 29.86/4.63 % (2021332)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=1381320660:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 29.86/4.63 % TRYING [8]
% 29.86/4.63 % (2021327)Instruction limit reached!
% 29.86/4.63 % (2021327)------------------------------
% 29.86/4.63 % (2021327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.86/4.63 % (2021327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.86/4.63 % (2021327)CaDiCaL version: 2.1.3
% 29.86/4.63 % (2021327)Termination reason: Instruction limit
% 29.86/4.63 % (2021327)Termination phase: Finite model building SAT solving
% 29.86/4.63 % (2021327)Time elapsed: 0.176 s
% 29.86/4.63 % (2021327)Peak memory usage: 20 MB
% 29.86/4.63 % (2021327)Instructions burned: 868 (million)
% 29.86/4.63 % TRYING [14]
% 29.86/4.63 % (2021335)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=536011140:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 53.94/8.08 % (2021331)Instruction limit reached!
% 53.94/8.08 % (2021331)------------------------------
% 53.94/8.08 % (2021331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021331)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021331)Termination reason: Instruction limit
% 53.94/8.08 % (2021331)Termination phase: Finite model building constraint generation
% 53.94/8.08 % (2021331)Time elapsed: 0.172 s
% 53.94/8.08 % (2021331)Peak memory usage: 69 MB
% 53.94/8.08 % (2021331)Instructions burned: 893 (million)
% 53.94/8.08 % (2021337)fmb+10_1_sil=64000:random_seed=1742009882:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 53.94/8.08 % TRYING [1]
% 53.94/8.08 % TRYING [2]
% 53.94/8.08 % TRYING [3]
% 53.94/8.08 % TRYING [4]
% 53.94/8.08 % TRYING [5]
% 53.94/8.08 % TRYING [6]
% 53.94/8.08 % (2021332)Instruction limit reached!
% 53.94/8.08 % (2021332)------------------------------
% 53.94/8.08 % (2021332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021332)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021332)Termination reason: Instruction limit
% 53.94/8.08 % (2021332)Termination phase: Saturation
% 53.94/8.08 % (2021332)Time elapsed: 0.247 s
% 53.94/8.08 % (2021332)Peak memory usage: 21 MB
% 53.94/8.08 % (2021332)Instructions burned: 692 (million)
% 53.94/8.08 % (2021339)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1775718275:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 53.94/8.08 % TRYING [20]
% 53.94/8.08 % (2021335)Instruction limit reached!
% 53.94/8.08 % (2021335)------------------------------
% 53.94/8.08 % (2021335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021335)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021335)Termination reason: Instruction limit
% 53.94/8.08 % (2021335)Termination phase: Saturation
% 53.94/8.08 % (2021335)Time elapsed: 0.271 s
% 53.94/8.08 % (2021335)Peak memory usage: 18 MB
% 53.94/8.08 % (2021335)Instructions burned: 881 (million)
% 53.94/8.08 % TRYING [7]
% 53.94/8.08 % (2021341)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4132131170:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 53.94/8.08 % TRYING [8]
% 53.94/8.08 % (2021329)Instruction limit reached!
% 53.94/8.08 % (2021329)------------------------------
% 53.94/8.08 % (2021329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021329)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021329)Termination reason: Instruction limit
% 53.94/8.08 % (2021329)Termination phase: Saturation
% 53.94/8.08 % (2021329)Time elapsed: 0.350 s
% 53.94/8.08 % (2021329)Peak memory usage: 20 MB
% 53.94/8.08 % (2021329)Instructions burned: 1179 (million)
% 53.94/8.08 % (2021343)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3335634307:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 53.94/8.08 % TRYING [8]
% 53.94/8.08 % (2021341)Instruction limit reached!
% 53.94/8.08 % (2021341)------------------------------
% 53.94/8.08 % (2021341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021341)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021341)Termination reason: Instruction limit
% 53.94/8.08 % (2021341)Termination phase: Finite model building SAT solving
% 53.94/8.08 % (2021341)Time elapsed: 0.270 s
% 53.94/8.08 % (2021341)Peak memory usage: 45 MB
% 53.94/8.08 % (2021341)Instructions burned: 923 (million)
% 53.94/8.08 % (2021346)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=979885923:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 53.94/8.08 % TRYING [9]
% 53.94/8.08 % TRYING [9]
% 53.94/8.08 % (2021346)Instruction limit reached!
% 53.94/8.08 % (2021346)------------------------------
% 53.94/8.08 % (2021346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.94/8.08 % (2021346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.94/8.08 % (2021346)CaDiCaL version: 2.1.3
% 53.94/8.08 % (2021346)Termination reason: Instruction limit
% 53.94/8.08 % (2021346)Termination phase: Saturation
% 53.94/8.08 % (2021346)Time elapsed: 0.510 s
% 53.94/8.08 % (2021346)Peak memory usage: 38 MB
% 53.94/8.08 % (2021346)Instructions burned: 1472 (million)
% 53.94/8.08 % TRYING [10]
% 53.94/8.08 % (2021348)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1428732768:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 165.27/23.85 % TRYING [77]
% 165.27/23.85 % TRYING [10]
% 165.27/23.85 % (2021343)Instruction limit reached!
% 165.27/23.85 % (2021343)------------------------------
% 165.27/23.85 % (2021343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021343)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021343)Termination reason: Instruction limit
% 165.27/23.85 % (2021343)Termination phase: Saturation
% 165.27/23.85 % (2021343)Time elapsed: 1.369 s
% 165.27/23.85 % (2021343)Peak memory usage: 24 MB
% 165.27/23.85 % (2021343)Instructions burned: 5134 (million)
% 165.27/23.85 % (2021350)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1638931554:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 165.27/23.85 % TRYING [16]
% 165.27/23.85 % TRYING [11]
% 165.27/23.85 % TRYING [11]
% 165.27/23.85 % (2021350)Instruction limit reached!
% 165.27/23.85 % (2021350)------------------------------
% 165.27/23.85 % (2021350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021350)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021350)Termination reason: Instruction limit
% 165.27/23.85 % (2021350)Termination phase: Finite model building constraint generation
% 165.27/23.85 % (2021350)Time elapsed: 0.417 s
% 165.27/23.85 % (2021350)Peak memory usage: 141 MB
% 165.27/23.85 % (2021350)Instructions burned: 2176 (million)
% 165.27/23.85 % (2021352)ott-2_1_sil=16000:newcnf=on:random_seed=4064733832:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 165.27/23.85 % TRYING [12]
% 165.27/23.85 % (2021352)Instruction limit reached!
% 165.27/23.85 % (2021352)------------------------------
% 165.27/23.85 % (2021352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021352)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021352)Termination reason: Instruction limit
% 165.27/23.85 % (2021352)Termination phase: Saturation
% 165.27/23.85 % (2021352)Time elapsed: 0.266 s
% 165.27/23.85 % (2021352)Peak memory usage: 16 MB
% 165.27/23.85 % (2021352)Instructions burned: 872 (million)
% 165.27/23.85 % (2021354)ott+10_1_sil=32000:tgt=ground:random_seed=3504443036:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi)
% 165.27/23.85 % (2021348)Instruction limit reached!
% 165.27/23.85 % (2021348)------------------------------
% 165.27/23.85 % (2021348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021348)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021348)Termination reason: Instruction limit
% 165.27/23.85 % (2021348)Termination phase: Finite model building constraint generation
% 165.27/23.85 % (2021348)Time elapsed: 1.325 s
% 165.27/23.85 % (2021348)Peak memory usage: 517 MB
% 165.27/23.85 % (2021348)Instructions burned: 6326 (million)
% 165.27/23.85 % (2021356)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=201250617:i=54282_2972 on theBenchmark for (2972ds/54282Mi)
% 165.27/23.85 % TRYING [1]
% 165.27/23.85 % TRYING [2]
% 165.27/23.85 % TRYING [3]
% 165.27/23.85 % TRYING [4]
% 165.27/23.85 % TRYING [5]
% 165.27/23.85 % TRYING [6]
% 165.27/23.85 % TRYING [7]
% 165.27/23.85 % TRYING [8]
% 165.27/23.85 % (2021339)Instruction limit reached!
% 165.27/23.85 % (2021339)------------------------------
% 165.27/23.85 % (2021339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021339)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021339)Termination reason: Instruction limit
% 165.27/23.85 % (2021339)Termination phase: Finite model building constraint generation
% 165.27/23.85 % (2021339)Time elapsed: 2.615 s
% 165.27/23.85 % (2021339)Peak memory usage: 677 MB
% 165.27/23.85 % (2021339)Instructions burned: 9515 (million)
% 165.27/23.85 % TRYING [9]
% 165.27/23.85 % (2021358)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2925641082:i=3512:aac=none_2967 on theBenchmark for (2967ds/3512Mi)
% 165.27/23.85 % TRYING [12]
% 165.27/23.85 % TRYING [10]
% 165.27/23.85 % (2021358)Instruction limit reached!
% 165.27/23.85 % (2021358)------------------------------
% 165.27/23.85 % (2021358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 165.27/23.85 % (2021358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.27/23.85 % (2021358)CaDiCaL version: 2.1.3
% 165.27/23.85 % (2021358)Termination reason: Instruction limit
% 165.27/23.85 % (2021358)Termination phase: Saturation
% 218.73/31.45 % (2021358)Time elapsed: 1.015 s
% 218.73/31.45 % (2021358)Peak memory usage: 22 MB
% 218.73/31.45 % (2021358)Instructions burned: 3513 (million)
% 218.73/31.45 % (2021360)dis+21_1_sil=32000:sas=cadical:random_seed=2593758768:i=3773:amm=off_2957 on theBenchmark for (2957ds/3773Mi)
% 218.73/31.45 % (2021354)Instruction limit reached!
% 218.73/31.45 % (2021354)------------------------------
% 218.73/31.45 % (2021354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021354)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021354)Termination reason: Instruction limit
% 218.73/31.45 % (2021354)Termination phase: Saturation
% 218.73/31.45 % (2021354)Time elapsed: 1.610 s
% 218.73/31.45 % (2021354)Peak memory usage: 39 MB
% 218.73/31.45 % (2021354)Instructions burned: 5116 (million)
% 218.73/31.45 % (2021362)ott+11_1_sil=16000:gs=on:random_seed=3892424950:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2956 on theBenchmark for (2956ds/2251Mi)
% 218.73/31.45 % TRYING [11]
% 218.73/31.45 % (2021362)Instruction limit reached!
% 218.73/31.45 % (2021362)------------------------------
% 218.73/31.45 % (2021362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021362)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021362)Termination reason: Instruction limit
% 218.73/31.45 % (2021362)Termination phase: Saturation
% 218.73/31.45 % (2021362)Time elapsed: 0.662 s
% 218.73/31.45 % (2021362)Peak memory usage: 19 MB
% 218.73/31.45 % (2021362)Instructions burned: 2253 (million)
% 218.73/31.45 % (2021364)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3344707493:fmbsr=1.6:i=67534_2949 on theBenchmark for (2949ds/67534Mi)
% 218.73/31.45 % TRYING [7]
% 218.73/31.45 % (2021337)Instruction limit reached!
% 218.73/31.45 % (2021337)------------------------------
% 218.73/31.45 % (2021337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021337)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021337)Termination reason: Instruction limit
% 218.73/31.45 % (2021337)Termination phase: Finite model building SAT solving
% 218.73/31.45 % (2021337)Time elapsed: 4.733 s
% 218.73/31.45 % (2021337)Peak memory usage: 104 MB
% 218.73/31.45 % (2021337)Instructions burned: 22062 (million)
% 218.73/31.45 % (2021366)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4080585592:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2947 on theBenchmark for (2947ds/4591Mi)
% 218.73/31.45 % TRYING [8]
% 218.73/31.45 % (2021360)Instruction limit reached!
% 218.73/31.45 % (2021360)------------------------------
% 218.73/31.45 % (2021360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021360)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021360)Termination reason: Instruction limit
% 218.73/31.45 % (2021360)Termination phase: Saturation
% 218.73/31.45 % (2021360)Time elapsed: 1.139 s
% 218.73/31.45 % (2021360)Peak memory usage: 32 MB
% 218.73/31.45 % (2021360)Instructions burned: 3777 (million)
% 218.73/31.45 % (2021368)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3975322282:i=29340_2945 on theBenchmark for (2945ds/29340Mi)
% 218.73/31.45 % TRYING [12]
% 218.73/31.45 % TRYING [9]
% 218.73/31.45 % (2021366)Instruction limit reached!
% 218.73/31.45 % (2021366)------------------------------
% 218.73/31.45 % (2021366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021366)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021366)Termination reason: Instruction limit
% 218.73/31.45 % (2021366)Termination phase: Saturation
% 218.73/31.45 % (2021366)Time elapsed: 1.095 s
% 218.73/31.45 % (2021366)Peak memory usage: 37 MB
% 218.73/31.45 % (2021366)Instructions burned: 4592 (million)
% 218.73/31.45 % (2021370)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=140659778:i=5211_2936 on theBenchmark for (2936ds/5211Mi)
% 218.73/31.45 % TRYING [13]
% 218.73/31.45 % TRYING [10]
% 218.73/31.45 % (2021370)Instruction limit reached!
% 218.73/31.45 % (2021370)------------------------------
% 218.73/31.45 % (2021370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.73/31.45 % (2021370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.73/31.45 % (2021370)CaDiCaL version: 2.1.3
% 218.73/31.45 % (2021370)Termination reason: Instruction limit
% 181.23/31.72 % (2021370)Termination phase: Saturation
% 181.23/31.72 % (2021370)Time elapsed: 1.359 s
% 181.23/31.72 % (2021370)Peak memory usage: 43 MB
% 181.23/31.72 % (2021370)Instructions burned: 5212 (million)
% 181.23/31.72 % (2021372)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3627374303:i=5497:nm=2_2922 on theBenchmark for (2922ds/5497Mi)
% 181.23/31.72 % TRYING [17]
% 181.23/31.72 % TRYING [14]
% 181.23/31.72 % TRYING [11]
% 181.23/31.72 % (2021372)Instruction limit reached!
% 181.23/31.72 % (2021372)------------------------------
% 181.23/31.72 % (2021372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021372)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021372)Termination reason: Instruction limit
% 181.23/31.72 % (2021372)Termination phase: Finite model building constraint generation
% 181.23/31.72 % (2021372)Time elapsed: 1.493 s
% 181.23/31.72 % (2021372)Peak memory usage: 387 MB
% 181.23/31.72 % (2021372)Instructions burned: 5497 (million)
% 181.23/31.72 % (2021374)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2428328065:fmbsr=2:i=46332_2907 on theBenchmark for (2907ds/46332Mi)
% 181.23/31.72 % TRYING [15]
% 181.23/31.72 % TRYING [12]
% 181.23/31.72 % TRYING [15]
% 181.23/31.72 % TRYING [13]
% 181.23/31.72 % (2021368)Instruction limit reached!
% 181.23/31.72 % (2021368)------------------------------
% 181.23/31.72 % (2021368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021368)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021368)Termination reason: Instruction limit
% 181.23/31.72 % (2021368)Termination phase: Saturation
% 181.23/31.72 % (2021368)Time elapsed: 8.373 s
% 181.23/31.72 % (2021368)Peak memory usage: 475 MB
% 181.23/31.72 % (2021368)Instructions burned: 29341 (million)
% 181.23/31.72 % (2021376)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=240675337:i=14071_2861 on theBenchmark for (2861ds/14071Mi)
% 181.23/31.72 % TRYING [12]
% 181.23/31.72 % TRYING [13]
% 181.23/31.72 % TRYING [13]
% 181.23/31.72 % TRYING [14]
% 181.23/31.72 % (2021376)Instruction limit reached!
% 181.23/31.72 % (2021376)------------------------------
% 181.23/31.72 % (2021376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021376)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021376)Termination reason: Instruction limit
% 181.23/31.72 % (2021376)Termination phase: Finite model building SAT solving
% 181.23/31.72 % (2021376)Time elapsed: 5.130 s
% 181.23/31.72 % (2021376)Peak memory usage: 250 MB
% 181.23/31.72 % (2021376)Instructions burned: 14075 (million)
% 181.23/31.72 % (2021378)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1763998968:i=22565:add=on:rawr=on_2809 on theBenchmark for (2809ds/22565Mi)
% 181.23/31.72 % (2021356)Instruction limit reached!
% 181.23/31.72 % (2021356)------------------------------
% 181.23/31.72 % (2021356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021356)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021356)Termination reason: Instruction limit
% 181.23/31.72 % (2021356)Termination phase: Finite model building SAT solving
% 181.23/31.72 % (2021356)Time elapsed: 17.912 s
% 181.23/31.72 % (2021356)Peak memory usage: 288 MB
% 181.23/31.72 % (2021356)Instructions burned: 54283 (million)
% 181.23/31.72 % (2021380)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3671712942:i=8173:av=off_2792 on theBenchmark for (2792ds/8173Mi)
% 181.23/31.72 % (2021364)Instruction limit reached!
% 181.23/31.72 % (2021364)------------------------------
% 181.23/31.72 % (2021364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021364)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021364)Termination reason: Instruction limit
% 181.23/31.72 % (2021364)Termination phase: Finite model building SAT solving
% 181.23/31.72 % (2021364)Time elapsed: 17.320 s
% 181.23/31.72 % (2021364)Peak memory usage: 223 MB
% 181.23/31.72 % (2021364)Instructions burned: 67534 (million)
% 181.23/31.72 % (2021382)dis+10_16:1_sil=16000:random_seed=3501343327:i=9155:fsr=off_2775 on theBenchmark for (2775ds/9155Mi)
% 181.23/31.72 % (2021380)Instruction limit reached!
% 181.23/31.72 % (2021380)------------------------------
% 181.23/31.72 % (2021380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021380)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021380)Termination reason: Instruction limit
% 181.23/31.72 % (2021380)Termination phase: Saturation
% 181.23/31.72 % (2021380)Time elapsed: 2.744 s
% 181.23/31.72 % (2021380)Peak memory usage: 79 MB
% 181.23/31.72 % (2021380)Instructions burned: 8174 (million)
% 181.23/31.72 % (2021384)ott-3_8_sil=64000:random_seed=2665242067:i=20139:bs=on_2764 on theBenchmark for (2764ds/20139Mi)
% 181.23/31.72 % (2021378)Instruction limit reached!
% 181.23/31.72 % (2021378)------------------------------
% 181.23/31.72 % (2021378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021378)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021378)Termination reason: Instruction limit
% 181.23/31.72 % (2021378)Termination phase: Saturation
% 181.23/31.72 % (2021378)Time elapsed: 4.763 s
% 181.23/31.72 % (2021378)Peak memory usage: 37 MB
% 181.23/31.72 % (2021378)Instructions burned: 22566 (million)
% 181.23/31.72 % (2021386)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1400276173:fmbsr=2:i=32576_2761 on theBenchmark for (2761ds/32576Mi)
% 181.23/31.72 % TRYING [9]
% 181.23/31.72 % TRYING [10]
% 181.23/31.72 % TRYING [11]
% 181.23/31.72 % (2021382)Instruction limit reached!
% 181.23/31.72 % (2021382)------------------------------
% 181.23/31.72 % (2021382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021382)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021382)Termination reason: Instruction limit
% 181.23/31.72 % (2021382)Termination phase: Saturation
% 181.23/31.72 % (2021382)Time elapsed: 2.514 s
% 181.23/31.72 % (2021382)Peak memory usage: 31 MB
% 181.23/31.72 % (2021382)Instructions burned: 9157 (million)
% 181.23/31.72 % (2021388)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2502521385:i=11404_2750 on theBenchmark for (2750ds/11404Mi)
% 181.23/31.72 % TRYING [12]
% 181.23/31.72 % TRYING [13]
% 181.23/31.72 % (2021374)Instruction limit reached!
% 181.23/31.72 % (2021374)------------------------------
% 181.23/31.72 % (2021374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021374)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021374)Termination reason: Instruction limit
% 181.23/31.72 % (2021374)Termination phase: Finite model building SAT solving
% 181.23/31.72 % (2021374)Time elapsed: 17.736 s
% 181.23/31.72 % (2021374)Peak memory usage: 454 MB
% 181.23/31.72 % (2021374)Instructions burned: 46332 (million)
% 181.23/31.72 % (2021390)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3396887843:i=14134_2729 on theBenchmark for (2729ds/14134Mi)
% 181.23/31.72 % (2021388)Instruction limit reached!
% 181.23/31.72 % (2021388)------------------------------
% 181.23/31.72 % (2021388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021388)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021388)Termination reason: Instruction limit
% 181.23/31.72 % (2021388)Termination phase: Saturation
% 181.23/31.72 % (2021388)Time elapsed: 3.745 s
% 181.23/31.72 % (2021388)Peak memory usage: 63 MB
% 181.23/31.72 % (2021388)Instructions burned: 11405 (million)
% 181.23/31.72 % (2021392)dis+33_16_sil=32000:sac=on:random_seed=3607826918:i=15851:nm=0_2712 on theBenchmark for (2712ds/15851Mi)
% 181.23/31.72 % TRYING [16]
% 181.23/31.72 % (2021384)Instruction limit reached!
% 181.23/31.72 % (2021384)------------------------------
% 181.23/31.72 % (2021384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021384)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021384)Termination reason: Instruction limit
% 181.23/31.72 % (2021384)Termination phase: Saturation
% 181.23/31.72 % (2021384)Time elapsed: 7.387 s
% 181.23/31.72 % (2021384)Peak memory usage: 62 MB
% 181.23/31.72 % (2021384)Instructions burned: 20141 (million)
% 181.23/31.72 % (2021394)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=850302771:avsq=on:i=17627:add=on:amm=off_2690 on theBenchmark for (2690ds/17627Mi)
% 181.23/31.72 % (2021390)Instruction limit reached!
% 181.23/31.72 % (2021390)------------------------------
% 181.23/31.72 % (2021390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021390)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021390)Termination reason: Instruction limit
% 181.23/31.72 % (2021390)Termination phase: Saturation
% 181.23/31.72 % (2021390)Time elapsed: 4.023 s
% 181.23/31.72 % (2021390)Peak memory usage: 46 MB
% 181.23/31.72 % (2021390)Instructions burned: 14136 (million)
% 181.23/31.72 % (2021396)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3457826523:s2a=on:i=53295_2688 on theBenchmark for (2688ds/53295Mi)
% 181.23/31.72 % (2021392) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2021298-2021392"...
% 181.23/31.72 % (2021392)...printing done.
% 181.23/31.72 % (2021392)Refutation found. Thanks to Tanya!
% 181.23/31.72 % SZS status Theorem for theBenchmark
% 181.23/31.72 % SZS output start Proof for theBenchmark
% See solution above
% 181.23/31.72 % (2021392)------------------------------
% 181.23/31.72 % (2021392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 181.23/31.72 % (2021392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.23/31.72 % (2021392)CaDiCaL version: 2.1.3
% 181.23/31.72 % (2021392)Termination reason: Refutation
% 181.23/31.72 % (2021392)Time elapsed: 2.599 s
% 181.23/31.72 % (2021392)Peak memory usage: 78 MB
% 181.23/31.72 % (2021392)Instructions burned: 8467 (million)
% 181.23/31.72 % (2021298)Success in time 31.37 s
% 181.23/31.72 % Vampire exiting
%------------------------------------------------------------------------------