%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEV521+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:32:58 PM UTC 2026
% Result : Theorem 29.31s 4.13s
% Output : CNFRefutation 29.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 64
% Syntax : Number of formulae : 316 ( 26 unt; 51 def)
% Number of atoms : 954 ( 111 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1032 ( 394 ~; 459 |; 105 &)
% ( 67 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 58 ( 56 usr; 51 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 2 con; 0-3 aty)
% Number of variables : 444 ( 412 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( equal_set(A,B)
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,A] :
( member(X,power_set(A))
<=> subset(X,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,B)
& member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,B)
| member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,A] :
( member(X,sum(A))
<=> ? [Y] :
( member(X,Y)
& member(Y,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( disjoint(A,B)
<=> ~ ? [X] :
( member(X,B)
& member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( ( member(Y,A)
& member(X,A) )
=> ( ? [Z] :
( member(Z,Y)
& member(Z,X) )
=> X = Y ) )
& ! [X] :
( member(X,E)
=> ? [Y] :
( member(X,Y)
& member(Y,A) ) )
& ! [X] :
( member(X,A)
=> subset(X,E) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B] :
( B = unaryUnion(A)
<=> ! [C] :
( member(C,B)
<=> ? [D] :
( member(D,A)
& member(C,D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,conjecture,
! [E] :
( E != empty_set
=> partition(singleton(E),E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
~ ! [E] :
( E != empty_set
=> partition(singleton(E),E) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,plain,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f23,plain,
! [A,B] :
( ( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
( ! [A,B] :
( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f25,plain,
( ! [A,B] :
( ( ~ member(sK0_skl(B,A),B)
& member(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(B,A))],[f24]) ).
fof(f26,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f28,plain,
! [X0,X1] :
( ~ member(sK0_skl(X1,X0),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f29,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| equal_set(A,B) )
& ( ( subset(B,A)
& subset(A,B) )
| ~ equal_set(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| equal_set(A,B) )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| ~ equal_set(A,B) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f33,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| equal_set(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f34,plain,
! [X,A] :
( ( ~ subset(X,A)
| member(X,power_set(A)) )
& ( subset(X,A)
| ~ member(X,power_set(A)) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f35,plain,
( ! [X,A] :
( ~ subset(X,A)
| member(X,power_set(A)) )
& ! [X,A] :
( subset(X,A)
| ~ member(X,power_set(A)) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f37,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| member(X0,power_set(X1)) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f38,plain,
! [X,A,B] :
( ( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f39,plain,
( ! [X,A,B] :
( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ! [X,A,B] :
( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f43,plain,
! [X,A,B] :
( ( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f44,plain,
( ! [X,A,B] :
( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ! [X,A,B] :
( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( member(X0,X2)
| member(X0,X1)
| ~ member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f48,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f49,plain,
! [B,A,E] :
( ( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f50,plain,
( ! [B,A,E] :
( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ! [B,A,E] :
( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [X,A] :
( ( X != A
| member(X,singleton(A)) )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f55,plain,
( ! [X,A] :
( X != A
| member(X,singleton(A)) )
& ! [X,A] :
( X = A
| ~ member(X,singleton(A)) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1] :
( X0 != X1
| member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f63,plain,
! [X,A] :
( ( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f64,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,sum(A)) ) ),
inference(miniscoping,[status(thm)],[f63]) ).
fof(f65,plain,
( ! [X,A] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
| member(X,sum(A)) )
& ! [X,A] :
( ( member(X,sK1_skl(A,X))
& member(sK1_skl(A,X),A) )
| ~ member(X,sum(A)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y,sK1_skl(A,X))],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( member(sK1_skl(X1,X0),X1)
| ~ member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X2,X1)
| member(X0,sum(X1)) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f76,plain,
! [A,B] :
( disjoint(A,B)
<=> ! [X] :
( ~ member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f77,plain,
! [A,B] :
( ( ? [X] :
( member(X,B)
& member(X,A) )
| disjoint(A,B) )
& ( ! [X] :
( ~ member(X,B)
| ~ member(X,A) )
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
( ! [A,B] :
( ? [X] :
( member(X,B)
& member(X,A) )
| disjoint(A,B) )
& ! [A,B] :
( ! [X] :
( ~ member(X,B)
| ~ member(X,A) )
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
( ! [A,B] :
( ( member(sK3_skl(B,A),B)
& member(sK3_skl(B,A),A) )
| disjoint(A,B) )
& ! [A,B] :
( ! [X] :
( ~ member(X,B)
| ~ member(X,A) )
| ~ disjoint(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(B,A))],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X2,X0)
| ~ disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [X0,X1] :
( member(sK3_skl(X1,X0),X1)
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f83,plain,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f84,definition,
! [A,E] :
( sP0_prd(E,A)
<=> ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f85,plain,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) ) ),
inference(formula_renaming,[status(thm)],[f83,f84]) ).
fof(f86,plain,
! [A,E] :
( ( ? [X,Y] :
( X != Y
& ? [Z] :
( member(Z,Y)
& member(Z,X) )
& member(Y,A)
& member(X,A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(NNF_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
( ! [A,E] :
( ? [X,Y] :
( X != Y
& ? [Z] :
( member(Z,Y)
& member(Z,X) )
& member(Y,A)
& member(X,A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ! [A,E] :
( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
( ! [A,E] :
( ( sK4_skl(E,A) != sK5_skl(E,A)
& member(sK6_skl(E,A),sK5_skl(E,A))
& member(sK6_skl(E,A),sK4_skl(E,A))
& member(sK5_skl(E,A),A)
& member(sK4_skl(E,A),A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ! [A,E] :
( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(X,sK4_skl(E,A)),skolemize(Y,sK5_skl(E,A)),skolemize(Z,sK6_skl(E,A))],[f87]) ).
fof(f90,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X3
| ~ member(X4,X3)
| ~ member(X4,X2)
| ~ member(X3,X0)
| ~ member(X2,X0)
| ~ partition(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f91,plain,
! [X0,X1] :
( member(sK4_skl(X1,X0),X0)
| ~ sP0_prd(X1,X0)
| partition(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f92,plain,
! [X0,X1] :
( member(sK5_skl(X1,X0),X0)
| ~ sP0_prd(X1,X0)
| partition(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f95,plain,
! [X0,X1] :
( sK4_skl(X1,X0) != sK5_skl(X1,X0)
| ~ sP0_prd(X1,X0)
| partition(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f135,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( member(D,A)
& member(C,D) )
| member(C,B) )
& ( ! [D] :
( ~ member(D,A)
| ~ member(C,D) )
| ~ member(C,B) ) )
| B = unaryUnion(A) )
& ( ! [C] :
( ( ! [D] :
( ~ member(D,A)
| ~ member(C,D) )
| member(C,B) )
& ( ? [D] :
( member(D,A)
& member(C,D) )
| ~ member(C,B) ) )
| B != unaryUnion(A) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f136,plain,
( ! [A,B] :
( ? [C] :
( ( ? [D] :
( member(D,A)
& member(C,D) )
| member(C,B) )
& ( ! [D] :
( ~ member(D,A)
| ~ member(C,D) )
| ~ member(C,B) ) )
| B = unaryUnion(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ member(D,A)
| ~ member(C,D) )
| member(C,B) )
& ! [C] :
( ? [D] :
( member(D,A)
& member(C,D) )
| ~ member(C,B) ) )
| B != unaryUnion(A) ) ),
inference(miniscoping,[status(thm)],[f135]) ).
fof(f137,plain,
( ! [A,B] :
( ( ( ( member(sK17_skl(B,A),A)
& member(sK16_skl(B,A),sK17_skl(B,A)) )
| member(sK16_skl(B,A),B) )
& ( ! [D] :
( ~ member(D,A)
| ~ member(sK16_skl(B,A),D) )
| ~ member(sK16_skl(B,A),B) ) )
| B = unaryUnion(A) )
& ! [A,B] :
( ( ! [C] :
( ! [D] :
( ~ member(D,A)
| ~ member(C,D) )
| member(C,B) )
& ! [C] :
( ( member(sK15_skl(C,B,A),A)
& member(C,sK15_skl(C,B,A)) )
| ~ member(C,B) ) )
| B != unaryUnion(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(D,sK15_skl(C,B,A)),skolemize(C,sK16_skl(B,A)),skolemize(D,sK17_skl(B,A))],[f136]) ).
fof(f139,plain,
! [X0,X1,X2] :
( member(sK15_skl(X2,X0,X1),X1)
| ~ member(X2,X0)
| X0 != unaryUnion(X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
! [X0,X1,X2,X3] :
( ~ member(X3,X1)
| ~ member(X2,X3)
| member(X2,X0)
| X0 != unaryUnion(X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f142,plain,
! [X0,X1] :
( member(sK16_skl(X0,X1),sK17_skl(X0,X1))
| member(sK16_skl(X0,X1),X0)
| X0 = unaryUnion(X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f143,plain,
! [X0,X1] :
( member(sK17_skl(X0,X1),X1)
| member(sK16_skl(X0,X1),X0)
| X0 = unaryUnion(X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f144,plain,
? [E] :
( ~ partition(singleton(E),E)
& E != empty_set ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f145,plain,
( ~ partition(singleton(sK18_skl),sK18_skl)
& sK18_skl != empty_set ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(E,sK18_skl)],[f144]) ).
fof(f147,plain,
~ partition(singleton(sK18_skl),sK18_skl),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f148,plain,
! [A,E] :
( ( ? [X] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
& member(X,E) )
| ? [X] :
( ~ subset(X,E)
& member(X,A) )
| sP0_prd(E,A) )
& ( ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(NNF_transformation,[status(thm)],[f84]) ).
fof(f149,plain,
( ! [A,E] :
( ? [X] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
& member(X,E) )
| ? [X] :
( ~ subset(X,E)
& member(X,A) )
| sP0_prd(E,A) )
& ! [A,E] :
( ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f150,plain,
( ! [A,E] :
( ( ! [Y] :
( ~ member(sK21_skl(E,A),Y)
| ~ member(Y,A) )
& member(sK21_skl(E,A),E) )
| ( ~ subset(sK20_skl(E,A),E)
& member(sK20_skl(E,A),A) )
| sP0_prd(E,A) )
& ! [A,E] :
( ( ! [X] :
( ( member(X,sK19_skl(X,E,A))
& member(sK19_skl(X,E,A),A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(Y,sK19_skl(X,E,A)),skolemize(X,sK20_skl(E,A)),skolemize(X,sK21_skl(E,A))],[f149]) ).
fof(f154,plain,
! [X0,X1] :
( member(sK21_skl(X0,X1),X0)
| member(sK20_skl(X0,X1),X1)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f155,plain,
! [X0,X1,X2] :
( ~ member(sK21_skl(X0,X1),X2)
| ~ member(X2,X1)
| member(sK20_skl(X0,X1),X1)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f156,plain,
! [X0,X1] :
( member(sK21_skl(X0,X1),X0)
| ~ subset(sK20_skl(X0,X1),X0)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f157,plain,
! [X0,X1,X2] :
( ~ member(sK21_skl(X0,X1),X2)
| ~ member(X2,X1)
| ~ subset(sK20_skl(X0,X1),X0)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f179,plain,
! [X0] : member(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f57]) ).
fof(f183,plain,
! [X0,X1] :
( member(sK15_skl(X0,unaryUnion(X1),X1),X1)
| ~ member(X0,unaryUnion(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f139]) ).
fof(f184,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X0,X2)
| member(X0,unaryUnion(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f140]) ).
fof(f186,plain,
! [X0,X1,X2] :
( member(X2,X0)
| ~ member(X2,X1)
| member(sK0_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f27,f26]) ).
fof(f189,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| member(X0,power_set(X1)) ),
inference(resolution,[status(thm)],[f37,f27]) ).
fof(f204,plain,
! [X0,X1,X2] :
( member(sK1_skl(X1,X2),X1)
| ~ member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f68,f66]) ).
fof(f205,plain,
! [X0,X1,X2] :
( member(sK3_skl(X2,X1),X2)
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f80,f82]) ).
fof(f226,plain,
! [X0,X1] :
( member(X1,X0)
| member(sK0_skl(X0,singleton(X1)),singleton(X1)) ),
inference(resolution,[status(thm)],[f186,f179]) ).
fof(f228,plain,
! [X0,X1] :
( sK0_skl(X1,singleton(X0)) = X0
| member(X0,X1) ),
inference(resolution,[status(thm)],[f226,f56]) ).
fof(f236,plain,
! [X0,X1] :
( member(sK1_skl(X0,X1),X0)
| sK0_skl(sum(X0),singleton(X1)) = X1 ),
inference(resolution,[status(thm)],[f228,f66]) ).
fof(f245,plain,
! [X0] : sK0_skl(empty_set,singleton(X0)) = X0,
inference(resolution,[status(thm)],[f228,f48]) ).
fof(f590,plain,
! [X0,X1,X2] :
( sK1_skl(singleton(X1),X2) = X1
| ~ member(X2,X0)
| ~ member(X0,singleton(X1)) ),
inference(resolution,[status(thm)],[f204,f56]) ).
fof(f607,plain,
! [X0,X1,X2] :
( sK3_skl(singleton(X2),X1) = X2
| ~ member(X0,singleton(X2))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f205,f56]) ).
fof(f693,plain,
! [X0,X1] :
( sK1_skl(singleton(X1),X0) = X1
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f590,f179]) ).
fof(f738,plain,
! [X0,X1] :
( sK0_skl(X0,singleton(X1)) = X1
| sK1_skl(singleton(X0),X1) = X0 ),
inference(resolution,[status(thm)],[f693,f228]) ).
fof(f749,plain,
! [X0,X1] :
( sK3_skl(singleton(X0),X1) = X0
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f607,f179]) ).
fof(f791,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| sK3_skl(singleton(X0),power_set(X1)) = X0 ),
inference(resolution,[status(thm)],[f749,f189]) ).
fof(f824,plain,
! [X0,X1] :
( member(sK15_skl(sK17_skl(X0,unaryUnion(X1)),unaryUnion(X1),X1),X1)
| member(sK16_skl(X0,unaryUnion(X1)),X0)
| X0 = unaryUnion(unaryUnion(X1)) ),
inference(resolution,[status(thm)],[f143,f183]) ).
fof(f841,plain,
! [X0] :
( member(sK16_skl(X0,empty_set),X0)
| X0 = unaryUnion(empty_set) ),
inference(resolution,[status(thm)],[f143,f48]) ).
fof(f924,plain,
! [X0,X1] :
( member(sK16_skl(difference(X0,X1),empty_set),X0)
| difference(X0,X1) = unaryUnion(empty_set) ),
inference(resolution,[status(thm)],[f841,f51]) ).
fof(f926,plain,
! [X0,X1] :
( member(sK16_skl(intersection(X0,X1),empty_set),X1)
| intersection(X0,X1) = unaryUnion(empty_set) ),
inference(resolution,[status(thm)],[f841,f41]) ).
fof(f927,plain,
! [X0,X1] :
( member(sK16_skl(intersection(X0,X1),empty_set),X0)
| intersection(X0,X1) = unaryUnion(empty_set) ),
inference(resolution,[status(thm)],[f841,f40]) ).
fof(f933,plain,
empty_set = unaryUnion(empty_set),
inference(resolution,[status(thm)],[f841,f48]) ).
fof(f939,plain,
! [X0,X1] :
( member(sK16_skl(X0,empty_set),X1)
| member(sK0_skl(X1,X0),X0)
| X0 = unaryUnion(empty_set) ),
inference(resolution,[status(thm)],[f841,f186]) ).
fof(f962,plain,
! [X0] :
( member(sK16_skl(X0,empty_set),X0)
| X0 = empty_set ),
inference(backward_demodulation,[status(thm)],[f933,f841]) ).
fof(f990,plain,
! [X0] :
( sK16_skl(singleton(X0),empty_set) = X0
| singleton(X0) = empty_set ),
inference(resolution,[status(thm)],[f962,f56]) ).
fof(f1003,plain,
! [X0,X1] :
( member(sK5_skl(X0,X1),X1)
| partition(X1,X0)
| member(sK21_skl(X0,X1),X0)
| member(sK20_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f154,f92]) ).
fof(f1042,plain,
( sK16_skl(singleton(sK18_skl),empty_set) = sK18_skl
| ~ partition(empty_set,sK18_skl) ),
inference(paramodulation,[status(thm)],[f990,f147]) ).
fof(f1096,definition,
( sQ2_spl
<=> partition(empty_set,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
( sQ2_spl
| ~ partition(empty_set,sK18_skl) ),
inference(component_clause,[status(thm)],[f1096]) ).
fof(f1099,definition,
( sQ3_spl
<=> sK16_skl(singleton(sK18_skl),empty_set) = sK18_skl ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1102,plain,
( sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f1042,f1096,f1099]) ).
fof(f2300,plain,
! [X0,X1] :
( member(sK16_skl(difference(X0,X1),empty_set),X0)
| difference(X0,X1) = empty_set ),
inference(forward_demodulation,[status(thm)],[f933,f924]) ).
fof(f2320,plain,
! [X0] : difference(empty_set,X0) = empty_set,
inference(resolution,[status(thm)],[f2300,f48]) ).
fof(f2362,plain,
! [X0] :
( member(sK16_skl(empty_set,empty_set),empty_set)
| difference(empty_set,X0) = empty_set ),
inference(paramodulation,[status(thm)],[f2320,f2300]) ).
fof(f2372,definition,
! [X0] :
( sQ16_spl
<=> difference(empty_set,X0) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f2375,definition,
( sQ17_spl
<=> member(sK16_skl(empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f2376,plain,
( ~ sQ17_spl
| member(sK16_skl(empty_set,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f2375]) ).
fof(f2378,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f2362,f2372,f2375]) ).
fof(f2418,plain,
! [X0,X1] :
( member(sK16_skl(intersection(X0,X1),empty_set),X1)
| intersection(X0,X1) = empty_set ),
inference(forward_demodulation,[status(thm)],[f933,f926]) ).
fof(f2437,plain,
! [X0] : intersection(X0,empty_set) = empty_set,
inference(resolution,[status(thm)],[f2418,f48]) ).
fof(f2453,plain,
! [X0] :
( member(sK16_skl(empty_set,empty_set),empty_set)
| intersection(X0,empty_set) = empty_set ),
inference(paramodulation,[status(thm)],[f2437,f2418]) ).
fof(f2462,definition,
! [X0] :
( sQ18_spl
<=> intersection(X0,empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f2465,plain,
( sQ17_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2453,f2462,f2375]) ).
fof(f2472,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2376,f48]) ).
fof(f2473,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f2472]) ).
fof(f2495,plain,
! [X0] : sK3_skl(singleton(empty_set),power_set(X0)) = empty_set,
inference(resolution,[status(thm)],[f791,f48]) ).
fof(f2653,plain,
! [X0,X1] :
( member(empty_set,singleton(empty_set))
| ~ member(X0,singleton(empty_set))
| ~ member(X0,power_set(X1)) ),
inference(paramodulation,[status(thm)],[f2495,f205]) ).
fof(f2659,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ member(X0,singleton(empty_set))
| ~ member(X0,power_set(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f2660,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ member(X0,singleton(empty_set))
| ~ member(X0,power_set(X1)) ),
inference(component_clause,[status(thm)],[f2659]) ).
fof(f2662,definition,
( sQ21_spl
<=> member(empty_set,singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f2665,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f2653,f2659,f2662]) ).
fof(f2666,plain,
! [X0,X1] :
( member(sK16_skl(intersection(X0,X1),empty_set),X0)
| intersection(X0,X1) = empty_set ),
inference(forward_demodulation,[status(thm)],[f933,f927]) ).
fof(f2685,plain,
! [X0] : intersection(empty_set,X0) = empty_set,
inference(resolution,[status(thm)],[f2666,f48]) ).
fof(f2703,plain,
! [X0] :
( member(sK16_skl(empty_set,empty_set),empty_set)
| intersection(empty_set,X0) = empty_set ),
inference(paramodulation,[status(thm)],[f2685,f2666]) ).
fof(f2713,definition,
! [X0] :
( sQ22_spl
<=> intersection(empty_set,X0) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f2716,plain,
( sQ17_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f2703,f2713,f2375]) ).
fof(f2729,plain,
! [X0,X1] :
( member(sK16_skl(X0,empty_set),X1)
| member(sK0_skl(X1,X0),X0)
| X0 = empty_set ),
inference(forward_demodulation,[status(thm)],[f933,f939]) ).
fof(f2752,plain,
! [X0] :
( member(sK0_skl(empty_set,X0),X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f2729,f48]) ).
fof(f2835,plain,
! [X0,X1] :
( ~ sQ20_spl
| member(sK0_skl(X1,X0),X0)
| ~ member(X0,singleton(empty_set)) ),
inference(resolution,[status(thm)],[f2660,f189]) ).
fof(f3015,plain,
! [X0] :
( ~ sQ20_spl
| member(sK0_skl(X0,empty_set),empty_set) ),
inference(resolution,[status(thm)],[f2835,f179]) ).
fof(f3032,definition,
( sQ24_spl
<=> singleton(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f3033,plain,
( ~ sQ24_spl
| singleton(empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f3032]) ).
fof(f3034,plain,
( sQ24_spl
| singleton(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f3032]) ).
fof(f3043,definition,
! [X0] :
( sQ27_spl
<=> member(sK0_skl(X0,sK0_skl(empty_set,singleton(empty_set))),sK0_skl(empty_set,singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f3044,plain,
! [X0] :
( ~ sQ27_spl
| member(sK0_skl(X0,sK0_skl(empty_set,singleton(empty_set))),sK0_skl(empty_set,singleton(empty_set))) ),
inference(component_clause,[status(thm)],[f3043]) ).
fof(f3051,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3015,f48]) ).
fof(f3052,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f3051]) ).
fof(f3196,plain,
! [X0] :
( member(sK15_skl(sK17_skl(empty_set,unaryUnion(X0)),unaryUnion(X0),X0),X0)
| empty_set = unaryUnion(unaryUnion(X0)) ),
inference(resolution,[status(thm)],[f824,f48]) ).
fof(f4292,plain,
! [X0] :
( ~ sQ27_spl
| member(sK0_skl(X0,empty_set),sK0_skl(empty_set,singleton(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f245,f3044]) ).
fof(f4293,plain,
! [X0] :
( ~ sQ27_spl
| member(sK0_skl(X0,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f245,f4292]) ).
fof(f4294,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4293,f48]) ).
fof(f4295,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f4294]) ).
fof(f4392,plain,
( ~ sQ24_spl
| member(empty_set,empty_set) ),
inference(paramodulation,[status(thm)],[f3033,f179]) ).
fof(f4396,definition,
( sQ41_spl
<=> member(empty_set,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f4397,plain,
( ~ sQ41_spl
| member(empty_set,empty_set) ),
inference(component_clause,[status(thm)],[f4396]) ).
fof(f4410,definition,
! [X0] :
( sQ44_spl
<=> ~ member(X0,singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f4411,plain,
! [X0] :
( ~ sQ44_spl
| ~ member(X0,singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f4410]) ).
fof(f4413,definition,
! [X1] :
( sQ45_spl
<=> member(empty_set,union(empty_set,X1)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f4414,plain,
! [X0] :
( ~ sQ45_spl
| member(empty_set,union(empty_set,X0)) ),
inference(component_clause,[status(thm)],[f4413]) ).
fof(f4417,definition,
! [X1] :
( sQ46_spl
<=> member(empty_set,union(X1,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f4418,plain,
! [X0] :
( ~ sQ46_spl
| member(empty_set,union(X0,empty_set)) ),
inference(component_clause,[status(thm)],[f4417]) ).
fof(f4425,definition,
( sQ47_spl
<=> sK1_skl(empty_set,sK16_skl(empty_set,empty_set)) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f4426,plain,
( ~ sQ47_spl
| sK1_skl(empty_set,sK16_skl(empty_set,empty_set)) = empty_set ),
inference(component_clause,[status(thm)],[f4425]) ).
fof(f4432,definition,
( sQ49_spl
<=> sK17_skl(empty_set,singleton(empty_set)) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f4433,plain,
( ~ sQ49_spl
| sK17_skl(empty_set,singleton(empty_set)) = empty_set ),
inference(component_clause,[status(thm)],[f4432]) ).
fof(f4511,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4392,f48]) ).
fof(f4512,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f4511]) ).
fof(f4710,plain,
( member(sK15_skl(sK17_skl(empty_set,unaryUnion(empty_set)),empty_set,empty_set),empty_set)
| empty_set = unaryUnion(unaryUnion(empty_set)) ),
inference(paramodulation,[status(thm)],[f933,f3196]) ).
fof(f4714,definition,
( sQ51_spl
<=> empty_set = unaryUnion(unaryUnion(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f4717,definition,
( sQ52_spl
<=> member(sK15_skl(sK17_skl(empty_set,empty_set),unaryUnion(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f4718,plain,
( ~ sQ52_spl
| member(sK15_skl(sK17_skl(empty_set,empty_set),unaryUnion(empty_set),empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f4717]) ).
fof(f4721,definition,
( sQ53_spl
<=> member(sK15_skl(sK17_skl(empty_set,unaryUnion(empty_set)),empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f4722,plain,
( ~ sQ53_spl
| member(sK15_skl(sK17_skl(empty_set,unaryUnion(empty_set)),empty_set,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f4721]) ).
fof(f4724,plain,
( sQ53_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f4710,f4714,f4721]) ).
fof(f4726,plain,
( ~ sQ53_spl
| member(sK15_skl(sK17_skl(empty_set,empty_set),empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f933,f4722]) ).
fof(f4727,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4726,f48]) ).
fof(f4728,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f4727]) ).
fof(f4729,plain,
( ~ sQ52_spl
| member(sK15_skl(sK17_skl(empty_set,empty_set),empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f933,f4718]) ).
fof(f4730,plain,
( ~ sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4729,f48]) ).
fof(f4731,plain,
~ sQ52_spl,
inference(contradiction_clause,[status(thm)],[f4730]) ).
fof(f4777,plain,
( ~ sQ44_spl
| $false ),
inference(resolution,[status(thm)],[f4411,f179]) ).
fof(f4795,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f4777]) ).
fof(f4796,plain,
( sQ2_spl
| member(sK5_skl(sK18_skl,empty_set),empty_set)
| member(sK21_skl(sK18_skl,empty_set),sK18_skl)
| member(sK20_skl(sK18_skl,empty_set),empty_set) ),
inference(resolution,[status(thm)],[f1003,f1098]) ).
fof(f4799,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X3
| ~ member(X4,X3)
| ~ member(X4,X2)
| ~ member(X3,X1)
| ~ member(X2,X1)
| member(sK5_skl(X0,X1),X1)
| member(sK21_skl(X0,X1),X0)
| member(sK20_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f1003,f90]) ).
fof(f4801,definition,
( sQ54_spl
<=> member(sK20_skl(sK18_skl,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f4802,plain,
( ~ sQ54_spl
| member(sK20_skl(sK18_skl,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f4801]) ).
fof(f4804,definition,
( sQ55_spl
<=> member(sK21_skl(sK18_skl,empty_set),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f4805,plain,
( ~ sQ55_spl
| member(sK21_skl(sK18_skl,empty_set),sK18_skl) ),
inference(component_clause,[status(thm)],[f4804]) ).
fof(f4807,definition,
( sQ56_spl
<=> member(sK5_skl(sK18_skl,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f4808,plain,
( ~ sQ56_spl
| member(sK5_skl(sK18_skl,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f4807]) ).
fof(f4810,plain,
( sQ2_spl
| sQ56_spl
| sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f4796,f4801,f4804,f4807,f1096]) ).
fof(f4811,definition,
( sQ57_spl
<=> member(sK20_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f4812,plain,
( ~ sQ57_spl
| member(sK20_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f4811]) ).
fof(f4814,definition,
( sQ58_spl
<=> member(sK21_skl(sK18_skl,singleton(sK18_skl)),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f4815,plain,
( ~ sQ58_spl
| member(sK21_skl(sK18_skl,singleton(sK18_skl)),sK18_skl) ),
inference(component_clause,[status(thm)],[f4814]) ).
fof(f4817,definition,
( sQ59_spl
<=> member(sK5_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f4818,plain,
( ~ sQ59_spl
| member(sK5_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f4817]) ).
fof(f4821,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4808,f48]) ).
fof(f4822,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f4821]) ).
fof(f4823,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4802,f48]) ).
fof(f4824,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f4823]) ).
fof(f4829,definition,
( sQ60_spl
<=> member(sK4_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f4830,plain,
( ~ sQ60_spl
| member(sK4_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f4829]) ).
fof(f4844,plain,
( ~ sQ55_spl
| sK1_skl(singleton(sK18_skl),sK21_skl(sK18_skl,empty_set)) = sK18_skl ),
inference(resolution,[status(thm)],[f4805,f693]) ).
fof(f4853,plain,
( ~ sQ59_spl
| sK5_skl(sK18_skl,singleton(sK18_skl)) = sK18_skl ),
inference(resolution,[status(thm)],[f4818,f56]) ).
fof(f4876,plain,
! [X0] :
( ~ sQ46_spl
| member(empty_set,empty_set)
| member(empty_set,X0) ),
inference(resolution,[status(thm)],[f4418,f45]) ).
fof(f4888,definition,
! [X0] :
( sQ61_spl
<=> member(empty_set,X0) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f4889,plain,
! [X0] :
( ~ sQ61_spl
| member(empty_set,X0) ),
inference(component_clause,[status(thm)],[f4888]) ).
fof(f4891,plain,
( ~ sQ46_spl
| sQ41_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f4876,f4888,f4396,f4417]) ).
fof(f4979,plain,
! [X0] :
( ~ sQ61_spl
| ~ member(empty_set,X0) ),
inference(resolution,[status(thm)],[f4889,f52]) ).
fof(f5002,definition,
! [X0] :
( sQ62_spl
<=> empty_set = X0 ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f5003,plain,
! [X0] :
( ~ sQ62_spl
| empty_set = X0 ),
inference(component_clause,[status(thm)],[f5002]) ).
fof(f5006,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4979,f4889]) ).
fof(f5007,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f5006]) ).
fof(f5008,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4397,f48]) ).
fof(f5009,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f5008]) ).
fof(f5010,plain,
( sQ24_spl
| ~ sQ62_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3034,f5003]) ).
fof(f5030,plain,
( sQ24_spl
| ~ sQ62_spl ),
inference(contradiction_clause,[status(thm)],[f5010]) ).
fof(f5078,definition,
! [X0] :
( sQ63_spl
<=> ( ~ member(sK21_skl(sK18_skl,singleton(sK18_skl)),X0)
| ~ member(X0,singleton(sK18_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f5079,plain,
! [X0] :
( ~ sQ63_spl
| ~ member(sK21_skl(sK18_skl,singleton(sK18_skl)),X0)
| ~ member(X0,singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f5078]) ).
fof(f5081,definition,
( sQ64_spl
<=> partition(singleton(sK18_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f5082,plain,
( ~ sQ64_spl
| partition(singleton(sK18_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f5081]) ).
fof(f5084,definition,
( sQ65_spl
<=> sK4_skl(sK18_skl,singleton(sK18_skl)) = sK18_skl ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f5085,plain,
( ~ sQ65_spl
| sK4_skl(sK18_skl,singleton(sK18_skl)) = sK18_skl ),
inference(component_clause,[status(thm)],[f5084]) ).
fof(f5086,plain,
( sQ65_spl
| sK4_skl(sK18_skl,singleton(sK18_skl)) != sK18_skl ),
inference(component_clause,[status(thm)],[f5084]) ).
fof(f5089,definition,
( sQ66_spl
<=> sP0_prd(sK18_skl,singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f5090,plain,
( ~ sQ66_spl
| sP0_prd(sK18_skl,singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f5089]) ).
fof(f5091,plain,
( sQ66_spl
| ~ sP0_prd(sK18_skl,singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f5089]) ).
fof(f5096,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5082,f147]) ).
fof(f5097,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f5096]) ).
fof(f5332,plain,
! [X0] :
( sQ66_spl
| ~ member(sK21_skl(sK18_skl,singleton(sK18_skl)),X0)
| ~ member(X0,singleton(sK18_skl))
| member(sK20_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
inference(resolution,[status(thm)],[f5091,f155]) ).
fof(f5333,plain,
( sQ66_spl
| member(sK21_skl(sK18_skl,singleton(sK18_skl)),sK18_skl)
| member(sK20_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl)) ),
inference(resolution,[status(thm)],[f5091,f154]) ).
fof(f5334,plain,
( sQ66_spl
| sQ63_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f5332,f4811,f5078,f5089]) ).
fof(f5335,plain,
( sQ66_spl
| sQ58_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f5333,f4811,f4814,f5089]) ).
fof(f5341,plain,
( ~ sQ57_spl
| sK20_skl(sK18_skl,singleton(sK18_skl)) = sK18_skl ),
inference(resolution,[status(thm)],[f4812,f56]) ).
fof(f5507,plain,
! [X0] :
( ~ sQ45_spl
| member(empty_set,X0)
| member(empty_set,empty_set) ),
inference(resolution,[status(thm)],[f4414,f45]) ).
fof(f5518,plain,
( ~ sQ45_spl
| sQ61_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f5507,f4396,f4888,f4413]) ).
fof(f5553,plain,
( ~ sQ60_spl
| sK4_skl(sK18_skl,singleton(sK18_skl)) = sK18_skl ),
inference(resolution,[status(thm)],[f4830,f56]) ).
fof(f5564,plain,
( ~ sQ60_spl
| sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5553,f5086]) ).
fof(f5565,plain,
( ~ sQ60_spl
| sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f5564]) ).
fof(f5721,plain,
( ~ sQ49_spl
| member(sK16_skl(empty_set,singleton(empty_set)),empty_set)
| member(sK16_skl(empty_set,singleton(empty_set)),empty_set)
| empty_set = unaryUnion(singleton(empty_set)) ),
inference(paramodulation,[status(thm)],[f4433,f142]) ).
fof(f5722,definition,
( sQ68_spl
<=> empty_set = unaryUnion(singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f5723,plain,
( ~ sQ68_spl
| empty_set = unaryUnion(singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f5722]) ).
fof(f5725,definition,
( sQ69_spl
<=> member(sK16_skl(empty_set,singleton(empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f5726,plain,
( ~ sQ69_spl
| member(sK16_skl(empty_set,singleton(empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f5725]) ).
fof(f5729,plain,
( ~ sQ49_spl
| sQ69_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f5721,f5722,f5725,f4432]) ).
fof(f5730,plain,
( ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5726,f48]) ).
fof(f5731,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f5730]) ).
fof(f5748,plain,
! [X0] :
( ~ sQ57_spl
| ~ member(sK21_skl(sK18_skl,singleton(sK18_skl)),X0)
| ~ member(X0,singleton(sK18_skl))
| ~ subset(sK18_skl,sK18_skl)
| sP0_prd(sK18_skl,singleton(sK18_skl)) ),
inference(paramodulation,[status(thm)],[f5341,f157]) ).
fof(f5749,plain,
( ~ sQ57_spl
| member(sK21_skl(sK18_skl,singleton(sK18_skl)),sK18_skl)
| ~ subset(sK18_skl,sK18_skl)
| sP0_prd(sK18_skl,singleton(sK18_skl)) ),
inference(paramodulation,[status(thm)],[f5341,f156]) ).
fof(f5750,definition,
( sQ70_spl
<=> member(sK18_skl,singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f5757,definition,
( sQ72_spl
<=> subset(sK18_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f5758,plain,
( ~ sQ72_spl
| subset(sK18_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f5757]) ).
fof(f5759,plain,
( sQ72_spl
| ~ subset(sK18_skl,sK18_skl) ),
inference(component_clause,[status(thm)],[f5757]) ).
fof(f5760,plain,
( ~ sQ57_spl
| sQ63_spl
| ~ sQ72_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f5748,f5089,f5757,f5078,f4811]) ).
fof(f5761,plain,
( ~ sQ57_spl
| sQ58_spl
| ~ sQ72_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f5749,f5089,f5757,f4814,f4811]) ).
fof(f5781,plain,
( sQ72_spl
| member(sK0_skl(sK18_skl,sK18_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f5759,f27]) ).
fof(f5800,plain,
! [X0,X1] :
( ~ sQ68_spl
| ~ member(X1,singleton(empty_set))
| ~ member(X0,X1)
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f5723,f184]) ).
fof(f5826,plain,
! [X0,X1] :
( ~ sQ68_spl
| ~ member(X1,singleton(empty_set))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f5800,f48]) ).
fof(f6025,plain,
( sQ72_spl
| subset(sK18_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f5781,f28]) ).
fof(f6036,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6025,f5759]) ).
fof(f6037,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f6036]) ).
fof(f6057,plain,
( ~ sQ72_spl
| ~ subset(sK18_skl,sK18_skl)
| equal_set(sK18_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f5758,f33]) ).
fof(f6059,definition,
( sQ78_spl
<=> equal_set(sK18_skl,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f6062,plain,
( ~ sQ72_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f6057,f6059,f5757]) ).
fof(f6406,plain,
! [X0] :
( ~ sQ68_spl
| singleton(empty_set) = empty_set
| ~ member(X0,sK16_skl(singleton(empty_set),empty_set)) ),
inference(resolution,[status(thm)],[f5826,f962]) ).
fof(f6417,plain,
! [X0] :
( ~ sQ68_spl
| singleton(empty_set) = empty_set
| ~ member(X0,sK0_skl(empty_set,singleton(empty_set))) ),
inference(resolution,[status(thm)],[f5826,f2752]) ).
fof(f6450,definition,
! [X0] :
( sQ79_spl
<=> ~ member(X0,sK16_skl(singleton(empty_set),empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f6453,plain,
( ~ sQ68_spl
| sQ24_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f6406,f6450,f3032,f5722]) ).
fof(f6454,definition,
! [X0] :
( sQ80_spl
<=> ~ member(X0,sK0_skl(empty_set,singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f6457,plain,
( ~ sQ68_spl
| sQ24_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f6417,f6454,f3032,f5722]) ).
fof(f6470,plain,
! [X0] :
( ~ sQ47_spl
| member(empty_set,empty_set)
| ~ member(sK16_skl(empty_set,empty_set),X0)
| ~ member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f4426,f204]) ).
fof(f6472,plain,
( ~ sQ47_spl
| member(empty_set,empty_set)
| sK0_skl(sum(empty_set),singleton(sK16_skl(empty_set,empty_set))) = sK16_skl(empty_set,empty_set) ),
inference(paramodulation,[status(thm)],[f4426,f236]) ).
fof(f6474,definition,
! [X0] :
( sQ81_spl
<=> ( ~ member(sK16_skl(empty_set,empty_set),X0)
| ~ member(X0,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f6477,plain,
( ~ sQ47_spl
| sQ41_spl
| sQ81_spl ),
inference(split_clause,[status(thm)],[f6470,f6474,f4396,f4425]) ).
fof(f6479,definition,
( sQ82_spl
<=> sK0_skl(sum(empty_set),singleton(sK16_skl(empty_set,empty_set))) = sK16_skl(empty_set,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f6482,plain,
( ~ sQ47_spl
| sQ41_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f6472,f6479,f4396,f4425]) ).
fof(f6546,plain,
( ~ sQ55_spl
| sK0_skl(sK18_skl,singleton(sK21_skl(sK18_skl,empty_set))) = sK21_skl(sK18_skl,empty_set)
| sK18_skl = sK18_skl ),
inference(paramodulation,[status(thm)],[f738,f4844]) ).
fof(f6548,plain,
! [X0] :
( ~ sQ55_spl
| member(sK18_skl,singleton(sK18_skl))
| ~ member(sK21_skl(sK18_skl,empty_set),X0)
| ~ member(X0,singleton(sK18_skl)) ),
inference(paramodulation,[status(thm)],[f4844,f204]) ).
fof(f6550,plain,
( ~ sQ55_spl
| member(sK18_skl,singleton(sK18_skl))
| sK0_skl(sum(singleton(sK18_skl)),singleton(sK21_skl(sK18_skl,empty_set))) = sK21_skl(sK18_skl,empty_set) ),
inference(paramodulation,[status(thm)],[f4844,f236]) ).
fof(f6552,definition,
( sQ83_spl
<=> sK18_skl = sK18_skl ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f6555,definition,
( sQ84_spl
<=> sK0_skl(sK18_skl,singleton(sK21_skl(sK18_skl,empty_set))) = sK21_skl(sK18_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f6558,plain,
( ~ sQ55_spl
| sQ84_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f6546,f6552,f6555,f4804]) ).
fof(f6560,definition,
! [X0] :
( sQ85_spl
<=> ( ~ member(sK21_skl(sK18_skl,empty_set),X0)
| ~ member(X0,singleton(sK18_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f6563,plain,
( ~ sQ55_spl
| sQ70_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f6548,f6560,f5750,f4804]) ).
fof(f6565,definition,
( sQ86_spl
<=> sK0_skl(sum(singleton(sK18_skl)),singleton(sK21_skl(sK18_skl,empty_set))) = sK21_skl(sK18_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f6568,plain,
( ~ sQ55_spl
| sQ70_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f6550,f6565,f5750,f4804]) ).
fof(f6570,plain,
( ~ sQ58_spl
| ~ sQ63_spl
| ~ member(sK18_skl,singleton(sK18_skl)) ),
inference(resolution,[status(thm)],[f5079,f4815]) ).
fof(f6609,plain,
( ~ sQ58_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6570,f179]) ).
fof(f6610,plain,
( ~ sQ58_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f6609]) ).
fof(f6613,plain,
( ~ sQ66_spl
| sK4_skl(sK18_skl,singleton(sK18_skl)) != sK5_skl(sK18_skl,singleton(sK18_skl))
| partition(singleton(sK18_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f5090,f95]) ).
fof(f6614,plain,
( ~ sQ66_spl
| member(sK5_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl))
| partition(singleton(sK18_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f5090,f92]) ).
fof(f6615,plain,
( ~ sQ66_spl
| member(sK4_skl(sK18_skl,singleton(sK18_skl)),singleton(sK18_skl))
| partition(singleton(sK18_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f5090,f91]) ).
fof(f6617,definition,
( sQ87_spl
<=> sK4_skl(sK18_skl,singleton(sK18_skl)) = sK5_skl(sK18_skl,singleton(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f6619,plain,
( sQ87_spl
| sK4_skl(sK18_skl,singleton(sK18_skl)) != sK5_skl(sK18_skl,singleton(sK18_skl)) ),
inference(component_clause,[status(thm)],[f6617]) ).
fof(f6620,plain,
( ~ sQ66_spl
| ~ sQ87_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f6613,f5081,f6617,f5089]) ).
fof(f6621,plain,
( ~ sQ66_spl
| sQ59_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f6614,f5081,f4817,f5089]) ).
fof(f6622,plain,
( ~ sQ66_spl
| sQ60_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f6615,f5081,f4829,f5089]) ).
fof(f6623,plain,
( sQ87_spl
| ~ sQ65_spl
| sK18_skl != sK5_skl(sK18_skl,singleton(sK18_skl)) ),
inference(forward_demodulation,[status(thm)],[f5085,f6619]) ).
fof(f6712,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ68_spl
| ~ member(X4,sK5_skl(X0,singleton(empty_set)))
| X1 = X2
| ~ member(X3,X2)
| ~ member(X3,X1)
| ~ member(X2,singleton(empty_set))
| ~ member(X1,singleton(empty_set))
| member(sK21_skl(X0,singleton(empty_set)),X0)
| member(sK20_skl(X0,singleton(empty_set)),singleton(empty_set)) ),
inference(resolution,[status(thm)],[f4799,f5826]) ).
fof(f6719,plain,
! [X0,X1,X2,X3] :
( X1 = X2
| ~ member(X3,X2)
| ~ member(X3,X1)
| ~ member(X2,empty_set)
| ~ member(X1,empty_set)
| member(sK21_skl(X0,empty_set),X0)
| member(sK20_skl(X0,empty_set),empty_set) ),
inference(resolution,[status(thm)],[f4799,f48]) ).
fof(f6730,definition,
! [X0,X4] :
( sQ91_spl
<=> ( ~ member(X4,sK5_skl(X0,singleton(empty_set)))
| member(sK21_skl(X0,singleton(empty_set)),X0)
| member(sK20_skl(X0,singleton(empty_set)),singleton(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f6733,definition,
! [X1,X2,X3] :
( sQ92_spl
<=> ( X1 = X2
| ~ member(X3,X2)
| ~ member(X3,X1)
| ~ member(X2,singleton(empty_set))
| ~ member(X1,singleton(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f6736,plain,
( ~ sQ68_spl
| sQ92_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f6712,f6730,f6733,f5722]) ).
fof(f6737,definition,
! [X0] :
( sQ93_spl
<=> ( member(sK21_skl(X0,empty_set),X0)
| member(sK20_skl(X0,empty_set),empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f6738,plain,
! [X0] :
( ~ sQ93_spl
| member(sK21_skl(X0,empty_set),X0)
| member(sK20_skl(X0,empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f6737]) ).
fof(f6740,definition,
! [X1,X2,X3] :
( sQ94_spl
<=> ( X1 = X2
| ~ member(X3,X2)
| ~ member(X3,X1)
| ~ member(X2,empty_set)
| ~ member(X1,empty_set) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f6743,plain,
( sQ94_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f6719,f6737,f6740]) ).
fof(f6744,plain,
! [X0] :
( ~ sQ93_spl
| member(sK21_skl(X0,empty_set),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6738,f48]) ).
fof(f6764,plain,
( ~ sQ93_spl
| $false ),
inference(resolution,[status(thm)],[f6744,f48]) ).
fof(f6775,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f6764]) ).
fof(f6831,plain,
( ~ sQ59_spl
| sQ87_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4853,f6623]) ).
fof(f6832,plain,
( ~ sQ59_spl
| sQ87_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f6831]) ).
fof(f6833,plain,
$false,
inference(sat_refutation,[status(thm)],[f1102,f2378,f2465,f2473,f2665,f2716,f3052,f4295,f4512,f4724,f4728,f4731,f4795,f4810,f4822,f4824,f4891,f5007,f5009,f5030,f5097,f5334,f5335,f5518,f5565,f5729,f5731,f5760,f5761,f6037,f6062,f6453,f6457,f6477,f6482,f6558,f6563,f6568,f6610,f6620,f6621,f6622,f6736,f6743,f6775,f6832]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV521+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n009.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:24:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 29.31/4.13 % Refutation found
% 29.31/4.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.31/4.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 29.31/4.18 % Elapsed time: 3.806322 seconds
% 29.31/4.18 % CPU time: 29.784731 seconds
% 29.31/4.18 % Total memory used: 257.925 MB
% 29.31/4.18 % Net memory used: 232.564 MB
%------------------------------------------------------------------------------