%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU271+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 : n007.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.63s 2.08s
% Output : Refutation 9.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 13
% Syntax : Number of formulae : 98 ( 26 unt; 5 def)
% Number of atoms : 349 ( 55 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 423 ( 172 ~; 185 |; 46 &)
% ( 14 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 5 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 121 ( 0 sgn 110 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
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(f167,axiom,
! [X0] :
( relation(X0)
=> ( antisymmetric(X0)
<=> ! [X1,X2] :
( ( in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X1),X0) )
=> X1 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l3_wellord1) ).
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(f314,conjecture,
! [X0] : antisymmetric(inclusion_relation(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_wellord2) ).
fof(f315,negated_conjecture,
~ ! [X0] : antisymmetric(inclusion_relation(X0)),
inference(negated_conjecture,[status(cth)],[f314]) ).
fof(f324,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f395,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(f396,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,[],[f395]) ).
fof(f495,plain,
! [X0] :
( ( antisymmetric(X0)
<=> ! [X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X1),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f167]) ).
fof(f496,plain,
! [X0] :
( ( antisymmetric(X0)
<=> ! [X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X1),X0) ) )
| ~ relation(X0) ),
inference(flattening,[],[f495]) ).
fof(f595,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(f596,plain,
! [X0,X1,X2] :
( ( in(X0,relation_field(X2))
& in(X1,relation_field(X2)) )
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(flattening,[],[f595]) ).
fof(f658,plain,
? [X0] : ~ antisymmetric(inclusion_relation(X0)),
inference(ennf_transformation,[],[f315]) ).
fof(f703,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f704,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f703]) ).
fof(f753,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,[],[f396]) ).
fof(f754,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,[],[f753]) ).
fof(f755,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,[],[f754]) ).
fof(f756,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))],[f755]) ).
fof(f868,plain,
! [X0] :
( ( ( antisymmetric(X0)
| ? [X1,X2] :
( X1 != X2
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X1),X0) ) )
& ( ! [X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(ordered_pair(X2,X1),X0) )
| ~ antisymmetric(X0) ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f496]) ).
fof(f869,plain,
! [X0] :
( ( ( antisymmetric(X0)
| ? [X1,X2] :
( X1 != X2
& in(ordered_pair(X1,X2),X0)
& in(ordered_pair(X2,X1),X0) ) )
& ( ! [X3,X4] :
( X3 = X4
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X4,X3),X0) )
| ~ antisymmetric(X0) ) )
| ~ relation(X0) ),
inference(rectify,[],[f868]) ).
fof(f870,plain,
! [X0] :
( ( ( antisymmetric(X0)
| ( sK95(X0) != sK96(X0)
& in(ordered_pair(sK95(X0),sK96(X0)),X0)
& in(ordered_pair(sK96(X0),sK95(X0)),X0) ) )
& ( ! [X3,X4] :
( X3 = X4
| ~ in(ordered_pair(X3,X4),X0)
| ~ in(ordered_pair(X4,X3),X0) )
| ~ antisymmetric(X0) ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95,sK96]),skolemize(X1,sK95(X0)),skolemize(X2,sK96(X0))],[f869]) ).
fof(f950,plain,
~ antisymmetric(inclusion_relation(sK133)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK133]),skolemize(X0,sK133)],[f658]) ).
fof(f993,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f704]) ).
fof(f1076,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,[],[f756]) ).
fof(f1078,plain,
! [X0,X1] :
( relation_field(X1) = X0
| inclusion_relation(X0) != X1
| ~ relation(X1) ),
inference(cnf_transformation,[],[f756]) ).
fof(f1198,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f61]) ).
fof(f1262,plain,
! [X0] : relation(inclusion_relation(X0)),
inference(cnf_transformation,[],[f86]) ).
fof(f1363,plain,
! [X0] :
( antisymmetric(X0)
| in(ordered_pair(sK96(X0),sK95(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1364,plain,
! [X0] :
( antisymmetric(X0)
| in(ordered_pair(sK95(X0),sK96(X0)),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1365,plain,
! [X0] :
( sK95(X0) != sK96(X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1524,plain,
! [X2,X0,X1] :
( in(X0,relation_field(X2))
| ~ in(ordered_pair(X0,X1),X2)
| ~ relation(X2) ),
inference(cnf_transformation,[],[f596]) ).
fof(f1620,plain,
~ antisymmetric(inclusion_relation(sK133)),
inference(cnf_transformation,[],[f950]) ).
fof(f1636,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f324]) ).
fof(f1677,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f1198,f1636]) ).
fof(f1723,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,[],[f1076,f1677]) ).
fof(f1806,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK95(X0),sK96(X0)),unordered_pair(sK95(X0),sK95(X0))),X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f1364,f1677]) ).
fof(f1807,plain,
! [X0] :
( in(unordered_pair(unordered_pair(sK96(X0),sK95(X0)),unordered_pair(sK96(X0),sK96(X0))),X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f1363,f1677]) ).
fof(f1841,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,[],[f1524,f1677]) ).
fof(f1932,plain,
! [X0] :
( relation_field(inclusion_relation(X0)) = X0
| ~ relation(inclusion_relation(X0)) ),
inference(equality_resolution,[],[f1078]) ).
fof(f1934,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,[],[f1723]) ).
fof(f2005,definition,
sF138 = inclusion_relation(sK133),
introduced(definition,[new_symbols(definition,[sF138])],[function_definition]) ).
fof(f2006,plain,
inclusion_relation(sK133) = sF138,
inference(reorient_equations,[],[f2005]) ).
fof(f2007,plain,
~ antisymmetric(sF138),
inference(definition_folding,[],[f1620,f2006]) ).
fof(f2029,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,[],[f1934,f1262]) ).
fof(f2031,plain,
! [X0] : relation_field(inclusion_relation(X0)) = X0,
inference(forward_subsumption_resolution,[],[f1932,f1262]) ).
fof(f2044,plain,
relation(sF138),
inference(superposition,[],[f1262,f2006]) ).
fof(f2047,plain,
sK133 = relation_field(sF138),
inference(superposition,[],[f2031,f2006]) ).
fof(f2070,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),sF138)
| subset(X0,X1)
| ~ in(X0,sK133)
| ~ in(X1,sK133) ),
inference(superposition,[],[f2029,f2006]) ).
fof(f2075,plain,
( subset(sK95(sF138),sK96(sF138))
| ~ in(sK95(sF138),sK133)
| ~ in(sK96(sF138),sK133)
| antisymmetric(sF138)
| ~ relation(sF138) ),
inference(resolution,[],[f2070,f1806]) ).
fof(f2076,plain,
( subset(sK96(sF138),sK95(sF138))
| ~ in(sK96(sF138),sK133)
| ~ in(sK95(sF138),sK133)
| antisymmetric(sF138)
| ~ relation(sF138) ),
inference(resolution,[],[f2070,f1807]) ).
fof(f2082,plain,
( subset(sK96(sF138),sK95(sF138))
| ~ in(sK96(sF138),sK133)
| ~ in(sK95(sF138),sK133)
| ~ relation(sF138) ),
inference(forward_subsumption_resolution,[],[f2076,f2007]) ).
fof(f2083,plain,
( subset(sK95(sF138),sK96(sF138))
| ~ in(sK95(sF138),sK133)
| ~ in(sK96(sF138),sK133)
| ~ relation(sF138) ),
inference(forward_subsumption_resolution,[],[f2075,f2007]) ).
fof(f2084,plain,
( subset(sK96(sF138),sK95(sF138))
| ~ in(sK96(sF138),sK133)
| ~ in(sK95(sF138),sK133) ),
inference(forward_subsumption_resolution,[],[f2082,f2044]) ).
fof(f2085,plain,
( subset(sK95(sF138),sK96(sF138))
| ~ in(sK95(sF138),sK133)
| ~ in(sK96(sF138),sK133) ),
inference(forward_subsumption_resolution,[],[f2083,f2044]) ).
fof(f2087,definition,
( spl139_3
<=> in(sK95(sF138),sK133) ),
introduced(definition,[new_symbols(definition,[spl139_3])],[avatar_definition]) ).
fof(f2089,plain,
( ~ in(sK95(sF138),sK133)
| spl139_3 ),
inference(avatar_component_clause,[],[f2087]) ).
fof(f2091,definition,
( spl139_4
<=> in(sK96(sF138),sK133) ),
introduced(definition,[new_symbols(definition,[spl139_4])],[avatar_definition]) ).
fof(f2093,plain,
( ~ in(sK96(sF138),sK133)
| spl139_4 ),
inference(avatar_component_clause,[],[f2091]) ).
fof(f2095,definition,
( spl139_5
<=> subset(sK96(sF138),sK95(sF138)) ),
introduced(definition,[new_symbols(definition,[spl139_5])],[avatar_definition]) ).
fof(f2097,plain,
( subset(sK96(sF138),sK95(sF138))
| ~ spl139_5 ),
inference(avatar_component_clause,[],[f2095]) ).
fof(f2098,plain,
( ~ spl139_3
| ~ spl139_4
| spl139_5 ),
inference(avatar_split_clause,[],[f2084,f2095,f2091,f2087]) ).
fof(f2100,definition,
( spl139_6
<=> subset(sK95(sF138),sK96(sF138)) ),
introduced(definition,[new_symbols(definition,[spl139_6])],[avatar_definition]) ).
fof(f2102,plain,
( subset(sK95(sF138),sK96(sF138))
| ~ spl139_6 ),
inference(avatar_component_clause,[],[f2100]) ).
fof(f2103,plain,
( ~ spl139_4
| ~ spl139_3
| spl139_6 ),
inference(avatar_split_clause,[],[f2085,f2100,f2087,f2091]) ).
fof(f2169,plain,
! [X0] :
( in(sK95(X0),relation_field(X0))
| ~ relation(X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(resolution,[],[f1841,f1806]) ).
fof(f2170,plain,
! [X0] :
( in(sK96(X0),relation_field(X0))
| ~ relation(X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(resolution,[],[f1841,f1807]) ).
fof(f2175,plain,
! [X0] :
( in(sK96(X0),relation_field(X0))
| ~ relation(X0)
| antisymmetric(X0) ),
inference(duplicate_literal_removal,[],[f2170]) ).
fof(f2176,plain,
! [X0] :
( in(sK95(X0),relation_field(X0))
| ~ relation(X0)
| antisymmetric(X0) ),
inference(duplicate_literal_removal,[],[f2169]) ).
fof(f2191,plain,
( in(sK95(sF138),sK133)
| ~ relation(sF138)
| antisymmetric(sF138) ),
inference(superposition,[],[f2176,f2047]) ).
fof(f2192,plain,
( ~ relation(sF138)
| antisymmetric(sF138)
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2191,f2089]) ).
fof(f2194,plain,
( antisymmetric(sF138)
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2192,f2044]) ).
fof(f2195,plain,
( $false
| spl139_3 ),
inference(forward_subsumption_resolution,[],[f2194,f2007]) ).
fof(f2196,plain,
spl139_3,
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2200,plain,
( in(sK96(sF138),sK133)
| ~ relation(sF138)
| antisymmetric(sF138) ),
inference(superposition,[],[f2175,f2047]) ).
fof(f2201,plain,
( ~ relation(sF138)
| antisymmetric(sF138)
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2200,f2093]) ).
fof(f2203,plain,
( antisymmetric(sF138)
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2201,f2044]) ).
fof(f2204,plain,
( $false
| spl139_4 ),
inference(forward_subsumption_resolution,[],[f2203,f2007]) ).
fof(f2205,plain,
spl139_4,
inference(avatar_contradiction_clause,[],[f2204]) ).
fof(f2207,plain,
( ~ subset(sK96(sF138),sK95(sF138))
| sK95(sF138) = sK96(sF138)
| ~ spl139_6 ),
inference(resolution,[],[f2102,f993]) ).
fof(f2209,plain,
( sK95(sF138) = sK96(sF138)
| ~ spl139_5
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2207,f2097]) ).
fof(f2217,plain,
( sK95(sF138) != sK95(sF138)
| antisymmetric(sF138)
| ~ relation(sF138)
| ~ spl139_5
| ~ spl139_6 ),
inference(superposition,[],[f1365,f2209]) ).
fof(f2218,plain,
( antisymmetric(sF138)
| ~ relation(sF138)
| ~ spl139_5
| ~ spl139_6 ),
inference(trivial_inequality_removal,[],[f2217]) ).
fof(f2219,plain,
( ~ relation(sF138)
| ~ spl139_5
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2218,f2007]) ).
fof(f2224,plain,
( $false
| ~ spl139_5
| ~ spl139_6 ),
inference(forward_subsumption_resolution,[],[f2219,f2044]) ).
fof(f2225,plain,
( ~ spl139_5
| ~ spl139_6 ),
inference(avatar_contradiction_clause,[],[f2224]) ).
cnf(s2,plain,
( ~ spl139_3
| ~ spl139_4
| spl139_5 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s3,plain,
( ~ spl139_3
| ~ spl139_4
| spl139_6 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s5,plain,
spl139_3,
inference(sat_conversion,[],[f2196]) ).
cnf(s6,plain,
spl139_4,
inference(sat_conversion,[],[f2205]) ).
cnf(s7,plain,
( ~ spl139_5
| ~ spl139_6 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s8,plain,
spl139_6,
inference(rat,[],[s3,s6,s5]) ).
cnf(s9,plain,
~ spl139_5,
inference(rat,[],[s7,s8]) ).
cnf(s10,plain,
$false,
inference(rat,[],[s2,s9,s6,s5]) ).
fof(f2230,plain,
$false,
inference(avatar_sat_refutation,[],[s10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU271+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n007.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:23:55 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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.63/2.08 % (2022701)Detected formulas, will run a generic FOF schedule.
% 8.63/2.08 % (2022711)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2222793101:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.63/2.08 % (2022707)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=1401153760:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.63/2.08 % (2022708)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=4068103517:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.63/2.08 % (2022706)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=3681718407:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.63/2.08 % (2022709)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2181003003:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.63/2.08 % (2022710)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2066466960:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.63/2.08 % (2022711)Instruction limit reached!
% 8.63/2.08 % (2022711)------------------------------
% 8.63/2.08 % (2022711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022711)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022711)Termination reason: Instruction limit
% 8.63/2.08 % (2022711)Termination phase: Saturation
% 8.63/2.08 % (2022711)Time elapsed: 0.053 s
% 8.63/2.08 % (2022711)Peak memory usage: 91 MB
% 8.63/2.08 % (2022711)Instructions burned: 139 (million)
% 8.63/2.08 % (2022712)dis-21_1_sil=8000:lcm=predicate:random_seed=459900725: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.63/2.08 % (2022709)Instruction limit reached!
% 8.63/2.08 % (2022709)------------------------------
% 8.63/2.08 % (2022709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022709)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022709)Termination reason: Instruction limit
% 8.63/2.08 % (2022709)Termination phase: Saturation
% 8.63/2.08 % (2022709)Time elapsed: 0.069 s
% 8.63/2.08 % (2022709)Peak memory usage: 90 MB
% 8.63/2.08 % (2022709)Instructions burned: 110 (million)
% 8.63/2.08 % (2022710)Instruction limit reached!
% 8.63/2.08 % (2022710)------------------------------
% 8.63/2.08 % (2022710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022710)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022710)Termination reason: Instruction limit
% 8.63/2.08 % (2022710)Termination phase: Saturation
% 8.63/2.08 % (2022710)Time elapsed: 0.080 s
% 8.63/2.08 % (2022710)Peak memory usage: 90 MB
% 8.63/2.08 % (2022710)Instructions burned: 119 (million)
% 8.63/2.08 % (2022712)Instruction limit reached!
% 8.63/2.08 % (2022712)------------------------------
% 8.63/2.08 % (2022712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022712)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022712)Termination reason: Instruction limit
% 8.63/2.08 % (2022712)Termination phase: Saturation
% 8.63/2.08 % (2022712)Time elapsed: 0.077 s
% 8.63/2.08 % (2022712)Peak memory usage: 90 MB
% 8.63/2.08 % (2022712)Instructions burned: 130 (million)
% 8.63/2.08 % (2022719)lrs+10_1_sil=8000:sp=occurrence:random_seed=985225966:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 8.63/2.08 % (2022721)lrs+10_1_sil=32000:urr=on:br=off:random_seed=883643129:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.63/2.08 % (2022722)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3662878296:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.63/2.08 % (2022721)Refutation not found, incomplete strategy
% 8.63/2.08 % (2022721)------------------------------
% 8.63/2.08 % (2022721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022721)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022721)Termination reason: Refutation not found, incomplete strategy
% 8.63/2.08 % (2022721)Time elapsed: 0.005 s
% 8.63/2.08 % (2022721)Peak memory usage: 89 MB
% 8.63/2.08 % (2022721)Instructions burned: 6 (million)
% 8.63/2.08 % (2022719)Instruction limit reached!
% 8.63/2.08 % (2022719)------------------------------
% 8.63/2.08 % (2022719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022719)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022719)Termination reason: Instruction limit
% 8.63/2.08 % (2022719)Termination phase: Saturation
% 8.63/2.08 % (2022719)Time elapsed: 0.103 s
% 8.63/2.08 % (2022719)Peak memory usage: 93 MB
% 8.63/2.08 % (2022719)Instructions burned: 287 (million)
% 8.63/2.08 % (2022723)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=1281548166:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 8.63/2.08 % (2022727)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3236690537:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.63/2.08 % (2022723)Instruction limit reached!
% 8.63/2.08 % (2022723)------------------------------
% 8.63/2.08 % (2022723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022723)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022723)Termination reason: Instruction limit
% 8.63/2.08 % (2022723)Termination phase: Saturation
% 8.63/2.08 % (2022723)Time elapsed: 0.149 s
% 8.63/2.08 % (2022723)Peak memory usage: 93 MB
% 8.63/2.08 % (2022723)Instructions burned: 249 (million)
% 8.63/2.08 % (2022722)Instruction limit reached!
% 8.63/2.08 % (2022722)------------------------------
% 8.63/2.08 % (2022722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022722)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022722)Termination reason: Instruction limit
% 8.63/2.08 % (2022722)Termination phase: Saturation
% 8.63/2.08 % (2022722)Time elapsed: 0.229 s
% 8.63/2.08 % (2022722)Peak memory usage: 93 MB
% 8.63/2.08 % (2022722)Instructions burned: 326 (million)
% 8.63/2.08 % (2022727)Instruction limit reached!
% 8.63/2.08 % (2022727)------------------------------
% 8.63/2.08 % (2022727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022727)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022727)Termination reason: Instruction limit
% 8.63/2.08 % (2022727)Termination phase: Saturation
% 8.63/2.08 % (2022727)Time elapsed: 0.100 s
% 8.63/2.08 % (2022727)Peak memory usage: 91 MB
% 8.63/2.08 % (2022727)Instructions burned: 296 (million)
% 8.63/2.08 % (2022721)------------------------------
% 8.63/2.08 % (2022721)------------------------------
% 8.63/2.08 % (2022730)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2406216224:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.63/2.08 % (2022732)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=460796278:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 8.63/2.08 % (2022731)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1697627526:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.63/2.08 % (2022732)Instruction limit reached!
% 8.63/2.08 % (2022732)------------------------------
% 8.63/2.08 % (2022732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022732)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022732)Termination reason: Instruction limit
% 8.63/2.08 % (2022732)Termination phase: Saturation
% 8.63/2.08 % (2022732)Time elapsed: 0.038 s
% 8.63/2.08 % (2022732)Peak memory usage: 90 MB
% 8.63/2.08 % (2022732)Instructions burned: 128 (million)
% 8.63/2.08 % (2022733)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3192226391:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 8.63/2.08 % (2022731)Instruction limit reached!
% 8.63/2.08 % (2022731)------------------------------
% 8.63/2.08 % (2022731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022731)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022731)Termination reason: Instruction limit
% 8.63/2.08 % (2022731)Termination phase: Saturation
% 8.63/2.08 % (2022731)Time elapsed: 0.071 s
% 8.63/2.08 % (2022731)Peak memory usage: 90 MB
% 8.63/2.08 % (2022731)Instructions burned: 114 (million)
% 8.63/2.08 % (2022733)Instruction limit reached!
% 8.63/2.08 % (2022733)------------------------------
% 8.63/2.08 % (2022733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.63/2.08 % (2022733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.63/2.08 % (2022733)CaDiCaL version: 2.1.3
% 8.63/2.08 % (2022733)Termination reason: Instruction limit
% 8.63/2.08 % (2022733)Termination phase: Saturation
% 8.63/2.08 % (2022733)Time elapsed: 0.069 s
% 8.63/2.08 % (2022733)Peak memory usage: 89 MB
% 8.63/2.08 % (2022733)Instructions burned: 116 (million)
% 8.63/2.08 % (2022737)lrs+10_1_sil=8000:sp=occurrence:random_seed=1728605750:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 8.63/2.08 % (2022706)First to succeed.
% 8.63/2.08 % (2022706)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2022701"
% 8.63/2.08 % (2022739)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1159115727:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 8.63/2.08 % (2022740)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2371400495:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 8.63/2.08 % (2022706)Refutation found. Thanks to Tanya!
% 8.63/2.08 % SZS status Theorem for theBenchmark
% 8.63/2.08 % SZS output start Proof for theBenchmark
% See solution above
% 9.05/2.18 % (2022706)------------------------------
% 9.05/2.18 % (2022706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.05/2.18 % (2022706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.05/2.18 % (2022706)CaDiCaL version: 2.1.3
% 9.05/2.18 % (2022706)Termination reason: Refutation
% 9.05/2.18 % (2022706)Time elapsed: 0.785 s
% 9.05/2.18 % (2022706)Peak memory usage: 136 MB
% 9.05/2.18 % (2022706)Instructions burned: 1202 (million)
% 9.05/2.18 % (2022706)------------------------------
% 9.05/2.18 % (2022706)------------------------------
% 9.05/2.18 % (2022701)Success in time 1.214 s
% 9.05/2.18 % Vampire exiting
%------------------------------------------------------------------------------