%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU244+1 : 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 : n017.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:34 PM UTC 2026
% Result : Theorem 0.15s 5.47s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 19
% Syntax : Number of formulae : 185 ( 14 unt; 11 def)
% Number of atoms : 519 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 612 ( 278 ~; 280 |; 17 &)
% ( 27 <=>; 9 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 12 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 72 ( 0 sgn 71 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] :
( relation(X0)
=> ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_relat_2) ).
fof(f3,axiom,
! [X0] :
( relation(X0)
=> ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d14_relat_2) ).
fof(f4,axiom,
! [X0] :
( relation(X0)
=> ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_relat_2) ).
fof(f5,axiom,
! [X0] :
( relation(X0)
=> ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_wellord1) ).
fof(f6,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( well_orders(X0,X1)
<=> ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_wellord1) ).
fof(f8,axiom,
! [X0] :
( relation(X0)
=> ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d9_relat_2) ).
fof(f14,axiom,
! [X0] :
( relation(X0)
=> ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_wellord1) ).
fof(f15,conjecture,
! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_wellord1) ).
fof(f16,negated_conjecture,
~ ! [X0] :
( relation(X0)
=> ( well_orders(X0,relation_field(X0))
<=> well_ordering(X0) ) ),
inference(negated_conjecture,[status(cth)],[f15]) ).
fof(f18,plain,
! [X0] :
( ( antisymmetric(X0)
<=> is_antisymmetric_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f19,plain,
! [X0] :
( ( connected(X0)
<=> is_connected_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f20,plain,
! [X0] :
( ( transitive(X0)
<=> is_transitive_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f21,plain,
! [X0] :
( ( well_ordering(X0)
<=> ( reflexive(X0)
& transitive(X0)
& antisymmetric(X0)
& connected(X0)
& well_founded_relation(X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f5]) ).
fof(f22,plain,
! [X0] :
( ! [X1] :
( well_orders(X0,X1)
<=> ( is_reflexive_in(X0,X1)
& is_transitive_in(X0,X1)
& is_antisymmetric_in(X0,X1)
& is_connected_in(X0,X1)
& is_well_founded_in(X0,X1) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f24,plain,
! [X0] :
( ( reflexive(X0)
<=> is_reflexive_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f25,plain,
! [X0] :
( ( well_founded_relation(X0)
<=> is_well_founded_in(X0,relation_field(X0)) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f26,plain,
? [X0] :
( ( well_orders(X0,relation_field(X0))
<~> well_ordering(X0) )
& relation(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f28,plain,
! [X0] :
( ~ relation(X0)
| ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f29,plain,
! [X0] :
( ~ relation(X0)
| is_antisymmetric_in(X0,relation_field(X0))
| ~ antisymmetric(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f30,plain,
! [X0] :
( ~ relation(X0)
| ~ is_connected_in(X0,relation_field(X0))
| connected(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f31,plain,
! [X0] :
( ~ relation(X0)
| is_connected_in(X0,relation_field(X0))
| ~ connected(X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f32,plain,
! [X0] :
( ~ relation(X0)
| ~ is_transitive_in(X0,relation_field(X0))
| transitive(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f33,plain,
! [X0] :
( ~ relation(X0)
| is_transitive_in(X0,relation_field(X0))
| ~ transitive(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f34,plain,
! [X0] :
( ~ well_ordering(X0)
| well_founded_relation(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f35,plain,
! [X0] :
( ~ relation(X0)
| connected(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f36,plain,
! [X0] :
( ~ relation(X0)
| antisymmetric(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f37,plain,
! [X0] :
( ~ relation(X0)
| transitive(X0)
| ~ well_ordering(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f38,plain,
! [X0] :
( ~ well_ordering(X0)
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f39,plain,
! [X0] :
( ~ relation(X0)
| ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f40,plain,
! [X0,X1] :
( ~ relation(X0)
| is_well_founded_in(X0,X1)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f41,plain,
! [X0,X1] :
( ~ relation(X0)
| is_connected_in(X0,X1)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f42,plain,
! [X0,X1] :
( ~ relation(X0)
| is_antisymmetric_in(X0,X1)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f43,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| is_transitive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f22]) ).
fof(f44,plain,
! [X0,X1] :
( ~ relation(X0)
| is_reflexive_in(X0,X1)
| ~ well_orders(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f45,plain,
! [X0,X1] :
( ~ relation(X0)
| ~ is_well_founded_in(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| ~ is_reflexive_in(X0,X1)
| well_orders(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f47,plain,
! [X0] :
( ~ relation(X0)
| ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f48,plain,
! [X0] :
( ~ relation(X0)
| is_reflexive_in(X0,relation_field(X0))
| ~ reflexive(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f50,plain,
! [X0] :
( ~ relation(X0)
| ~ is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0) ),
inference(cnf_transformation,[],[f25]) ).
fof(f51,plain,
! [X0] :
( ~ relation(X0)
| is_well_founded_in(X0,relation_field(X0))
| ~ well_founded_relation(X0) ),
inference(cnf_transformation,[],[f25]) ).
fof(f52,plain,
( well_ordering(sK0)
| well_orders(sK0,relation_field(sK0)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f53,plain,
( ~ well_ordering(sK0)
| ~ well_orders(sK0,relation_field(sK0)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f54,plain,
relation(sK0),
inference(cnf_transformation,[],[f26]) ).
fof(f55,plain,
! [X0] :
( ~ is_antisymmetric_in(X0,relation_field(X0))
| ~ relation(X0)
| antisymmetric(X0) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f56,plain,
! [X0] :
( ~ antisymmetric(X0)
| is_antisymmetric_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f57,plain,
! [X0] :
( ~ is_connected_in(X0,relation_field(X0))
| ~ relation(X0)
| connected(X0) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f58,plain,
! [X0] :
( ~ connected(X0)
| is_connected_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f59,plain,
! [X0] :
( is_transitive_in(X0,relation_field(X0))
| ~ relation(X0)
| transitive(X0) ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f60,plain,
! [X0] :
( ~ transitive(X0)
| ~ is_transitive_in(X0,relation_field(X0))
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f61,plain,
! [X0] :
( ~ well_founded_relation(X0)
| ~ relation(X0)
| connected(X0)
| antisymmetric(X0)
| transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f62,plain,
! [X0] :
( ~ well_ordering(X0)
| ~ transitive(X0)
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f63,plain,
! [X0] :
( ~ well_ordering(X0)
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f64,plain,
! [X0] :
( ~ well_ordering(X0)
| ~ connected(X0)
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f65,plain,
! [X0,X1] :
( ~ relation(X0)
| is_well_founded_in(X0,X1)
| is_connected_in(X0,X1)
| is_antisymmetric_in(X0,X1)
| ~ is_transitive_in(X0,X1)
| is_reflexive_in(X0,X1)
| well_orders(X0,X1) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f66,plain,
! [X0,X1] :
( ~ is_reflexive_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f67,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| ~ is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f68,plain,
! [X0,X1] :
( ~ well_orders(X0,X1)
| ~ is_connected_in(X0,X1)
| ~ relation(X0) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f69,plain,
! [X0,X1] :
( ~ is_well_founded_in(X0,X1)
| ~ relation(X0)
| ~ well_orders(X0,X1) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f70,plain,
! [X0] :
( ~ is_reflexive_in(X0,relation_field(X0))
| ~ relation(X0)
| ~ reflexive(X0) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f71,plain,
! [X0] :
( ~ relation(X0)
| is_reflexive_in(X0,relation_field(X0))
| reflexive(X0) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f72,plain,
! [X0] :
( ~ is_well_founded_in(X0,relation_field(X0))
| ~ relation(X0)
| ~ well_founded_relation(X0) ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f73,plain,
! [X0] :
( ~ relation(X0)
| is_well_founded_in(X0,relation_field(X0))
| well_founded_relation(X0) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f75,definition,
( spl1_1
<=> well_orders(sK0,relation_field(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
fof(f77,plain,
( well_orders(sK0,relation_field(sK0))
| ~ spl1_1 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f79,definition,
( spl1_2
<=> well_ordering(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
fof(f80,plain,
( ~ well_ordering(sK0)
| spl1_2 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f81,plain,
( well_ordering(sK0)
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f82,plain,
( spl1_1
| spl1_2 ),
inference(avatar_split_clause,[],[f52,f79,f75]) ).
fof(f83,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f53,f79,f75]) ).
fof(f84,plain,
( well_founded_relation(sK0)
| ~ relation(sK0)
| ~ spl1_2 ),
inference(resolution,[],[f34,f81]) ).
fof(f85,plain,
( well_founded_relation(sK0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f84,f54]) ).
fof(f86,plain,
( reflexive(sK0)
| ~ relation(sK0)
| ~ spl1_2 ),
inference(resolution,[],[f38,f81]) ).
fof(f87,plain,
( reflexive(sK0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f86,f54]) ).
fof(f88,plain,
( ~ transitive(sK0)
| ~ relation(sK0)
| ~ spl1_2 ),
inference(resolution,[],[f62,f81]) ).
fof(f89,plain,
( ~ transitive(sK0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f88,f54]) ).
fof(f90,plain,
( ~ antisymmetric(sK0)
| ~ relation(sK0)
| ~ spl1_2 ),
inference(resolution,[],[f63,f81]) ).
fof(f91,plain,
( ~ antisymmetric(sK0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f90,f54]) ).
fof(f92,plain,
( ~ connected(sK0)
| ~ relation(sK0)
| ~ spl1_2 ),
inference(resolution,[],[f64,f81]) ).
fof(f93,plain,
( ~ connected(sK0)
| ~ spl1_2 ),
inference(forward_subsumption_resolution,[],[f92,f54]) ).
fof(f94,plain,
( is_reflexive_in(sK0,relation_field(sK0))
| reflexive(sK0) ),
inference(resolution,[],[f71,f54]) ).
fof(f95,plain,
( is_well_founded_in(sK0,relation_field(sK0))
| well_founded_relation(sK0) ),
inference(resolution,[],[f73,f54]) ).
fof(f98,plain,
! [X0] :
( ~ is_transitive_in(sK0,X0)
| is_connected_in(sK0,X0)
| is_antisymmetric_in(sK0,X0)
| is_well_founded_in(sK0,X0)
| is_reflexive_in(sK0,X0)
| well_orders(sK0,X0) ),
inference(resolution,[],[f65,f54]) ).
fof(f99,plain,
( is_connected_in(sK0,relation_field(sK0))
| is_antisymmetric_in(sK0,relation_field(sK0))
| is_well_founded_in(sK0,relation_field(sK0))
| is_reflexive_in(sK0,relation_field(sK0))
| well_orders(sK0,relation_field(sK0))
| ~ relation(sK0)
| transitive(sK0) ),
inference(resolution,[],[f98,f59]) ).
fof(f104,definition,
( spl1_3
<=> is_reflexive_in(sK0,relation_field(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f106,plain,
( is_reflexive_in(sK0,relation_field(sK0))
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f108,definition,
( spl1_4
<=> is_well_founded_in(sK0,relation_field(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f110,plain,
( is_well_founded_in(sK0,relation_field(sK0))
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f112,definition,
( spl1_5
<=> is_antisymmetric_in(sK0,relation_field(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f114,plain,
( is_antisymmetric_in(sK0,relation_field(sK0))
| ~ spl1_5 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f116,definition,
( spl1_6
<=> is_connected_in(sK0,relation_field(sK0)) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
fof(f118,plain,
( is_connected_in(sK0,relation_field(sK0))
| ~ spl1_6 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f120,plain,
( ~ relation(sK0)
| ~ reflexive(sK0)
| ~ spl1_3 ),
inference(resolution,[],[f106,f70]) ).
fof(f121,plain,
( ~ relation(sK0)
| ~ well_orders(sK0,relation_field(sK0))
| ~ spl1_3 ),
inference(resolution,[],[f106,f66]) ).
fof(f122,plain,
( ~ reflexive(sK0)
| ~ spl1_3 ),
inference(forward_subsumption_resolution,[],[f120,f54]) ).
fof(f123,plain,
( $false
| ~ spl1_2
| ~ spl1_3 ),
inference(forward_subsumption_resolution,[],[f122,f87]) ).
fof(f124,plain,
( ~ spl1_2
| ~ spl1_3 ),
inference(avatar_contradiction_clause,[],[f123]) ).
fof(f126,definition,
( spl1_7
<=> well_founded_relation(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f128,plain,
( well_founded_relation(sK0)
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
( spl1_7
| spl1_4 ),
inference(avatar_split_clause,[],[f95,f108,f126]) ).
fof(f130,plain,
( ~ well_orders(sK0,relation_field(sK0))
| ~ spl1_3 ),
inference(forward_subsumption_resolution,[],[f121,f54]) ).
fof(f131,plain,
( ~ spl1_1
| ~ spl1_3 ),
inference(avatar_split_clause,[],[f130,f104,f75]) ).
fof(f134,definition,
( spl1_8
<=> transitive(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f135,plain,
( ~ transitive(sK0)
| spl1_8 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f136,plain,
( transitive(sK0)
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f138,plain,
( spl1_7
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f85,f79,f126]) ).
fof(f139,plain,
( ~ spl1_8
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f89,f79,f134]) ).
fof(f141,definition,
( spl1_9
<=> reflexive(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f143,plain,
( reflexive(sK0)
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
( spl1_9
| spl1_3 ),
inference(avatar_split_clause,[],[f94,f104,f141]) ).
fof(f145,plain,
( is_connected_in(sK0,relation_field(sK0))
| is_antisymmetric_in(sK0,relation_field(sK0))
| is_well_founded_in(sK0,relation_field(sK0))
| is_reflexive_in(sK0,relation_field(sK0))
| well_orders(sK0,relation_field(sK0))
| transitive(sK0) ),
inference(forward_subsumption_resolution,[],[f99,f54]) ).
fof(f146,plain,
( spl1_8
| spl1_1
| spl1_3
| spl1_4
| spl1_5
| spl1_6 ),
inference(avatar_split_clause,[],[f145,f116,f112,f108,f104,f75,f134]) ).
fof(f158,plain,
( ~ relation(sK0)
| connected(sK0)
| antisymmetric(sK0)
| transitive(sK0)
| ~ reflexive(sK0)
| well_ordering(sK0)
| ~ spl1_7 ),
inference(resolution,[],[f128,f61]) ).
fof(f159,plain,
( ~ relation(sK0)
| ~ well_founded_relation(sK0)
| ~ spl1_4 ),
inference(resolution,[],[f110,f72]) ).
fof(f160,plain,
( ~ relation(sK0)
| ~ well_orders(sK0,relation_field(sK0))
| ~ spl1_4 ),
inference(resolution,[],[f110,f69]) ).
fof(f161,plain,
( ~ well_founded_relation(sK0)
| ~ spl1_4 ),
inference(forward_subsumption_resolution,[],[f159,f54]) ).
fof(f164,plain,
( ~ relation(sK0)
| antisymmetric(sK0)
| ~ spl1_5 ),
inference(resolution,[],[f114,f55]) ).
fof(f165,plain,
( antisymmetric(sK0)
| ~ spl1_5 ),
inference(forward_subsumption_resolution,[],[f164,f54]) ).
fof(f166,plain,
( $false
| ~ spl1_2
| ~ spl1_5 ),
inference(forward_subsumption_resolution,[],[f165,f91]) ).
fof(f167,plain,
( ~ spl1_2
| ~ spl1_5 ),
inference(avatar_contradiction_clause,[],[f166]) ).
fof(f168,plain,
( ~ relation(sK0)
| connected(sK0)
| ~ spl1_6 ),
inference(resolution,[],[f118,f57]) ).
fof(f169,plain,
( connected(sK0)
| ~ spl1_6 ),
inference(forward_subsumption_resolution,[],[f168,f54]) ).
fof(f170,plain,
( $false
| ~ spl1_2
| ~ spl1_6 ),
inference(forward_subsumption_resolution,[],[f169,f93]) ).
fof(f171,plain,
( ~ spl1_2
| ~ spl1_6 ),
inference(avatar_contradiction_clause,[],[f170]) ).
fof(f172,plain,
( connected(sK0)
| antisymmetric(sK0)
| transitive(sK0)
| ~ reflexive(sK0)
| well_ordering(sK0)
| ~ spl1_7 ),
inference(forward_subsumption_resolution,[],[f158,f54]) ).
fof(f173,plain,
( connected(sK0)
| antisymmetric(sK0)
| ~ reflexive(sK0)
| well_ordering(sK0)
| ~ spl1_7
| spl1_8 ),
inference(forward_subsumption_resolution,[],[f172,f135]) ).
fof(f176,definition,
( spl1_10
<=> antisymmetric(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
fof(f178,plain,
( antisymmetric(sK0)
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl1_11
<=> connected(sK0) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f182,plain,
( connected(sK0)
| ~ spl1_11 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,plain,
( ~ is_connected_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_1 ),
inference(resolution,[],[f77,f68]) ).
fof(f185,plain,
( ~ is_antisymmetric_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_1 ),
inference(resolution,[],[f77,f67]) ).
fof(f186,plain,
( is_transitive_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_1 ),
inference(resolution,[],[f77,f43]) ).
fof(f187,plain,
( is_transitive_in(sK0,relation_field(sK0))
| ~ spl1_1 ),
inference(forward_subsumption_resolution,[],[f186,f54]) ).
fof(f188,plain,
( ~ is_connected_in(sK0,relation_field(sK0))
| ~ spl1_1 ),
inference(forward_subsumption_resolution,[],[f184,f54]) ).
fof(f189,plain,
( ~ spl1_6
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f188,f75,f116]) ).
fof(f191,plain,
( is_antisymmetric_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_10 ),
inference(resolution,[],[f178,f56]) ).
fof(f195,plain,
( is_connected_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_11 ),
inference(resolution,[],[f182,f58]) ).
fof(f196,plain,
( is_connected_in(sK0,relation_field(sK0))
| ~ spl1_11 ),
inference(forward_subsumption_resolution,[],[f195,f54]) ).
fof(f197,plain,
( spl1_6
| ~ spl1_11 ),
inference(avatar_split_clause,[],[f196,f180,f116]) ).
fof(f202,plain,
( ~ is_transitive_in(sK0,relation_field(sK0))
| ~ relation(sK0)
| ~ spl1_8 ),
inference(resolution,[],[f136,f60]) ).
fof(f203,plain,
( ~ relation(sK0)
| ~ spl1_1
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f202,f187]) ).
fof(f204,plain,
( $false
| ~ spl1_1
| ~ spl1_8 ),
inference(forward_subsumption_resolution,[],[f203,f54]) ).
fof(f205,plain,
( ~ spl1_1
| ~ spl1_8 ),
inference(avatar_contradiction_clause,[],[f204]) ).
fof(f206,plain,
( ~ well_orders(sK0,relation_field(sK0))
| ~ spl1_4 ),
inference(forward_subsumption_resolution,[],[f160,f54]) ).
fof(f207,plain,
( ~ spl1_7
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f161,f108,f126]) ).
fof(f208,plain,
( $false
| ~ spl1_1
| ~ spl1_4 ),
inference(forward_subsumption_resolution,[],[f206,f77]) ).
fof(f209,plain,
( ~ spl1_1
| ~ spl1_4 ),
inference(avatar_contradiction_clause,[],[f208]) ).
fof(f212,plain,
( connected(sK0)
| antisymmetric(sK0)
| well_ordering(sK0)
| ~ spl1_7
| spl1_8
| ~ spl1_9 ),
inference(forward_subsumption_resolution,[],[f173,f143]) ).
fof(f214,plain,
( is_antisymmetric_in(sK0,relation_field(sK0))
| ~ spl1_10 ),
inference(forward_subsumption_resolution,[],[f191,f54]) ).
fof(f215,plain,
( ~ is_antisymmetric_in(sK0,relation_field(sK0))
| ~ spl1_1 ),
inference(forward_subsumption_resolution,[],[f185,f54]) ).
fof(f217,plain,
( connected(sK0)
| antisymmetric(sK0)
| spl1_2
| ~ spl1_7
| spl1_8
| ~ spl1_9 ),
inference(forward_subsumption_resolution,[],[f212,f80]) ).
fof(f219,plain,
( spl1_5
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f214,f176,f112]) ).
fof(f220,plain,
( ~ spl1_5
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f215,f75,f112]) ).
fof(f222,plain,
( spl1_10
| spl1_11
| spl1_2
| ~ spl1_7
| spl1_8
| ~ spl1_9 ),
inference(avatar_split_clause,[],[f217,f141,f134,f126,f79,f180,f176]) ).
cnf(s1,plain,
( spl1_1
| spl1_2 ),
inference(sat_conversion,[],[f82]) ).
cnf(s2,plain,
( ~ spl1_1
| ~ spl1_2 ),
inference(sat_conversion,[],[f83]) ).
cnf(s4,plain,
( ~ spl1_2
| ~ spl1_3 ),
inference(sat_conversion,[],[f124]) ).
cnf(s5,plain,
( spl1_4
| spl1_7 ),
inference(sat_conversion,[],[f129]) ).
cnf(s6,plain,
( ~ spl1_1
| ~ spl1_3 ),
inference(sat_conversion,[],[f131]) ).
cnf(s9,plain,
( ~ spl1_2
| spl1_7 ),
inference(sat_conversion,[],[f138]) ).
cnf(s10,plain,
( ~ spl1_2
| ~ spl1_8 ),
inference(sat_conversion,[],[f139]) ).
cnf(s11,plain,
( spl1_3
| spl1_9 ),
inference(sat_conversion,[],[f144]) ).
cnf(s12,plain,
( spl1_1
| spl1_3
| spl1_4
| spl1_5
| spl1_6
| spl1_8 ),
inference(sat_conversion,[],[f146]) ).
cnf(s18,plain,
( ~ spl1_2
| ~ spl1_5 ),
inference(sat_conversion,[],[f167]) ).
cnf(s19,plain,
( ~ spl1_2
| ~ spl1_6 ),
inference(sat_conversion,[],[f171]) ).
cnf(s21,plain,
( ~ spl1_1
| ~ spl1_6 ),
inference(sat_conversion,[],[f189]) ).
cnf(s23,plain,
( spl1_6
| ~ spl1_11 ),
inference(sat_conversion,[],[f197]) ).
cnf(s25,plain,
( ~ spl1_1
| ~ spl1_8 ),
inference(sat_conversion,[],[f205]) ).
cnf(s26,plain,
( ~ spl1_4
| ~ spl1_7 ),
inference(sat_conversion,[],[f207]) ).
cnf(s27,plain,
( ~ spl1_1
| ~ spl1_4 ),
inference(sat_conversion,[],[f209]) ).
cnf(s30,plain,
( spl1_5
| ~ spl1_10 ),
inference(sat_conversion,[],[f219]) ).
cnf(s31,plain,
( ~ spl1_1
| ~ spl1_5 ),
inference(sat_conversion,[],[f220]) ).
cnf(s33,plain,
( spl1_2
| ~ spl1_7
| spl1_8
| ~ spl1_9
| spl1_10
| spl1_11 ),
inference(sat_conversion,[],[f222]) ).
cnf(s34,plain,
spl1_1,
inference(rat,[],[s12,s26,s4,s9,s10,s18,s19,s1]) ).
cnf(s35,plain,
~ spl1_5,
inference(rat,[],[s31,s34]) ).
cnf(s36,plain,
~ spl1_4,
inference(rat,[],[s27,s34]) ).
cnf(s37,plain,
~ spl1_8,
inference(rat,[],[s25,s34]) ).
cnf(s38,plain,
~ spl1_6,
inference(rat,[],[s21,s34]) ).
cnf(s39,plain,
~ spl1_3,
inference(rat,[],[s6,s34]) ).
cnf(s40,plain,
~ spl1_2,
inference(rat,[],[s2,s34]) ).
cnf(s41,plain,
~ spl1_10,
inference(rat,[],[s30,s35]) ).
cnf(s42,plain,
spl1_7,
inference(rat,[],[s5,s36]) ).
cnf(s43,plain,
~ spl1_11,
inference(rat,[],[s23,s38]) ).
cnf(s44,plain,
spl1_9,
inference(rat,[],[s11,s39]) ).
cnf(s45,plain,
$false,
inference(rat,[],[s33,s43,s41,s37,s40,s44,s42]) ).
fof(f223,plain,
$false,
inference(avatar_sat_refutation,[],[s45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU244+1 : 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/5.39 % Computer : n017.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Mon Sep 28 04:12:28 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/5.42 Running first-order model finding
% 0.15/5.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.47 % (3193441)Will run a generic schedule for satisfiability detection.
% 0.15/5.47 % (3193447)% WARNING: option uhcvi not known.
% 0.15/5.47 % (3193447)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=732431482:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.15/5.47 % (3193447) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3193441-3193447"...
% 0.15/5.47 % (3193447)...printing done.
% 0.15/5.47 % (3193447)Refutation found. Thanks to Tanya!
% 0.15/5.47 % SZS status Theorem for theBenchmark
% 0.15/5.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/5.47 % (3193447)------------------------------
% 0.15/5.47 % (3193447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.15/5.47 % (3193447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/5.47 % (3193447)CaDiCaL version: 2.1.3
% 0.15/5.47 % (3193447)Termination reason: Refutation
% 0.15/5.47 % (3193447)Time elapsed: 0.004 s
% 0.15/5.47 % (3193447)Peak memory usage: 12 MB
% 0.15/5.47 % (3193447)Instructions burned: 7 (million)
% 0.15/5.47 % (3193441)Success in time 0.033 s
% 0.15/5.47 % Vampire exiting
%------------------------------------------------------------------------------