%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.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 12:52:58 PM UTC 2026
% Result : Theorem 142.71s 25.91s
% Output : Refutation 142.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 5
% Syntax : Number of formulae : 61 ( 10 unt; 0 def)
% Number of atoms : 232 ( 16 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 282 ( 111 ~; 116 |; 37 &)
% ( 5 <=>; 11 =>; 0 <=; 2 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 82 ( 70 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f97,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> cast_to_el_of_LattPOSet(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f106,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(poset_of_lattice(X0)))
=> cast_to_el_of_lattice(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f191,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0)
& element(X1,the_carrier(poset_of_lattice(X0))) )
=> element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f532,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_lattice3) ).
fof(f535,conjecture,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_lattice3) ).
fof(f536,negated_conjecture,
~ ! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f535]) ).
fof(f814,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f815,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f814]) ).
fof(f825,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f106]) ).
fof(f826,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f825]) ).
fof(f904,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(ennf_transformation,[],[f191]) ).
fof(f905,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(flattening,[],[f904]) ).
fof(f1315,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f532]) ).
fof(f1316,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_element_smaller(X1,X2,X0)
<=> relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f1315]) ).
fof(f1320,plain,
? [X0,X1] :
( ? [X2] :
( ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& element(X2,the_carrier(poset_of_lattice(X1))) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(ennf_transformation,[],[f536]) ).
fof(f1321,plain,
? [X0,X1] :
( ? [X2] :
( ( relstr_set_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) )
& element(X2,the_carrier(poset_of_lattice(X1))) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(flattening,[],[f1320]) ).
fof(f2126,plain,
! [X0,X1] :
( ! [X2] :
( ( ( latt_element_smaller(X1,X2,X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
& ( relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_element_smaller(X1,X2,X0) ) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f1316]) ).
fof(f2128,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2) )
& ( latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_set_smaller(poset_of_lattice(X1),X0,X2) )
& element(X2,the_carrier(poset_of_lattice(X1))) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(nnf_transformation,[],[f1321]) ).
fof(f2129,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,X2) )
& ( latt_element_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_set_smaller(poset_of_lattice(X1),X0,X2) )
& element(X2,the_carrier(poset_of_lattice(X1))) )
& ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) ),
inference(flattening,[],[f2128]) ).
fof(f2130,plain,
( ( ~ latt_element_smaller(sK481,cast_to_el_of_lattice(sK481,sK482),sK480)
| ~ relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482) )
& ( latt_element_smaller(sK481,cast_to_el_of_lattice(sK481,sK482),sK480)
| relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482) )
& element(sK482,the_carrier(poset_of_lattice(sK481)))
& ~ empty_carrier(sK481)
& lattice(sK481)
& latt_str(sK481) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK480,sK481,sK482]),skolemize(X0,sK480),skolemize(X1,sK481),skolemize(X2,sK482)],[f2129]) ).
fof(f2501,plain,
! [X0,X1] :
( ~ lattice(X0)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f815]) ).
fof(f2532,plain,
! [X0,X1] :
( ~ lattice(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| empty_carrier(X0)
| cast_to_el_of_lattice(X0,X1) = X1
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f826]) ).
fof(f2715,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(cnf_transformation,[],[f905]) ).
fof(f3774,plain,
! [X2,X0,X1] :
( ~ lattice(X1)
| ~ latt_element_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f2126]) ).
fof(f3775,plain,
! [X2,X0,X1] :
( ~ lattice(X1)
| ~ relstr_set_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| latt_element_smaller(X1,X2,X0)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f2126]) ).
fof(f3780,plain,
latt_str(sK481),
inference(cnf_transformation,[],[f2130]) ).
fof(f3781,plain,
lattice(sK481),
inference(cnf_transformation,[],[f2130]) ).
fof(f3782,plain,
~ empty_carrier(sK481),
inference(cnf_transformation,[],[f2130]) ).
fof(f3783,plain,
element(sK482,the_carrier(poset_of_lattice(sK481))),
inference(cnf_transformation,[],[f2130]) ).
fof(f3784,plain,
( latt_element_smaller(sK481,cast_to_el_of_lattice(sK481,sK482),sK480)
| relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482) ),
inference(cnf_transformation,[],[f2130]) ).
fof(f3785,plain,
( ~ latt_element_smaller(sK481,cast_to_el_of_lattice(sK481,sK482),sK480)
| ~ relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482) ),
inference(cnf_transformation,[],[f2130]) ).
fof(f24096,plain,
! [X0] :
( ~ element(X0,the_carrier(sK481))
| empty_carrier(sK481)
| cast_to_el_of_LattPOSet(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(resolution,[],[f2501,f3781]) ).
fof(f24101,plain,
! [X0] :
( ~ element(X0,the_carrier(sK481))
| cast_to_el_of_LattPOSet(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f24096,f3782]) ).
fof(f24104,plain,
! [X0] :
( ~ element(X0,the_carrier(sK481))
| cast_to_el_of_LattPOSet(sK481,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f24101,f3780]) ).
fof(f26375,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK481)))
| empty_carrier(sK481)
| cast_to_el_of_lattice(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(resolution,[],[f2532,f3781]) ).
fof(f26380,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK481)))
| cast_to_el_of_lattice(sK481,X0) = X0
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f26375,f3782]) ).
fof(f26383,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK481)))
| cast_to_el_of_lattice(sK481,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f26380,f3780]) ).
fof(f26707,plain,
sK482 = cast_to_el_of_lattice(sK481,sK482),
inference(resolution,[],[f26383,f3783]) ).
fof(f26709,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482)
| ~ latt_element_smaller(sK481,sK482,sK480) ),
inference(superposition,[],[f3785,f26707]) ).
fof(f26710,plain,
( relstr_set_smaller(poset_of_lattice(sK481),sK480,sK482)
| latt_element_smaller(sK481,sK482,sK480) ),
inference(superposition,[],[f3784,f26707]) ).
fof(f30660,plain,
( element(sK482,the_carrier(sK481))
| empty_carrier(sK481)
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(poset_of_lattice(sK481))) ),
inference(superposition,[],[f2715,f26707]) ).
fof(f30663,plain,
( element(sK482,the_carrier(sK481))
| ~ lattice(sK481)
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(poset_of_lattice(sK481))) ),
inference(forward_subsumption_resolution,[],[f30660,f3782]) ).
fof(f30667,plain,
( element(sK482,the_carrier(sK481))
| ~ latt_str(sK481)
| ~ element(sK482,the_carrier(poset_of_lattice(sK481))) ),
inference(forward_subsumption_resolution,[],[f30663,f3781]) ).
fof(f30670,plain,
( element(sK482,the_carrier(sK481))
| ~ element(sK482,the_carrier(poset_of_lattice(sK481))) ),
inference(forward_subsumption_resolution,[],[f30667,f3780]) ).
fof(f30672,plain,
element(sK482,the_carrier(sK481)),
inference(forward_subsumption_resolution,[],[f30670,f3783]) ).
fof(f30673,plain,
sK482 = cast_to_el_of_LattPOSet(sK481,sK482),
inference(resolution,[],[f30672,f24104]) ).
fof(f42679,plain,
! [X0,X1] :
( ~ latt_element_smaller(sK481,X0,X1)
| ~ element(X0,the_carrier(sK481))
| empty_carrier(sK481)
| relstr_set_smaller(poset_of_lattice(sK481),X1,cast_to_el_of_LattPOSet(sK481,X0))
| ~ latt_str(sK481) ),
inference(resolution,[],[f3774,f3781]) ).
fof(f42684,plain,
! [X0,X1] :
( ~ latt_element_smaller(sK481,X0,X1)
| ~ element(X0,the_carrier(sK481))
| relstr_set_smaller(poset_of_lattice(sK481),X1,cast_to_el_of_LattPOSet(sK481,X0))
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f42679,f3782]) ).
fof(f42687,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(sK481))
| ~ latt_element_smaller(sK481,X0,X1)
| relstr_set_smaller(poset_of_lattice(sK481),X1,cast_to_el_of_LattPOSet(sK481,X0)) ),
inference(forward_subsumption_resolution,[],[f42684,f3780]) ).
fof(f42690,plain,
! [X0,X1] :
( ~ relstr_set_smaller(poset_of_lattice(sK481),X0,cast_to_el_of_LattPOSet(sK481,X1))
| ~ element(X1,the_carrier(sK481))
| empty_carrier(sK481)
| latt_element_smaller(sK481,X1,X0)
| ~ latt_str(sK481) ),
inference(resolution,[],[f3775,f3781]) ).
fof(f42695,plain,
! [X0,X1] :
( ~ relstr_set_smaller(poset_of_lattice(sK481),X0,cast_to_el_of_LattPOSet(sK481,X1))
| ~ element(X1,the_carrier(sK481))
| latt_element_smaller(sK481,X1,X0)
| ~ latt_str(sK481) ),
inference(forward_subsumption_resolution,[],[f42690,f3782]) ).
fof(f42698,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(sK481))
| ~ relstr_set_smaller(poset_of_lattice(sK481),X0,cast_to_el_of_LattPOSet(sK481,X1))
| latt_element_smaller(sK481,X1,X0) ),
inference(forward_subsumption_resolution,[],[f42695,f3780]) ).
fof(f78060,plain,
! [X0] :
( ~ latt_element_smaller(sK481,sK482,X0)
| relstr_set_smaller(poset_of_lattice(sK481),X0,cast_to_el_of_LattPOSet(sK481,sK482)) ),
inference(resolution,[],[f42687,f30672]) ).
fof(f78061,plain,
! [X0] :
( relstr_set_smaller(poset_of_lattice(sK481),X0,sK482)
| ~ latt_element_smaller(sK481,sK482,X0) ),
inference(forward_demodulation,[],[f78060,f30673]) ).
fof(f78115,plain,
! [X0] :
( ~ relstr_set_smaller(poset_of_lattice(sK481),X0,cast_to_el_of_LattPOSet(sK481,sK482))
| latt_element_smaller(sK481,sK482,X0) ),
inference(resolution,[],[f42698,f30672]) ).
fof(f78116,plain,
! [X0] :
( ~ relstr_set_smaller(poset_of_lattice(sK481),X0,sK482)
| latt_element_smaller(sK481,sK482,X0) ),
inference(forward_demodulation,[],[f78115,f30673]) ).
fof(f78148,plain,
( ~ latt_element_smaller(sK481,sK482,sK480)
| ~ latt_element_smaller(sK481,sK482,sK480) ),
inference(resolution,[],[f78061,f26709]) ).
fof(f78149,plain,
~ latt_element_smaller(sK481,sK482,sK480),
inference(duplicate_literal_removal,[],[f78148]) ).
fof(f78210,plain,
( latt_element_smaller(sK481,sK482,sK480)
| latt_element_smaller(sK481,sK482,sK480) ),
inference(resolution,[],[f78116,f26710]) ).
fof(f78212,plain,
latt_element_smaller(sK481,sK482,sK480),
inference(duplicate_literal_removal,[],[f78210]) ).
fof(f78213,plain,
$false,
inference(forward_subsumption_resolution,[],[f78212,f78149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n005.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 04:50:25 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 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.54/1.90 % (439917)Will run a generic schedule for satisfiability detection.
% 8.54/1.90 % (439928)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1662198182:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.54/1.90 % (439923)% WARNING: option uhcvi not known.
% 8.54/1.90 % (439922)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2125351289_2999 on theBenchmark for (2999ds/0Mi)
% 8.54/1.90 % (439923)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3980569198:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.54/1.90 % (439924)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3941855585:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.54/1.90 % (439925)dis+10_1_sil=32000:sp=arity:random_seed=451396668:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.54/1.90 % (439926)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3801388522:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.54/1.90 % (439927)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=435880667:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.54/1.90 % (439928)Instruction limit reached!
% 8.54/1.90 % (439928)------------------------------
% 8.54/1.90 % (439928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.90 % (439928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.90 % (439928)CaDiCaL version: 2.1.3
% 8.54/1.90 % (439928)Termination reason: Instruction limit
% 8.54/1.90 % (439928)Termination phase: Saturation
% 8.54/1.90 % (439928)Time elapsed: 0.052 s
% 8.54/1.90 % (439928)Peak memory usage: 16 MB
% 8.54/1.90 % (439928)Instructions burned: 161 (million)
% 8.54/1.90 % (439936)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1846149312:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.54/1.90 % (439925)Instruction limit reached!
% 8.54/1.90 % (439925)------------------------------
% 8.54/1.90 % (439925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.90 % (439925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.90 % (439925)CaDiCaL version: 2.1.3
% 8.54/1.90 % (439925)Termination reason: Instruction limit
% 8.54/1.90 % (439925)Termination phase: Saturation
% 8.54/1.90 % (439925)Time elapsed: 0.057 s
% 8.54/1.90 % (439925)Peak memory usage: 15 MB
% 8.54/1.90 % (439925)Instructions burned: 104 (million)
% 8.54/1.90 % (439926)Instruction limit reached!
% 8.54/1.90 % (439926)------------------------------
% 8.54/1.90 % (439926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.90 % (439926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.90 % (439926)CaDiCaL version: 2.1.3
% 8.54/1.90 % (439926)Termination reason: Instruction limit
% 8.54/1.90 % (439926)Termination phase: Blocked clause elimination
% 8.54/1.90 % (439926)Time elapsed: 0.059 s
% 8.54/1.90 % (439926)Peak memory usage: 14 MB
% 8.54/1.90 % (439926)Instructions burned: 118 (million)
% 8.54/1.90 % (439927)Instruction limit reached!
% 8.54/1.90 % (439927)------------------------------
% 8.54/1.90 % (439927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.90 % (439927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.90 % (439927)CaDiCaL version: 2.1.3
% 8.54/1.90 % (439927)Termination reason: Instruction limit
% 8.54/1.90 % (439927)Termination phase: Saturation
% 8.54/1.90 % (439927)Time elapsed: 0.073 s
% 8.54/1.90 % (439927)Peak memory usage: 15 MB
% 8.54/1.90 % (439927)Instructions burned: 132 (million)
% 8.54/1.90 % (439938)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=912392724:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.54/1.90 % (439939)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=2909956027:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.54/1.90 % (439940)ott-21_1_sil=16000:fs=off:random_seed=394212239:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.54/1.90 % (439938)Instruction limit reached!
% 8.54/1.90 % (439938)------------------------------
% 8.54/1.90 % (439938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.54/1.90 % (439938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/1.90 % (439938)CaDiCaL version: 2.1.3
% 8.54/1.90 % (439938)Termination reason: Instruction limit
% 34.44/5.37 % (439938)Termination phase: Saturation
% 34.44/5.37 % (439938)Time elapsed: 0.068 s
% 34.44/5.37 % (439938)Peak memory usage: 15 MB
% 34.44/5.37 % (439938)Instructions burned: 131 (million)
% 34.44/5.37 % TRYING [1]
% 34.44/5.37 % TRYING [2]
% 34.44/5.37 % (439944)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2152757295:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 34.44/5.37 % (439940)Instruction limit reached!
% 34.44/5.37 % (439940)------------------------------
% 34.44/5.37 % (439940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.37 % (439940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.37 % (439940)CaDiCaL version: 2.1.3
% 34.44/5.37 % (439940)Termination reason: Instruction limit
% 34.44/5.37 % (439940)Termination phase: Saturation
% 34.44/5.37 % (439940)Time elapsed: 0.093 s
% 34.44/5.37 % (439940)Peak memory usage: 15 MB
% 34.44/5.37 % (439940)Instructions burned: 180 (million)
% 34.44/5.37 % TRYING [3]
% 34.44/5.37 % (439946)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1414330343:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.44/5.37 % (439936)Instruction limit reached!
% 34.44/5.37 % (439936)------------------------------
% 34.44/5.37 % (439936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.37 % (439936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.37 % (439936)CaDiCaL version: 2.1.3
% 34.44/5.37 % (439936)Termination reason: Instruction limit
% 34.44/5.37 % (439936)Termination phase: Finite model building constraint generation
% 34.44/5.37 % (439936)Time elapsed: 0.167 s
% 34.44/5.37 % (439936)Peak memory usage: 31 MB
% 34.44/5.37 % (439936)Instructions burned: 718 (million)
% 34.44/5.37 % TRYING [1]
% 34.44/5.37 % (439948)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1229236624:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 34.44/5.37 % TRYING [2]
% 34.44/5.37 % TRYING [3]
% 34.44/5.37 % TRYING [1]
% 34.44/5.37 % TRYING [2]
% 34.44/5.37 % (439939)Instruction limit reached!
% 34.44/5.37 % (439939)------------------------------
% 34.44/5.37 % (439939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.37 % (439939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.37 % (439939)CaDiCaL version: 2.1.3
% 34.44/5.37 % (439939)Termination reason: Instruction limit
% 34.44/5.37 % (439939)Termination phase: Saturation
% 34.44/5.37 % (439939)Time elapsed: 0.389 s
% 34.44/5.37 % (439939)Peak memory usage: 22 MB
% 34.44/5.37 % (439939)Instructions burned: 684 (million)
% 34.44/5.37 % (439944)Instruction limit reached!
% 34.44/5.37 % (439944)------------------------------
% 34.44/5.37 % (439944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.37 % (439944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.37 % (439944)CaDiCaL version: 2.1.3
% 34.44/5.37 % (439944)Termination reason: Instruction limit
% 34.44/5.37 % (439944)Termination phase: Saturation
% 34.44/5.37 % (439944)Time elapsed: 0.312 s
% 34.44/5.37 % (439944)Peak memory usage: 17 MB
% 34.44/5.37 % (439944)Instructions burned: 477 (million)
% 34.44/5.37 % (439950)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1052859280:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 34.44/5.37 % (439951)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=1128135576: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)
% 34.44/5.38 % (439948)Instruction limit reached!
% 34.44/5.38 % (439948)------------------------------
% 34.44/5.38 % (439948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.38 % (439948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.38 % (439948)CaDiCaL version: 2.1.3
% 34.44/5.38 % (439948)Termination reason: Instruction limit
% 34.44/5.38 % (439948)Termination phase: Saturation
% 34.44/5.38 % (439948)Time elapsed: 0.391 s
% 34.44/5.38 % (439948)Peak memory usage: 30 MB
% 34.44/5.38 % (439948)Instructions burned: 1182 (million)
% 34.44/5.38 % (439954)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3314744529:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 34.44/5.38 % (439946)Instruction limit reached!
% 34.44/5.38 % (439946)------------------------------
% 34.44/5.38 % (439946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.44/5.38 % (439946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439946)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439946)Termination reason: Instruction limit
% 104.67/15.20 % (439946)Termination phase: Finite model building SAT solving
% 104.67/15.20 % (439946)Time elapsed: 0.435 s
% 104.67/15.20 % (439946)Peak memory usage: 35 MB
% 104.67/15.20 % (439946)Instructions burned: 865 (million)
% 104.67/15.20 % (439956)fmb+10_1_sil=64000:random_seed=3630030032:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 104.67/15.20 % TRYING [1]
% 104.67/15.20 % TRYING [2]
% 104.67/15.20 % (439954)Instruction limit reached!
% 104.67/15.20 % (439954)------------------------------
% 104.67/15.20 % (439954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439954)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439954)Termination reason: Instruction limit
% 104.67/15.20 % (439954)Termination phase: Saturation
% 104.67/15.20 % (439954)Time elapsed: 0.215 s
% 104.67/15.20 % (439954)Peak memory usage: 22 MB
% 104.67/15.20 % (439954)Instructions burned: 880 (million)
% 104.67/15.20 % (439958)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3503368654:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 104.67/15.20 % (439951)Instruction limit reached!
% 104.67/15.20 % (439951)------------------------------
% 104.67/15.20 % (439951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439951)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439951)Termination reason: Instruction limit
% 104.67/15.20 % (439951)Termination phase: Saturation
% 104.67/15.20 % (439951)Time elapsed: 0.414 s
% 104.67/15.20 % (439951)Peak memory usage: 22 MB
% 104.67/15.20 % (439951)Instructions burned: 693 (million)
% 104.67/15.20 % (439950)Instruction limit reached!
% 104.67/15.20 % (439950)------------------------------
% 104.67/15.20 % (439950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439950)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439950)Termination reason: Instruction limit
% 104.67/15.20 % (439950)Termination phase: Finite model building constraint generation
% 104.67/15.20 % (439950)Time elapsed: 0.435 s
% 104.67/15.20 % (439950)Peak memory usage: 80 MB
% 104.67/15.20 % (439950)Instructions burned: 890 (million)
% 104.67/15.20 % (439960)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=66231380:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 104.67/15.20 % (439961)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1465776673:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 104.67/15.20 % TRYING [4]
% 104.67/15.20 % (439958)Cannot represent all propositional literals internally
% 104.67/15.20 % (439958)Refutation not found, incomplete strategy
% 104.67/15.20 % (439958)------------------------------
% 104.67/15.20 % (439958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439958)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439958)Termination reason: Refutation not found, incomplete strategy
% 104.67/15.20 % (439958)Time elapsed: 0.106 s
% 104.67/15.20 % (439958)Peak memory usage: 19 MB
% 104.67/15.20 % (439958)Instructions burned: 390 (million)
% 104.67/15.20 % (439958)------------------------------
% 104.67/15.20 % (439958)------------------------------
% 104.67/15.20 % (439964)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1806601607:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 104.67/15.20 % TRYING [3]
% 104.67/15.20 % TRYING [8]
% 104.67/15.20 % (439960)Instruction limit reached!
% 104.67/15.20 % (439960)------------------------------
% 104.67/15.20 % (439960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.67/15.20 % (439960)CaDiCaL version: 2.1.3
% 104.67/15.20 % (439960)Termination reason: Instruction limit
% 104.67/15.20 % (439960)Termination phase: Finite model building constraint generation
% 104.67/15.20 % (439960)Time elapsed: 0.380 s
% 104.67/15.20 % (439960)Peak memory usage: 53 MB
% 104.67/15.20 % (439960)Instructions burned: 926 (million)
% 104.67/15.20 % (439966)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1084444384:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 104.67/15.20 % (439964)Instruction limit reached!
% 104.67/15.20 % (439964)------------------------------
% 104.67/15.20 % (439964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 104.67/15.20 % (439964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439964)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439964)Termination reason: Instruction limit
% 142.71/25.91 % (439964)Termination phase: Saturation
% 142.71/25.91 % (439964)Time elapsed: 0.428 s
% 142.71/25.91 % (439964)Peak memory usage: 29 MB
% 142.71/25.91 % (439964)Instructions burned: 1477 (million)
% 142.71/25.91 % (439968)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2907433246:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 142.71/25.91 % (439966)Cannot represent all propositional literals internally
% 142.71/25.91 % (439966)Refutation not found, incomplete strategy
% 142.71/25.91 % (439966)------------------------------
% 142.71/25.91 % (439966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439966)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439966)Termination reason: Refutation not found, incomplete strategy
% 142.71/25.91 % (439966)Time elapsed: 0.228 s
% 142.71/25.91 % (439966)Peak memory usage: 20 MB
% 142.71/25.91 % (439966)Instructions burned: 457 (million)
% 142.71/25.91 % (439966)------------------------------
% 142.71/25.91 % (439966)------------------------------
% 142.71/25.91 % (439970)ott-2_1_sil=16000:newcnf=on:random_seed=2264135249:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 142.71/25.91 % (439968)Instruction limit reached!
% 142.71/25.91 % (439968)------------------------------
% 142.71/25.91 % (439968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439968)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439968)Termination reason: Instruction limit
% 142.71/25.91 % (439968)Termination phase: Finite model building preprocessing
% 142.71/25.91 % (439968)Time elapsed: 0.572 s
% 142.71/25.91 % (439968)Peak memory usage: 40 MB
% 142.71/25.91 % (439968)Instructions burned: 2179 (million)
% 142.71/25.91 % (439972)ott+10_1_sil=32000:tgt=ground:random_seed=1810723269:i=5114:av=off_2979 on theBenchmark for (2979ds/5114Mi)
% 142.71/25.91 % (439970)Instruction limit reached!
% 142.71/25.91 % (439970)------------------------------
% 142.71/25.91 % (439970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439970)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439970)Termination reason: Instruction limit
% 142.71/25.91 % (439970)Termination phase: Saturation
% 142.71/25.91 % (439970)Time elapsed: 0.472 s
% 142.71/25.91 % (439970)Peak memory usage: 19 MB
% 142.71/25.91 % (439970)Instructions burned: 871 (million)
% 142.71/25.91 % (439974)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1154429084:i=54282_2978 on theBenchmark for (2978ds/54282Mi)
% 142.71/25.91 % TRYING [1]
% 142.71/25.91 % TRYING [2]
% 142.71/25.91 % TRYING [3]
% 142.71/25.91 % TRYING [4]
% 142.71/25.91 % TRYING [4]
% 142.71/25.91 % TRYING [5]
% 142.71/25.91 % (439972)Instruction limit reached!
% 142.71/25.91 % (439972)------------------------------
% 142.71/25.91 % (439972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439972)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439972)Termination reason: Instruction limit
% 142.71/25.91 % (439972)Termination phase: Saturation
% 142.71/25.91 % (439972)Time elapsed: 1.737 s
% 142.71/25.91 % (439972)Peak memory usage: 74 MB
% 142.71/25.91 % (439972)Instructions burned: 5116 (million)
% 142.71/25.91 % (439976)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1726516937:i=3512:aac=none_2961 on theBenchmark for (2961ds/3512Mi)
% 142.71/25.91 % (439961)Instruction limit reached!
% 142.71/25.91 % (439961)------------------------------
% 142.71/25.91 % (439961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439961)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439961)Termination reason: Instruction limit
% 142.71/25.91 % (439961)Termination phase: Saturation
% 142.71/25.91 % (439961)Time elapsed: 2.988 s
% 142.71/25.91 % (439961)Peak memory usage: 48 MB
% 142.71/25.91 % (439961)Instructions burned: 5132 (million)
% 142.71/25.91 % (439978)dis+21_1_sil=32000:sas=cadical:random_seed=3712861578:i=3773:amm=off_2959 on theBenchmark for (2959ds/3773Mi)
% 142.71/25.91 % (439976)Instruction limit reached!
% 142.71/25.91 % (439976)------------------------------
% 142.71/25.91 % (439976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439976)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439976)Termination reason: Instruction limit
% 142.71/25.91 % (439976)Termination phase: Saturation
% 142.71/25.91 % (439976)Time elapsed: 1.122 s
% 142.71/25.91 % (439976)Peak memory usage: 43 MB
% 142.71/25.91 % (439976)Instructions burned: 3513 (million)
% 142.71/25.91 % (439980)ott+11_1_sil=16000:gs=on:random_seed=1292358332:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2950 on theBenchmark for (2950ds/2251Mi)
% 142.71/25.91 % (439980)Instruction limit reached!
% 142.71/25.91 % (439980)------------------------------
% 142.71/25.91 % (439980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439980)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439980)Termination reason: Instruction limit
% 142.71/25.91 % (439980)Termination phase: Saturation
% 142.71/25.91 % (439980)Time elapsed: 0.671 s
% 142.71/25.91 % (439980)Peak memory usage: 34 MB
% 142.71/25.91 % (439980)Instructions burned: 2251 (million)
% 142.71/25.91 % (439982)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=222644842:fmbsr=1.6:i=67534_2943 on theBenchmark for (2943ds/67534Mi)
% 142.71/25.91 % TRYING [5]
% 142.71/25.91 % (439978)Instruction limit reached!
% 142.71/25.91 % (439978)------------------------------
% 142.71/25.91 % (439978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439978)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439978)Termination reason: Instruction limit
% 142.71/25.91 % (439978)Termination phase: Saturation
% 142.71/25.91 % (439978)Time elapsed: 2.321 s
% 142.71/25.91 % (439978)Peak memory usage: 46 MB
% 142.71/25.91 % (439978)Instructions burned: 3774 (million)
% 142.71/25.91 % (439984)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2096594968:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi)
% 142.71/25.91 % TRYING [7]
% 142.71/25.91 % (439984)Instruction limit reached!
% 142.71/25.91 % (439984)------------------------------
% 142.71/25.91 % (439984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439984)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439984)Termination reason: Instruction limit
% 142.71/25.91 % (439984)Termination phase: Saturation
% 142.71/25.91 % (439984)Time elapsed: 2.512 s
% 142.71/25.91 % (439984)Peak memory usage: 69 MB
% 142.71/25.91 % (439984)Instructions burned: 4593 (million)
% 142.71/25.91 % (439986)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2060745660:i=29340_2911 on theBenchmark for (2911ds/29340Mi)
% 142.71/25.91 % TRYING [5]
% 142.71/25.91 % (439956)Instruction limit reached!
% 142.71/25.91 % (439956)------------------------------
% 142.71/25.91 % (439956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439956)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439956)Termination reason: Instruction limit
% 142.71/25.91 % (439956)Termination phase: Finite model building constraint generation
% 142.71/25.91 % (439956)Time elapsed: 9.728 s
% 142.71/25.91 % (439956)Peak memory usage: 292 MB
% 142.71/25.91 % (439956)Instructions burned: 22062 (million)
% 142.71/25.91 % (439988)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=833028595:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 142.71/25.91 % TRYING [6]
% 142.71/25.91 % (439988)Instruction limit reached!
% 142.71/25.91 % (439988)------------------------------
% 142.71/25.91 % (439988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439988)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439988)Termination reason: Instruction limit
% 142.71/25.91 % (439988)Termination phase: Saturation
% 142.71/25.91 % (439988)Time elapsed: 2.266 s
% 142.71/25.91 % (439988)Peak memory usage: 52 MB
% 142.71/25.91 % (439988)Instructions burned: 5211 (million)
% 142.71/25.91 % (439990)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=497801288:i=5497:nm=2_2872 on theBenchmark for (2872ds/5497Mi)
% 142.71/25.91 % TRYING [17]
% 142.71/25.91 % TRYING [6]
% 142.71/25.91 % (439990)Instruction limit reached!
% 142.71/25.91 % (439990)------------------------------
% 142.71/25.91 % (439990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439990)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439990)Termination reason: Instruction limit
% 142.71/25.91 % (439990)Termination phase: Finite model building constraint generation
% 142.71/25.91 % (439990)Time elapsed: 1.977 s
% 142.71/25.91 % (439990)Peak memory usage: 339 MB
% 142.71/25.91 % (439990)Instructions burned: 5500 (million)
% 142.71/25.91 % (439992)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=272421332:fmbsr=2:i=46332_2851 on theBenchmark for (2851ds/46332Mi)
% 142.71/25.91 % TRYING [15]
% 142.71/25.91 % (439982)Instruction limit reached!
% 142.71/25.91 % (439982)------------------------------
% 142.71/25.91 % (439982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439982)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439982)Termination reason: Instruction limit
% 142.71/25.91 % (439982)Termination phase: Finite model building constraint generation
% 142.71/25.91 % (439982)Time elapsed: 12.628 s
% 142.71/25.91 % (439982)Peak memory usage: 2865 MB
% 142.71/25.91 % (439982)Instructions burned: 67538 (million)
% 142.71/25.91 % (439994)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=297294992:i=14071_2814 on theBenchmark for (2814ds/14071Mi)
% 142.71/25.91 % TRYING [12]
% 142.71/25.91 % (439994)Instruction limit reached!
% 142.71/25.91 % (439994)------------------------------
% 142.71/25.91 % (439994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439994)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439994)Termination reason: Instruction limit
% 142.71/25.91 % (439994)Termination phase: Finite model building constraint generation
% 142.71/25.91 % (439994)Time elapsed: 2.547 s
% 142.71/25.91 % (439994)Peak memory usage: 614 MB
% 142.71/25.91 % (439994)Instructions burned: 14077 (million)
% 142.71/25.91 % (439996)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2300626105:i=22565:add=on:rawr=on_2788 on theBenchmark for (2788ds/22565Mi)
% 142.71/25.91 % (439974)Instruction limit reached!
% 142.71/25.91 % (439974)------------------------------
% 142.71/25.91 % (439974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439974)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439974)Termination reason: Instruction limit
% 142.71/25.91 % (439974)Termination phase: Finite model building constraint generation
% 142.71/25.91 % (439974)Time elapsed: 19.166 s
% 142.71/25.91 % (439974)Peak memory usage: 1367 MB
% 142.71/25.91 % (439974)Instructions burned: 54283 (million)
% 142.71/25.91 % (439998)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=330640352:i=8173:av=off_2785 on theBenchmark for (2785ds/8173Mi)
% 142.71/25.91 % (439998) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-439917-439998"...
% 142.71/25.91 % (439998)...printing done.
% 142.71/25.91 % (439998)Refutation found. Thanks to Tanya!
% 142.71/25.91 % SZS status Theorem for theBenchmark
% 142.71/25.91 % SZS output start Proof for theBenchmark
% See solution above
% 142.71/25.91 % (439998)------------------------------
% 142.71/25.91 % (439998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 142.71/25.91 % (439998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.71/25.91 % (439998)CaDiCaL version: 2.1.3
% 142.71/25.91 % (439998)Termination reason: Refutation
% 142.71/25.91 % (439998)Time elapsed: 3.595 s
% 142.71/25.91 % (439998)Peak memory usage: 94 MB
% 142.71/25.91 % (439998)Instructions burned: 5938 (million)
% 142.71/25.91 % (439917)Success in time 25.482 s
% 142.71/25.91 % Vampire exiting
%------------------------------------------------------------------------------