%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU348+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 : n010.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:57 PM UTC 2026
% Result : Theorem 112.47s 31.47s
% Output : Refutation 112.47s
% 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(f96,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(f105,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(f189,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(f519,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_lattice3) ).
fof(f522,conjecture,
! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_lattice3) ).
fof(f523,negated_conjecture,
~ ! [X0,X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(poset_of_lattice(X1)))
=> ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<=> latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f522]) ).
fof(f808,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,[],[f96]) ).
fof(f809,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,[],[f808]) ).
fof(f819,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,[],[f105]) ).
fof(f820,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,[],[f819]) ).
fof(f896,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,[],[f189]) ).
fof(f897,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,[],[f896]) ).
fof(f1295,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_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,[],[f519]) ).
fof(f1296,plain,
! [X0,X1] :
( ! [X2] :
( ( latt_set_smaller(X1,X2,X0)
<=> relstr_element_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,[],[f1295]) ).
fof(f1300,plain,
? [X0,X1] :
( ? [X2] :
( ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_set_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,[],[f523]) ).
fof(f1301,plain,
? [X0,X1] :
( ? [X2] :
( ( relstr_element_smaller(poset_of_lattice(X1),X0,X2)
<~> latt_set_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,[],[f1300]) ).
fof(f2101,plain,
! [X0,X1] :
( ! [X2] :
( ( ( latt_set_smaller(X1,X2,X0)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2)) )
& ( relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_set_smaller(X1,X2,X0) ) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f1296]) ).
fof(f2103,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2) )
& ( latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_element_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,[],[f1301]) ).
fof(f2104,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,X2) )
& ( latt_set_smaller(X1,cast_to_el_of_lattice(X1,X2),X0)
| relstr_element_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,[],[f2103]) ).
fof(f2105,plain,
( ( ~ latt_set_smaller(sK478,cast_to_el_of_lattice(sK478,sK479),sK477)
| ~ relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479) )
& ( latt_set_smaller(sK478,cast_to_el_of_lattice(sK478,sK479),sK477)
| relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479) )
& element(sK479,the_carrier(poset_of_lattice(sK478)))
& ~ empty_carrier(sK478)
& lattice(sK478)
& latt_str(sK478) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK477,sK478,sK479]),skolemize(X0,sK477),skolemize(X1,sK478),skolemize(X2,sK479)],[f2104]) ).
fof(f2477,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,[],[f809]) ).
fof(f2508,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,[],[f820]) ).
fof(f2687,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,[],[f897]) ).
fof(f3723,plain,
! [X2,X0,X1] :
( ~ lattice(X1)
| ~ latt_set_smaller(X1,X2,X0)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f2101]) ).
fof(f3724,plain,
! [X2,X0,X1] :
( ~ lattice(X1)
| ~ relstr_element_smaller(poset_of_lattice(X1),X0,cast_to_el_of_LattPOSet(X1,X2))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| latt_set_smaller(X1,X2,X0)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f2101]) ).
fof(f3734,plain,
latt_str(sK478),
inference(cnf_transformation,[],[f2105]) ).
fof(f3735,plain,
lattice(sK478),
inference(cnf_transformation,[],[f2105]) ).
fof(f3736,plain,
~ empty_carrier(sK478),
inference(cnf_transformation,[],[f2105]) ).
fof(f3737,plain,
element(sK479,the_carrier(poset_of_lattice(sK478))),
inference(cnf_transformation,[],[f2105]) ).
fof(f3738,plain,
( latt_set_smaller(sK478,cast_to_el_of_lattice(sK478,sK479),sK477)
| relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479) ),
inference(cnf_transformation,[],[f2105]) ).
fof(f3739,plain,
( ~ latt_set_smaller(sK478,cast_to_el_of_lattice(sK478,sK479),sK477)
| ~ relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479) ),
inference(cnf_transformation,[],[f2105]) ).
fof(f24064,plain,
! [X0] :
( ~ element(X0,the_carrier(sK478))
| empty_carrier(sK478)
| cast_to_el_of_LattPOSet(sK478,X0) = X0
| ~ latt_str(sK478) ),
inference(resolution,[],[f2477,f3735]) ).
fof(f24069,plain,
! [X0] :
( ~ element(X0,the_carrier(sK478))
| cast_to_el_of_LattPOSet(sK478,X0) = X0
| ~ latt_str(sK478) ),
inference(forward_subsumption_resolution,[],[f24064,f3736]) ).
fof(f24072,plain,
! [X0] :
( ~ element(X0,the_carrier(sK478))
| cast_to_el_of_LattPOSet(sK478,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f24069,f3734]) ).
fof(f26343,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK478)))
| empty_carrier(sK478)
| cast_to_el_of_lattice(sK478,X0) = X0
| ~ latt_str(sK478) ),
inference(resolution,[],[f2508,f3735]) ).
fof(f26348,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK478)))
| cast_to_el_of_lattice(sK478,X0) = X0
| ~ latt_str(sK478) ),
inference(forward_subsumption_resolution,[],[f26343,f3736]) ).
fof(f26351,plain,
! [X0] :
( ~ element(X0,the_carrier(poset_of_lattice(sK478)))
| cast_to_el_of_lattice(sK478,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f26348,f3734]) ).
fof(f26671,plain,
sK479 = cast_to_el_of_lattice(sK478,sK479),
inference(resolution,[],[f26351,f3737]) ).
fof(f26678,plain,
( ~ relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479)
| ~ latt_set_smaller(sK478,sK479,sK477) ),
inference(superposition,[],[f3739,f26671]) ).
fof(f26679,plain,
( relstr_element_smaller(poset_of_lattice(sK478),sK477,sK479)
| latt_set_smaller(sK478,sK479,sK477) ),
inference(superposition,[],[f3738,f26671]) ).
fof(f30587,plain,
( element(sK479,the_carrier(sK478))
| empty_carrier(sK478)
| ~ lattice(sK478)
| ~ latt_str(sK478)
| ~ element(sK479,the_carrier(poset_of_lattice(sK478))) ),
inference(superposition,[],[f2687,f26671]) ).
fof(f30590,plain,
( element(sK479,the_carrier(sK478))
| ~ lattice(sK478)
| ~ latt_str(sK478)
| ~ element(sK479,the_carrier(poset_of_lattice(sK478))) ),
inference(forward_subsumption_resolution,[],[f30587,f3736]) ).
fof(f30594,plain,
( element(sK479,the_carrier(sK478))
| ~ latt_str(sK478)
| ~ element(sK479,the_carrier(poset_of_lattice(sK478))) ),
inference(forward_subsumption_resolution,[],[f30590,f3735]) ).
fof(f30597,plain,
( element(sK479,the_carrier(sK478))
| ~ element(sK479,the_carrier(poset_of_lattice(sK478))) ),
inference(forward_subsumption_resolution,[],[f30594,f3734]) ).
fof(f30599,plain,
element(sK479,the_carrier(sK478)),
inference(forward_subsumption_resolution,[],[f30597,f3737]) ).
fof(f30600,plain,
sK479 = cast_to_el_of_LattPOSet(sK478,sK479),
inference(resolution,[],[f30599,f24072]) ).
fof(f42437,plain,
! [X0,X1] :
( ~ latt_set_smaller(sK478,X0,X1)
| ~ element(X0,the_carrier(sK478))
| empty_carrier(sK478)
| relstr_element_smaller(poset_of_lattice(sK478),X1,cast_to_el_of_LattPOSet(sK478,X0))
| ~ latt_str(sK478) ),
inference(resolution,[],[f3723,f3735]) ).
fof(f42442,plain,
! [X0,X1] :
( ~ latt_set_smaller(sK478,X0,X1)
| ~ element(X0,the_carrier(sK478))
| relstr_element_smaller(poset_of_lattice(sK478),X1,cast_to_el_of_LattPOSet(sK478,X0))
| ~ latt_str(sK478) ),
inference(forward_subsumption_resolution,[],[f42437,f3736]) ).
fof(f42445,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(sK478))
| ~ latt_set_smaller(sK478,X0,X1)
| relstr_element_smaller(poset_of_lattice(sK478),X1,cast_to_el_of_LattPOSet(sK478,X0)) ),
inference(forward_subsumption_resolution,[],[f42442,f3734]) ).
fof(f42495,plain,
! [X0,X1] :
( ~ relstr_element_smaller(poset_of_lattice(sK478),X0,cast_to_el_of_LattPOSet(sK478,X1))
| ~ element(X1,the_carrier(sK478))
| empty_carrier(sK478)
| latt_set_smaller(sK478,X1,X0)
| ~ latt_str(sK478) ),
inference(resolution,[],[f3724,f3735]) ).
fof(f42500,plain,
! [X0,X1] :
( ~ relstr_element_smaller(poset_of_lattice(sK478),X0,cast_to_el_of_LattPOSet(sK478,X1))
| ~ element(X1,the_carrier(sK478))
| latt_set_smaller(sK478,X1,X0)
| ~ latt_str(sK478) ),
inference(forward_subsumption_resolution,[],[f42495,f3736]) ).
fof(f42503,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(sK478))
| ~ relstr_element_smaller(poset_of_lattice(sK478),X0,cast_to_el_of_LattPOSet(sK478,X1))
| latt_set_smaller(sK478,X1,X0) ),
inference(forward_subsumption_resolution,[],[f42500,f3734]) ).
fof(f76269,plain,
! [X0] :
( ~ latt_set_smaller(sK478,sK479,X0)
| relstr_element_smaller(poset_of_lattice(sK478),X0,cast_to_el_of_LattPOSet(sK478,sK479)) ),
inference(resolution,[],[f42445,f30599]) ).
fof(f76270,plain,
! [X0] :
( relstr_element_smaller(poset_of_lattice(sK478),X0,sK479)
| ~ latt_set_smaller(sK478,sK479,X0) ),
inference(forward_demodulation,[],[f76269,f30600]) ).
fof(f76424,plain,
! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK478),X0,cast_to_el_of_LattPOSet(sK478,sK479))
| latt_set_smaller(sK478,sK479,X0) ),
inference(resolution,[],[f42503,f30599]) ).
fof(f76425,plain,
! [X0] :
( ~ relstr_element_smaller(poset_of_lattice(sK478),X0,sK479)
| latt_set_smaller(sK478,sK479,X0) ),
inference(forward_demodulation,[],[f76424,f30600]) ).
fof(f76455,plain,
( ~ latt_set_smaller(sK478,sK479,sK477)
| ~ latt_set_smaller(sK478,sK479,sK477) ),
inference(resolution,[],[f76270,f26678]) ).
fof(f76456,plain,
~ latt_set_smaller(sK478,sK479,sK477),
inference(duplicate_literal_removal,[],[f76455]) ).
fof(f76595,plain,
( latt_set_smaller(sK478,sK479,sK477)
| latt_set_smaller(sK478,sK479,sK477) ),
inference(resolution,[],[f76425,f26679]) ).
fof(f76597,plain,
latt_set_smaller(sK478,sK479,sK477),
inference(duplicate_literal_removal,[],[f76595]) ).
fof(f76598,plain,
$false,
inference(forward_subsumption_resolution,[],[f76597,f76456]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU348+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n010.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 04:50:33 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 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
% 11.99/2.20 % (1561986)Will run a generic schedule for satisfiability detection.
% 11.99/2.20 % (1561992)% WARNING: option uhcvi not known.
% 11.99/2.20 % (1561992)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=911793266:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 11.99/2.20 % (1561991)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1393691618_2999 on theBenchmark for (2999ds/0Mi)
% 11.99/2.20 % (1561993)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4188479749:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 11.99/2.20 % (1561994)dis+10_1_sil=32000:sp=arity:random_seed=2463894774:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 11.99/2.20 % (1561995)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1271288917:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 11.99/2.20 % (1561996)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=562757300:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 11.99/2.20 % (1561997)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1064187155:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 11.99/2.20 % (1561994)Instruction limit reached!
% 11.99/2.20 % (1561994)------------------------------
% 11.99/2.20 % (1561994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.99/2.20 % (1561994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.20 % (1561994)CaDiCaL version: 2.1.3
% 11.99/2.20 % (1561994)Termination reason: Instruction limit
% 11.99/2.20 % (1561994)Termination phase: Saturation
% 11.99/2.20 % (1561994)Time elapsed: 0.056 s
% 11.99/2.20 % (1561994)Peak memory usage: 15 MB
% 11.99/2.20 % (1561994)Instructions burned: 104 (million)
% 11.99/2.20 % (1561995)Instruction limit reached!
% 11.99/2.20 % (1561995)------------------------------
% 11.99/2.20 % (1561995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.99/2.20 % (1561995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.20 % (1561995)CaDiCaL version: 2.1.3
% 11.99/2.20 % (1561995)Termination reason: Instruction limit
% 11.99/2.20 % (1561995)Termination phase: Blocked clause elimination
% 11.99/2.20 % (1561995)Time elapsed: 0.058 s
% 11.99/2.20 % (1561995)Peak memory usage: 14 MB
% 11.99/2.20 % (1561995)Instructions burned: 117 (million)
% 11.99/2.20 % (1561996)Instruction limit reached!
% 11.99/2.20 % (1561996)------------------------------
% 11.99/2.20 % (1561996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.99/2.20 % (1561996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.20 % (1561996)CaDiCaL version: 2.1.3
% 11.99/2.20 % (1561996)Termination reason: Instruction limit
% 11.99/2.20 % (1561996)Termination phase: Saturation
% 11.99/2.20 % (1561996)Time elapsed: 0.071 s
% 11.99/2.20 % (1561996)Peak memory usage: 15 MB
% 11.99/2.20 % (1561996)Instructions burned: 131 (million)
% 11.99/2.20 % (1562006)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2729093648:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 11.99/2.20 % (1562005)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1753825860:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 11.99/2.20 % (1562007)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=2006540679:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 11.99/2.20 % (1561997)Instruction limit reached!
% 11.99/2.20 % (1561997)------------------------------
% 11.99/2.20 % (1561997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.99/2.20 % (1561997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.99/2.20 % (1561997)CaDiCaL version: 2.1.3
% 11.99/2.20 % (1561997)Termination reason: Instruction limit
% 11.99/2.20 % (1561997)Termination phase: Saturation
% 11.99/2.20 % (1561997)Time elapsed: 0.092 s
% 11.99/2.20 % (1561997)Peak memory usage: 17 MB
% 11.99/2.20 % (1561997)Instructions burned: 160 (million)
% 11.99/2.20 % (1562011)ott-21_1_sil=16000:fs=off:random_seed=4095464403:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 11.99/2.20 % (1562006)Instruction limit reached!
% 11.99/2.20 % (1562006)------------------------------
% 11.99/2.20 % (1562006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.99/2.20 % (1562006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562006)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562006)Termination reason: Instruction limit
% 40.39/6.19 % (1562006)Termination phase: Saturation
% 40.39/6.19 % (1562006)Time elapsed: 0.069 s
% 40.39/6.19 % (1562006)Peak memory usage: 15 MB
% 40.39/6.19 % (1562006)Instructions burned: 131 (million)
% 40.39/6.19 % (1562013)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1930379194:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.39/6.19 % (1562011)Instruction limit reached!
% 40.39/6.19 % (1562011)------------------------------
% 40.39/6.19 % (1562011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.39/6.19 % (1562011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562011)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562011)Termination reason: Instruction limit
% 40.39/6.19 % (1562011)Termination phase: Saturation
% 40.39/6.19 % (1562011)Time elapsed: 0.093 s
% 40.39/6.19 % (1562011)Peak memory usage: 15 MB
% 40.39/6.19 % (1562011)Instructions burned: 181 (million)
% 40.39/6.19 % TRYING [1]
% 40.39/6.19 % (1562015)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2871172249:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 40.39/6.19 % TRYING [2]
% 40.39/6.19 % TRYING [1]
% 40.39/6.19 % TRYING [2]
% 40.39/6.19 % TRYING [3]
% 40.39/6.19 % TRYING [3]
% 40.39/6.19 % (1562005)Instruction limit reached!
% 40.39/6.19 % (1562005)------------------------------
% 40.39/6.19 % (1562005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.39/6.19 % (1562005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562005)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562005)Termination reason: Instruction limit
% 40.39/6.19 % (1562005)Termination phase: Finite model building constraint generation
% 40.39/6.19 % (1562005)Time elapsed: 0.309 s
% 40.39/6.19 % (1562005)Peak memory usage: 31 MB
% 40.39/6.19 % (1562005)Instructions burned: 715 (million)
% 40.39/6.19 % (1562017)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=545290290:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 40.39/6.19 % TRYING [1]
% 40.39/6.19 % TRYING [2]
% 40.39/6.19 % (1562007)Instruction limit reached!
% 40.39/6.19 % (1562007)------------------------------
% 40.39/6.19 % (1562007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.39/6.19 % (1562007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562007)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562007)Termination reason: Instruction limit
% 40.39/6.19 % (1562007)Termination phase: Saturation
% 40.39/6.19 % (1562007)Time elapsed: 0.385 s
% 40.39/6.19 % (1562007)Peak memory usage: 22 MB
% 40.39/6.19 % (1562007)Instructions burned: 685 (million)
% 40.39/6.19 % (1562013)Instruction limit reached!
% 40.39/6.19 % (1562013)------------------------------
% 40.39/6.19 % (1562013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.39/6.19 % (1562013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562013)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562013)Termination reason: Instruction limit
% 40.39/6.19 % (1562013)Termination phase: Saturation
% 40.39/6.19 % (1562013)Time elapsed: 0.310 s
% 40.39/6.19 % (1562013)Peak memory usage: 17 MB
% 40.39/6.19 % (1562013)Instructions burned: 477 (million)
% 40.39/6.19 % (1562019)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=468396303:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 40.39/6.19 % (1562020)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=4020490052: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)
% 40.39/6.19 % (1562015)Instruction limit reached!
% 40.39/6.19 % (1562015)------------------------------
% 40.39/6.19 % (1562015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.39/6.19 % (1562015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.39/6.19 % (1562015)CaDiCaL version: 2.1.3
% 40.39/6.19 % (1562015)Termination reason: Instruction limit
% 40.39/6.19 % (1562015)Termination phase: Finite model building SAT solving
% 40.39/6.19 % (1562015)Time elapsed: 0.426 s
% 40.39/6.19 % (1562015)Peak memory usage: 34 MB
% 40.39/6.19 % (1562015)Instructions burned: 865 (million)
% 40.39/6.19 % (1562023)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2662985248:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 40.39/6.19 % (1562020)Instruction limit reached!
% 40.39/6.19 % (1562020)------------------------------
% 40.39/6.19 % (1562020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562020)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562020)Termination reason: Instruction limit
% 91.92/13.43 % (1562020)Termination phase: Saturation
% 91.92/13.43 % (1562020)Time elapsed: 0.422 s
% 91.92/13.43 % (1562020)Peak memory usage: 27 MB
% 91.92/13.43 % (1562020)Instructions burned: 692 (million)
% 91.92/13.43 % (1562019)Instruction limit reached!
% 91.92/13.43 % (1562019)------------------------------
% 91.92/13.43 % (1562019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562019)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562019)Termination reason: Instruction limit
% 91.92/13.43 % (1562019)Termination phase: Finite model building constraint generation
% 91.92/13.43 % (1562019)Time elapsed: 0.423 s
% 91.92/13.43 % (1562019)Peak memory usage: 80 MB
% 91.92/13.43 % (1562019)Instructions burned: 891 (million)
% 91.92/13.43 % TRYING [4]
% 91.92/13.43 % (1562025)fmb+10_1_sil=64000:random_seed=3786232181:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 91.92/13.43 % (1562026)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3270026919:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 91.92/13.43 % (1562023)Instruction limit reached!
% 91.92/13.43 % (1562023)------------------------------
% 91.92/13.43 % (1562023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562023)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562023)Termination reason: Instruction limit
% 91.92/13.43 % (1562023)Termination phase: Saturation
% 91.92/13.43 % (1562023)Time elapsed: 0.400 s
% 91.92/13.43 % (1562023)Peak memory usage: 22 MB
% 91.92/13.43 % (1562023)Instructions burned: 880 (million)
% 91.92/13.43 % (1562029)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=303431442:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 91.92/13.43 % TRYING [1]
% 91.92/13.43 % TRYING [2]
% 91.92/13.43 % (1562017)Instruction limit reached!
% 91.92/13.43 % (1562017)------------------------------
% 91.92/13.43 % (1562017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562017)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562017)Termination reason: Instruction limit
% 91.92/13.43 % (1562017)Termination phase: Saturation
% 91.92/13.43 % (1562017)Time elapsed: 0.722 s
% 91.92/13.43 % (1562017)Peak memory usage: 30 MB
% 91.92/13.43 % (1562017)Instructions burned: 1180 (million)
% 91.92/13.43 % (1562026)Cannot represent all propositional literals internally
% 91.92/13.43 % (1562026)Refutation not found, incomplete strategy
% 91.92/13.43 % (1562026)------------------------------
% 91.92/13.43 % (1562026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562026)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562026)Termination reason: Refutation not found, incomplete strategy
% 91.92/13.43 % (1562026)Time elapsed: 0.191 s
% 91.92/13.43 % (1562026)Peak memory usage: 19 MB
% 91.92/13.43 % (1562026)Instructions burned: 388 (million)
% 91.92/13.43 % (1562026)------------------------------
% 91.92/13.43 % (1562026)------------------------------
% 91.92/13.43 % (1562031)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3927465426:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 91.92/13.43 % (1562032)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3087767566:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 91.92/13.43 % TRYING [8]
% 91.92/13.43 % TRYING [3]
% 91.92/13.43 % (1562029)Instruction limit reached!
% 91.92/13.43 % (1562029)------------------------------
% 91.92/13.43 % (1562029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.92/13.43 % (1562029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.92/13.43 % (1562029)CaDiCaL version: 2.1.3
% 91.92/13.43 % (1562029)Termination reason: Instruction limit
% 91.92/13.43 % (1562029)Termination phase: Finite model building constraint generation
% 91.92/13.43 % (1562029)Time elapsed: 0.377 s
% 91.92/13.43 % (1562029)Peak memory usage: 52 MB
% 91.92/13.43 % (1562029)Instructions burned: 924 (million)
% 91.92/13.43 % (1562035)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4046681765:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 91.92/13.43 % (1562035)Cannot represent all propositional literals internally
% 112.47/31.47 % (1562035)Refutation not found, incomplete strategy
% 112.47/31.47 % (1562035)------------------------------
% 112.47/31.47 % (1562035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562035)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562035)Termination reason: Refutation not found, incomplete strategy
% 112.47/31.47 % (1562035)Time elapsed: 0.226 s
% 112.47/31.47 % (1562035)Peak memory usage: 20 MB
% 112.47/31.47 % (1562035)Instructions burned: 453 (million)
% 112.47/31.47 % (1562035)------------------------------
% 112.47/31.47 % (1562035)------------------------------
% 112.47/31.47 % (1562037)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=910129014:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 112.47/31.47 % (1562032)Instruction limit reached!
% 112.47/31.47 % (1562032)------------------------------
% 112.47/31.47 % (1562032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562032)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562032)Termination reason: Instruction limit
% 112.47/31.47 % (1562032)Termination phase: Saturation
% 112.47/31.47 % (1562032)Time elapsed: 0.786 s
% 112.47/31.47 % (1562032)Peak memory usage: 29 MB
% 112.47/31.47 % (1562032)Instructions burned: 1474 (million)
% 112.47/31.47 % (1562039)ott-2_1_sil=16000:newcnf=on:random_seed=3606462966:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 112.47/31.47 % (1562039)Instruction limit reached!
% 112.47/31.47 % (1562039)------------------------------
% 112.47/31.47 % (1562039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562039)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562039)Termination reason: Instruction limit
% 112.47/31.47 % (1562039)Termination phase: Saturation
% 112.47/31.47 % (1562039)Time elapsed: 0.472 s
% 112.47/31.47 % (1562039)Peak memory usage: 19 MB
% 112.47/31.47 % (1562039)Instructions burned: 871 (million)
% 112.47/31.47 % (1562041)ott+10_1_sil=32000:tgt=ground:random_seed=247448060:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 112.47/31.47 % (1562037)Instruction limit reached!
% 112.47/31.47 % (1562037)------------------------------
% 112.47/31.47 % (1562037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562037)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562037)Termination reason: Instruction limit
% 112.47/31.47 % (1562037)Termination phase: Finite model building preprocessing
% 112.47/31.47 % (1562037)Time elapsed: 1.056 s
% 112.47/31.47 % (1562037)Peak memory usage: 40 MB
% 112.47/31.47 % (1562037)Instructions burned: 2174 (million)
% 112.47/31.47 % (1562043)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=197747726:i=54282_2971 on theBenchmark for (2971ds/54282Mi)
% 112.47/31.47 % TRYING [4]
% 112.47/31.47 % TRYING [1]
% 112.47/31.47 % TRYING [2]
% 112.47/31.47 % TRYING [3]
% 112.47/31.47 % TRYING [5]
% 112.47/31.47 % TRYING [4]
% 112.47/31.47 % (1562031)Instruction limit reached!
% 112.47/31.47 % (1562031)------------------------------
% 112.47/31.47 % (1562031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562031)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562031)Termination reason: Instruction limit
% 112.47/31.47 % (1562031)Termination phase: Saturation
% 112.47/31.47 % (1562031)Time elapsed: 2.985 s
% 112.47/31.47 % (1562031)Peak memory usage: 48 MB
% 112.47/31.47 % (1562031)Instructions burned: 5132 (million)
% 112.47/31.47 % (1562045)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1911066602:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 112.47/31.47 % (1562041)Instruction limit reached!
% 112.47/31.47 % (1562041)------------------------------
% 112.47/31.47 % (1562041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562041)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562041)Termination reason: Instruction limit
% 112.47/31.47 % (1562041)Termination phase: Saturation
% 112.47/31.47 % (1562041)Time elapsed: 3.223 s
% 112.47/31.47 % (1562041)Peak memory usage: 74 MB
% 112.47/31.47 % (1562041)Instructions burned: 5115 (million)
% 112.47/31.47 % (1562047)dis+21_1_sil=32000:sas=cadical:random_seed=2270264027:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 112.47/31.47 % (1562045)Instruction limit reached!
% 112.47/31.47 % (1562045)------------------------------
% 112.47/31.47 % (1562045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562045)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562045)Termination reason: Instruction limit
% 112.47/31.47 % (1562045)Termination phase: Saturation
% 112.47/31.47 % (1562045)Time elapsed: 2.128 s
% 112.47/31.47 % (1562045)Peak memory usage: 43 MB
% 112.47/31.47 % (1562045)Instructions burned: 3512 (million)
% 112.47/31.47 % TRYING [5]
% 112.47/31.47 % (1562049)ott+11_1_sil=16000:gs=on:random_seed=3363459255:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 112.47/31.47 % (1562049)Instruction limit reached!
% 112.47/31.47 % (1562049)------------------------------
% 112.47/31.47 % (1562049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562049)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562049)Termination reason: Instruction limit
% 112.47/31.47 % (1562049)Termination phase: Saturation
% 112.47/31.47 % (1562049)Time elapsed: 1.235 s
% 112.47/31.47 % (1562049)Peak memory usage: 34 MB
% 112.47/31.47 % (1562049)Instructions burned: 2251 (million)
% 112.47/31.47 % (1562051)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3430907893:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 112.47/31.47 % (1562047)Instruction limit reached!
% 112.47/31.47 % (1562047)------------------------------
% 112.47/31.47 % (1562047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562047)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562047)Termination reason: Instruction limit
% 112.47/31.47 % (1562047)Termination phase: Saturation
% 112.47/31.47 % (1562047)Time elapsed: 2.270 s
% 112.47/31.47 % (1562047)Peak memory usage: 46 MB
% 112.47/31.47 % (1562047)Instructions burned: 3774 (million)
% 112.47/31.47 % (1562053)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1244288277:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2919 on theBenchmark for (2919ds/4591Mi)
% 112.47/31.47 % TRYING [7]
% 112.47/31.47 % TRYING [5]
% 112.47/31.47 % (1562053)Instruction limit reached!
% 112.47/31.47 % (1562053)------------------------------
% 112.47/31.47 % (1562053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562053)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562053)Termination reason: Instruction limit
% 112.47/31.47 % (1562053)Termination phase: Saturation
% 112.47/31.47 % (1562053)Time elapsed: 2.503 s
% 112.47/31.47 % (1562053)Peak memory usage: 69 MB
% 112.47/31.47 % (1562053)Instructions burned: 4592 (million)
% 112.47/31.47 % (1562055)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2055627163:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 112.47/31.47 % (1562025)Instruction limit reached!
% 112.47/31.47 % (1562025)------------------------------
% 112.47/31.47 % (1562025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562025)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562025)Termination reason: Instruction limit
% 112.47/31.47 % (1562025)Termination phase: Finite model building constraint generation
% 112.47/31.47 % (1562025)Time elapsed: 9.677 s
% 112.47/31.47 % (1562025)Peak memory usage: 291 MB
% 112.47/31.47 % (1562025)Instructions burned: 22062 (million)
% 112.47/31.47 % (1562057)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1969008246:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 112.47/31.47 % TRYING [6]
% 112.47/31.47 % (1562057)Instruction limit reached!
% 112.47/31.47 % (1562057)------------------------------
% 112.47/31.47 % (1562057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562057)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562057)Termination reason: Instruction limit
% 112.47/31.47 % (1562057)Termination phase: Saturation
% 112.47/31.47 % (1562057)Time elapsed: 2.257 s
% 112.47/31.47 % (1562057)Peak memory usage: 52 MB
% 112.47/31.47 % (1562057)Instructions burned: 5212 (million)
% 112.47/31.47 % (1562059)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1064583247:i=5497:nm=2_2870 on theBenchmark for (2870ds/5497Mi)
% 112.47/31.47 % TRYING [17]
% 112.47/31.47 % (1562059)Instruction limit reached!
% 112.47/31.47 % (1562059)------------------------------
% 112.47/31.47 % (1562059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562059)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562059)Termination reason: Instruction limit
% 112.47/31.47 % (1562059)Termination phase: Finite model building constraint generation
% 112.47/31.47 % (1562059)Time elapsed: 1.946 s
% 112.47/31.47 % (1562059)Peak memory usage: 338 MB
% 112.47/31.47 % (1562059)Instructions burned: 5498 (million)
% 112.47/31.47 % TRYING [6]
% 112.47/31.47 % (1562061)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2432724223:fmbsr=2:i=46332_2850 on theBenchmark for (2850ds/46332Mi)
% 112.47/31.47 % TRYING [15]
% 112.47/31.47 % (1562043)Instruction limit reached!
% 112.47/31.47 % (1562043)------------------------------
% 112.47/31.47 % (1562043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562043)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562043)Termination reason: Instruction limit
% 112.47/31.47 % (1562043)Termination phase: Finite model building constraint generation
% 112.47/31.47 % (1562043)Time elapsed: 19.176 s
% 112.47/31.47 % (1562043)Peak memory usage: 1367 MB
% 112.47/31.47 % (1562043)Instructions burned: 54282 (million)
% 112.47/31.47 % (1562063)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2370724160:i=14071_2777 on theBenchmark for (2777ds/14071Mi)
% 112.47/31.47 % TRYING [12]
% 112.47/31.47 % (1562063)Instruction limit reached!
% 112.47/31.47 % (1562063)------------------------------
% 112.47/31.47 % (1562063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562063)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562063)Termination reason: Instruction limit
% 112.47/31.47 % (1562063)Termination phase: Finite model building constraint generation
% 112.47/31.47 % (1562063)Time elapsed: 4.664 s
% 112.47/31.47 % (1562063)Peak memory usage: 614 MB
% 112.47/31.47 % (1562063)Instructions burned: 14072 (million)
% 112.47/31.47 % (1562055)Instruction limit reached!
% 112.47/31.47 % (1562055)------------------------------
% 112.47/31.47 % (1562055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562055)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562055)Termination reason: Instruction limit
% 112.47/31.47 % (1562055)Termination phase: Saturation
% 112.47/31.47 % (1562055)Time elapsed: 16.357 s
% 112.47/31.47 % (1562055)Peak memory usage: 625 MB
% 112.47/31.47 % (1562055)Instructions burned: 29341 (million)
% 112.47/31.47 % (1562065)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=460092641:i=22565:add=on:rawr=on_2730 on theBenchmark for (2730ds/22565Mi)
% 112.47/31.47 % (1562067)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2444184578:i=8173:av=off_2729 on theBenchmark for (2729ds/8173Mi)
% 112.47/31.47 % (1562067) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1561986-1562067"...
% 112.47/31.47 % (1562067)...printing done.
% 112.47/31.47 % (1562067)Refutation found. Thanks to Tanya!
% 112.47/31.47 % SZS status Theorem for theBenchmark
% 112.47/31.47 % SZS output start Proof for theBenchmark
% See solution above
% 112.47/31.47 % (1562067)------------------------------
% 112.47/31.47 % (1562067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.47/31.47 % (1562067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.47/31.47 % (1562067)CaDiCaL version: 2.1.3
% 112.47/31.47 % (1562067)Termination reason: Refutation
% 112.47/31.47 % (1562067)Time elapsed: 3.495 s
% 112.47/31.47 % (1562067)Peak memory usage: 93 MB
% 112.47/31.47 % (1562067)Instructions burned: 5885 (million)
% 112.47/31.47 % (1561986)Success in time 31.054 s
% 112.47/31.47 % Vampire exiting
%------------------------------------------------------------------------------