%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU291+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 : n002.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:44 PM UTC 2026
% Result : Theorem 15.42s 6.27s
% Output : Refutation 15.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 15
% Syntax : Number of formulae : 111 ( 30 unt; 0 def)
% Number of atoms : 345 ( 109 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 372 ( 138 ~; 141 |; 67 &)
% ( 10 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 171 ( 157 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(f27,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> ( ( ( X1 = empty_set
=> X0 = empty_set )
=> ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) ) )
& ( X1 = empty_set
=> ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f37,axiom,
! [X0] :
( X0 = empty_set
<=> ! [X1] : ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f45,axiom,
! [X0,X1,X2] :
( X2 = set_union2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
| in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f143,axiom,
! [X0,X1] :
( ~ empty(X0)
=> ~ empty(set_union2(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_xboole_0) ).
fof(f146,axiom,
( empty(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f196,axiom,
! [X0,X1,X2] :
( relation_of2(X2,X0,X1)
=> relation_dom_as_subset(X0,X1,X2) = relation_dom(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f201,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
<=> relation_of2(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f238,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> ( subset(relation_dom(X2),X0)
& subset(relation_rng(X2),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_relset_1) ).
fof(f239,axiom,
! [X0,X1] :
( subset(X0,X1)
=> set_union2(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(f249,axiom,
! [X0,X1,X2,X3] :
( relation_of2_as_subset(X3,X2,X0)
=> ( subset(relation_rng(X3),X1)
=> relation_of2_as_subset(X3,X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t14_relset_1) ).
fof(f264,axiom,
! [X0,X1,X2] :
( ( subset(X0,X1)
& subset(X1,X2) )
=> subset(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f356,axiom,
! [X0] :
( empty(X0)
=> X0 = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f366,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& ! [X2] :
~ ( in(X2,X1)
& ! [X3] :
~ ( in(X3,X1)
& in(X3,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_tarski) ).
fof(f382,conjecture,
! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( subset(X1,X2)
=> ( ( X1 = empty_set
& X0 != empty_set )
| ( function(X3)
& quasi_total(X3,X0,X2)
& relation_of2_as_subset(X3,X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_funct_2) ).
fof(f383,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( subset(X1,X2)
=> ( ( X1 = empty_set
& X0 != empty_set )
| ( function(X3)
& quasi_total(X3,X0,X2)
& relation_of2_as_subset(X3,X0,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f382]) ).
fof(f440,plain,
! [X0,X1,X2] :
( ( ( ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f441,plain,
! [X0,X1,X2] :
( ( ( ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(flattening,[],[f440]) ).
fof(f520,plain,
! [X0,X1] :
( ~ empty(set_union2(X1,X0))
| empty(X0) ),
inference(ennf_transformation,[],[f143]) ).
fof(f559,plain,
! [X0,X1,X2] :
( relation_dom_as_subset(X0,X1,X2) = relation_dom(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f196]) ).
fof(f612,plain,
! [X0,X1,X2] :
( ( subset(relation_dom(X2),X0)
& subset(relation_rng(X2),X1) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f238]) ).
fof(f613,plain,
! [X0,X1] :
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(ennf_transformation,[],[f239]) ).
fof(f627,plain,
! [X0,X1,X2,X3] :
( relation_of2_as_subset(X3,X2,X1)
| ~ subset(relation_rng(X3),X1)
| ~ relation_of2_as_subset(X3,X2,X0) ),
inference(ennf_transformation,[],[f249]) ).
fof(f628,plain,
! [X0,X1,X2,X3] :
( relation_of2_as_subset(X3,X2,X1)
| ~ subset(relation_rng(X3),X1)
| ~ relation_of2_as_subset(X3,X2,X0) ),
inference(flattening,[],[f627]) ).
fof(f646,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(ennf_transformation,[],[f264]) ).
fof(f647,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(flattening,[],[f646]) ).
fof(f759,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(ennf_transformation,[],[f356]) ).
fof(f770,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ? [X2] :
( in(X2,X1)
& ! [X3] :
( ~ in(X3,X1)
| ~ in(X3,X2) ) ) ),
inference(ennf_transformation,[],[f366]) ).
fof(f785,plain,
? [X0,X1,X2,X3] :
( ( empty_set != X1
| empty_set = X0 )
& ( ~ function(X3)
| ~ quasi_total(X3,X0,X2)
| ~ relation_of2_as_subset(X3,X0,X2) )
& subset(X1,X2)
& function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) ),
inference(ennf_transformation,[],[f383]) ).
fof(f786,plain,
? [X0,X1,X2,X3] :
( ( empty_set != X1
| empty_set = X0 )
& ( ~ function(X3)
| ~ quasi_total(X3,X0,X2)
| ~ relation_of2_as_subset(X3,X0,X2) )
& subset(X1,X2)
& function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) ),
inference(flattening,[],[f785]) ).
fof(f863,plain,
! [X0,X1,X2] :
( ( ( ( ( quasi_total(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) != X0 )
& ( X0 = relation_dom_as_subset(X0,X1,X2)
| ~ quasi_total(X2,X0,X1) ) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( ( quasi_total(X2,X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| ~ quasi_total(X2,X0,X1) ) )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(nnf_transformation,[],[f441]) ).
fof(f888,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X1] : ~ in(X1,X0)
| empty_set != X0 ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f889,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(rectify,[],[f888]) ).
fof(f890,plain,
! [X0] :
( ( X0 = empty_set
| in(sK56(X0),X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X1,sK56(X0))],[f889]) ).
fof(f911,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f45]) ).
fof(f912,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(flattening,[],[f911]) ).
fof(f913,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(rectify,[],[f912]) ).
fof(f914,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ( ( ( ~ in(sK66(X0,X1,X2),X0)
& ~ in(sK66(X0,X1,X2),X1) )
| ~ in(sK66(X0,X1,X2),X2) )
& ( in(sK66(X0,X1,X2),X0)
| in(sK66(X0,X1,X2),X1)
| in(sK66(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(X3,sK66(X0,X1,X2))],[f913]) ).
fof(f1033,plain,
! [X0,X1,X2] :
( ( relation_of2_as_subset(X2,X0,X1)
| ~ relation_of2(X2,X0,X1) )
& ( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f201]) ).
fof(f1207,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ( in(sK272(X1),X1)
& ! [X3] :
( ~ in(X3,X1)
| ~ in(X3,sK272(X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK272]),skolemize(X2,sK272(X1))],[f770]) ).
fof(f1214,plain,
( ( empty_set != sK274
| empty_set = sK273 )
& ( ~ function(sK276)
| ~ quasi_total(sK276,sK273,sK275)
| ~ relation_of2_as_subset(sK276,sK273,sK275) )
& subset(sK274,sK275)
& function(sK276)
& quasi_total(sK276,sK273,sK274)
& relation_of2_as_subset(sK276,sK273,sK274) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK273,sK274,sK275,sK276]),skolemize(X0,sK273),skolemize(X1,sK274),skolemize(X2,sK275),skolemize(X3,sK276)],[f786]) ).
fof(f1231,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f1301,plain,
! [X2,X0,X1] :
( ~ quasi_total(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) = X0
| empty_set = X1
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f863]) ).
fof(f1303,plain,
! [X2,X0,X1] :
( relation_dom_as_subset(X0,X1,X2) != X0
| quasi_total(X2,X0,X1)
| empty_set = X1
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f863]) ).
fof(f1342,plain,
! [X2,X0] :
( ~ in(X2,X0)
| empty_set != X0 ),
inference(cnf_transformation,[],[f890]) ).
fof(f1343,plain,
! [X0] :
( in(sK56(X0),X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f890]) ).
fof(f1375,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f914]) ).
fof(f1585,plain,
! [X0,X1] :
( ~ empty(set_union2(X1,X0))
| empty(X0) ),
inference(cnf_transformation,[],[f520]) ).
fof(f1592,plain,
empty(empty_set),
inference(cnf_transformation,[],[f146]) ).
fof(f1700,plain,
! [X2,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) = relation_dom(X2) ),
inference(cnf_transformation,[],[f559]) ).
fof(f1705,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f1033]) ).
fof(f1933,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| subset(relation_rng(X2),X1) ),
inference(cnf_transformation,[],[f612]) ).
fof(f1934,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| subset(relation_dom(X2),X0) ),
inference(cnf_transformation,[],[f612]) ).
fof(f1935,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_union2(X0,X1) = X1 ),
inference(cnf_transformation,[],[f613]) ).
fof(f1951,plain,
! [X2,X3,X0,X1] :
( ~ relation_of2_as_subset(X3,X2,X0)
| ~ subset(relation_rng(X3),X1)
| relation_of2_as_subset(X3,X2,X1) ),
inference(cnf_transformation,[],[f628]) ).
fof(f1972,plain,
! [X2,X0,X1] :
( ~ subset(X1,X2)
| ~ subset(X0,X1)
| subset(X0,X2) ),
inference(cnf_transformation,[],[f647]) ).
fof(f2134,plain,
! [X0] :
( ~ empty(X0)
| empty_set = X0 ),
inference(cnf_transformation,[],[f759]) ).
fof(f2149,plain,
! [X0,X1] :
( ~ in(X0,X1)
| in(sK272(X1),X1) ),
inference(cnf_transformation,[],[f1207]) ).
fof(f2171,plain,
relation_of2_as_subset(sK276,sK273,sK274),
inference(cnf_transformation,[],[f1214]) ).
fof(f2172,plain,
quasi_total(sK276,sK273,sK274),
inference(cnf_transformation,[],[f1214]) ).
fof(f2173,plain,
function(sK276),
inference(cnf_transformation,[],[f1214]) ).
fof(f2174,plain,
subset(sK274,sK275),
inference(cnf_transformation,[],[f1214]) ).
fof(f2175,plain,
( ~ function(sK276)
| ~ quasi_total(sK276,sK273,sK275)
| ~ relation_of2_as_subset(sK276,sK273,sK275) ),
inference(cnf_transformation,[],[f1214]) ).
fof(f2176,plain,
( empty_set != sK274
| empty_set = sK273 ),
inference(cnf_transformation,[],[f1214]) ).
fof(f2525,plain,
! [X2] : ~ in(X2,empty_set),
inference(equality_resolution,[],[f1342]) ).
fof(f2539,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X0) ),
inference(equality_resolution,[],[f1375]) ).
fof(f2639,plain,
( ~ quasi_total(sK276,sK273,sK275)
| ~ relation_of2_as_subset(sK276,sK273,sK275) ),
inference(forward_subsumption_resolution,[],[f2175,f2173]) ).
fof(f3424,plain,
subset(relation_rng(sK276),sK274),
inference(resolution,[],[f1933,f2171]) ).
fof(f3427,plain,
subset(relation_dom(sK276),sK273),
inference(resolution,[],[f1934,f2171]) ).
fof(f3436,plain,
sK273 = set_union2(relation_dom(sK276),sK273),
inference(resolution,[],[f1935,f3427]) ).
fof(f3444,plain,
sK275 = set_union2(sK274,sK275),
inference(resolution,[],[f1935,f2174]) ).
fof(f3450,plain,
sK273 = set_union2(sK273,relation_dom(sK276)),
inference(forward_demodulation,[],[f3436,f1231]) ).
fof(f3610,plain,
( empty(relation_dom(sK276))
| ~ empty(sK273) ),
inference(superposition,[],[f1585,f3450]) ).
fof(f3651,plain,
( ~ empty(sK273)
| empty_set = relation_dom(sK276) ),
inference(resolution,[],[f3610,f2134]) ).
fof(f4091,plain,
relation_of2(sK276,sK273,sK274),
inference(resolution,[],[f1705,f2171]) ).
fof(f4223,plain,
! [X0] :
( ~ in(X0,sK274)
| in(X0,sK275) ),
inference(superposition,[],[f2539,f3444]) ).
fof(f4226,plain,
( in(sK56(sK274),sK275)
| empty_set = sK274 ),
inference(resolution,[],[f4223,f1343]) ).
fof(f4607,plain,
! [X0] :
( ~ subset(X0,sK274)
| subset(X0,sK275) ),
inference(resolution,[],[f1972,f2174]) ).
fof(f4641,plain,
subset(relation_rng(sK276),sK275),
inference(resolution,[],[f4607,f3424]) ).
fof(f6615,plain,
( in(sK272(sK275),sK275)
| empty_set = sK274 ),
inference(resolution,[],[f4226,f2149]) ).
fof(f8300,plain,
relation_dom(sK276) = relation_dom_as_subset(sK273,sK274,sK276),
inference(resolution,[],[f1700,f4091]) ).
fof(f8936,plain,
! [X0] :
( ~ subset(relation_rng(sK276),X0)
| relation_of2_as_subset(sK276,sK273,X0) ),
inference(resolution,[],[f1951,f2171]) ).
fof(f17245,plain,
( sK273 = relation_dom_as_subset(sK273,sK274,sK276)
| empty_set = sK274
| ~ relation_of2_as_subset(sK276,sK273,sK274) ),
inference(resolution,[],[f1301,f2172]) ).
fof(f17248,plain,
( sK273 = relation_dom_as_subset(sK273,sK274,sK276)
| empty_set = sK274 ),
inference(forward_subsumption_resolution,[],[f17245,f2171]) ).
fof(f17250,plain,
( sK273 = relation_dom(sK276)
| empty_set = sK274 ),
inference(forward_demodulation,[],[f17248,f8300]) ).
fof(f28410,plain,
relation_of2_as_subset(sK276,sK273,sK275),
inference(resolution,[],[f8936,f4641]) ).
fof(f28698,plain,
relation_of2(sK276,sK273,sK275),
inference(resolution,[],[f28410,f1705]) ).
fof(f28967,plain,
relation_dom(sK276) = relation_dom_as_subset(sK273,sK275,sK276),
inference(resolution,[],[f28698,f1700]) ).
fof(f33501,plain,
( sK273 != relation_dom(sK276)
| quasi_total(sK276,sK273,sK275)
| empty_set = sK275
| ~ relation_of2_as_subset(sK276,sK273,sK275) ),
inference(superposition,[],[f1303,f28967]) ).
fof(f33503,plain,
( sK273 != relation_dom(sK276)
| empty_set = sK275
| ~ relation_of2_as_subset(sK276,sK273,sK275) ),
inference(forward_subsumption_resolution,[],[f33501,f2639]) ).
fof(f33505,plain,
( sK273 != relation_dom(sK276)
| empty_set = sK275 ),
inference(forward_subsumption_resolution,[],[f33503,f28410]) ).
fof(f34341,plain,
( sK273 != sK273
| empty_set = sK275
| empty_set = sK274 ),
inference(superposition,[],[f33505,f17250]) ).
fof(f34342,plain,
( empty_set = sK275
| empty_set = sK274 ),
inference(trivial_inequality_removal,[],[f34341]) ).
fof(f34779,plain,
( in(sK272(empty_set),empty_set)
| empty_set = sK274
| empty_set = sK274 ),
inference(superposition,[],[f6615,f34342]) ).
fof(f34820,plain,
( in(sK272(empty_set),empty_set)
| empty_set = sK274 ),
inference(duplicate_literal_removal,[],[f34779]) ).
fof(f34852,plain,
empty_set = sK274,
inference(forward_subsumption_resolution,[],[f34820,f2525]) ).
fof(f35018,plain,
relation_of2_as_subset(sK276,sK273,empty_set),
inference(superposition,[],[f2171,f34852]) ).
fof(f35019,plain,
quasi_total(sK276,sK273,empty_set),
inference(superposition,[],[f2172,f34852]) ).
fof(f35021,plain,
( empty_set != empty_set
| empty_set = sK273 ),
inference(superposition,[],[f2176,f34852]) ).
fof(f35156,plain,
empty_set = sK273,
inference(trivial_inequality_removal,[],[f35021]) ).
fof(f35202,plain,
quasi_total(sK276,empty_set,empty_set),
inference(forward_demodulation,[],[f35019,f35156]) ).
fof(f35203,plain,
relation_of2_as_subset(sK276,empty_set,empty_set),
inference(forward_demodulation,[],[f35018,f35156]) ).
fof(f35532,plain,
( ~ empty(empty_set)
| empty_set = relation_dom(sK276) ),
inference(superposition,[],[f3651,f35156]) ).
fof(f35601,plain,
empty_set = relation_dom(sK276),
inference(forward_subsumption_resolution,[],[f35532,f1592]) ).
fof(f39044,plain,
( empty_set != sK273
| empty_set = sK275 ),
inference(superposition,[],[f33505,f35601]) ).
fof(f39101,plain,
empty_set = sK275,
inference(forward_subsumption_resolution,[],[f39044,f35156]) ).
fof(f39250,plain,
( ~ quasi_total(sK276,sK273,empty_set)
| ~ relation_of2_as_subset(sK276,sK273,empty_set) ),
inference(superposition,[],[f2639,f39101]) ).
fof(f39528,plain,
( ~ quasi_total(sK276,empty_set,empty_set)
| ~ relation_of2_as_subset(sK276,sK273,empty_set) ),
inference(forward_demodulation,[],[f39250,f35156]) ).
fof(f39620,plain,
~ relation_of2_as_subset(sK276,sK273,empty_set),
inference(forward_subsumption_resolution,[],[f39528,f35202]) ).
fof(f39621,plain,
~ relation_of2_as_subset(sK276,empty_set,empty_set),
inference(forward_demodulation,[],[f39620,f35156]) ).
fof(f39622,plain,
$false,
inference(forward_subsumption_resolution,[],[f39621,f35203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU291+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.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 04:34:22 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/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
% 16.06/2.78 % (4146530)Will run a generic schedule for satisfiability detection.
% 16.06/2.78 % (4146539)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2445388786:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.06/2.78 % (4146536)% WARNING: option uhcvi not known.
% 16.06/2.78 % (4146535)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3177631629_2999 on theBenchmark for (2999ds/0Mi)
% 16.06/2.78 % (4146536)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1588471975:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.06/2.78 % (4146537)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2068450031:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.06/2.78 % (4146538)dis+10_1_sil=32000:sp=arity:random_seed=2987730910:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.06/2.78 % (4146540)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2474214925:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.06/2.78 % (4146541)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=159428524:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.06/2.78 % (4146539)Instruction limit reached!
% 16.06/2.78 % (4146539)------------------------------
% 16.06/2.78 % (4146539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.06/2.78 % (4146539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/2.78 % (4146539)CaDiCaL version: 2.1.3
% 16.06/2.78 % (4146539)Termination reason: Instruction limit
% 16.06/2.78 % (4146539)Termination phase: Saturation
% 16.06/2.78 % (4146539)Time elapsed: 0.032 s
% 16.06/2.78 % (4146539)Peak memory usage: 13 MB
% 16.06/2.78 % (4146539)Instructions burned: 116 (million)
% 16.06/2.78 % (4146549)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4020248329:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.06/2.78 % (4146538)Instruction limit reached!
% 16.06/2.78 % (4146538)------------------------------
% 16.06/2.78 % (4146538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.06/2.78 % (4146538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/2.78 % (4146538)CaDiCaL version: 2.1.3
% 16.06/2.78 % (4146538)Termination reason: Instruction limit
% 16.06/2.78 % (4146538)Termination phase: Saturation
% 16.06/2.78 % (4146538)Time elapsed: 0.065 s
% 16.06/2.78 % (4146538)Peak memory usage: 14 MB
% 16.06/2.78 % (4146538)Instructions burned: 103 (million)
% 16.06/2.78 % (4146540)Instruction limit reached!
% 16.06/2.78 % (4146540)------------------------------
% 16.06/2.78 % (4146540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.06/2.78 % (4146540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/2.78 % (4146540)CaDiCaL version: 2.1.3
% 16.06/2.78 % (4146540)Termination reason: Instruction limit
% 16.06/2.78 % (4146540)Termination phase: Saturation
% 16.06/2.78 % (4146540)Time elapsed: 0.075 s
% 16.06/2.78 % (4146540)Peak memory usage: 14 MB
% 16.06/2.78 % (4146540)Instructions burned: 131 (million)
% 16.06/2.78 % (4146551)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3716614401:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.06/2.78 % TRYING [1]
% 16.06/2.78 % TRYING [2]
% 16.06/2.78 % (4146541)Instruction limit reached!
% 16.06/2.78 % (4146541)------------------------------
% 16.06/2.78 % (4146541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.06/2.78 % (4146541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/2.78 % (4146541)CaDiCaL version: 2.1.3
% 16.06/2.78 % (4146541)Termination reason: Instruction limit
% 16.06/2.78 % (4146541)Termination phase: Saturation
% 16.06/2.78 % (4146541)Time elapsed: 0.094 s
% 16.06/2.78 % (4146541)Peak memory usage: 15 MB
% 16.06/2.78 % (4146541)Instructions burned: 159 (million)
% 16.06/2.78 % (4146552)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=331764024:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.06/2.78 % (4146555)ott-21_1_sil=16000:fs=off:random_seed=2072509202:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.06/2.78 % TRYING [1]
% 16.06/2.78 % TRYING [3]
% 16.06/2.78 % TRYING [2]
% 16.06/2.78 % (4146551)Instruction limit reached!
% 16.06/2.78 % (4146551)------------------------------
% 16.06/2.78 % (4146551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.06/2.78 % (4146551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146551)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146551)Termination reason: Instruction limit
% 15.42/6.27 % (4146551)Termination phase: Saturation
% 15.42/6.27 % (4146551)Time elapsed: 0.074 s
% 15.42/6.27 % (4146551)Peak memory usage: 14 MB
% 15.42/6.27 % (4146551)Instructions burned: 131 (million)
% 15.42/6.27 % (4146557)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1785475774:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 15.42/6.27 % TRYING [3]
% 15.42/6.27 % (4146549)Instruction limit reached!
% 15.42/6.27 % (4146549)------------------------------
% 15.42/6.27 % (4146549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146549)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146549)Termination reason: Instruction limit
% 15.42/6.27 % (4146549)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146549)Time elapsed: 0.163 s
% 15.42/6.27 % (4146549)Peak memory usage: 45 MB
% 15.42/6.27 % (4146549)Instructions burned: 716 (million)
% 15.42/6.27 % (4146555)Instruction limit reached!
% 15.42/6.27 % (4146555)------------------------------
% 15.42/6.27 % (4146555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146555)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146555)Termination reason: Instruction limit
% 15.42/6.27 % (4146555)Termination phase: Saturation
% 15.42/6.27 % (4146555)Time elapsed: 0.096 s
% 15.42/6.27 % (4146555)Peak memory usage: 14 MB
% 15.42/6.27 % (4146555)Instructions burned: 181 (million)
% 15.42/6.27 % (4146559)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2280673585:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.42/6.27 % (4146560)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2037077915:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 15.42/6.27 % TRYING [1]
% 15.42/6.27 % TRYING [2]
% 15.42/6.27 % TRYING [3]
% 15.42/6.27 % (4146559)Instruction limit reached!
% 15.42/6.27 % (4146559)------------------------------
% 15.42/6.27 % (4146559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146559)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146559)Termination reason: Instruction limit
% 15.42/6.27 % (4146559)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146559)Time elapsed: 0.201 s
% 15.42/6.27 % (4146559)Peak memory usage: 39 MB
% 15.42/6.27 % (4146559)Instructions burned: 867 (million)
% 15.42/6.27 % (4146563)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1862905242:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 15.42/6.27 % (4146552)Instruction limit reached!
% 15.42/6.27 % (4146552)------------------------------
% 15.42/6.27 % (4146552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146552)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146552)Termination reason: Instruction limit
% 15.42/6.27 % (4146552)Termination phase: Saturation
% 15.42/6.27 % (4146552)Time elapsed: 0.392 s
% 15.42/6.27 % (4146552)Peak memory usage: 20 MB
% 15.42/6.27 % (4146552)Instructions burned: 684 (million)
% 15.42/6.27 % (4146565)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=3338637973: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)
% 15.42/6.27 % (4146557)Instruction limit reached!
% 15.42/6.27 % (4146557)------------------------------
% 15.42/6.27 % (4146557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146557)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146557)Termination reason: Instruction limit
% 15.42/6.27 % (4146557)Termination phase: Saturation
% 15.42/6.27 % (4146557)Time elapsed: 0.328 s
% 15.42/6.27 % (4146557)Peak memory usage: 15 MB
% 15.42/6.27 % (4146557)Instructions burned: 477 (million)
% 15.42/6.27 % (4146567)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=396947546:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 15.42/6.27 % TRYING [4]
% 15.42/6.27 % (4146563)Instruction limit reached!
% 15.42/6.27 % (4146563)------------------------------
% 15.42/6.27 % (4146563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146563)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146563)Termination reason: Instruction limit
% 15.42/6.27 % (4146563)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146563)Time elapsed: 0.245 s
% 15.42/6.27 % (4146563)Peak memory usage: 97 MB
% 15.42/6.27 % (4146563)Instructions burned: 895 (million)
% 15.42/6.27 % (4146569)fmb+10_1_sil=64000:random_seed=3592275974:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 15.42/6.27 % TRYING [1]
% 15.42/6.27 % TRYING [2]
% 15.42/6.27 % TRYING [3]
% 15.42/6.27 % (4146565)Instruction limit reached!
% 15.42/6.27 % (4146565)------------------------------
% 15.42/6.27 % (4146565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146565)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146565)Termination reason: Instruction limit
% 15.42/6.27 % (4146565)Termination phase: Saturation
% 15.42/6.27 % (4146565)Time elapsed: 0.443 s
% 15.42/6.27 % (4146565)Peak memory usage: 24 MB
% 15.42/6.27 % (4146565)Instructions burned: 692 (million)
% 15.42/6.27 % (4146560)Instruction limit reached!
% 15.42/6.27 % (4146560)------------------------------
% 15.42/6.27 % (4146560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146560)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146560)Termination reason: Instruction limit
% 15.42/6.27 % (4146560)Termination phase: Saturation
% 15.42/6.27 % (4146560)Time elapsed: 0.732 s
% 15.42/6.27 % (4146560)Peak memory usage: 28 MB
% 15.42/6.27 % (4146560)Instructions burned: 1179 (million)
% 15.42/6.27 % (4146571)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2560647493:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 15.42/6.27 % (4146572)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2704692240:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 15.42/6.27 % (4146567)Instruction limit reached!
% 15.42/6.27 % (4146567)------------------------------
% 15.42/6.27 % (4146567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146567)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146567)Termination reason: Instruction limit
% 15.42/6.27 % (4146567)Termination phase: Saturation
% 15.42/6.27 % (4146567)Time elapsed: 0.460 s
% 15.42/6.27 % (4146567)Peak memory usage: 22 MB
% 15.42/6.27 % (4146567)Instructions burned: 879 (million)
% 15.42/6.27 % (4146575)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1931087514:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 15.42/6.27 % TRYING [20]
% 15.42/6.27 % TRYING [8]
% 15.42/6.27 % TRYING [4]
% 15.42/6.27 % (4146572)Instruction limit reached!
% 15.42/6.27 % (4146572)------------------------------
% 15.42/6.27 % (4146572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146572)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146572)Termination reason: Instruction limit
% 15.42/6.27 % (4146572)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146572)Time elapsed: 0.344 s
% 15.42/6.27 % (4146572)Peak memory usage: 57 MB
% 15.42/6.27 % (4146572)Instructions burned: 923 (million)
% 15.42/6.27 % (4146577)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2359917296:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 15.42/6.27 % TRYING [5]
% 15.42/6.27 % (4146577)Instruction limit reached!
% 15.42/6.27 % (4146577)------------------------------
% 15.42/6.27 % (4146577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146577)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146577)Termination reason: Instruction limit
% 15.42/6.27 % (4146577)Termination phase: Saturation
% 15.42/6.27 % (4146577)Time elapsed: 0.812 s
% 15.42/6.27 % (4146577)Peak memory usage: 27 MB
% 15.42/6.27 % (4146577)Instructions burned: 1472 (million)
% 15.42/6.27 % (4146579)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2223504820:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 15.42/6.27 % (4146579)Cannot represent all propositional literals internally
% 15.42/6.27 % (4146579)Refutation not found, incomplete strategy
% 15.42/6.27 % (4146579)------------------------------
% 15.42/6.27 % (4146579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146579)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146579)Termination reason: Refutation not found, incomplete strategy
% 15.42/6.27 % (4146579)Time elapsed: 0.121 s
% 15.42/6.27 % (4146579)Peak memory usage: 16 MB
% 15.42/6.27 % (4146579)Instructions burned: 236 (million)
% 15.42/6.27 % (4146579)------------------------------
% 15.42/6.27 % (4146579)------------------------------
% 15.42/6.27 % (4146581)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=605749164:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 15.42/6.27 % TRYING [16]
% 15.42/6.27 % TRYING [5]
% 15.42/6.27 % (4146581)Instruction limit reached!
% 15.42/6.27 % (4146581)------------------------------
% 15.42/6.27 % (4146581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146581)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146581)Termination reason: Instruction limit
% 15.42/6.27 % (4146581)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146581)Time elapsed: 0.930 s
% 15.42/6.27 % (4146581)Peak memory usage: 82 MB
% 15.42/6.27 % (4146581)Instructions burned: 2176 (million)
% 15.42/6.27 % (4146585)ott-2_1_sil=16000:newcnf=on:random_seed=1202627300:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 15.42/6.27 % (4146585)Instruction limit reached!
% 15.42/6.27 % (4146585)------------------------------
% 15.42/6.27 % (4146585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146585)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146585)Termination reason: Instruction limit
% 15.42/6.27 % (4146585)Termination phase: Saturation
% 15.42/6.27 % (4146585)Time elapsed: 0.521 s
% 15.42/6.27 % (4146585)Peak memory usage: 23 MB
% 15.42/6.27 % (4146585)Instructions burned: 870 (million)
% 15.42/6.27 % (4146587)ott+10_1_sil=32000:tgt=ground:random_seed=793195462:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 15.42/6.27 % (4146575)Instruction limit reached!
% 15.42/6.27 % (4146575)------------------------------
% 15.42/6.27 % (4146575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146575)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146575)Termination reason: Instruction limit
% 15.42/6.27 % (4146575)Termination phase: Saturation
% 15.42/6.27 % (4146575)Time elapsed: 3.068 s
% 15.42/6.27 % (4146575)Peak memory usage: 48 MB
% 15.42/6.27 % (4146575)Instructions burned: 5133 (million)
% 15.42/6.27 % (4146589)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2106659471:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 15.42/6.27 % TRYING [1]
% 15.42/6.27 % TRYING [2]
% 15.42/6.27 % TRYING [3]
% 15.42/6.27 % (4146571)Instruction limit reached!
% 15.42/6.27 % (4146571)------------------------------
% 15.42/6.27 % (4146571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146571)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146571)Termination reason: Instruction limit
% 15.42/6.27 % (4146571)Termination phase: Finite model building constraint generation
% 15.42/6.27 % (4146571)Time elapsed: 3.427 s
% 15.42/6.27 % (4146571)Peak memory usage: 618 MB
% 15.42/6.27 % (4146571)Instructions burned: 9518 (million)
% 15.42/6.27 % (4146591)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=796347127:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 15.42/6.27 % TRYING [4]
% 15.42/6.27 % (4146587) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4146530-4146587"...
% 15.42/6.27 % (4146587)...printing done.
% 15.42/6.27 % (4146587)Refutation found. Thanks to Tanya!
% 15.42/6.27 % SZS status Theorem for theBenchmark
% 15.42/6.27 % SZS output start Proof for theBenchmark
% See solution above
% 15.42/6.27 % (4146587)------------------------------
% 15.42/6.27 % (4146587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.42/6.27 % (4146587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.42/6.27 % (4146587)CaDiCaL version: 2.1.3
% 15.42/6.27 % (4146587)Termination reason: Refutation
% 15.42/6.27 % (4146587)Time elapsed: 1.871 s
% 15.42/6.27 % (4146587)Peak memory usage: 49 MB
% 15.42/6.27 % (4146587)Instructions burned: 2979 (million)
% 15.42/6.27 % (4146530)Success in time 5.846 s
% 15.42/6.27 % Vampire exiting
%------------------------------------------------------------------------------