%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET611+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:10:14 PM UTC 2026
% Result : Theorem 0.14s 6.07s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 62
% Syntax : Number of formulae : 306 ( 26 unt; 53 def)
% Number of atoms : 767 ( 142 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 774 ( 313 ~; 367 |; 28 &)
% ( 62 <=>; 2 =>; 0 <=; 2 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 58 ( 56 usr; 54 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 472 ( 462 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B,C] :
( ! [D] :
( member(D,B)
<=> member(D,C) )
=> B = C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [B,C,D] :
( member(D,intersection(B,C))
<=> ( member(D,C)
& member(D,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [B,C,D] :
( member(D,difference(B,C))
<=> ( ~ member(D,C)
& member(D,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [B] : ~ member(B,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [B,C] :
( B = C
<=> ( subset(C,B)
& subset(B,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [B,C] : intersection(B,C) = intersection(C,B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [B,C] :
( subset(B,C)
<=> ! [D] :
( member(D,B)
=> member(D,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [B] :
( empty(B)
<=> ! [C] : ~ member(C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,conjecture,
! [B,C] :
( intersection(B,C) = empty_set
<=> difference(B,C) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
~ ! [B,C] :
( intersection(B,C) = empty_set
<=> difference(B,C) = B ),
inference(negated_conjecture,[status(cth)],[f11]) ).
fof(f13,plain,
! [B,C] :
( B = C
| ? [D] :
( member(D,B)
<~> member(D,C) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
! [B,C] :
( B = C
| ? [D] :
( ( ~ member(D,C)
| ~ member(D,B) )
& ( member(D,C)
| member(D,B) ) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f15,plain,
! [B,C] :
( B = C
| ( ( ~ member(sK0_skl(C,B),C)
| ~ member(sK0_skl(C,B),B) )
& ( member(sK0_skl(C,B),C)
| member(sK0_skl(C,B),B) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B))],[f14]) ).
fof(f16,plain,
! [X0,X1] :
( X1 = X0
| member(sK0_skl(X0,X1),X0)
| member(sK0_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f17,plain,
! [X0,X1] :
( X1 = X0
| ~ member(sK0_skl(X0,X1),X0)
| ~ member(sK0_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f18,plain,
! [B,C,D] :
( ( ~ member(D,C)
| ~ member(D,B)
| member(D,intersection(B,C)) )
& ( ( member(D,C)
& member(D,B) )
| ~ member(D,intersection(B,C)) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f19,plain,
( ! [B,C,D] :
( ~ member(D,C)
| ~ member(D,B)
| member(D,intersection(B,C)) )
& ! [B,C,D] :
( ( member(D,C)
& member(D,B) )
| ~ member(D,intersection(B,C)) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f22,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f23,plain,
! [B,C,D] :
( ( member(D,C)
| ~ member(D,B)
| member(D,difference(B,C)) )
& ( ( ~ member(D,C)
& member(D,B) )
| ~ member(D,difference(B,C)) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f24,plain,
( ! [B,C,D] :
( member(D,C)
| ~ member(D,B)
| member(D,difference(B,C)) )
& ! [B,C,D] :
( ( ~ member(D,C)
& member(D,B) )
| ~ member(D,difference(B,C)) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f27,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,X1)
| member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f28,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f29,plain,
! [B,C] :
( ( ~ subset(C,B)
| ~ subset(B,C)
| B = C )
& ( ( subset(C,B)
& subset(B,C) )
| B != C ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f30,plain,
( ! [B,C] :
( ~ subset(C,B)
| ~ subset(B,C)
| B = C )
& ! [B,C] :
( ( subset(C,B)
& subset(B,C) )
| B != C ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f33,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f34,plain,
! [X0,X1] : intersection(X0,X1) = intersection(X1,X0),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f42,plain,
! [B,C] :
( subset(B,C)
<=> ! [D] :
( member(D,C)
| ~ member(D,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f43,plain,
! [B,C] :
( ( ? [D] :
( ~ member(D,C)
& member(D,B) )
| subset(B,C) )
& ( ! [D] :
( member(D,C)
| ~ member(D,B) )
| ~ subset(B,C) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
( ! [B,C] :
( ? [D] :
( ~ member(D,C)
& member(D,B) )
| subset(B,C) )
& ! [B,C] :
( ! [D] :
( member(D,C)
| ~ member(D,B) )
| ~ subset(B,C) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f45,plain,
( ! [B,C] :
( ( ~ member(sK2_skl(C,B),C)
& member(sK2_skl(C,B),B) )
| subset(B,C) )
& ! [B,C] :
( ! [D] :
( member(D,C)
| ~ member(D,B) )
| ~ subset(B,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(D,sK2_skl(C,B))],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0,X1] :
( member(sK2_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
! [X0,X1] :
( ~ member(sK2_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f50,plain,
! [B] :
( ( ? [C] : member(C,B)
| empty(B) )
& ( ! [C] : ~ member(C,B)
| ~ empty(B) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f51,plain,
( ! [B] :
( ? [C] : member(C,B)
| empty(B) )
& ! [B] :
( ! [C] : ~ member(C,B)
| ~ empty(B) ) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f52,plain,
( ! [B] :
( member(sK3_skl(B),B)
| empty(B) )
& ! [B] :
( ! [C] : ~ member(C,B)
| ~ empty(B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B))],[f51]) ).
fof(f53,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0] :
( member(sK3_skl(X0),X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f55,plain,
? [B,C] :
( intersection(B,C) = empty_set
<~> difference(B,C) = B ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f56,plain,
? [B,C] :
( ( difference(B,C) != B
| intersection(B,C) != empty_set )
& ( difference(B,C) = B
| intersection(B,C) = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
( ( difference(sK4_skl,sK5_skl) != sK4_skl
| intersection(sK4_skl,sK5_skl) != empty_set )
& ( difference(sK4_skl,sK5_skl) = sK4_skl
| intersection(sK4_skl,sK5_skl) = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(B,sK4_skl),skolemize(C,sK5_skl)],[f56]) ).
fof(f58,plain,
( difference(sK4_skl,sK5_skl) = sK4_skl
| intersection(sK4_skl,sK5_skl) = empty_set ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
( difference(sK4_skl,sK5_skl) != sK4_skl
| intersection(sK4_skl,sK5_skl) != empty_set ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,definition,
( sQ0_spl
<=> intersection(sK4_skl,sK5_skl) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f61,plain,
( ~ sQ0_spl
| intersection(sK4_skl,sK5_skl) = empty_set ),
inference(component_clause,[status(thm)],[f60]) ).
fof(f63,definition,
( sQ1_spl
<=> difference(sK4_skl,sK5_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f64,plain,
( ~ sQ1_spl
| difference(sK4_skl,sK5_skl) = sK4_skl ),
inference(component_clause,[status(thm)],[f63]) ).
fof(f66,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f58,f60,f63]) ).
fof(f67,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f59,f60,f63]) ).
fof(f68,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f31]) ).
fof(f81,plain,
! [X0] :
( ~ sQ1_spl
| ~ member(X0,sK5_skl)
| ~ member(X0,sK4_skl) ),
inference(paramodulation,[status(thm)],[f64,f26]) ).
fof(f91,plain,
! [X0,X1,X2] :
( member(sK0_skl(X0,difference(X1,X2)),X1)
| difference(X1,X2) = X0
| member(sK0_skl(X0,difference(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f16,f25]) ).
fof(f92,plain,
! [X0,X1,X2] :
( member(sK0_skl(X0,intersection(X1,X2)),X2)
| intersection(X1,X2) = X0
| member(sK0_skl(X0,intersection(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f16,f21]) ).
fof(f93,plain,
! [X0,X1,X2] :
( member(sK0_skl(X0,intersection(X1,X2)),X1)
| intersection(X1,X2) = X0
| member(sK0_skl(X0,intersection(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f16,f20]) ).
fof(f94,plain,
! [X0] :
( empty_set = X0
| member(sK0_skl(X0,empty_set),X0) ),
inference(resolution,[status(thm)],[f16,f28]) ).
fof(f100,plain,
! [X0,X1] :
( X0 = X1
| member(sK0_skl(X1,X0),X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f53,f16]) ).
fof(f101,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ empty(difference(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f27]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X2,X0)
| ~ empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f53,f22]) ).
fof(f104,plain,
! [X0,X1] :
( ~ member(sK3_skl(difference(X0,X1)),X1)
| empty(difference(X0,X1)) ),
inference(resolution,[status(thm)],[f54,f26]) ).
fof(f105,plain,
! [X0,X1] :
( member(sK3_skl(difference(X0,X1)),X0)
| empty(difference(X0,X1)) ),
inference(resolution,[status(thm)],[f54,f25]) ).
fof(f106,plain,
! [X0,X1] :
( member(sK3_skl(intersection(X0,X1)),X1)
| empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f54,f21]) ).
fof(f107,plain,
! [X0,X1] :
( member(sK3_skl(intersection(X0,X1)),X0)
| empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f54,f20]) ).
fof(f108,plain,
empty(empty_set),
inference(resolution,[status(thm)],[f54,f28]) ).
fof(f120,plain,
! [X0,X1,X2] :
( member(sK2_skl(X2,difference(X0,X1)),X0)
| subset(difference(X0,X1),X2) ),
inference(resolution,[status(thm)],[f47,f25]) ).
fof(f121,plain,
! [X0,X1,X2] :
( member(sK2_skl(X2,intersection(X0,X1)),X1)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f47,f21]) ).
fof(f122,plain,
! [X0,X1,X2] :
( member(sK2_skl(X2,intersection(X0,X1)),X0)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f47,f20]) ).
fof(f123,plain,
! [X0] : subset(empty_set,X0),
inference(resolution,[status(thm)],[f47,f28]) ).
fof(f124,plain,
! [X0,X1] :
( ~ empty(X0)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f47,f53]) ).
fof(f125,plain,
! [X0] :
( ~ subset(X0,empty_set)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f123,f33]) ).
fof(f126,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| X1 = X0
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f124,f33]) ).
fof(f128,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f125,f124]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ~ member(sK0_skl(X0,intersection(X1,X2)),X2)
| ~ member(sK0_skl(X0,intersection(X1,X2)),X1)
| intersection(X1,X2) = X0
| ~ member(sK0_skl(X0,intersection(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f17,f22]) ).
fof(f195,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| difference(X1,X2) = X0
| member(sK0_skl(X0,difference(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f91,f53]) ).
fof(f205,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| intersection(X1,X2) = X0
| member(sK0_skl(X0,intersection(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f92,f53]) ).
fof(f209,plain,
! [X0,X1] :
( ~ empty(X1)
| X1 = X0
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f126,f124]) ).
fof(f220,plain,
! [X0,X1,X2] :
( member(sK2_skl(difference(X1,X2),X0),X2)
| ~ member(sK2_skl(difference(X1,X2),X0),X1)
| subset(X0,difference(X1,X2)) ),
inference(resolution,[status(thm)],[f48,f27]) ).
fof(f226,plain,
! [X0,X1] :
( ~ member(sK0_skl(difference(X0,X1),empty_set),X1)
| empty_set = difference(X0,X1) ),
inference(resolution,[status(thm)],[f94,f26]) ).
fof(f231,definition,
( sQ6_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f268,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| member(sK2_skl(X2,X0),X1)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f46,f47]) ).
fof(f269,plain,
! [X0,X1] :
( empty(X0)
| member(sK3_skl(X0),X1)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f46,f54]) ).
fof(f281,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| intersection(X1,X2) = X0
| member(sK0_skl(X0,intersection(X1,X2)),X0) ),
inference(resolution,[status(thm)],[f93,f53]) ).
fof(f291,plain,
! [X0,X1,X2] :
( member(sK0_skl(X1,X0),X2)
| ~ subset(X1,X2)
| X0 = X1
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f100,f46]) ).
fof(f399,plain,
! [X0] :
( empty(difference(X0,X0))
| empty(difference(X0,X0)) ),
inference(resolution,[status(thm)],[f105,f104]) ).
fof(f406,plain,
! [X0,X1] :
( ~ empty(X0)
| empty(difference(X0,X1)) ),
inference(resolution,[status(thm)],[f105,f53]) ).
fof(f408,plain,
! [X0] : empty(difference(X0,X0)),
inference(duplicate_literals_removal,[status(thm)],[f399]) ).
fof(f428,definition,
! [X0,X1] :
( sQ14_spl
<=> ( member(X0,X1)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f441,plain,
! [X0] : empty(difference(empty_set,X0)),
inference(resolution,[status(thm)],[f28,f105]) ).
fof(f450,plain,
! [X0] : difference(X0,X0) = empty_set,
inference(resolution,[status(thm)],[f128,f408]) ).
fof(f455,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,X1)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f450,f101]) ).
fof(f463,definition,
( sQ15_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( sQ15_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f466,plain,
( sQ14_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f455,f463,f428]) ).
fof(f508,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(X0,sK5_skl)
| ~ member(X0,sK4_skl)
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f61,f22]) ).
fof(f521,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(X0,sK5_skl)
| ~ member(X0,sK4_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f508,f28]) ).
fof(f535,plain,
! [X0] :
( ~ sQ0_spl
| subset(sK4_skl,X0)
| ~ member(sK2_skl(X0,sK4_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f521,f47]) ).
fof(f545,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f465,f108]) ).
fof(f546,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f584,plain,
! [X0] : difference(empty_set,X0) = empty_set,
inference(resolution,[status(thm)],[f441,f128]) ).
fof(f590,plain,
! [X0] :
( member(sK3_skl(empty_set),empty_set)
| empty(difference(empty_set,X0)) ),
inference(paramodulation,[status(thm)],[f584,f105]) ).
fof(f592,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,empty_set)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f101]) ).
fof(f598,definition,
! [X0] :
( sQ17_spl
<=> empty(difference(empty_set,X0)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f601,definition,
( sQ18_spl
<=> member(sK3_skl(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f602,plain,
( ~ sQ18_spl
| member(sK3_skl(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,plain,
( sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f590,f598,f601]) ).
fof(f606,definition,
! [X0,X1] :
( sQ19_spl
<=> ( member(X0,X1)
| ~ member(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( sQ19_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f592,f463,f606]) ).
fof(f623,plain,
! [X0] : empty(intersection(X0,empty_set)),
inference(resolution,[status(thm)],[f106,f28]) ).
fof(f629,plain,
! [X0,X1] :
( ~ empty(X1)
| empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f106,f53]) ).
fof(f632,plain,
! [X0] : empty(intersection(empty_set,X0)),
inference(resolution,[status(thm)],[f107,f28]) ).
fof(f663,plain,
! [X0] : intersection(X0,empty_set) = empty_set,
inference(resolution,[status(thm)],[f623,f128]) ).
fof(f668,plain,
! [X0] : intersection(empty_set,X0) = empty_set,
inference(resolution,[status(thm)],[f632,f128]) ).
fof(f677,plain,
! [X0] :
( member(sK3_skl(empty_set),empty_set)
| empty(intersection(X0,empty_set)) ),
inference(paramodulation,[status(thm)],[f663,f106]) ).
fof(f678,plain,
! [X0,X1] :
( ~ member(X0,empty_set)
| ~ member(X0,X1)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f663,f102]) ).
fof(f687,definition,
! [X0] :
( sQ20_spl
<=> empty(intersection(X0,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( sQ18_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f677,f687,f601]) ).
fof(f691,definition,
! [X0,X1] :
( sQ21_spl
<=> ( ~ member(X0,empty_set)
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f694,plain,
( sQ21_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f678,f463,f691]) ).
fof(f699,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f602,f28]) ).
fof(f700,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f699]) ).
fof(f707,plain,
! [X0] :
( member(sK3_skl(empty_set),empty_set)
| empty(intersection(empty_set,X0)) ),
inference(paramodulation,[status(thm)],[f668,f107]) ).
fof(f717,definition,
! [X0] :
( sQ22_spl
<=> empty(intersection(empty_set,X0)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( sQ18_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f707,f717,f601]) ).
fof(f729,plain,
! [X0,X1] :
( subset(difference(X0,X1),X0)
| subset(difference(X0,X1),X0) ),
inference(resolution,[status(thm)],[f120,f48]) ).
fof(f737,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| subset(difference(X0,X1),X2) ),
inference(resolution,[status(thm)],[f120,f53]) ).
fof(f744,plain,
! [X0,X1] : subset(difference(X0,X1),X0),
inference(duplicate_literals_removal,[status(thm)],[f729]) ).
fof(f749,plain,
! [X0,X1] :
( subset(intersection(X0,X1),X1)
| subset(intersection(X0,X1),X1) ),
inference(resolution,[status(thm)],[f121,f48]) ).
fof(f757,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f121,f53]) ).
fof(f762,plain,
! [X0,X1] : subset(intersection(X0,X1),X1),
inference(duplicate_literals_removal,[status(thm)],[f749]) ).
fof(f767,plain,
! [X0,X1] :
( difference(X0,X1) = X0
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f744,f126]) ).
fof(f768,plain,
! [X0,X1] :
( ~ subset(X0,difference(X0,X1))
| X0 = difference(X0,X1) ),
inference(resolution,[status(thm)],[f744,f33]) ).
fof(f774,plain,
! [X0,X1] :
( ~ subset(X0,intersection(X1,X0))
| X0 = intersection(X1,X0) ),
inference(resolution,[status(thm)],[f762,f33]) ).
fof(f777,plain,
! [X0,X1] : subset(intersection(X0,X1),X0),
inference(paramodulation,[status(thm)],[f34,f762]) ).
fof(f781,plain,
! [X0,X1] :
( ~ subset(X0,intersection(X0,X1))
| X0 = intersection(X0,X1) ),
inference(resolution,[status(thm)],[f777,f33]) ).
fof(f786,plain,
( empty_set = empty_set
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f767]) ).
fof(f789,plain,
( sQ6_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f786,f463,f231]) ).
fof(f803,plain,
! [X0,X1,X2] :
( difference(X0,X2) = X1
| ~ empty(X1)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f406,f209]) ).
fof(f809,definition,
! [X0] :
( sQ23_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f810,plain,
! [X0] :
( ~ sQ23_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f809]) ).
fof(f842,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f122,f53]) ).
fof(f871,plain,
! [X0] :
( intersection(X0,X0) = X0
| ~ empty(intersection(X0,X0))
| intersection(X0,X0) = X0
| ~ member(sK0_skl(X0,intersection(X0,X0)),X0) ),
inference(resolution,[status(thm)],[f146,f100]) ).
fof(f891,plain,
! [X0] :
( ~ empty(intersection(X0,X0))
| intersection(X0,X0) = X0
| ~ member(sK0_skl(X0,intersection(X0,X0)),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f871]) ).
fof(f892,plain,
! [X0] :
( ~ empty(intersection(X0,X0))
| intersection(X0,X0) = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f891,f100]) ).
fof(f916,definition,
( sQ24_spl
<=> subset(sK4_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f918,plain,
( sQ24_spl
| ~ subset(sK4_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f916]) ).
fof(f941,plain,
( ~ sQ23_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f108,f810]) ).
fof(f942,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f941]) ).
fof(f1407,plain,
! [X0,X1,X2] :
( ~ subset(X1,difference(X0,X2))
| X1 = difference(X0,X2)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f737,f33]) ).
fof(f1408,plain,
! [X0] :
( ~ empty(empty_set)
| subset(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f584,f737]) ).
fof(f1411,definition,
! [X0] :
( sQ28_spl
<=> subset(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1414,plain,
( ~ sQ15_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1408,f1411,f463]) ).
fof(f1422,plain,
! [X0,X1,X2] :
( ~ subset(X1,intersection(X2,X0))
| X1 = intersection(X2,X0)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f757,f33]) ).
fof(f1431,plain,
! [X0,X1,X2] :
( ~ subset(X1,intersection(X0,X2))
| X1 = intersection(X0,X2)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f842,f33]) ).
fof(f1467,plain,
! [X0,X1] :
( subset(X0,difference(X0,X1))
| member(sK2_skl(difference(X0,X1),X0),X1)
| subset(X0,difference(X0,X1)) ),
inference(resolution,[status(thm)],[f220,f47]) ).
fof(f1476,plain,
! [X0,X1] :
( member(sK2_skl(difference(X0,X1),X0),X1)
| subset(X0,difference(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f1467]) ).
fof(f1555,plain,
! [X0] :
( empty_set = X0
| ~ empty(X0)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f803]) ).
fof(f1558,definition,
! [X0] :
( sQ32_spl
<=> ( empty_set = X0
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1561,plain,
( sQ32_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1555,f463,f1558]) ).
fof(f1742,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| subset(X0,X2)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f268,f53]) ).
fof(f1753,plain,
! [X0,X1] :
( ~ empty(X1)
| empty(X0)
| ~ subset(X0,X1) ),
inference(resolution,[status(thm)],[f269,f53]) ).
fof(f1763,plain,
! [X0] :
( ~ sQ1_spl
| empty(X0)
| ~ subset(X0,sK4_skl)
| ~ member(sK3_skl(X0),sK5_skl) ),
inference(resolution,[status(thm)],[f81,f269]) ).
fof(f1821,plain,
( ~ empty(empty_set)
| intersection(empty_set,empty_set) = empty_set ),
inference(paramodulation,[status(thm)],[f668,f892]) ).
fof(f1823,definition,
( sQ37_spl
<=> intersection(empty_set,empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1826,plain,
( ~ sQ15_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f1821,f1823,f463]) ).
fof(f1844,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| ~ empty(X2)
| empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f1753,f842]) ).
fof(f1845,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| ~ empty(X2)
| empty(intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f1753,f757]) ).
fof(f1848,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| ~ empty(X2)
| empty(difference(X0,X1)) ),
inference(resolution,[status(thm)],[f1753,f737]) ).
fof(f1850,plain,
! [X0,X1] :
( ~ empty(X0)
| ~ empty(X1)
| empty(X0) ),
inference(resolution,[status(thm)],[f1753,f124]) ).
fof(f1853,definition,
! [X0,X1] :
( sQ38_spl
<=> ( ~ empty(X0)
| empty(intersection(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1856,plain,
( sQ23_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1844,f1853,f809]) ).
fof(f1857,definition,
! [X0,X1] :
( sQ39_spl
<=> ( ~ empty(X1)
| empty(intersection(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1860,plain,
( sQ23_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1845,f1857,f809]) ).
fof(f1861,definition,
! [X0,X1] :
( sQ40_spl
<=> ( ~ empty(X0)
| empty(difference(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1864,plain,
( sQ23_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1848,f1861,f809]) ).
fof(f1865,definition,
! [X0] :
( sQ41_spl
<=> ( ~ empty(X0)
| empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1868,plain,
( sQ23_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1850,f1865,f809]) ).
fof(f1870,plain,
! [X0,X1,X2,X3] :
( ~ empty(X0)
| ~ empty(X3)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f1742,f842]) ).
fof(f1871,plain,
! [X0,X1,X2,X3] :
( ~ empty(X1)
| ~ empty(X3)
| subset(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f1742,f757]) ).
fof(f1874,plain,
! [X0,X1,X2,X3] :
( ~ empty(X0)
| ~ empty(X3)
| subset(difference(X0,X1),X2) ),
inference(resolution,[status(thm)],[f1742,f737]) ).
fof(f1876,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| ~ empty(X2)
| subset(X0,X1) ),
inference(resolution,[status(thm)],[f1742,f124]) ).
fof(f1879,definition,
! [X0,X1,X2] :
( sQ42_spl
<=> ( ~ empty(X0)
| subset(intersection(X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1882,plain,
( sQ23_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1870,f1879,f809]) ).
fof(f1883,definition,
! [X0,X1,X2] :
( sQ43_spl
<=> ( ~ empty(X1)
| subset(intersection(X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1886,plain,
( sQ23_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1871,f1883,f809]) ).
fof(f1887,definition,
! [X0,X1,X2] :
( sQ44_spl
<=> ( ~ empty(X0)
| subset(difference(X0,X1),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1890,plain,
( sQ23_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1874,f1887,f809]) ).
fof(f1891,definition,
! [X0,X1] :
( sQ45_spl
<=> ( ~ empty(X0)
| subset(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1894,plain,
( sQ23_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f1876,f1891,f809]) ).
fof(f1896,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| intersection(X0,X1) = difference(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f768,f842]) ).
fof(f1897,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| intersection(X0,X1) = difference(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f768,f757]) ).
fof(f1898,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| difference(X0,X1) = difference(difference(X0,X1),X2) ),
inference(resolution,[status(thm)],[f768,f737]) ).
fof(f1901,plain,
! [X0] :
( ~ subset(empty_set,empty_set)
| empty_set = difference(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f584,f768]) ).
fof(f1904,definition,
! [X0] :
( sQ46_spl
<=> empty_set = difference(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1907,definition,
( sQ47_spl
<=> subset(empty_set,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1909,plain,
( sQ47_spl
| ~ subset(empty_set,empty_set) ),
inference(component_clause,[status(thm)],[f1907]) ).
fof(f1910,plain,
( ~ sQ47_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1901,f1904,f1907]) ).
fof(f1913,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| intersection(X0,X1) = intersection(X2,intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f774,f842]) ).
fof(f1914,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| intersection(X0,X1) = intersection(X2,intersection(X0,X1)) ),
inference(resolution,[status(thm)],[f774,f757]) ).
fof(f1918,plain,
! [X0] :
( ~ subset(empty_set,empty_set)
| empty_set = intersection(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f663,f774]) ).
fof(f1922,definition,
! [X0] :
( sQ48_spl
<=> empty_set = intersection(X0,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1925,plain,
( ~ sQ47_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1918,f1922,f1907]) ).
fof(f1926,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1909,f123]) ).
fof(f1927,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1926]) ).
fof(f2153,plain,
! [X0,X1,X2] :
( ~ empty(X0)
| intersection(X0,X1) = intersection(intersection(X0,X1),X2) ),
inference(resolution,[status(thm)],[f781,f842]) ).
fof(f2157,plain,
! [X0] :
( ~ subset(empty_set,empty_set)
| empty_set = intersection(empty_set,X0) ),
inference(paramodulation,[status(thm)],[f668,f781]) ).
fof(f2161,definition,
! [X0] :
( sQ52_spl
<=> empty_set = intersection(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2164,plain,
( ~ sQ47_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f2157,f2161,f1907]) ).
fof(f2264,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(empty_set,X0) = difference(empty_set,X1) ),
inference(paramodulation,[status(thm)],[f668,f1896]) ).
fof(f2268,definition,
! [X0,X1] :
( sQ54_spl
<=> intersection(empty_set,X0) = difference(empty_set,X1) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2271,plain,
( ~ sQ15_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f2264,f2268,f463]) ).
fof(f2276,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(X0,empty_set) = difference(empty_set,X1) ),
inference(paramodulation,[status(thm)],[f663,f1897]) ).
fof(f2280,definition,
! [X0,X1] :
( sQ55_spl
<=> intersection(X0,empty_set) = difference(empty_set,X1) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2283,plain,
( ~ sQ15_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f2276,f2280,f463]) ).
fof(f2287,plain,
! [X0,X1] :
( ~ empty(empty_set)
| difference(empty_set,X0) = difference(empty_set,X1) ),
inference(paramodulation,[status(thm)],[f584,f1898]) ).
fof(f2293,definition,
! [X0,X1] :
( sQ57_spl
<=> difference(empty_set,X0) = difference(empty_set,X1) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2296,plain,
( ~ sQ15_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f2287,f2293,f463]) ).
fof(f2302,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(empty_set,X0) = intersection(X1,empty_set) ),
inference(paramodulation,[status(thm)],[f668,f1913]) ).
fof(f2306,definition,
! [X0,X1] :
( sQ58_spl
<=> intersection(empty_set,X0) = intersection(X1,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2309,plain,
( ~ sQ15_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f2302,f2306,f463]) ).
fof(f2316,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(X0,empty_set) = intersection(X1,empty_set) ),
inference(paramodulation,[status(thm)],[f663,f1914]) ).
fof(f2320,definition,
! [X0,X1] :
( sQ59_spl
<=> intersection(X0,empty_set) = intersection(X1,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f2323,plain,
( ~ sQ15_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f2316,f2320,f463]) ).
fof(f2355,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(empty_set,X0) = intersection(empty_set,X1) ),
inference(paramodulation,[status(thm)],[f668,f2153]) ).
fof(f2359,definition,
! [X0,X1] :
( sQ62_spl
<=> intersection(empty_set,X0) = intersection(empty_set,X1) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f2362,plain,
( ~ sQ15_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f2355,f2359,f463]) ).
fof(f2431,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f918,f68]) ).
fof(f2432,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f2431]) ).
fof(f2736,plain,
! [X0,X1,X2,X3] :
( ~ empty(X1)
| intersection(X1,X2) = difference(X0,X3)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1407,f842]) ).
fof(f2737,plain,
! [X0,X1,X2,X3] :
( ~ empty(X2)
| intersection(X1,X2) = difference(X0,X3)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f1407,f757]) ).
fof(f2745,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| X0 = difference(empty_set,X1)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f1407]) ).
fof(f2751,definition,
! [X0,X1] :
( sQ72_spl
<=> ( ~ subset(X0,empty_set)
| X0 = difference(empty_set,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f2754,plain,
( sQ72_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2745,f463,f2751]) ).
fof(f2757,plain,
! [X0,X1] :
( ~ empty(empty_set)
| empty_set = difference(X0,X1)
| ~ empty(X0) ),
inference(paramodulation,[status(thm)],[f668,f2736]) ).
fof(f2761,plain,
! [X0,X1] :
( ~ empty(X0)
| intersection(X0,X1) = empty_set
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f2736]) ).
fof(f2763,definition,
! [X0,X1] :
( sQ73_spl
<=> ( empty_set = difference(X0,X1)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2766,plain,
( ~ sQ15_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f2757,f2763,f463]) ).
fof(f2768,definition,
! [X0,X1] :
( sQ74_spl
<=> ( ~ empty(X0)
| intersection(X0,X1) = empty_set ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f2771,plain,
( sQ74_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2761,f463,f2768]) ).
fof(f2777,plain,
! [X0,X1] :
( ~ empty(X1)
| intersection(X0,X1) = empty_set
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f584,f2737]) ).
fof(f2781,definition,
! [X0,X1] :
( sQ75_spl
<=> ( ~ empty(X1)
| intersection(X0,X1) = empty_set ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f2784,plain,
( sQ75_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2777,f463,f2781]) ).
fof(f2885,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| X0 = intersection(X1,empty_set)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f663,f1422]) ).
fof(f2889,definition,
! [X0,X1] :
( sQ77_spl
<=> ( ~ subset(X0,empty_set)
| X0 = intersection(X1,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2892,plain,
( sQ77_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2885,f463,f2889]) ).
fof(f2939,plain,
! [X0,X1] :
( ~ subset(X0,empty_set)
| X0 = intersection(empty_set,X1)
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f668,f1431]) ).
fof(f2943,definition,
! [X0,X1] :
( sQ78_spl
<=> ( ~ subset(X0,empty_set)
| X0 = intersection(empty_set,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2946,plain,
( sQ78_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f2939,f463,f2943]) ).
fof(f3015,plain,
! [X0,X1] :
( ~ empty(empty_set)
| difference(empty_set,X1) = X0
| member(sK0_skl(X0,empty_set),X0) ),
inference(paramodulation,[status(thm)],[f584,f195]) ).
fof(f3030,definition,
! [X0,X1] :
( sQ81_spl
<=> ( difference(empty_set,X1) = X0
| member(sK0_skl(X0,empty_set),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f3033,plain,
( ~ sQ15_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f3015,f3030,f463]) ).
fof(f3070,plain,
! [X0] :
( ~ sQ1_spl
| empty(intersection(X0,sK5_skl))
| empty(intersection(X0,sK5_skl))
| ~ subset(intersection(X0,sK5_skl),sK4_skl) ),
inference(resolution,[status(thm)],[f1763,f106]) ).
fof(f3076,plain,
! [X0] :
( ~ sQ1_spl
| empty(intersection(X0,sK5_skl))
| ~ subset(intersection(X0,sK5_skl),sK4_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f3070]) ).
fof(f3089,definition,
( sQ82_spl
<=> subset(empty_set,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3091,plain,
( sQ82_spl
| ~ subset(empty_set,sK5_skl) ),
inference(component_clause,[status(thm)],[f3089]) ).
fof(f3287,plain,
! [X0,X1] :
( intersection(X0,X0) = X1
| ~ member(sK0_skl(X1,intersection(X0,X0)),X1)
| ~ subset(X1,X0)
| intersection(X0,X0) = X1
| ~ empty(intersection(X0,X0)) ),
inference(resolution,[status(thm)],[f291,f146]) ).
fof(f3304,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ subset(X1,X2)
| X0 = X1
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f291,f53]) ).
fof(f3318,plain,
! [X0,X1] :
( ~ member(sK0_skl(X1,intersection(X0,X0)),X1)
| ~ subset(X1,X0)
| intersection(X0,X0) = X1
| ~ empty(intersection(X0,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3287]) ).
fof(f3319,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| intersection(X0,X0) = X1
| ~ empty(intersection(X0,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3318,f100]) ).
fof(f3384,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(X1,empty_set) = X0
| member(sK0_skl(X0,empty_set),X0) ),
inference(paramodulation,[status(thm)],[f663,f205]) ).
fof(f3397,definition,
! [X0,X1] :
( sQ88_spl
<=> ( intersection(X1,empty_set) = X0
| member(sK0_skl(X0,empty_set),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f3400,plain,
( ~ sQ15_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f3384,f3397,f463]) ).
fof(f3475,plain,
! [X0,X1] :
( ~ empty(X0)
| ~ subset(X1,X0)
| intersection(X0,X0) = X1 ),
inference(resolution,[status(thm)],[f3319,f629]) ).
fof(f3477,plain,
! [X0] :
( ~ subset(X0,empty_set)
| intersection(empty_set,empty_set) = X0
| ~ empty(empty_set) ),
inference(paramodulation,[status(thm)],[f668,f3319]) ).
fof(f3479,definition,
! [X0] :
( sQ94_spl
<=> ( ~ subset(X0,empty_set)
| intersection(empty_set,empty_set) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f3482,plain,
( sQ94_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f3477,f463,f3479]) ).
fof(f3485,plain,
! [X0] :
( ~ empty(empty_set)
| ~ subset(X0,empty_set)
| empty_set = X0 ),
inference(paramodulation,[status(thm)],[f668,f3475]) ).
fof(f3487,definition,
! [X0] :
( sQ95_spl
<=> ( ~ subset(X0,empty_set)
| empty_set = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f3490,plain,
( ~ sQ15_spl
| sQ95_spl ),
inference(split_clause,[status(thm)],[f3485,f3487,f463]) ).
fof(f3553,plain,
! [X0,X1] :
( ~ subset(difference(X0,X1),X1)
| empty_set = difference(X0,X1)
| ~ empty(empty_set)
| empty_set = difference(X0,X1) ),
inference(resolution,[status(thm)],[f226,f291]) ).
fof(f3561,definition,
! [X0,X1] :
( sQ98_spl
<=> ( ~ subset(difference(X0,X1),X1)
| empty_set = difference(X0,X1)
| empty_set = difference(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f3564,plain,
( ~ sQ15_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f3553,f3561,f463]) ).
fof(f3569,plain,
! [X0,X1,X2,X3] :
( ~ empty(X1)
| ~ empty(X3)
| X0 = intersection(X1,X2)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f3304,f842]) ).
fof(f3570,plain,
! [X0,X1,X2,X3] :
( ~ empty(X2)
| ~ empty(X3)
| X0 = intersection(X1,X2)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f3304,f757]) ).
fof(f3573,plain,
! [X0,X1,X2,X3] :
( ~ empty(X1)
| ~ empty(X3)
| X0 = difference(X1,X2)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f3304,f737]) ).
fof(f3575,plain,
! [X0,X1,X2] :
( ~ empty(X1)
| ~ empty(X2)
| X0 = X1
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f3304,f124]) ).
fof(f3578,definition,
! [X0,X1,X2] :
( sQ99_spl
<=> ( ~ empty(X1)
| X0 = intersection(X1,X2)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f3581,plain,
( sQ23_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f3569,f3578,f809]) ).
fof(f3582,definition,
! [X0,X1,X2] :
( sQ100_spl
<=> ( ~ empty(X2)
| X0 = intersection(X1,X2)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f3585,plain,
( sQ23_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f3570,f3582,f809]) ).
fof(f3586,definition,
! [X0,X1,X2] :
( sQ101_spl
<=> ( ~ empty(X1)
| X0 = difference(X1,X2)
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f3589,plain,
( sQ23_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f3573,f3586,f809]) ).
fof(f3590,definition,
! [X0,X1] :
( sQ102_spl
<=> ( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f3593,plain,
( sQ23_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f3575,f3590,f809]) ).
fof(f3726,definition,
( sQ107_spl
<=> subset(empty_set,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f3728,plain,
( sQ107_spl
| ~ subset(empty_set,sK4_skl) ),
inference(component_clause,[status(thm)],[f3726]) ).
fof(f3733,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3728,f123]) ).
fof(f3734,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f3733]) ).
fof(f3738,plain,
( ~ sQ1_spl
| empty(intersection(sK4_skl,sK5_skl)) ),
inference(resolution,[status(thm)],[f3076,f777]) ).
fof(f3754,plain,
( ~ sQ1_spl
| intersection(sK4_skl,sK5_skl) = empty_set ),
inference(resolution,[status(thm)],[f3738,f128]) ).
fof(f3757,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f3754,f60,f63]) ).
fof(f4537,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3091,f123]) ).
fof(f4538,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f4537]) ).
fof(f5065,plain,
( ~ sQ0_spl
| subset(sK4_skl,difference(sK4_skl,sK5_skl))
| subset(sK4_skl,difference(sK4_skl,sK5_skl)) ),
inference(resolution,[status(thm)],[f1476,f535]) ).
fof(f5081,definition,
( sQ153_spl
<=> subset(sK4_skl,difference(sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f5082,plain,
( ~ sQ153_spl
| subset(sK4_skl,difference(sK4_skl,sK5_skl)) ),
inference(component_clause,[status(thm)],[f5081]) ).
fof(f5084,plain,
( ~ sQ0_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f5065,f5081,f60]) ).
fof(f5121,plain,
! [X0,X1] :
( ~ empty(empty_set)
| intersection(empty_set,X1) = X0
| member(sK0_skl(X0,empty_set),X0) ),
inference(paramodulation,[status(thm)],[f668,f281]) ).
fof(f5133,definition,
! [X0,X1] :
( sQ154_spl
<=> ( intersection(empty_set,X1) = X0
| member(sK0_skl(X0,empty_set),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f5136,plain,
( ~ sQ15_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f5121,f5133,f463]) ).
fof(f5174,plain,
( ~ sQ153_spl
| sK4_skl = difference(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f5082,f768]) ).
fof(f5184,plain,
( ~ sQ153_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f5174,f63,f5081]) ).
fof(f5194,plain,
$false,
inference(sat_refutation,[status(thm)],[f66,f67,f466,f546,f604,f609,f690,f694,f700,f720,f789,f942,f1414,f1561,f1826,f1856,f1860,f1864,f1868,f1882,f1886,f1890,f1894,f1910,f1925,f1927,f2164,f2271,f2283,f2296,f2309,f2323,f2362,f2432,f2754,f2766,f2771,f2784,f2892,f2946,f3033,f3400,f3482,f3490,f3564,f3581,f3585,f3589,f3593,f3734,f3757,f4538,f5084,f5136,f5184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET611+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.55 % Computer : n011.cluster.edu
% 0.10/5.55 % Model : x86_64 x86_64
% 0.10/5.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.55 % Memory : 8046.5625MB
% 0.10/5.55 % OS : Linux 6.8.0-71-generic
% 0.10/5.55 % CPULimit : 300
% 0.10/5.55 % WCLimit : 300
% 0.10/5.55 % DateTime : Mon Sep 21 05:29:01 UTC 2026
% 0.10/5.55 % CPUTime :
% 0.10/5.57 % Drodi V4.1.1
% 0.14/6.07 % Refutation found
% 0.14/6.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/6.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.86/6.10 % Elapsed time: 0.532670 seconds
% 1.86/6.10 % CPU time: 3.985191 seconds
% 1.86/6.10 % Total memory used: 155.158 MB
% 1.86/6.10 % Net memory used: 146.967 MB
%------------------------------------------------------------------------------