%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU269+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:48:06 PM UTC 2026
% Result : Theorem 8.46s 2.10s
% Output : Refutation 9.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 14
% Syntax : Number of formulae : 118 ( 29 unt; 6 def)
% Number of atoms : 416 ( 38 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 513 ( 215 ~; 235 |; 42 &)
% ( 14 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-2 aty)
% Number of variables : 159 ( 0 sgn 146 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [X0,X1] :
( relation(X1)
=> ( X1 = inclusion_relation(X0)
<=> ( relation_field(X1) = X0
& ! [X2,X3] :
( ( in(X2,X0)
& in(X3,X0) )
=> ( in(ordered_pair(X2,X3),X1)
<=> subset(X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_wellord2) ).
fof(f61,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f86,axiom,
! [X0] : relation(inclusion_relation(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_wellord2) ).
fof(f163,axiom,
! [X0] :
( relation(X0)
=> ( transitive(X0)
<=> ! [X1,X2,X3] :
( ( in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X3),X0) )
=> in(ordered_pair(X1,X3),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2_wellord1) ).
fof(f235,axiom,
! [X0,X1,X2] :
( ( subset(X0,X1)
& subset(X1,X2) )
=> subset(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_xboole_1) ).
fof(f261,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(ordered_pair(X0,X1),X2)
=> ( in(X0,relation_field(X2))
& in(X1,relation_field(X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_relat_1) ).
fof(f282,conjecture,
! [X0] : transitive(inclusion_relation(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_wellord2) ).
fof(f283,negated_conjecture,
~ ! [X0] : transitive(inclusion_relation(X0)),
inference(negated_conjecture,[status(cth)],[f282]) ).
fof(f322,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f393,plain,
! [X0,X1] :
( ( X1 = inclusion_relation(X0)
<=> ( relation_field(X1) = X0
& ! [X2,X3] :
( ( in(ordered_pair(X2,X3),X1)
<=> subset(X2,X3) )
| ~ in(X2,X0)
| ~ in(X3,X0) ) ) )
| ~ relation(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f394,plain,
! [X0,X1] :
( ( X1 = inclusion_relation(X0)
<=> ( relation_field(X1) = X0
& ! [X2,X3] :
( ( in(ordered_pair(X2,X3),X1)
<=> subset(X2,X3) )
| ~ in(X2,X0)
| ~ in(X3,X0) ) ) )
| ~ relation(X1) ),
inference(flattening,[],[f393]) ).
fof(f490,plain,
! [X0] :
( ( transitive(X0)
<=> ! [X1,X2,X3] :
( in(ordered_pair(X1,X3),X0)
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f163]) ).
fof(f491,plain,
! [X0] :
( ( transitive(X0)
<=> ! [X1,X2,X3] :
( in(ordered_pair(X1,X3),X0)
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(flattening,[],[f490]) ).
fof(f557,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(ennf_transformation,[],[f235]) ).
fof(f558,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ subset(X0,X1)
| ~ subset(X1,X2) ),
inference(flattening,[],[f557]) ).
fof(f593,plain,
! [X0,X1,X2] :
( ( in(X0,relation_field(X2))
& in(X1,relation_field(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(ennf_transformation,[],[f261]) ).
fof(f594,plain,
! [X0,X1,X2] :
( ( in(X0,relation_field(X2))
& in(X1,relation_field(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(flattening,[],[f593]) ).
fof(f612,plain,
? [X0] : ~ transitive(inclusion_relation(X0)),
inference(ennf_transformation,[],[f283]) ).
fof(f750,plain,
! [X0,X1] :
( ( ( X1 = inclusion_relation(X0)
| relation_field(X1) != X0
| ? [X2,X3] :
( ( ~ subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X1) )
& ( subset(X2,X3)
| in(ordered_pair(X2,X3),X1) )
& in(X2,X0)
& in(X3,X0) ) )
& ( ( relation_field(X1) = X0
& ! [X2,X3] :
( ( ( in(ordered_pair(X2,X3),X1)
| ~ subset(X2,X3) )
& ( subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X1) ) )
| ~ in(X2,X0)
| ~ in(X3,X0) ) )
| inclusion_relation(X0) != X1 ) )
| ~ relation(X1) ),
inference(nnf_transformation,[],[f394]) ).
fof(f751,plain,
! [X0,X1] :
( ( ( X1 = inclusion_relation(X0)
| relation_field(X1) != X0
| ? [X2,X3] :
( ( ~ subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X1) )
& ( subset(X2,X3)
| in(ordered_pair(X2,X3),X1) )
& in(X2,X0)
& in(X3,X0) ) )
& ( ( relation_field(X1) = X0
& ! [X2,X3] :
( ( ( in(ordered_pair(X2,X3),X1)
| ~ subset(X2,X3) )
& ( subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X1) ) )
| ~ in(X2,X0)
| ~ in(X3,X0) ) )
| inclusion_relation(X0) != X1 ) )
| ~ relation(X1) ),
inference(flattening,[],[f750]) ).
fof(f752,plain,
! [X0,X1] :
( ( ( X1 = inclusion_relation(X0)
| relation_field(X1) != X0
| ? [X2,X3] :
( ( ~ subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X1) )
& ( subset(X2,X3)
| in(ordered_pair(X2,X3),X1) )
& in(X2,X0)
& in(X3,X0) ) )
& ( ( relation_field(X1) = X0
& ! [X4,X5] :
( ( ( in(ordered_pair(X4,X5),X1)
| ~ subset(X4,X5) )
& ( subset(X4,X5)
| ~ in(ordered_pair(X4,X5),X1) ) )
| ~ in(X4,X0)
| ~ in(X5,X0) ) )
| inclusion_relation(X0) != X1 ) )
| ~ relation(X1) ),
inference(rectify,[],[f751]) ).
fof(f753,plain,
! [X0,X1] :
( ( ( X1 = inclusion_relation(X0)
| relation_field(X1) != X0
| ( ( ~ subset(sK31(X0,X1),sK32(X0,X1))
| ~ in(ordered_pair(sK31(X0,X1),sK32(X0,X1)),X1) )
& ( subset(sK31(X0,X1),sK32(X0,X1))
| in(ordered_pair(sK31(X0,X1),sK32(X0,X1)),X1) )
& in(sK31(X0,X1),X0)
& in(sK32(X0,X1),X0) ) )
& ( ( relation_field(X1) = X0
& ! [X4,X5] :
( ( ( in(ordered_pair(X4,X5),X1)
| ~ subset(X4,X5) )
& ( subset(X4,X5)
| ~ in(ordered_pair(X4,X5),X1) ) )
| ~ in(X4,X0)
| ~ in(X5,X0) ) )
| inclusion_relation(X0) != X1 ) )
| ~ relation(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32]),skolemize(X2,sK31(X0,X1)),skolemize(X3,sK32(X0,X1))],[f752]) ).
fof(f860,plain,
! [X0] :
( ( ( transitive(X0)
| ? [X1,X2,X3] :
( ~ in(ordered_pair(X1,X3),X0)
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X3),X0) ) )
& ( ! [X1,X2,X3] :
( in(ordered_pair(X1,X3),X0)
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X3),X0) )
| ~ transitive(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f491]) ).
fof(f861,plain,
! [X0] :
( ( ( transitive(X0)
| ? [X1,X2,X3] :
( ~ in(ordered_pair(X1,X3),X0)
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X3),X0) ) )
& ( ! [X4,X5,X6] :
( in(ordered_pair(X4,X6),X0)
| ~ in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X5,X6),X0) )
| ~ transitive(X0) ) )
| ~ relation(X0) ),
inference(rectify,[],[f860]) ).
fof(f862,plain,
! [X0] :
( ( ( transitive(X0)
| ( ~ in(ordered_pair(sK92(X0),sK94(X0)),X0)
& in(ordered_pair(sK92(X0),sK93(X0)),X0)
& in(ordered_pair(sK93(X0),sK94(X0)),X0) ) )
& ( ! [X4,X5,X6] :
( in(ordered_pair(X4,X6),X0)
| ~ in(ordered_pair(X4,X5),X0)
| ~ in(ordered_pair(X5,X6),X0) )
| ~ transitive(X0) ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92,sK93,sK94]),skolemize(X1,sK92(X0)),skolemize(X2,sK93(X0)),skolemize(X3,sK94(X0))],[f861]) ).
fof(f931,plain,
~ transitive(inclusion_relation(sK125)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK125]),skolemize(X0,sK125)],[f612]) ).
fof(f1073,plain,
! [X0,X1,X4,X5] :
( subset(X4,X5)
| ~ in(ordered_pair(X4,X5),X1)
| ~ in(X4,X0)
| ~ in(X5,X0)
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(cnf_transformation,[],[f753]) ).
fof(f1074,plain,
! [X0,X1,X4,X5] :
( in(ordered_pair(X4,X5),X1)
| ~ subset(X4,X5)
| ~ in(X4,X0)
| ~ in(X5,X0)
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(cnf_transformation,[],[f753]) ).
fof(f1075,plain,
! [X0,X1] :
( relation_field(X1) = X0
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(cnf_transformation,[],[f753]) ).
fof(f1195,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f61]) ).
fof(f1259,plain,
! [X0] : relation(inclusion_relation(X0)),
inference(cnf_transformation,[],[f86]) ).
fof(f1351,plain,
! [X0] :
( transitive(X0)
| in(ordered_pair(sK93(X0),sK94(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f862]) ).
fof(f1352,plain,
! [X0] :
( transitive(X0)
| in(ordered_pair(sK92(X0),sK93(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f862]) ).
fof(f1353,plain,
! [X0] :
( transitive(X0)
| ~ in(ordered_pair(sK92(X0),sK94(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f862]) ).
fof(f1484,plain,
! [X2,X0,X1] :
( ~ subset(X1,X2)
| ~ subset(X0,X1)
| subset(X0,X2) ),
inference(cnf_transformation,[],[f558]) ).
fof(f1520,plain,
! [X2,X0,X1] :
( in(X1,relation_field(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f594]) ).
fof(f1521,plain,
! [X2,X0,X1] :
( in(X0,relation_field(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f594]) ).
fof(f1558,plain,
~ transitive(inclusion_relation(sK125)),
inference(cnf_transformation,[],[f931]) ).
fof(f1631,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f322]) ).
fof(f1672,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f1195,f1631]) ).
fof(f1717,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),X1)
| ~ subset(X4,X5)
| ~ in(X4,X0)
| ~ in(X5,X0)
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(definition_unfolding,[],[f1074,f1672]) ).
fof(f1718,plain,
! [X0,X1,X4,X5] :
( subset(X4,X5)
| ~ in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),X1)
| ~ in(X4,X0)
| ~ in(X5,X0)
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(definition_unfolding,[],[f1073,f1672]) ).
fof(f1795,plain,
! [X0] :
( ~ in(unordered_pair(unordered_pair(sK92(X0),sK94(X0)),unordered_pair(sK92(X0),sK92(X0))),X0)
| transitive(X0)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f1353,f1672]) ).
fof(f1796,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK92(X0),sK93(X0)),unordered_pair(sK92(X0),sK92(X0))),X0)
| transitive(X0)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f1352,f1672]) ).
fof(f1797,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK93(X0),sK94(X0)),unordered_pair(sK93(X0),sK93(X0))),X0)
| transitive(X0)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f1351,f1672]) ).
fof(f1836,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| in(X0,relation_field(X2))
| ~ relation(X2) ),
inference(definition_unfolding,[],[f1521,f1672]) ).
fof(f1837,plain,
! [X2,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),X2)
| in(X1,relation_field(X2))
| ~ relation(X2) ),
inference(definition_unfolding,[],[f1520,f1672]) ).
fof(f1927,plain,
! [X0] :
( relation_field(inclusion_relation(X0)) = X0
| ~ relation(inclusion_relation(X0)) ),
inference(equality_resolution,[],[f1075]) ).
fof(f1928,plain,
! [X0,X4,X5] :
( in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),inclusion_relation(X0))
| ~ subset(X4,X5)
| ~ in(X4,X0)
| ~ in(X5,X0)
| ~ relation(inclusion_relation(X0)) ),
inference(equality_resolution,[],[f1717]) ).
fof(f1929,plain,
! [X0,X4,X5] :
( subset(X4,X5)
| ~ in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),inclusion_relation(X0))
| ~ in(X4,X0)
| ~ in(X5,X0)
| ~ relation(inclusion_relation(X0)) ),
inference(equality_resolution,[],[f1718]) ).
fof(f2000,definition,
sF138 = inclusion_relation(sK125),
introduced(definition,[new_symbols(definition,[sF138])],[function_definition]) ).
fof(f2001,plain,
inclusion_relation(sK125) = sF138,
inference(reorient_equations,[],[f2000]) ).
fof(f2002,plain,
~ transitive(sF138),
inference(definition_folding,[],[f1558,f2001]) ).
fof(f2024,plain,
! [X0,X4,X5] :
( ~ in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),inclusion_relation(X0))
| subset(X4,X5)
| ~ in(X4,X0)
| ~ in(X5,X0) ),
inference(forward_subsumption_resolution,[],[f1929,f1259]) ).
fof(f2025,plain,
! [X0,X4,X5] :
( in(unordered_pair(unordered_pair(X4,X5),unordered_pair(X4,X4)),inclusion_relation(X0))
| ~ subset(X4,X5)
| ~ in(X4,X0)
| ~ in(X5,X0) ),
inference(forward_subsumption_resolution,[],[f1928,f1259]) ).
fof(f2026,plain,
! [X0] : relation_field(inclusion_relation(X0)) = X0,
inference(forward_subsumption_resolution,[],[f1927,f1259]) ).
fof(f2039,plain,
relation(sF138),
inference(superposition,[],[f1259,f2001]) ).
fof(f2041,plain,
sK125 = relation_field(sF138),
inference(superposition,[],[f2026,f2001]) ).
fof(f2051,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF138)
| ~ subset(X0,X1)
| ~ in(X0,sK125)
| ~ in(X1,sK125) ),
inference(superposition,[],[f2025,f2001]) ).
fof(f2053,plain,
( ~ subset(sK92(sF138),sK94(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK94(sF138),sK125)
| transitive(sF138)
| ~ relation(sF138) ),
inference(resolution,[],[f2051,f1795]) ).
fof(f2058,plain,
( ~ subset(sK92(sF138),sK94(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK94(sF138),sK125)
| ~ relation(sF138) ),
inference(forward_subsumption_resolution,[],[f2053,f2002]) ).
fof(f2059,plain,
( ~ subset(sK92(sF138),sK94(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK94(sF138),sK125) ),
inference(forward_subsumption_resolution,[],[f2058,f2039]) ).
fof(f2061,definition,
( spl139_3
<=> in(sK94(sF138),sK125) ),
introduced(definition,[new_symbols(definition,[spl139_3])],[avatar_definition]) ).
fof(f2062,plain,
( in(sK94(sF138),sK125)
| ~ spl139_3 ),
inference(avatar_component_clause,[],[f2061]) ).
fof(f2063,plain,
( ~ in(sK94(sF138),sK125)
| spl139_3 ),
inference(avatar_component_clause,[],[f2061]) ).
fof(f2065,definition,
( spl139_4
<=> in(sK92(sF138),sK125) ),
introduced(definition,[new_symbols(definition,[spl139_4])],[avatar_definition]) ).
fof(f2067,plain,
( ~ in(sK92(sF138),sK125)
| spl139_4 ),
inference(avatar_component_clause,[],[f2065]) ).
fof(f2069,definition,
( spl139_5
<=> subset(sK92(sF138),sK94(sF138)) ),
introduced(definition,[new_symbols(definition,[spl139_5])],[avatar_definition]) ).
fof(f2071,plain,
( ~ subset(sK92(sF138),sK94(sF138))
| spl139_5 ),
inference(avatar_component_clause,[],[f2069]) ).
fof(f2072,plain,
( ~ spl139_3
| ~ spl139_4
| ~ spl139_5 ),
inference(avatar_split_clause,[],[f2059,f2069,f2065,f2061]) ).
fof(f2093,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF138)
| subset(X0,X1)
| ~ in(X0,sK125)
| ~ in(X1,sK125) ),
inference(superposition,[],[f2024,f2001]) ).
fof(f2100,plain,
( subset(sK92(sF138),sK93(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK93(sF138),sK125)
| transitive(sF138)
| ~ relation(sF138) ),
inference(resolution,[],[f2093,f1796]) ).
fof(f2101,plain,
( subset(sK93(sF138),sK94(sF138))
| ~ in(sK93(sF138),sK125)
| ~ in(sK94(sF138),sK125)
| transitive(sF138)
| ~ relation(sF138) ),
inference(resolution,[],[f2093,f1797]) ).
fof(f2109,plain,
( subset(sK92(sF138),sK93(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK93(sF138),sK125)
| ~ relation(sF138) ),
inference(forward_subsumption_resolution,[],[f2100,f2002]) ).
fof(f2110,plain,
( subset(sK92(sF138),sK93(sF138))
| ~ in(sK92(sF138),sK125)
| ~ in(sK93(sF138),sK125) ),
inference(forward_subsumption_resolution,[],[f2109,f2039]) ).
fof(f2112,definition,
( spl139_6
<=> in(sK93(sF138),sK125) ),
introduced(definition,[new_symbols(definition,[spl139_6])],[avatar_definition]) ).
fof(f2113,plain,
( in(sK93(sF138),sK125)
| ~ spl139_6 ),
inference(avatar_component_clause,[],[f2112]) ).
fof(f2116,definition,
( spl139_7
<=> subset(sK92(sF138),sK93(sF138)) ),
introduced(definition,[new_symbols(definition,[spl139_7])],[avatar_definition]) ).
fof(f2118,plain,
( subset(sK92(sF138),sK93(sF138))
| ~ spl139_7 ),
inference(avatar_component_clause,[],[f2116]) ).
fof(f2119,plain,
( ~ spl139_6
| ~ spl139_4
| spl139_7 ),
inference(avatar_split_clause,[],[f2110,f2116,f2065,f2112]) ).
fof(f2159,plain,
! [X0] :
( in(sK92(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0)
| ~ relation(X0) ),
inference(resolution,[],[f1836,f1796]) ).
fof(f2160,plain,
! [X0] :
( in(sK93(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0)
| ~ relation(X0) ),
inference(resolution,[],[f1836,f1797]) ).
fof(f2172,plain,
! [X0] :
( in(sK93(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0) ),
inference(duplicate_literal_removal,[],[f2160]) ).
fof(f2173,plain,
! [X0] :
( in(sK92(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0) ),
inference(duplicate_literal_removal,[],[f2159]) ).
fof(f2186,plain,
( in(sK93(sF138),sK125)
| ~ relation(sF138)
| transitive(sF138) ),
inference(superposition,[],[f2172,f2041]) ).
fof(f2187,plain,
( in(sK93(sF138),sK125)
| transitive(sF138) ),
inference(forward_subsumption_resolution,[],[f2186,f2039]) ).
fof(f2189,plain,
in(sK93(sF138),sK125),
inference(forward_subsumption_resolution,[],[f2187,f2002]) ).
fof(f2190,plain,
spl139_6,
inference(avatar_split_clause,[],[f2189,f2112]) ).
fof(f2194,plain,
( in(sK92(sF138),sK125)
| ~ relation(sF138)
| transitive(sF138) ),
inference(superposition,[],[f2173,f2041]) ).
fof(f2195,plain,
( ~ relation(sF138)
| transitive(sF138)
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2194,f2067]) ).
fof(f2197,plain,
( transitive(sF138)
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2195,f2039]) ).
fof(f2198,plain,
( $false
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2197,f2002]) ).
fof(f2199,plain,
spl139_4,
inference(avatar_contradiction_clause,[],[f2198]) ).
fof(f2267,plain,
! [X0] :
( in(sK94(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0)
| ~ relation(X0) ),
inference(resolution,[],[f1837,f1797]) ).
fof(f2279,plain,
! [X0] :
( in(sK94(X0),relation_field(X0))
| ~ relation(X0)
| transitive(X0) ),
inference(duplicate_literal_removal,[],[f2267]) ).
fof(f2293,plain,
( in(sK94(sF138),sK125)
| ~ relation(sF138)
| transitive(sF138) ),
inference(superposition,[],[f2279,f2041]) ).
fof(f2294,plain,
( ~ relation(sF138)
| transitive(sF138)
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2293,f2063]) ).
fof(f2296,plain,
( transitive(sF138)
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2294,f2039]) ).
fof(f2297,plain,
( $false
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2296,f2002]) ).
fof(f2298,plain,
spl139_3,
inference(avatar_contradiction_clause,[],[f2297]) ).
fof(f2299,plain,
( subset(sK93(sF138),sK94(sF138))
| ~ in(sK94(sF138),sK125)
| transitive(sF138)
| ~ relation(sF138)
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2101,f2113]) ).
fof(f2301,plain,
( subset(sK93(sF138),sK94(sF138))
| transitive(sF138)
| ~ relation(sF138)
| ~ spl139_3
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2299,f2062]) ).
fof(f2303,plain,
( subset(sK93(sF138),sK94(sF138))
| ~ relation(sF138)
| ~ spl139_3
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2301,f2002]) ).
fof(f2305,plain,
( subset(sK93(sF138),sK94(sF138))
| ~ spl139_3
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2303,f2039]) ).
fof(f2574,plain,
( ! [X0] :
( ~ subset(X0,sK93(sF138))
| subset(X0,sK94(sF138)) )
| ~ spl139_3
| ~ spl139_6 ),
inference(resolution,[],[f1484,f2305]) ).
fof(f2714,plain,
( subset(sK92(sF138),sK94(sF138))
| ~ spl139_3
| ~ spl139_6
| ~ spl139_7 ),
inference(resolution,[],[f2574,f2118]) ).
fof(f2715,plain,
( $false
| ~ spl139_3
| spl139_5
| ~ spl139_6
| ~ spl139_7 ),
inference(forward_subsumption_resolution,[],[f2714,f2071]) ).
fof(f2716,plain,
( ~ spl139_3
| spl139_5
| ~ spl139_6
| ~ spl139_7 ),
inference(avatar_contradiction_clause,[],[f2715]) ).
cnf(s2,plain,
( ~ spl139_3
| ~ spl139_4
| ~ spl139_5 ),
inference(sat_conversion,[],[f2072]) ).
cnf(s3,plain,
( ~ spl139_4
| ~ spl139_6
| spl139_7 ),
inference(sat_conversion,[],[f2119]) ).
cnf(s4,plain,
spl139_6,
inference(sat_conversion,[],[f2190]) ).
cnf(s5,plain,
spl139_4,
inference(sat_conversion,[],[f2199]) ).
cnf(s13,plain,
spl139_3,
inference(sat_conversion,[],[f2298]) ).
cnf(s31,plain,
( ~ spl139_3
| spl139_5
| ~ spl139_6
| ~ spl139_7 ),
inference(sat_conversion,[],[f2716]) ).
cnf(s32,plain,
spl139_7,
inference(rat,[],[s3,s4,s5]) ).
cnf(s33,plain,
spl139_5,
inference(rat,[],[s31,s4,s13,s32]) ).
cnf(s34,plain,
$false,
inference(rat,[],[s2,s33,s5,s13]) ).
fof(f2717,plain,
$false,
inference(avatar_sat_refutation,[],[s34]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU269+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n003.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Mon Sep 28 04:27:12 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.46/2.10 % (1185422)Detected formulas, will run a generic FOF schedule.
% 8.46/2.10 % (1185431)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3585942020:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.46/2.10 % (1185433)dis-21_1_sil=8000:lcm=predicate:random_seed=2884419794:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.46/2.10 % (1185427)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2593397200:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.46/2.10 % (1185430)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1527048728:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.46/2.10 % (1185428)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2902606338:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.46/2.10 % (1185429)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3396492807:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.46/2.10 % (1185431)Instruction limit reached!
% 8.46/2.10 % (1185431)------------------------------
% 8.46/2.10 % (1185431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185431)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185431)Termination reason: Instruction limit
% 8.46/2.10 % (1185431)Termination phase: Saturation
% 8.46/2.10 % (1185431)Time elapsed: 0.044 s
% 8.46/2.10 % (1185431)Peak memory usage: 90 MB
% 8.46/2.10 % (1185431)Instructions burned: 120 (million)
% 8.46/2.10 % (1185432)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4041603400:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.46/2.10 % (1185430)Instruction limit reached!
% 8.46/2.10 % (1185430)------------------------------
% 8.46/2.10 % (1185430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185430)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185430)Termination reason: Instruction limit
% 8.46/2.10 % (1185430)Termination phase: Saturation
% 8.46/2.10 % (1185430)Time elapsed: 0.068 s
% 8.46/2.10 % (1185430)Peak memory usage: 90 MB
% 8.46/2.10 % (1185430)Instructions burned: 109 (million)
% 8.46/2.10 % (1185433)Instruction limit reached!
% 8.46/2.10 % (1185433)------------------------------
% 8.46/2.10 % (1185433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185433)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185433)Termination reason: Instruction limit
% 8.46/2.10 % (1185433)Termination phase: Saturation
% 8.46/2.10 % (1185433)Time elapsed: 0.076 s
% 8.46/2.10 % (1185433)Peak memory usage: 90 MB
% 8.46/2.10 % (1185433)Instructions burned: 130 (million)
% 8.46/2.10 % (1185441)lrs+10_1_sil=8000:sp=occurrence:random_seed=3244494497:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.46/2.10 % (1185432)Instruction limit reached!
% 8.46/2.10 % (1185432)------------------------------
% 8.46/2.10 % (1185432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185432)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185432)Termination reason: Instruction limit
% 8.46/2.10 % (1185432)Termination phase: Saturation
% 8.46/2.10 % (1185432)Time elapsed: 0.094 s
% 8.46/2.10 % (1185432)Peak memory usage: 91 MB
% 8.46/2.10 % (1185432)Instructions burned: 141 (million)
% 8.46/2.10 % (1185441)Instruction limit reached!
% 8.46/2.10 % (1185441)------------------------------
% 8.46/2.10 % (1185441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185441)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185441)Termination reason: Instruction limit
% 8.46/2.10 % (1185441)Termination phase: Saturation
% 8.46/2.10 % (1185441)Time elapsed: 0.102 s
% 8.46/2.10 % (1185441)Peak memory usage: 93 MB
% 8.46/2.10 % (1185441)Instructions burned: 285 (million)
% 8.46/2.10 % (1185442)lrs+10_1_sil=32000:urr=on:br=off:random_seed=464890389:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.46/2.10 % (1185442)Refutation not found, incomplete strategy
% 8.46/2.10 % (1185442)------------------------------
% 8.46/2.10 % (1185442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185442)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185442)Termination reason: Refutation not found, incomplete strategy
% 8.46/2.10 % (1185442)Time elapsed: 0.005 s
% 8.46/2.10 % (1185442)Peak memory usage: 89 MB
% 8.46/2.10 % (1185442)Instructions burned: 6 (million)
% 8.46/2.10 % (1185443)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4242817756:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.46/2.10 % (1185445)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3262816207:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 8.46/2.10 % (1185446)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=258648110:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 8.46/2.10 % (1185445)Instruction limit reached!
% 8.46/2.10 % (1185445)------------------------------
% 8.46/2.10 % (1185445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185445)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185445)Termination reason: Instruction limit
% 8.46/2.10 % (1185445)Termination phase: Saturation
% 8.46/2.10 % (1185445)Time elapsed: 0.148 s
% 8.46/2.10 % (1185445)Peak memory usage: 93 MB
% 8.46/2.10 % (1185445)Instructions burned: 249 (million)
% 8.46/2.10 % (1185446)Instruction limit reached!
% 8.46/2.10 % (1185446)------------------------------
% 8.46/2.10 % (1185446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185446)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185446)Termination reason: Instruction limit
% 8.46/2.10 % (1185446)Termination phase: Saturation
% 8.46/2.10 % (1185446)Time elapsed: 0.100 s
% 8.46/2.10 % (1185446)Peak memory usage: 91 MB
% 8.46/2.10 % (1185446)Instructions burned: 295 (million)
% 8.46/2.10 % (1185443)Instruction limit reached!
% 8.46/2.10 % (1185443)------------------------------
% 8.46/2.10 % (1185443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185443)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185443)Termination reason: Instruction limit
% 8.46/2.10 % (1185443)Termination phase: Saturation
% 8.46/2.10 % (1185443)Time elapsed: 0.227 s
% 8.46/2.10 % (1185443)Peak memory usage: 93 MB
% 8.46/2.10 % (1185443)Instructions burned: 326 (million)
% 8.46/2.10 % (1185442)------------------------------
% 8.46/2.10 % (1185442)------------------------------
% 8.46/2.10 % (1185452)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3610412306:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 8.46/2.10 % (1185452)Instruction limit reached!
% 8.46/2.10 % (1185452)------------------------------
% 8.46/2.10 % (1185452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185452)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185452)Termination reason: Instruction limit
% 8.46/2.10 % (1185452)Termination phase: Saturation
% 8.46/2.10 % (1185452)Time elapsed: 0.038 s
% 8.46/2.10 % (1185452)Peak memory usage: 90 MB
% 8.46/2.10 % (1185452)Instructions burned: 114 (million)
% 8.46/2.10 % (1185451)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=252729441:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.46/2.10 % (1185453)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3995070419:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 8.46/2.10 % (1185454)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1161428692:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 8.46/2.10 % (1185457)lrs+10_1_sil=8000:sp=occurrence:random_seed=3708765695:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 8.46/2.10 % (1185453)Instruction limit reached!
% 8.46/2.10 % (1185453)------------------------------
% 8.46/2.10 % (1185453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185453)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185453)Termination reason: Instruction limit
% 8.46/2.10 % (1185453)Termination phase: Saturation
% 8.46/2.10 % (1185453)Time elapsed: 0.070 s
% 8.46/2.10 % (1185453)Peak memory usage: 90 MB
% 8.46/2.10 % (1185453)Instructions burned: 128 (million)
% 8.46/2.10 % (1185454)Instruction limit reached!
% 8.46/2.10 % (1185454)------------------------------
% 8.46/2.10 % (1185454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185454)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185454)Termination reason: Instruction limit
% 8.46/2.10 % (1185454)Termination phase: Saturation
% 8.46/2.10 % (1185454)Time elapsed: 0.067 s
% 8.46/2.10 % (1185454)Peak memory usage: 89 MB
% 8.46/2.10 % (1185454)Instructions burned: 115 (million)
% 8.46/2.10 % (1185462)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=82092770:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 8.46/2.10 % (1185461)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4224961416:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 8.46/2.10 % (1185427)First to succeed.
% 8.46/2.10 % (1185427)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1185422"
% 8.46/2.10 % (1185457)Instruction limit reached!
% 8.46/2.10 % (1185457)------------------------------
% 8.46/2.10 % (1185457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185457)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185457)Termination reason: Instruction limit
% 8.46/2.10 % (1185457)Termination phase: Saturation
% 8.46/2.10 % (1185457)Time elapsed: 0.309 s
% 8.46/2.10 % (1185457)Peak memory usage: 101 MB
% 8.46/2.10 % (1185457)Instructions burned: 910 (million)
% 8.46/2.10 % (1185466)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3153778631:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 8.46/2.10 % (1185466)Instruction limit reached!
% 8.46/2.10 % (1185466)------------------------------
% 8.46/2.10 % (1185466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185466)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185466)Termination reason: Instruction limit
% 8.46/2.10 % (1185466)Termination phase: Saturation
% 8.46/2.10 % (1185466)Time elapsed: 0.044 s
% 8.46/2.10 % (1185466)Peak memory usage: 92 MB
% 8.46/2.10 % (1185466)Instructions burned: 134 (million)
% 8.46/2.10 % (1185461)Instruction limit reached!
% 8.46/2.10 % (1185461)------------------------------
% 8.46/2.10 % (1185461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.46/2.10 % (1185461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.46/2.10 % (1185461)CaDiCaL version: 2.1.3
% 8.46/2.10 % (1185461)Termination reason: Instruction limit
% 8.46/2.10 % (1185461)Termination phase: Saturation
% 8.46/2.10 % (1185461)Time elapsed: 0.266 s
% 8.46/2.10 % (1185461)Peak memory usage: 93 MB
% 8.46/2.10 % (1185461)Instructions burned: 438 (million)
% 8.46/2.10 % (1185427)Refutation found. Thanks to Tanya!
% 8.46/2.10 % SZS status Theorem for theBenchmark
% 8.46/2.10 % SZS output start Proof for theBenchmark
% See solution above
% 9.11/2.29 % (1185427)------------------------------
% 9.11/2.29 % (1185427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.11/2.29 % (1185427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.11/2.29 % (1185427)CaDiCaL version: 2.1.3
% 9.11/2.29 % (1185427)Termination reason: Refutation
% 9.11/2.29 % (1185427)Time elapsed: 0.810 s
% 9.11/2.29 % (1185427)Peak memory usage: 137 MB
% 9.11/2.29 % (1185427)Instructions burned: 1237 (million)
% 9.11/2.29 % (1185427)------------------------------
% 9.11/2.29 % (1185427)------------------------------
% 9.11/2.29 % (1185422)Success in time 1.219 s
% 9.11/2.29 % Vampire exiting
%------------------------------------------------------------------------------