%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:09 PM UTC 2026
% Result : Theorem 0.09s 0.41s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 30
% Syntax : Number of formulae : 138 ( 32 unt; 17 def)
% Number of atoms : 348 ( 76 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 342 ( 132 ~; 143 |; 36 &)
% ( 21 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 18 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 86 ( 79 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ( one_to_one(A)
<=> ! [B,C] :
( ( apply(A,B) = apply(A,C)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
=> B = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B] :
( ( function(B)
& relation(B) )
=> ( in(A,relation_dom(B))
=> relation_image(B,singleton(A)) = singleton(apply(B,A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( ! [B,C] : relation_image(A,set_difference(B,C)) = set_difference(relation_image(A,B),relation_image(A,C))
=> one_to_one(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( ! [B,C] : relation_image(A,set_difference(B,C)) = set_difference(relation_image(A,B),relation_image(A,C))
=> one_to_one(A) ) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f31,axiom,
! [A,B] :
( set_difference(singleton(A),singleton(B)) = singleton(A)
<=> A != B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f47,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f59,plain,
! [A] :
( ( one_to_one(A)
<=> ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f60,plain,
! [A] :
( ( ( ? [B,C] :
( B != C
& apply(A,B) = apply(A,C)
& in(C,relation_dom(A))
& in(B,relation_dom(A)) )
| one_to_one(A) )
& ( ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [A] :
( ( ( ( sK1_skl(A) != sK2_skl(A)
& apply(A,sK1_skl(A)) = apply(A,sK2_skl(A))
& in(sK2_skl(A),relation_dom(A))
& in(sK1_skl(A),relation_dom(A)) )
| one_to_one(A) )
& ( ! [B,C] :
( B = C
| apply(A,B) != apply(A,C)
| ~ in(C,relation_dom(A))
| ~ in(B,relation_dom(A)) )
| ~ one_to_one(A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B,sK1_skl(A)),skolemize(C,sK2_skl(A))],[f60]) ).
fof(f63,plain,
! [X0] :
( in(sK1_skl(X0),relation_dom(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f64,plain,
! [X0] :
( in(sK2_skl(X0),relation_dom(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
! [X0] :
( apply(X0,sK1_skl(X0)) = apply(X0,sK2_skl(X0))
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f66,plain,
! [X0] :
( sK1_skl(X0) != sK2_skl(X0)
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f69,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f87,plain,
( relation(sK5_skl)
& empty(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f17]) ).
fof(f89,plain,
relation(sK5_skl),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f94,plain,
empty(sK7_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f19]) ).
fof(f95,plain,
empty(sK7_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
( function(sK8_skl)
& empty(sK8_skl)
& relation(sK8_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f20]) ).
fof(f97,plain,
relation(sK8_skl),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f108,plain,
( one_to_one(sK12_skl)
& function(sK12_skl)
& relation(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f24]) ).
fof(f109,plain,
relation(sK12_skl),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
function(sK12_skl),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f115,plain,
! [A] : subset(A,A),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f116,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f117,plain,
! [A,B] :
( relation_image(B,singleton(A)) = singleton(apply(B,A))
| ~ in(A,relation_dom(B))
| ~ function(B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f118,plain,
! [B] :
( ! [A] :
( relation_image(B,singleton(A)) = singleton(apply(B,A))
| ~ in(A,relation_dom(B)) )
| ~ function(B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( relation_image(X0,singleton(X1)) = singleton(apply(X0,X1))
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
? [A] :
( ~ one_to_one(A)
& ! [B,C] : relation_image(A,set_difference(B,C)) = set_difference(relation_image(A,B),relation_image(A,C))
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f121,plain,
( ~ one_to_one(sK14_skl)
& ! [B,C] : relation_image(sK14_skl,set_difference(B,C)) = set_difference(relation_image(sK14_skl,B),relation_image(sK14_skl,C))
& function(sK14_skl)
& relation(sK14_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f120]) ).
fof(f122,plain,
relation(sK14_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
function(sK14_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f124,plain,
! [X0,X1] : relation_image(sK14_skl,set_difference(X0,X1)) = set_difference(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f125,plain,
~ one_to_one(sK14_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f128,plain,
! [A,B] :
( ( A = B
| set_difference(singleton(A),singleton(B)) = singleton(A) )
& ( A != B
| set_difference(singleton(A),singleton(B)) != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f129,plain,
( ! [A,B] :
( A = B
| set_difference(singleton(A),singleton(B)) = singleton(A) )
& ! [A,B] :
( A != B
| set_difference(singleton(A),singleton(B)) != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( X0 != X1
| set_difference(singleton(X0),singleton(X1)) != singleton(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( X0 = X1
| set_difference(singleton(X0),singleton(X1)) = singleton(X0) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f134,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f33]) ).
fof(f135,plain,
( ! [A,B] :
( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ! [A,B] :
( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f137,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| set_difference(X0,X1) = empty_set ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f160,plain,
! [X0] : set_difference(singleton(X0),singleton(X0)) != singleton(X0),
inference(destructive_equality_resolution,[status(thm)],[f130]) ).
fof(f168,definition,
( sQ1_spl
<=> one_to_one(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( ~ sQ1_spl
| one_to_one(sK14_skl) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f173,definition,
( sQ2_spl
<=> function(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f175,plain,
( sQ2_spl
| ~ function(sK14_skl) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f203,plain,
! [X0] :
( relation_image(sK14_skl,singleton(X0)) = singleton(apply(sK14_skl,X0))
| ~ in(X0,relation_dom(sK14_skl))
| ~ function(sK14_skl) ),
inference(resolution,[status(thm)],[f119,f122]) ).
fof(f212,definition,
! [X0] :
( sQ8_spl
<=> ( relation_image(sK14_skl,singleton(X0)) = singleton(apply(sK14_skl,X0))
| ~ in(X0,relation_dom(sK14_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f213,plain,
! [X0] :
( ~ sQ8_spl
| relation_image(sK14_skl,singleton(X0)) = singleton(apply(sK14_skl,X0))
| ~ in(X0,relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f215,plain,
( sQ8_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f203,f173,f212]) ).
fof(f217,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f175,f123]) ).
fof(f218,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f217]) ).
fof(f298,definition,
( sQ19_spl
<=> function(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f300,plain,
( sQ19_spl
| ~ function(sK12_skl) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f306,plain,
( ~ sQ8_spl
| relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = singleton(apply(sK14_skl,sK1_skl(sK14_skl)))
| one_to_one(sK14_skl)
| ~ function(sK14_skl)
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f63,f213]) ).
fof(f315,definition,
( sQ23_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f317,plain,
( sQ23_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f315]) ).
fof(f318,definition,
( sQ24_spl
<=> relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = singleton(apply(sK14_skl,sK1_skl(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f319,plain,
( ~ sQ24_spl
| relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = singleton(apply(sK14_skl,sK1_skl(sK14_skl))) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f321,plain,
( ~ sQ8_spl
| sQ24_spl
| sQ1_spl
| ~ sQ2_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f306,f315,f173,f168,f318,f212]) ).
fof(f322,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f169,f125]) ).
fof(f323,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f322]) ).
fof(f324,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f317,f122]) ).
fof(f325,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f324]) ).
fof(f327,plain,
( ~ sQ8_spl
| relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) = singleton(apply(sK14_skl,sK2_skl(sK14_skl)))
| one_to_one(sK14_skl)
| ~ function(sK14_skl)
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f64,f213]) ).
fof(f333,definition,
( sQ26_spl
<=> relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) = singleton(apply(sK14_skl,sK2_skl(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ26_spl
| relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) = singleton(apply(sK14_skl,sK2_skl(sK14_skl))) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f336,plain,
( ~ sQ8_spl
| sQ26_spl
| sQ1_spl
| ~ sQ2_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f327,f315,f173,f168,f333,f212]) ).
fof(f337,plain,
( apply(sK14_skl,sK1_skl(sK14_skl)) = apply(sK14_skl,sK2_skl(sK14_skl))
| ~ function(sK14_skl)
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f65,f125]) ).
fof(f338,definition,
( sQ27_spl
<=> apply(sK14_skl,sK1_skl(sK14_skl)) = apply(sK14_skl,sK2_skl(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( ~ sQ27_spl
| apply(sK14_skl,sK1_skl(sK14_skl)) = apply(sK14_skl,sK2_skl(sK14_skl)) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,plain,
( sQ27_spl
| ~ sQ2_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f337,f315,f173,f338]) ).
fof(f352,definition,
( sQ30_spl
<=> sK1_skl(sK14_skl) = sK2_skl(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( ~ sQ30_spl
| sK1_skl(sK14_skl) = sK2_skl(sK14_skl) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f366,plain,
! [X0] :
( ~ sQ24_spl
| relation_image(sK14_skl,set_difference(X0,singleton(sK1_skl(sK14_skl)))) = set_difference(relation_image(sK14_skl,X0),singleton(apply(sK14_skl,sK1_skl(sK14_skl)))) ),
inference(paramodulation,[status(thm)],[f319,f124]) ).
fof(f420,definition,
( sQ43_spl
<=> relation(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( sQ43_spl
| ~ relation(sK5_skl) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f431,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f89]) ).
fof(f432,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f431]) ).
fof(f442,plain,
( ~ sQ26_spl
| ~ sQ27_spl
| relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) = singleton(apply(sK14_skl,sK1_skl(sK14_skl))) ),
inference(forward_demodulation,[status(thm)],[f339,f334]) ).
fof(f447,plain,
! [X0] :
( ~ sQ26_spl
| ~ sQ27_spl
| relation_image(sK14_skl,set_difference(X0,singleton(sK2_skl(sK14_skl)))) = set_difference(relation_image(sK14_skl,X0),singleton(apply(sK14_skl,sK1_skl(sK14_skl)))) ),
inference(paramodulation,[status(thm)],[f442,f124]) ).
fof(f465,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f110]) ).
fof(f466,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f465]) ).
fof(f473,definition,
( sQ53_spl
<=> relation(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ53_spl
| ~ relation(sK8_skl) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f484,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f97]) ).
fof(f485,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f484]) ).
fof(f545,definition,
( sQ62_spl
<=> relation(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f547,plain,
( sQ62_spl
| ~ relation(sK7_skl) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,definition,
( sQ63_spl
<=> function(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( sQ63_spl
| ~ function(sK7_skl) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f559,plain,
( sQ63_spl
| ~ empty(sK7_skl) ),
inference(resolution,[status(thm)],[f550,f45]) ).
fof(f560,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f559,f95]) ).
fof(f561,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f562,plain,
( sQ62_spl
| ~ empty(sK7_skl) ),
inference(resolution,[status(thm)],[f547,f47]) ).
fof(f563,plain,
( sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f562,f95]) ).
fof(f564,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f563]) ).
fof(f571,definition,
( sQ67_spl
<=> relation(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ67_spl
| ~ relation(sK12_skl) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f582,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f109]) ).
fof(f583,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f582]) ).
fof(f601,plain,
! [X0] :
( ~ sQ26_spl
| ~ sQ27_spl
| ~ sQ24_spl
| relation_image(sK14_skl,set_difference(X0,singleton(sK2_skl(sK14_skl)))) = relation_image(sK14_skl,set_difference(X0,singleton(sK1_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f366,f447]) ).
fof(f602,plain,
! [X0] :
( ~ sQ26_spl
| ~ sQ27_spl
| ~ sQ24_spl
| X0 = sK2_skl(sK14_skl)
| relation_image(sK14_skl,singleton(X0)) = relation_image(sK14_skl,set_difference(singleton(X0),singleton(sK1_skl(sK14_skl)))) ),
inference(paramodulation,[status(thm)],[f131,f601]) ).
fof(f668,definition,
( sQ72_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( sQ72_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f686,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f670,f69]) ).
fof(f687,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f686]) ).
fof(f714,definition,
( sQ76_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f716,plain,
( sQ76_spl
| empty_set != empty_set ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f722,plain,
( sQ76_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f716]) ).
fof(f723,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f724,plain,
! [X0] : set_difference(X0,X0) = empty_set,
inference(resolution,[status(thm)],[f137,f116]) ).
fof(f747,plain,
! [X0] : empty_set != singleton(X0),
inference(backward_demodulation,[status(thm)],[f724,f160]) ).
fof(f751,plain,
! [X0] : relation_image(sK14_skl,set_difference(X0,X0)) = empty_set,
inference(paramodulation,[status(thm)],[f124,f724]) ).
fof(f753,plain,
( ~ sQ26_spl
| ~ sQ27_spl
| ~ sQ24_spl
| sK1_skl(sK14_skl) = sK2_skl(sK14_skl)
| relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = relation_image(sK14_skl,empty_set) ),
inference(paramodulation,[status(thm)],[f724,f602]) ).
fof(f762,plain,
relation_image(sK14_skl,empty_set) = empty_set,
inference(forward_demodulation,[status(thm)],[f724,f751]) ).
fof(f763,definition,
( sQ78_spl
<=> relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = relation_image(sK14_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f764,plain,
( ~ sQ78_spl
| relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = relation_image(sK14_skl,empty_set) ),
inference(component_clause,[status(thm)],[f763]) ).
fof(f766,plain,
( ~ sQ26_spl
| ~ sQ27_spl
| ~ sQ24_spl
| sQ30_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f753,f763,f352,f318,f338,f333]) ).
fof(f863,plain,
( ~ sQ30_spl
| one_to_one(sK14_skl)
| ~ function(sK14_skl)
| ~ relation(sK14_skl) ),
inference(resolution,[status(thm)],[f353,f66]) ).
fof(f866,plain,
( ~ sQ30_spl
| sQ1_spl
| ~ sQ2_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f863,f315,f173,f168,f352]) ).
fof(f872,plain,
( ~ sQ78_spl
| ~ sQ24_spl
| singleton(apply(sK14_skl,sK1_skl(sK14_skl))) = relation_image(sK14_skl,empty_set) ),
inference(forward_demodulation,[status(thm)],[f319,f764]) ).
fof(f873,plain,
( ~ sQ78_spl
| ~ sQ24_spl
| singleton(apply(sK14_skl,sK1_skl(sK14_skl))) = empty_set ),
inference(forward_demodulation,[status(thm)],[f762,f872]) ).
fof(f874,plain,
( ~ sQ78_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f873,f747]) ).
fof(f875,plain,
( ~ sQ78_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f874]) ).
fof(f876,plain,
$false,
inference(sat_refutation,[status(thm)],[f215,f218,f321,f323,f325,f336,f341,f432,f466,f485,f561,f564,f583,f687,f723,f766,f866,f875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:51:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.41 % Refutation found
% 0.09/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.45 % Elapsed time: 0.069165 seconds
% 0.09/0.45 % CPU time: 0.234407 seconds
% 0.09/0.45 % Total memory used: 107.021 MB
% 0.09/0.45 % Net memory used: 106.814 MB
%------------------------------------------------------------------------------