%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU253+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 02:19:55 PM UTC 2026
% Result : Theorem 0.07s 0.40s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 34
% Syntax : Number of formulae : 148 ( 24 unt; 23 def)
% Number of atoms : 392 ( 11 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 419 ( 175 ~; 162 |; 45 &)
% ( 28 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 24 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 119 ( 109 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [A,B] :
( relation(A)
=> relation(relation_restriction(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( relation(A)
=> ( connected(A)
<=> ! [B,C] :
~ ( ~ in(ordered_pair(C,B),A)
& ~ in(ordered_pair(B,C),A)
& B != C
& in(C,relation_field(A))
& in(B,relation_field(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A,B,C,D] :
( in(ordered_pair(A,B),cartesian_product2(C,D))
<=> ( in(B,D)
& in(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_field(relation_restriction(C,B)))
=> ( in(A,B)
& in(A,relation_field(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,conjecture,
! [A,B] :
( relation(B)
=> ( connected(B)
=> connected(relation_restriction(B,A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> ( connected(B)
=> connected(relation_restriction(B,A)) ) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f45,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,plain,
! [A,B] :
( relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f64,plain,
! [A] :
( ! [B] : relation(relation_restriction(A,B))
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( relation(relation_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [A] : element(sK0_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f22]) ).
fof(f67,plain,
! [X0] : element(sK0_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f80,plain,
! [A] :
( ( connected(A)
<=> ! [B,C] :
( in(ordered_pair(C,B),A)
| in(ordered_pair(B,C),A)
| B = C
| ~ in(C,relation_field(A))
| ~ in(B,relation_field(A)) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f81,plain,
! [A] :
( ( ( ? [B,C] :
( ~ in(ordered_pair(C,B),A)
& ~ in(ordered_pair(B,C),A)
& B != C
& in(C,relation_field(A))
& in(B,relation_field(A)) )
| connected(A) )
& ( ! [B,C] :
( in(ordered_pair(C,B),A)
| in(ordered_pair(B,C),A)
| B = C
| ~ in(C,relation_field(A))
| ~ in(B,relation_field(A)) )
| ~ connected(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f82,plain,
! [A] :
( ( ( ( ~ in(ordered_pair(sK2_skl(A),sK1_skl(A)),A)
& ~ in(ordered_pair(sK1_skl(A),sK2_skl(A)),A)
& sK1_skl(A) != sK2_skl(A)
& in(sK2_skl(A),relation_field(A))
& in(sK1_skl(A),relation_field(A)) )
| connected(A) )
& ( ! [B,C] :
( in(ordered_pair(C,B),A)
| in(ordered_pair(B,C),A)
| B = C
| ~ in(C,relation_field(A))
| ~ in(B,relation_field(A)) )
| ~ connected(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B,sK1_skl(A)),skolemize(C,sK2_skl(A))],[f81]) ).
fof(f83,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,X1),X0)
| in(ordered_pair(X1,X2),X0)
| X1 = X2
| ~ in(X2,relation_field(X0))
| ~ in(X1,relation_field(X0))
| ~ connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0] :
( in(sK1_skl(X0),relation_field(X0))
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f85,plain,
! [X0] :
( in(sK2_skl(X0),relation_field(X0))
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f86,plain,
! [X0] :
( sK1_skl(X0) != sK2_skl(X0)
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f87,plain,
! [X0] :
( ~ in(ordered_pair(sK1_skl(X0),sK2_skl(X0)),X0)
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f88,plain,
! [X0] :
( ~ in(ordered_pair(sK2_skl(X0),sK1_skl(X0)),X0)
| connected(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f89,plain,
( function(sK3_skl)
& relation(sK3_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f30]) ).
fof(f90,plain,
relation(sK3_skl),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f94,plain,
( function(sK5_skl)
& empty(sK5_skl)
& relation(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f32]) ).
fof(f95,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f100,plain,
( one_to_one(sK7_skl)
& function(sK7_skl)
& relation(sK7_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f34]) ).
fof(f101,plain,
relation(sK7_skl),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f104,plain,
! [A,B,C,D] :
( ( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f105,plain,
( ! [A,B,C,D] :
( ~ in(B,D)
| ~ in(A,C)
| in(ordered_pair(A,B),cartesian_product2(C,D)) )
& ! [A,B,C,D] :
( ( in(B,D)
& in(A,C) )
| ~ in(ordered_pair(A,B),cartesian_product2(C,D)) ) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( ~ in(X1,X3)
| ~ in(X0,X2)
| in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f109,plain,
! [A,B,C] :
( ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) )
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f110,plain,
! [A,B,C] :
( ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(NNF_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [C] :
( ( ! [A,B] :
( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C)
| in(A,relation_restriction(C,B)) )
& ! [A,B] :
( ( in(A,cartesian_product2(B,B))
& in(A,C) )
| ~ in(A,relation_restriction(C,B)) ) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f114,plain,
! [X0,X1,X2] :
( ~ in(X1,cartesian_product2(X2,X2))
| ~ in(X1,X0)
| in(X1,relation_restriction(X0,X2))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f115,plain,
! [A,B,C] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B)))
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f116,plain,
! [C] :
( ! [A,B] :
( ( in(A,B)
& in(A,relation_field(C)) )
| ~ in(A,relation_field(relation_restriction(C,B))) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f117,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(X1,relation_field(relation_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
! [X0,X1,X2] :
( in(X1,X2)
| ~ in(X1,relation_field(relation_restriction(X0,X2)))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f122,plain,
? [A,B] :
( ~ connected(relation_restriction(B,A))
& connected(B)
& relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f123,plain,
? [B] :
( ? [A] : ~ connected(relation_restriction(B,A))
& connected(B)
& relation(B) ),
inference(miniscoping,[status(thm)],[f122]) ).
fof(f124,plain,
( ~ connected(relation_restriction(sK8_skl,sK9_skl))
& connected(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(B,sK8_skl),skolemize(A,sK9_skl)],[f123]) ).
fof(f125,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
connected(sK8_skl),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f127,plain,
~ connected(relation_restriction(sK8_skl,sK9_skl)),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f133,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f134,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f190,plain,
( in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl)))
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(resolution,[status(thm)],[f84,f127]) ).
fof(f191,definition,
( sQ0_spl
<=> relation(relation_restriction(sK8_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ0_spl
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
( sQ1_spl
<=> in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f195,plain,
( ~ sQ1_spl
| in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl))) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f190,f191,f194]) ).
fof(f198,plain,
( sQ0_spl
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f193,f65]) ).
fof(f199,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f198,f125]) ).
fof(f200,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f199]) ).
fof(f201,plain,
( ~ sQ1_spl
| in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl))
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f195,f117]) ).
fof(f202,plain,
( ~ sQ1_spl
| in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f195,f118]) ).
fof(f205,definition,
( sQ2_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f207,plain,
( sQ2_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,definition,
( sQ3_spl
<=> in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( ~ sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f201,f205,f208,f194]) ).
fof(f212,definition,
( sQ4_spl
<=> in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f215,plain,
( ~ sQ1_spl
| sQ4_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f202,f205,f212,f194]) ).
fof(f223,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f207,f125]) ).
fof(f224,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f223]) ).
fof(f247,plain,
( in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl)))
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(resolution,[status(thm)],[f85,f127]) ).
fof(f248,definition,
( sQ7_spl
<=> in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f249,plain,
( ~ sQ7_spl
| in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(relation_restriction(sK8_skl,sK9_skl))) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,plain,
( sQ7_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f247,f191,f248]) ).
fof(f252,plain,
( sK1_skl(relation_restriction(sK8_skl,sK9_skl)) != sK2_skl(relation_restriction(sK8_skl,sK9_skl))
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(resolution,[status(thm)],[f86,f127]) ).
fof(f253,definition,
( sQ8_spl
<=> sK1_skl(relation_restriction(sK8_skl,sK9_skl)) = sK2_skl(relation_restriction(sK8_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ8_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f252,f191,f253]) ).
fof(f257,plain,
( ~ sQ7_spl
| in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl))
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f249,f117]) ).
fof(f258,plain,
( ~ sQ7_spl
| in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f249,f118]) ).
fof(f261,definition,
( sQ9_spl
<=> in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f264,plain,
( ~ sQ7_spl
| sQ9_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f257,f205,f261,f248]) ).
fof(f265,definition,
( sQ10_spl
<=> in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( ~ sQ7_spl
| sQ10_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f258,f205,f265,f248]) ).
fof(f285,definition,
( sQ12_spl
<=> connected(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f287,plain,
( sQ12_spl
| ~ connected(sK8_skl) ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f292,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f287,f126]) ).
fof(f293,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f292]) ).
fof(f325,plain,
! [X0,X1,X2,X3] :
( ~ in(X2,X3)
| ~ in(X1,X3)
| ~ in(ordered_pair(X1,X2),X0)
| in(ordered_pair(X1,X2),relation_restriction(X0,X3))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f114,f108]) ).
fof(f362,plain,
! [X0] : ~ in(X0,sK5_skl),
inference(resolution,[status(thm)],[f135,f96]) ).
fof(f377,definition,
( sQ21_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f379,plain,
( sQ21_spl
| ~ relation(sK5_skl) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f387,definition,
! [X0] :
( sQ24_spl
<=> ~ element(X0,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f388,plain,
! [X0] :
( ~ sQ24_spl
| ~ element(X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f395,plain,
( ~ sQ24_spl
| $false ),
inference(resolution,[status(thm)],[f388,f67]) ).
fof(f397,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f395]) ).
fof(f414,plain,
( ~ in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl))
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(resolution,[status(thm)],[f88,f127]) ).
fof(f415,definition,
( sQ26_spl
<=> in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ26_spl
| ~ in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,plain,
( ~ sQ26_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f414,f191,f415]) ).
fof(f419,plain,
( ~ in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl))
| ~ relation(relation_restriction(sK8_skl,sK9_skl)) ),
inference(resolution,[status(thm)],[f87,f127]) ).
fof(f420,definition,
( sQ27_spl
<=> in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( sQ27_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),relation_restriction(sK8_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,plain,
( ~ sQ27_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f419,f191,f420]) ).
fof(f435,definition,
( sQ29_spl
<=> in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f737,definition,
! [X0] :
( sQ54_spl
<=> ( ~ element(X0,sK5_skl)
| in(X0,sK5_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f738,plain,
! [X0] :
( ~ sQ54_spl
| ~ element(X0,sK5_skl)
| in(X0,sK5_skl) ),
inference(component_clause,[status(thm)],[f737]) ).
fof(f760,plain,
! [X0] :
( ~ sQ54_spl
| ~ element(X0,sK5_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f362]) ).
fof(f809,definition,
! [X0] :
( sQ68_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f810,plain,
! [X0] :
( ~ sQ68_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f809]) ).
fof(f816,plain,
( ~ sQ54_spl
| $false ),
inference(resolution,[status(thm)],[f760,f67]) ).
fof(f818,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f816]) ).
fof(f949,definition,
! [X0] :
( sQ76_spl
<=> ~ element(X0,relation_field(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f950,plain,
! [X0] :
( ~ sQ76_spl
| ~ element(X0,relation_field(sK5_skl)) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f953,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f95]) ).
fof(f954,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f953]) ).
fof(f1006,plain,
( sQ27_spl
| ~ in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f422,f325]) ).
fof(f1016,definition,
( sQ81_spl
<=> in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1018,plain,
( sQ81_spl
| ~ in(ordered_pair(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK2_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl) ),
inference(component_clause,[status(thm)],[f1016]) ).
fof(f1019,plain,
( sQ27_spl
| ~ sQ10_spl
| ~ sQ4_spl
| ~ sQ81_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1006,f205,f1016,f212,f265,f420]) ).
fof(f1038,plain,
( ~ sQ76_spl
| $false ),
inference(resolution,[status(thm)],[f950,f67]) ).
fof(f1040,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1038]) ).
fof(f1043,plain,
( sQ26_spl
| ~ in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK9_skl)
| ~ in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f417,f325]) ).
fof(f1053,plain,
( sQ26_spl
| ~ sQ4_spl
| ~ sQ10_spl
| ~ sQ29_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1043,f205,f435,f265,f212,f415]) ).
fof(f1069,plain,
( ~ sQ68_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f96,f810]) ).
fof(f1070,plain,
~ sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1069]) ).
fof(f1447,definition,
( sQ116_spl
<=> relation(relation_restriction(sK7_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1449,plain,
( sQ116_spl
| ~ relation(relation_restriction(sK7_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f1447]) ).
fof(f1476,plain,
( sQ116_spl
| ~ relation(sK7_skl) ),
inference(resolution,[status(thm)],[f1449,f65]) ).
fof(f1477,plain,
( sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1476,f101]) ).
fof(f1478,plain,
sQ116_spl,
inference(contradiction_clause,[status(thm)],[f1477]) ).
fof(f1481,definition,
( sQ123_spl
<=> relation(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1483,plain,
( sQ123_spl
| ~ relation(sK7_skl) ),
inference(component_clause,[status(thm)],[f1481]) ).
fof(f1492,plain,
( sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1483,f101]) ).
fof(f1493,plain,
sQ123_spl,
inference(contradiction_clause,[status(thm)],[f1492]) ).
fof(f1698,definition,
( sQ141_spl
<=> relation(relation_restriction(sK3_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1700,plain,
( sQ141_spl
| ~ relation(relation_restriction(sK3_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f1698]) ).
fof(f1758,plain,
( sQ141_spl
| ~ relation(sK3_skl) ),
inference(resolution,[status(thm)],[f1700,f65]) ).
fof(f1759,plain,
( sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1758,f90]) ).
fof(f1760,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f1759]) ).
fof(f1763,definition,
( sQ151_spl
<=> relation(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1765,plain,
( sQ151_spl
| ~ relation(sK3_skl) ),
inference(component_clause,[status(thm)],[f1763]) ).
fof(f1774,plain,
( sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1765,f90]) ).
fof(f1775,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f1774]) ).
fof(f2864,plain,
( sQ81_spl
| in(ordered_pair(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),sK1_skl(relation_restriction(sK8_skl,sK9_skl))),sK8_skl)
| sK2_skl(relation_restriction(sK8_skl,sK9_skl)) = sK1_skl(relation_restriction(sK8_skl,sK9_skl))
| ~ in(sK1_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl))
| ~ in(sK2_skl(relation_restriction(sK8_skl,sK9_skl)),relation_field(sK8_skl))
| ~ connected(sK8_skl)
| ~ relation(sK8_skl) ),
inference(resolution,[status(thm)],[f1018,f83]) ).
fof(f2875,plain,
( sQ81_spl
| sQ29_spl
| sQ8_spl
| ~ sQ3_spl
| ~ sQ9_spl
| ~ sQ12_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f2864,f205,f285,f261,f208,f253,f435,f1016]) ).
fof(f2880,plain,
$false,
inference(sat_refutation,[status(thm)],[f197,f200,f211,f215,f224,f251,f256,f264,f268,f293,f397,f418,f423,f818,f954,f1019,f1040,f1053,f1070,f1478,f1493,f1760,f1775,f2875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU253+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 06:03:22 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.07/0.40 % Refutation found
% 0.07/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.07/0.43 % Elapsed time: 0.119705 seconds
% 0.07/0.43 % CPU time: 0.691117 seconds
% 0.07/0.43 % Total memory used: 120.067 MB
% 0.07/0.43 % Net memory used: 118.443 MB
%------------------------------------------------------------------------------