%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU053+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 : n005.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 145.61s 18.96s
% Output : CNFRefutation 145.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 32
% Syntax : Number of formulae : 179 ( 38 unt; 17 def)
% Number of atoms : 481 ( 131 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 522 ( 220 ~; 232 |; 37 &)
% ( 22 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 18 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 164 ( 156 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_intersection2(A,B) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,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(f12,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] : set_intersection2(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,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(f35,conjecture,
! [A] :
( ( function(A)
& relation(A) )
=> ( ! [B,C] : relation_image(A,set_intersection2(B,C)) = set_intersection2(relation_image(A,B),relation_image(A,C))
=> one_to_one(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
~ ! [A] :
( ( function(A)
& relation(A) )
=> ( ! [B,C] : relation_image(A,set_intersection2(B,C)) = set_intersection2(relation_image(A,B),relation_image(A,C))
=> one_to_one(A) ) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [A] :
( relation(A)
=> relation_image(A,empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( A != B
=> disjoint(singleton(A),singleton(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f59,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f60,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
( ! [A,B] :
( ( ( sK0_skl(B,A) = A
| in(sK0_skl(B,A),B) )
& ( sK0_skl(B,A) != A
| ~ in(sK0_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f60]) ).
fof(f63,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f66,plain,
! [A,B] :
( ( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f67,plain,
( ! [A,B] :
( set_intersection2(A,B) != empty_set
| disjoint(A,B) )
& ! [A,B] :
( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f66]) ).
fof(f68,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = empty_set
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1] :
( disjoint(X0,X1)
| empty_set != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,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)],[f8]) ).
fof(f71,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)],[f70]) ).
fof(f72,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))],[f71]) ).
fof(f74,plain,
! [X0] :
( ~ relation(X0)
| one_to_one(X0)
| ~ function(X0)
| in(sK1_skl(X0),relation_dom(X0)) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f75,plain,
! [X0] :
( ~ relation(X0)
| in(sK2_skl(X0),relation_dom(X0))
| one_to_one(X0)
| ~ function(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f76,plain,
! [X0] :
( one_to_one(X0)
| apply(X0,sK1_skl(X0)) = apply(X0,sK2_skl(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f77,plain,
! [X0] :
( sK2_skl(X0) != sK1_skl(X0)
| one_to_one(X0)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f85,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f95,plain,
! [A] : set_intersection2(A,A) = A,
inference(miniscoping,[status(thm)],[f18]) ).
fof(f96,plain,
! [X0] : set_intersection2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f103,plain,
( relation(sK5_skl)
& empty(sK5_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f21]) ).
fof(f104,plain,
empty(sK5_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f110,plain,
empty(sK7_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f23]) ).
fof(f111,plain,
empty(sK7_skl),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f119,plain,
! [A] :
( empty(sK10_skl(A))
& element(sK10_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f26]) ).
fof(f120,plain,
! [X0] : element(sK10_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X0] : empty(sK10_skl(X0)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f141,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)],[f34]) ).
fof(f142,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)],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( ~ relation(X1)
| ~ function(X1)
| singleton(apply(X1,X0)) = relation_image(X1,singleton(X0))
| ~ in(X0,relation_dom(X1)) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
? [A] :
( ~ one_to_one(A)
& ! [B,C] : relation_image(A,set_intersection2(B,C)) = set_intersection2(relation_image(A,B),relation_image(A,C))
& function(A)
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f145,plain,
( ~ one_to_one(sK14_skl)
& ! [B,C] : relation_image(sK14_skl,set_intersection2(B,C)) = set_intersection2(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)],[f144]) ).
fof(f146,plain,
relation(sK14_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
function(sK14_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f148,plain,
! [X0,X1] : relation_image(sK14_skl,set_intersection2(X0,X1)) = set_intersection2(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f149,plain,
~ one_to_one(sK14_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f150,plain,
! [A] :
( relation_image(A,empty_set) = empty_set
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f151,plain,
! [X0] :
( relation_image(X0,empty_set) = empty_set
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [A,B] :
( disjoint(singleton(A),singleton(B))
| A = B ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f153,plain,
! [X0,X1] :
( disjoint(singleton(X1),singleton(X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f166,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f167,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| ~ in(X2,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f170,plain,
! [X0] :
( empty_set = X0
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f186,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f188,plain,
( apply(sK14_skl,sK2_skl(sK14_skl)) = apply(sK14_skl,sK1_skl(sK14_skl))
| ~ function(sK14_skl)
| one_to_one(sK14_skl) ),
inference(resolution,[status(thm)],[f76,f146]) ).
fof(f189,definition,
( sQ2_spl
<=> one_to_one(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f190,plain,
( ~ sQ2_spl
| one_to_one(sK14_skl) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,definition,
( sQ3_spl
<=> function(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f194,plain,
( sQ3_spl
| ~ function(sK14_skl) ),
inference(component_clause,[status(thm)],[f192]) ).
fof(f195,definition,
( sQ4_spl
<=> apply(sK14_skl,sK2_skl(sK14_skl)) = apply(sK14_skl,sK1_skl(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( ~ sQ4_spl
| apply(sK14_skl,sK1_skl(sK14_skl)) = apply(sK14_skl,sK2_skl(sK14_skl)) ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,plain,
( sQ4_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f188,f189,f192,f195]) ).
fof(f199,plain,
! [X0,X1] :
( disjoint(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1))
| relation_image(sK14_skl,set_intersection2(X0,X1)) != empty_set ),
inference(paramodulation,[status(thm)],[f148,f69]) ).
fof(f200,plain,
! [X0,X1] : relation_image(sK14_skl,set_intersection2(X0,X1)) = set_intersection2(relation_image(sK14_skl,X1),relation_image(sK14_skl,X0)),
inference(paramodulation,[status(thm)],[f148,f58]) ).
fof(f210,plain,
! [X0,X1] : relation_image(sK14_skl,set_intersection2(X0,X1)) = relation_image(sK14_skl,set_intersection2(X1,X0)),
inference(forward_demodulation,[status(thm)],[f148,f200]) ).
fof(f254,plain,
! [X0,X1] :
( empty_set != relation_image(sK14_skl,set_intersection2(X1,X0))
| disjoint(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)) ),
inference(paramodulation,[status(thm)],[f58,f199]) ).
fof(f276,plain,
( in(sK1_skl(sK14_skl),relation_dom(sK14_skl))
| ~ function(sK14_skl)
| one_to_one(sK14_skl) ),
inference(resolution,[status(thm)],[f74,f146]) ).
fof(f277,definition,
( sQ12_spl
<=> in(sK1_skl(sK14_skl),relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ12_spl
| in(sK1_skl(sK14_skl),relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( sQ12_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f276,f189,f192,f277]) ).
fof(f285,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f194,f147]) ).
fof(f286,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f285]) ).
fof(f287,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f190,f149]) ).
fof(f288,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f287]) ).
fof(f322,plain,
( ~ function(sK14_skl)
| in(sK2_skl(sK14_skl),relation_dom(sK14_skl))
| one_to_one(sK14_skl) ),
inference(resolution,[status(thm)],[f75,f146]) ).
fof(f331,definition,
( sQ21_spl
<=> in(sK2_skl(sK14_skl),relation_dom(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f332,plain,
( ~ sQ21_spl
| in(sK2_skl(sK14_skl),relation_dom(sK14_skl)) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,plain,
( ~ sQ3_spl
| sQ21_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f322,f189,f331,f192]) ).
fof(f531,plain,
( ~ sQ12_spl
| ~ relation(sK14_skl)
| singleton(apply(sK14_skl,sK1_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))
| ~ function(sK14_skl) ),
inference(resolution,[status(thm)],[f278,f143]) ).
fof(f533,definition,
( sQ46_spl
<=> singleton(apply(sK14_skl,sK1_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f534,plain,
( ~ sQ46_spl
| singleton(apply(sK14_skl,sK1_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) ),
inference(component_clause,[status(thm)],[f533]) ).
fof(f536,definition,
( sQ47_spl
<=> relation(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( sQ47_spl
| ~ relation(sK14_skl) ),
inference(component_clause,[status(thm)],[f536]) ).
fof(f539,plain,
( ~ sQ12_spl
| ~ sQ47_spl
| sQ46_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f531,f192,f533,f536,f277]) ).
fof(f540,plain,
( ~ sQ46_spl
| ~ sQ4_spl
| singleton(apply(sK14_skl,sK2_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) ),
inference(forward_demodulation,[status(thm)],[f196,f534]) ).
fof(f541,plain,
( ~ sQ21_spl
| ~ relation(sK14_skl)
| singleton(apply(sK14_skl,sK2_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))
| ~ function(sK14_skl) ),
inference(resolution,[status(thm)],[f332,f143]) ).
fof(f543,definition,
( sQ48_spl
<=> singleton(apply(sK14_skl,sK2_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( ~ sQ48_spl
| singleton(apply(sK14_skl,sK2_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) ),
inference(component_clause,[status(thm)],[f543]) ).
fof(f546,plain,
( ~ sQ21_spl
| ~ sQ47_spl
| sQ48_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f541,f192,f543,f536,f331]) ).
fof(f547,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f146]) ).
fof(f548,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f547]) ).
fof(f549,plain,
( ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))) = relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) ),
inference(forward_demodulation,[status(thm)],[f544,f540]) ).
fof(f710,plain,
! [X0,X1] :
( empty_set = set_intersection2(singleton(X0),singleton(X1))
| X0 = X1 ),
inference(resolution,[status(thm)],[f153,f68]) ).
fof(f1212,definition,
( sQ115_spl
<=> disjoint(relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1213,plain,
( ~ sQ115_spl
| disjoint(relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))) ),
inference(component_clause,[status(thm)],[f1212]) ).
fof(f1214,plain,
( sQ115_spl
| ~ disjoint(relation_image(sK14_skl,singleton(sK1_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))) ),
inference(component_clause,[status(thm)],[f1212]) ).
fof(f1219,plain,
( ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| disjoint(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f549,f1213]) ).
fof(f1220,plain,
( ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| disjoint(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f549,f1219]) ).
fof(f1378,plain,
( ~ function(sK14_skl)
| sK2_skl(sK14_skl) != sK1_skl(sK14_skl)
| one_to_one(sK14_skl) ),
inference(resolution,[status(thm)],[f77,f146]) ).
fof(f1411,definition,
( sQ143_spl
<=> sK2_skl(sK14_skl) = sK1_skl(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1413,plain,
( sQ143_spl
| sK1_skl(sK14_skl) != sK2_skl(sK14_skl) ),
inference(component_clause,[status(thm)],[f1411]) ).
fof(f1414,plain,
( ~ sQ3_spl
| ~ sQ143_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1378,f189,f1411,f192]) ).
fof(f1561,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ element(singleton(X0),powerset(X1)) ),
inference(resolution,[status(thm)],[f186,f168]) ).
fof(f1615,plain,
! [X0] : empty_set = sK10_skl(X0),
inference(resolution,[status(thm)],[f170,f121]) ).
fof(f1616,plain,
empty_set = sK7_skl,
inference(resolution,[status(thm)],[f170,f111]) ).
fof(f1618,plain,
empty_set = sK5_skl,
inference(resolution,[status(thm)],[f170,f104]) ).
fof(f1627,plain,
! [X0,X1] :
( relation_image(sK14_skl,set_intersection2(X1,X0)) != sK5_skl
| disjoint(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)) ),
inference(backward_demodulation,[status(thm)],[f1618,f254]) ).
fof(f1640,plain,
! [X0] :
( relation_image(X0,empty_set) = sK5_skl
| ~ relation(X0) ),
inference(backward_demodulation,[status(thm)],[f1618,f151]) ).
fof(f1643,plain,
! [X0,X1] :
( ~ disjoint(X0,X1)
| set_intersection2(X0,X1) = sK5_skl ),
inference(backward_demodulation,[status(thm)],[f1618,f68]) ).
fof(f1669,plain,
! [X0,X1] :
( X1 = X0
| sK5_skl = set_intersection2(singleton(X0),singleton(X1)) ),
inference(backward_demodulation,[status(thm)],[f1618,f710]) ).
fof(f1698,plain,
! [X0] : element(sK5_skl,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f1699,f120]) ).
fof(f1699,plain,
! [X0] : sK5_skl = sK10_skl(X0),
inference(forward_demodulation,[status(thm)],[f1618,f1615]) ).
fof(f1709,plain,
! [X0,X1] :
( sK7_skl != relation_image(sK14_skl,set_intersection2(X1,X0))
| disjoint(relation_image(sK14_skl,X0),relation_image(sK14_skl,X1)) ),
inference(backward_demodulation,[status(thm)],[f1772,f1627]) ).
fof(f1717,plain,
! [X0,X1] :
( X0 = X1
| sK7_skl = set_intersection2(singleton(X0),singleton(X1)) ),
inference(backward_demodulation,[status(thm)],[f1772,f1669]) ).
fof(f1718,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = sK7_skl
| ~ disjoint(X0,X1) ),
inference(backward_demodulation,[status(thm)],[f1772,f1643]) ).
fof(f1772,plain,
sK7_skl = sK5_skl,
inference(forward_demodulation,[status(thm)],[f1618,f1616]) ).
fof(f1775,plain,
! [X0] :
( relation_image(X0,sK5_skl) = sK5_skl
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f1618,f1640]) ).
fof(f1776,plain,
! [X0] :
( relation_image(X0,sK7_skl) = sK5_skl
| ~ relation(X0) ),
inference(forward_demodulation,[status(thm)],[f1772,f1775]) ).
fof(f1777,plain,
! [X0] :
( ~ relation(X0)
| sK7_skl = relation_image(X0,sK7_skl) ),
inference(forward_demodulation,[status(thm)],[f1772,f1776]) ).
fof(f1822,plain,
! [X0] : element(sK7_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f1772,f1698]) ).
fof(f2395,definition,
( sQ180_spl
<=> sK7_skl = relation_image(sK14_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition]) ).
fof(f2397,plain,
( sQ180_spl
| sK7_skl != relation_image(sK14_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f2395]) ).
fof(f2422,definition,
( sQ182_spl
<=> sK7_skl = sK7_skl ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2424,plain,
( sQ182_spl
| sK7_skl != sK7_skl ),
inference(component_clause,[status(thm)],[f2422]) ).
fof(f2435,plain,
sK7_skl = relation_image(sK14_skl,sK7_skl),
inference(resolution,[status(thm)],[f1777,f146]) ).
fof(f2475,plain,
( sQ182_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2424]) ).
fof(f2476,plain,
sQ182_spl,
inference(contradiction_clause,[status(thm)],[f2475]) ).
fof(f2502,definition,
( sQ185_spl
<=> sK7_skl = relation_image(sK14_skl,relation_image(sK14_skl,sK7_skl)) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2504,plain,
( sQ185_spl
| sK7_skl != relation_image(sK14_skl,relation_image(sK14_skl,sK7_skl)) ),
inference(component_clause,[status(thm)],[f2502]) ).
fof(f2509,plain,
( sQ185_spl
| sK7_skl != relation_image(sK14_skl,sK7_skl) ),
inference(forward_demodulation,[status(thm)],[f2435,f2504]) ).
fof(f2510,plain,
( sQ185_spl
| sK7_skl != sK7_skl ),
inference(forward_demodulation,[status(thm)],[f2435,f2509]) ).
fof(f2511,plain,
( sQ185_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2510]) ).
fof(f2512,plain,
sQ185_spl,
inference(contradiction_clause,[status(thm)],[f2511]) ).
fof(f2601,plain,
( sQ180_spl
| sK7_skl != sK7_skl ),
inference(forward_demodulation,[status(thm)],[f2435,f2397]) ).
fof(f2602,plain,
( sQ180_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2601]) ).
fof(f2603,plain,
sQ180_spl,
inference(contradiction_clause,[status(thm)],[f2602]) ).
fof(f2829,definition,
! [X1] :
( sQ196_spl
<=> ~ empty(X1) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2830,plain,
! [X0] :
( ~ sQ196_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f2829]) ).
fof(f2858,plain,
! [X0] :
( ~ sQ48_spl
| ~ element(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),powerset(X0))
| ~ empty(X0) ),
inference(paramodulation,[status(thm)],[f544,f1561]) ).
fof(f2917,plain,
! [X0,X1] :
( X1 = X0
| relation_image(sK14_skl,sK7_skl) = relation_image(sK14_skl,set_intersection2(singleton(X0),singleton(X1))) ),
inference(paramodulation,[status(thm)],[f1717,f210]) ).
fof(f2923,definition,
! [X0,X1] :
( sQ197_spl
<=> ( X0 = X1
| disjoint(relation_image(sK14_skl,singleton(X0)),relation_image(sK14_skl,singleton(X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2924,plain,
! [X0,X1] :
( ~ sQ197_spl
| disjoint(relation_image(sK14_skl,singleton(X0)),relation_image(sK14_skl,singleton(X1)))
| X0 = X1 ),
inference(component_clause,[status(thm)],[f2923]) ).
fof(f2927,plain,
! [X0,X1] :
( sK7_skl = relation_image(sK14_skl,set_intersection2(singleton(X1),singleton(X0)))
| X0 = X1 ),
inference(forward_demodulation,[status(thm)],[f2435,f2917]) ).
fof(f3232,plain,
! [X0,X1] :
( X0 = X1
| sK7_skl != sK7_skl
| disjoint(relation_image(sK14_skl,singleton(X0)),relation_image(sK14_skl,singleton(X1))) ),
inference(paramodulation,[status(thm)],[f2927,f1709]) ).
fof(f3246,plain,
( ~ sQ182_spl
| sQ197_spl ),
inference(split_clause,[status(thm)],[f3232,f2923,f2422]) ).
fof(f3389,plain,
! [X0] :
( ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ sQ197_spl
| X0 = sK1_skl(sK14_skl)
| disjoint(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(X0))) ),
inference(paramodulation,[status(thm)],[f549,f2924]) ).
fof(f3806,plain,
( ~ sQ196_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f111,f2830]) ).
fof(f3813,plain,
~ sQ196_spl,
inference(contradiction_clause,[status(thm)],[f3806]) ).
fof(f5495,plain,
( ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| sK7_skl = set_intersection2(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))) ),
inference(resolution,[status(thm)],[f1220,f1718]) ).
fof(f5497,plain,
( ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| sK7_skl = relation_image(sK14_skl,set_intersection2(singleton(sK2_skl(sK14_skl)),singleton(sK2_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f148,f5495]) ).
fof(f5510,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ empty(X0)
| ~ element(sK7_skl,powerset(X0)) ),
inference(backward_demodulation,[status(thm)],[f5528,f2858]) ).
fof(f5528,plain,
( ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| sK7_skl = relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))) ),
inference(forward_demodulation,[status(thm)],[f96,f5497]) ).
fof(f5544,plain,
( ~ sQ48_spl
| ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f111,f5554]) ).
fof(f5554,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5510,f1822]) ).
fof(f5579,plain,
( ~ sQ48_spl
| ~ sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f5544]) ).
fof(f5580,plain,
( sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ disjoint(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK1_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f549,f1214]) ).
fof(f5581,plain,
( sQ115_spl
| ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ disjoint(relation_image(sK14_skl,singleton(sK2_skl(sK14_skl))),relation_image(sK14_skl,singleton(sK2_skl(sK14_skl)))) ),
inference(forward_demodulation,[status(thm)],[f549,f5580]) ).
fof(f6405,definition,
( sQ381_spl
<=> sK7_skl = relation_image(sK14_skl,relation_image(sK14_skl,relation_image(sK14_skl,sK7_skl))) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f6407,plain,
( sQ381_spl
| sK7_skl != relation_image(sK14_skl,relation_image(sK14_skl,relation_image(sK14_skl,sK7_skl))) ),
inference(component_clause,[status(thm)],[f6405]) ).
fof(f6422,plain,
( sQ381_spl
| sK7_skl != relation_image(sK14_skl,relation_image(sK14_skl,sK7_skl)) ),
inference(forward_demodulation,[status(thm)],[f2435,f6407]) ).
fof(f6423,plain,
( sQ381_spl
| sK7_skl != relation_image(sK14_skl,sK7_skl) ),
inference(forward_demodulation,[status(thm)],[f2435,f6422]) ).
fof(f6424,plain,
( sQ381_spl
| sK7_skl != sK7_skl ),
inference(forward_demodulation,[status(thm)],[f2435,f6423]) ).
fof(f6425,plain,
( sQ381_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6424]) ).
fof(f6426,plain,
sQ381_spl,
inference(contradiction_clause,[status(thm)],[f6425]) ).
fof(f7041,definition,
( sQ462_spl
<=> empty(powerset(sK7_skl)) ),
introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition]) ).
fof(f7042,plain,
( ~ sQ462_spl
| empty(powerset(sK7_skl)) ),
inference(component_clause,[status(thm)],[f7041]) ).
fof(f7054,plain,
( ~ sQ462_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7042,f85]) ).
fof(f7055,plain,
~ sQ462_spl,
inference(contradiction_clause,[status(thm)],[f7054]) ).
fof(f12632,plain,
( ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ sQ197_spl
| sQ115_spl
| sK2_skl(sK14_skl) = sK1_skl(sK14_skl) ),
inference(resolution,[status(thm)],[f5581,f3389]) ).
fof(f12634,plain,
( ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ sQ197_spl
| sQ115_spl
| sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12632,f1413]) ).
fof(f12635,plain,
( ~ sQ46_spl
| ~ sQ4_spl
| ~ sQ48_spl
| ~ sQ197_spl
| sQ115_spl
| sQ143_spl ),
inference(contradiction_clause,[status(thm)],[f12634]) ).
fof(f12636,plain,
$false,
inference(sat_refutation,[status(thm)],[f198,f280,f286,f288,f334,f539,f546,f548,f1414,f2476,f2512,f2603,f3246,f3813,f5579,f6426,f7055,f12635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU053+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n005.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:48:04 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 145.61/18.96 % Refutation found
% 145.61/18.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 145.61/18.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 130.17/20.18 % Elapsed time: 19.596666 seconds
% 130.17/20.18 % CPU time: 142.998108 seconds
% 130.17/20.18 % Total memory used: 618.131 MB
% 130.17/20.18 % Net memory used: 579.618 MB
%------------------------------------------------------------------------------