%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU170+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:19:31 PM UTC 2026
% Result : Theorem 61.81s 8.91s
% Output : CNFRefutation 61.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 62
% Syntax : Number of formulae : 356 ( 67 unt; 44 def)
% Number of atoms : 827 ( 112 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 827 ( 356 ~; 360 |; 47 &)
% ( 50 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 51 ( 49 usr; 45 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 367 ( 348 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( in(C,B)
=> in(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] : set_difference(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,conjecture,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,powerset(A))
=> ( disjoint(B,C)
<=> subset(B,subset_complement(A,C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,powerset(A))
=> ( disjoint(B,C)
<=> subset(B,subset_complement(A,C)) ) ) ),
inference(negated_conjecture,[status(cth)],[f23]) ).
fof(f25,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f30,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,B)
| ~ in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
( ! [A,B] :
( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f34,plain,
( ! [A,B] :
( ( ~ in(sK0_skl(B,A),B)
& in(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f33]) ).
fof(f35,plain,
! [X0,X1,X2] :
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f37,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ in(sK0_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f38,plain,
! [A,B,C] :
( ( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f39,plain,
( ! [A,B,C] :
( ? [D] :
( ( ( ~ in(D,B)
& in(D,A) )
| in(D,C) )
& ( in(D,B)
| ~ in(D,A)
| ~ in(D,C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
( ! [A,B,C] :
( ( ( ( ~ in(sK1_skl(C,B,A),B)
& in(sK1_skl(C,B,A),A) )
| in(sK1_skl(C,B,A),C) )
& ( in(sK1_skl(C,B,A),B)
| ~ in(sK1_skl(C,B,A),A)
| ~ in(sK1_skl(C,B,A),C) ) )
| C = set_difference(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ! [D] :
( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f39]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X2)
| ~ in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| ~ in(X3,X1)
| in(X3,X0)
| X0 != set_difference(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,plain,
! [X0,X1,X2] :
( set_difference(X2,X1) = X0
| in(sK1_skl(X0,X1,X2),X1)
| ~ in(sK1_skl(X0,X1,X2),X2)
| ~ in(sK1_skl(X0,X1,X2),X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f45,plain,
! [X0,X1,X2] :
( in(sK1_skl(X0,X1,X2),X0)
| X0 = set_difference(X2,X1)
| in(sK1_skl(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f47,plain,
! [A,B] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f48,plain,
! [X0,X1] :
( subset_complement(X1,X0) = set_difference(X1,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f50,plain,
! [X0,X1] :
( element(subset_complement(X1,X0),powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [A] : element(sK2_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B,sK2_skl(A))],[f10]) ).
fof(f52,plain,
! [X0] : element(sK2_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f55,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f56,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| X0 = subset_complement(X1,subset_complement(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [A,B] :
( ! [C] :
( in(C,A)
| ~ in(C,B) )
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f58,plain,
! [X0,X1,X2] :
( in(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f60,plain,
! [A] :
( ( ~ empty(sK3_skl(A))
& element(sK3_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B,sK3_skl(A))],[f59]) ).
fof(f61,plain,
! [X0] :
( element(sK3_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0] :
( ~ empty(sK3_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
empty(sK4_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f16]) ).
fof(f64,plain,
empty(sK4_skl),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f65,plain,
! [A] :
( empty(sK5_skl(A))
& element(sK5_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f17]) ).
fof(f66,plain,
! [X0] : element(sK5_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0] : empty(sK5_skl(X0)),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
~ empty(sK6_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f18]) ).
fof(f69,plain,
~ empty(sK6_skl),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f74,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f75,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f76,plain,
( ! [A,B] :
( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ! [A,B] :
( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f75]) ).
fof(f77,plain,
( ! [A,B] :
( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ! [A,B] :
( ( in(sK7_skl(B,A),B)
& in(sK7_skl(B,A),A) )
| disjoint(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B,A))],[f76]) ).
fof(f78,plain,
! [X0,X1] :
( disjoint(X1,X0)
| in(sK7_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( disjoint(X1,X0)
| in(sK7_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ disjoint(X2,X1)
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f81,plain,
? [A,B] :
( ? [C] :
( ( disjoint(B,C)
<~> subset(B,subset_complement(A,C)) )
& element(C,powerset(A)) )
& element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f82,plain,
? [A,B] :
( ? [C] :
( ( ~ subset(B,subset_complement(A,C))
| ~ disjoint(B,C) )
& ( subset(B,subset_complement(A,C))
| disjoint(B,C) )
& element(C,powerset(A)) )
& element(B,powerset(A)) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
( ( ~ subset(sK9_skl,subset_complement(sK8_skl,sK10_skl))
| ~ disjoint(sK9_skl,sK10_skl) )
& ( subset(sK9_skl,subset_complement(sK8_skl,sK10_skl))
| disjoint(sK9_skl,sK10_skl) )
& element(sK10_skl,powerset(sK8_skl))
& element(sK9_skl,powerset(sK8_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl]),skolemize(A,sK8_skl),skolemize(B,sK9_skl),skolemize(C,sK10_skl)],[f82]) ).
fof(f84,plain,
element(sK9_skl,powerset(sK8_skl)),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f85,plain,
element(sK10_skl,powerset(sK8_skl)),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f86,plain,
( subset(sK9_skl,subset_complement(sK8_skl,sK10_skl))
| disjoint(sK9_skl,sK10_skl) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f87,plain,
( ~ subset(sK9_skl,subset_complement(sK8_skl,sK10_skl))
| ~ disjoint(sK9_skl,sK10_skl) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,plain,
! [X0] : set_difference(empty_set,X0) = empty_set,
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f89,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f90,plain,
! [X0] :
( ~ empty(X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f91,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f92,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f97,definition,
( sQ0_spl
<=> disjoint(sK9_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f98,plain,
( ~ sQ0_spl
| disjoint(sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f97]) ).
fof(f99,plain,
( sQ0_spl
| ~ disjoint(sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f97]) ).
fof(f100,definition,
( sQ1_spl
<=> subset(sK9_skl,subset_complement(sK8_skl,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f101,plain,
( ~ sQ1_spl
| subset(sK9_skl,subset_complement(sK8_skl,sK10_skl)) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f102,plain,
( sQ1_spl
| ~ subset(sK9_skl,subset_complement(sK8_skl,sK10_skl)) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f103,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f86,f97,f100]) ).
fof(f104,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f87,f97,f100]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ in(X0,set_difference(X2,X1))
| ~ in(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f42]) ).
fof(f106,plain,
! [X0,X1,X2] :
( in(X0,set_difference(X1,X2))
| in(X0,X2)
| ~ in(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f43]) ).
fof(f107,plain,
! [X0,X1,X2] :
( in(X0,X1)
| ~ in(X0,set_difference(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f41]) ).
fof(f108,plain,
! [X0,X1,X2] :
( disjoint(set_difference(X1,X2),X0)
| ~ in(sK7_skl(X0,set_difference(X1,X2)),X2) ),
inference(resolution,[status(thm)],[f105,f78]) ).
fof(f109,plain,
! [X0,X1,X2,X3] :
( ~ in(X0,X2)
| ~ element(X2,powerset(set_difference(X3,X1)))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f105,f58]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( ~ subset(X2,set_difference(X3,X1))
| ~ in(X0,X2)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f105,f35]) ).
fof(f111,plain,
sK9_skl = subset_complement(sK8_skl,subset_complement(sK8_skl,sK9_skl)),
inference(resolution,[status(thm)],[f56,f84]) ).
fof(f112,plain,
sK10_skl = subset_complement(sK8_skl,subset_complement(sK8_skl,sK10_skl)),
inference(resolution,[status(thm)],[f56,f85]) ).
fof(f113,plain,
subset_complement(sK8_skl,sK9_skl) = set_difference(sK8_skl,sK9_skl),
inference(resolution,[status(thm)],[f48,f84]) ).
fof(f114,plain,
subset_complement(sK8_skl,sK10_skl) = set_difference(sK8_skl,sK10_skl),
inference(resolution,[status(thm)],[f48,f85]) ).
fof(f116,plain,
element(subset_complement(sK8_skl,sK9_skl),powerset(sK8_skl)),
inference(resolution,[status(thm)],[f50,f84]) ).
fof(f117,plain,
element(subset_complement(sK8_skl,sK10_skl),powerset(sK8_skl)),
inference(resolution,[status(thm)],[f50,f85]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( ~ in(X0,X3)
| ~ in(sK0_skl(set_difference(X2,X1),X3),set_difference(X2,X1))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f110,f37]) ).
fof(f123,plain,
subset_complement(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK10_skl,
inference(backward_demodulation,[status(thm)],[f114,f112]) ).
fof(f124,plain,
( ~ sQ1_spl
| subset(sK9_skl,set_difference(sK8_skl,sK10_skl)) ),
inference(backward_demodulation,[status(thm)],[f114,f101]) ).
fof(f125,plain,
! [X0] :
( ~ sQ1_spl
| ~ in(X0,sK10_skl)
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f124,f110]) ).
fof(f127,plain,
sK9_skl = subset_complement(sK8_skl,set_difference(sK8_skl,sK9_skl)),
inference(backward_demodulation,[status(thm)],[f113,f111]) ).
fof(f129,plain,
element(set_difference(sK8_skl,sK10_skl),powerset(sK8_skl)),
inference(forward_demodulation,[status(thm)],[f114,f117]) ).
fof(f131,plain,
subset_complement(sK8_skl,set_difference(sK8_skl,sK10_skl)) = set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)),
inference(resolution,[status(thm)],[f129,f48]) ).
fof(f133,plain,
element(set_difference(sK8_skl,sK9_skl),powerset(sK8_skl)),
inference(forward_demodulation,[status(thm)],[f113,f116]) ).
fof(f135,plain,
subset_complement(sK8_skl,set_difference(sK8_skl,sK9_skl)) = set_difference(sK8_skl,set_difference(sK8_skl,sK9_skl)),
inference(resolution,[status(thm)],[f133,f48]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ~ in(X0,sK2_skl(powerset(set_difference(X2,X1))))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f52,f109]) ).
fof(f145,plain,
! [X0] : element(subset_complement(X0,sK2_skl(powerset(X0))),powerset(X0)),
inference(resolution,[status(thm)],[f52,f50]) ).
fof(f146,plain,
! [X0] : set_difference(X0,sK2_skl(powerset(X0))) = subset_complement(X0,sK2_skl(powerset(X0))),
inference(resolution,[status(thm)],[f52,f48]) ).
fof(f147,plain,
! [X0] : subset_complement(X0,subset_complement(X0,sK2_skl(powerset(X0)))) = sK2_skl(powerset(X0)),
inference(resolution,[status(thm)],[f52,f56]) ).
fof(f148,plain,
! [X0] : empty_set = sK5_skl(X0),
inference(resolution,[status(thm)],[f90,f67]) ).
fof(f150,plain,
sK4_skl = empty_set,
inference(resolution,[status(thm)],[f90,f64]) ).
fof(f159,plain,
! [X0] :
( X0 = sK4_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f150,f90]) ).
fof(f161,plain,
! [X0] : X0 = set_difference(X0,sK4_skl),
inference(backward_demodulation,[status(thm)],[f150,f74]) ).
fof(f165,plain,
! [X0] : sK4_skl = sK5_skl(X0),
inference(forward_demodulation,[status(thm)],[f150,f148]) ).
fof(f168,plain,
! [X0] : subset_complement(X0,subset_complement(X0,sK2_skl(powerset(X0)))) = set_difference(X0,subset_complement(X0,sK2_skl(powerset(X0)))),
inference(resolution,[status(thm)],[f145,f48]) ).
fof(f170,plain,
! [X0] : element(sK4_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f165,f66]) ).
fof(f172,plain,
! [X0] : element(subset_complement(X0,sK4_skl),powerset(X0)),
inference(resolution,[status(thm)],[f170,f50]) ).
fof(f173,plain,
! [X0] : subset_complement(X0,sK4_skl) = set_difference(X0,sK4_skl),
inference(resolution,[status(thm)],[f170,f48]) ).
fof(f174,plain,
! [X0] : subset_complement(X0,subset_complement(X0,sK4_skl)) = sK4_skl,
inference(resolution,[status(thm)],[f170,f56]) ).
fof(f182,plain,
! [X0] : subset_complement(X0,set_difference(X0,sK2_skl(powerset(X0)))) = sK2_skl(powerset(X0)),
inference(backward_demodulation,[status(thm)],[f146,f147]) ).
fof(f184,plain,
! [X0,X1,X2,X3] :
( ~ in(X3,X1)
| ~ in(X3,X2)
| in(sK0_skl(set_difference(X0,X1),X2),X2) ),
inference(resolution,[status(thm)],[f36,f110]) ).
fof(f196,plain,
! [X0] : set_difference(sK4_skl,X0) = empty_set,
inference(forward_demodulation,[status(thm)],[f150,f88]) ).
fof(f197,plain,
! [X0] : sK4_skl = set_difference(sK4_skl,X0),
inference(forward_demodulation,[status(thm)],[f150,f196]) ).
fof(f207,plain,
( sQ0_spl
| in(sK7_skl(sK10_skl,sK9_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f79,f99]) ).
fof(f208,plain,
! [X0,X1,X2] :
( ~ in(X0,X2)
| in(sK7_skl(X1,X2),X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f79,f80]) ).
fof(f210,plain,
element(sK3_skl(sK6_skl),powerset(sK6_skl)),
inference(resolution,[status(thm)],[f61,f69]) ).
fof(f212,plain,
( ~ sQ1_spl
| sQ0_spl
| ~ in(sK7_skl(sK10_skl,sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f207,f125]) ).
fof(f218,plain,
! [X0,X1,X2] :
( ~ in(X1,X0)
| ~ in(X0,set_difference(X1,X2)) ),
inference(resolution,[status(thm)],[f30,f107]) ).
fof(f222,plain,
! [X0] :
( X0 = sK4_skl
| element(sK3_skl(X0),powerset(X0)) ),
inference(resolution,[status(thm)],[f159,f61]) ).
fof(f229,plain,
! [X0] : ~ in(X0,sK4_skl),
inference(resolution,[status(thm)],[f93,f64]) ).
fof(f230,plain,
! [X0,X1] :
( element(sK3_skl(X1),powerset(X1))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f93,f61]) ).
fof(f231,plain,
set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK10_skl,
inference(forward_demodulation,[status(thm)],[f123,f131]) ).
fof(f232,plain,
! [X0,X1] :
( ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ element(X1,powerset(sK10_skl))
| ~ in(X0,X1) ),
inference(paramodulation,[status(thm)],[f231,f109]) ).
fof(f236,plain,
( ~ sQ1_spl
| sQ0_spl
| disjoint(sK9_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f212,f78]) ).
fof(f240,plain,
( ~ sQ1_spl
| sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f236,f99]) ).
fof(f241,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f240]) ).
fof(f242,plain,
( sQ1_spl
| ~ subset(sK9_skl,set_difference(sK8_skl,sK10_skl)) ),
inference(forward_demodulation,[status(thm)],[f114,f102]) ).
fof(f246,plain,
! [X0,X1] :
( in(sK1_skl(X0,X1,sK4_skl),X0)
| X0 = set_difference(sK4_skl,X1) ),
inference(resolution,[status(thm)],[f229,f45]) ).
fof(f250,plain,
! [X0,X1] :
( ~ subset(X1,sK4_skl)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f229,f35]) ).
fof(f253,plain,
! [X0,X1] :
( X0 = sK4_skl
| in(sK1_skl(X0,X1,sK4_skl),X0) ),
inference(forward_demodulation,[status(thm)],[f197,f246]) ).
fof(f256,plain,
! [X0] :
( ~ sQ0_spl
| ~ in(X0,sK10_skl)
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f98,f80]) ).
fof(f264,plain,
( sQ1_spl
| in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f242,f36]) ).
fof(f265,plain,
( sQ1_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),set_difference(sK8_skl,sK10_skl)) ),
inference(resolution,[status(thm)],[f242,f37]) ).
fof(f270,plain,
! [X0,X1] :
( in(sK0_skl(sK4_skl,X1),X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f250,f36]) ).
fof(f277,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ in(X0,set_difference(sK10_skl,X1))
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f256,f107]) ).
fof(f281,plain,
! [X0,X1,X2,X3] :
( ~ in(sK7_skl(X1,set_difference(X2,X3)),X3)
| ~ in(X0,set_difference(X2,X3))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f108,f80]) ).
fof(f289,plain,
! [X0] : subset_complement(X0,X0) = sK4_skl,
inference(backward_demodulation,[status(thm)],[f291,f174]) ).
fof(f290,plain,
! [X0] : element(X0,powerset(X0)),
inference(backward_demodulation,[status(thm)],[f291,f172]) ).
fof(f291,plain,
! [X0] : subset_complement(X0,sK4_skl) = X0,
inference(forward_demodulation,[status(thm)],[f161,f173]) ).
fof(f296,plain,
! [X0] : subset_complement(X0,X0) = set_difference(X0,X0),
inference(resolution,[status(thm)],[f290,f48]) ).
fof(f300,plain,
! [X0] : sK4_skl = set_difference(X0,X0),
inference(forward_demodulation,[status(thm)],[f289,f296]) ).
fof(f367,plain,
( sQ1_spl
| in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK10_skl)
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK8_skl) ),
inference(resolution,[status(thm)],[f265,f106]) ).
fof(f369,plain,
! [X0] :
( sQ1_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0)
| ~ element(X0,powerset(set_difference(sK8_skl,sK10_skl))) ),
inference(resolution,[status(thm)],[f265,f58]) ).
fof(f371,definition,
( sQ2_spl
<=> in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( sQ2_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK8_skl) ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f374,definition,
( sQ3_spl
<=> in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( sQ1_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f367,f371,f374,f100]) ).
fof(f379,plain,
set_difference(sK6_skl,sK3_skl(sK6_skl)) = subset_complement(sK6_skl,sK3_skl(sK6_skl)),
inference(resolution,[status(thm)],[f210,f48]) ).
fof(f415,plain,
! [X0,X1,X2,X3] :
( ~ in(X1,set_difference(X0,X3))
| ~ in(X0,set_difference(X1,X2)) ),
inference(resolution,[status(thm)],[f218,f107]) ).
fof(f423,plain,
! [X0] :
( X0 = sK4_skl
| element(subset_complement(X0,sK3_skl(X0)),powerset(X0)) ),
inference(resolution,[status(thm)],[f222,f50]) ).
fof(f424,plain,
! [X0] :
( X0 = sK4_skl
| set_difference(X0,sK3_skl(X0)) = subset_complement(X0,sK3_skl(X0)) ),
inference(resolution,[status(thm)],[f222,f48]) ).
fof(f425,plain,
! [X0] :
( subset_complement(X0,subset_complement(X0,sK3_skl(X0))) = sK3_skl(X0)
| X0 = sK4_skl ),
inference(resolution,[status(thm)],[f222,f56]) ).
fof(f443,plain,
! [X0,X1] :
( ~ in(X1,X0)
| element(subset_complement(X0,sK3_skl(X0)),powerset(X0)) ),
inference(resolution,[status(thm)],[f230,f50]) ).
fof(f451,plain,
sK9_skl = set_difference(sK8_skl,set_difference(sK8_skl,sK9_skl)),
inference(forward_demodulation,[status(thm)],[f127,f135]) ).
fof(f534,plain,
! [X0] :
( sQ1_spl
| ~ sQ0_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),set_difference(sK10_skl,X0)) ),
inference(resolution,[status(thm)],[f277,f264]) ).
fof(f560,definition,
! [X0] :
( sQ7_spl
<=> ~ in(X0,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f561,plain,
! [X0] :
( ~ sQ7_spl
| ~ in(X0,sK10_skl) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f594,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ element(X1,powerset(sK10_skl))
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f561,f58]) ).
fof(f669,plain,
! [X0] :
( ~ sQ7_spl
| sK10_skl = sK4_skl
| ~ in(X0,sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f594,f222]) ).
fof(f674,definition,
! [X0] :
( sQ11_spl
<=> ~ in(X0,sK3_skl(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f675,plain,
! [X0] :
( ~ sQ11_spl
| ~ in(X0,sK3_skl(sK10_skl)) ),
inference(component_clause,[status(thm)],[f674]) ).
fof(f678,definition,
( sQ12_spl
<=> sK10_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ12_spl
| sK4_skl = sK10_skl ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f680,plain,
( sQ12_spl
| sK4_skl != sK10_skl ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f681,plain,
( ~ sQ7_spl
| sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f669,f674,f678,f560]) ).
fof(f703,plain,
! [X0] :
( ~ sQ12_spl
| ~ in(X0,sK10_skl) ),
inference(backward_demodulation,[status(thm)],[f679,f229]) ).
fof(f859,plain,
! [X0] : subset_complement(X0,set_difference(X0,sK2_skl(powerset(X0)))) = set_difference(X0,subset_complement(X0,sK2_skl(powerset(X0)))),
inference(forward_demodulation,[status(thm)],[f146,f168]) ).
fof(f860,plain,
! [X0] : sK2_skl(powerset(X0)) = set_difference(X0,subset_complement(X0,sK2_skl(powerset(X0)))),
inference(forward_demodulation,[status(thm)],[f182,f859]) ).
fof(f861,plain,
! [X0] : sK2_skl(powerset(X0)) = set_difference(X0,set_difference(X0,sK2_skl(powerset(X0)))),
inference(forward_demodulation,[status(thm)],[f146,f860]) ).
fof(f927,definition,
! [X0,X1] :
( sQ13_spl
<=> ( ~ in(X0,sK3_skl(sK10_skl))
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f928,plain,
! [X0,X1] :
( ~ sQ13_spl
| ~ in(X0,X1)
| ~ in(X0,sK3_skl(sK10_skl)) ),
inference(component_clause,[status(thm)],[f927]) ).
fof(f1059,plain,
! [X0] :
( set_difference(X0,sK3_skl(X0)) = subset_complement(X0,sK3_skl(X0))
| X0 = sK4_skl ),
inference(resolution,[status(thm)],[f222,f48]) ).
fof(f1175,plain,
( ~ sQ11_spl
| sK3_skl(sK10_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f253,f675]) ).
fof(f1178,plain,
( ~ sQ7_spl
| sK10_skl = sK4_skl ),
inference(resolution,[status(thm)],[f253,f561]) ).
fof(f1180,plain,
! [X0,X1,X2] :
( set_difference(X0,X1) = sK4_skl
| ~ in(sK1_skl(set_difference(X0,X1),X2,sK4_skl),X1) ),
inference(resolution,[status(thm)],[f253,f105]) ).
fof(f1181,plain,
! [X0,X1,X2,X3] :
( sK4_skl = X0
| in(sK0_skl(set_difference(X3,X2),X0),X0)
| ~ in(sK1_skl(X0,X1,sK4_skl),X2) ),
inference(resolution,[status(thm)],[f253,f184]) ).
fof(f1183,plain,
! [X0,X1,X2,X3] :
( ~ in(sK1_skl(X0,X3,sK4_skl),X2)
| ~ in(sK0_skl(set_difference(X1,X2),X0),set_difference(X1,X2))
| X0 = sK4_skl ),
inference(resolution,[status(thm)],[f253,f120]) ).
fof(f1206,plain,
! [X0] :
( ~ sQ7_spl
| X0 = set_difference(X0,sK10_skl) ),
inference(backward_demodulation,[status(thm)],[f1178,f161]) ).
fof(f1223,plain,
( sQ1_spl
| ~ sQ7_spl
| in(sK0_skl(sK8_skl,sK9_skl),sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f1206,f264]) ).
fof(f1296,definition,
( sQ16_spl
<=> empty(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1297,plain,
( ~ sQ16_spl
| empty(sK10_skl) ),
inference(component_clause,[status(thm)],[f1296]) ).
fof(f1298,plain,
( sQ16_spl
| ~ empty(sK10_skl) ),
inference(component_clause,[status(thm)],[f1296]) ).
fof(f1438,plain,
! [X0,X1] :
( ~ in(sK7_skl(X1,sK9_skl),set_difference(sK8_skl,sK9_skl))
| ~ in(X0,set_difference(sK8_skl,set_difference(sK8_skl,sK9_skl)))
| ~ in(X0,X1) ),
inference(paramodulation,[status(thm)],[f451,f281]) ).
fof(f1442,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ in(sK7_skl(X1,sK9_skl),set_difference(sK8_skl,sK9_skl))
| ~ in(X0,sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f451,f1438]) ).
fof(f1630,plain,
! [X0] :
( sQ1_spl
| ~ sQ7_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0)
| ~ element(X0,powerset(sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f1206,f369]) ).
fof(f1631,plain,
! [X0] :
( sQ1_spl
| ~ sQ7_spl
| ~ in(sK0_skl(sK8_skl,sK9_skl),X0)
| ~ element(X0,powerset(sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f1206,f1630]) ).
fof(f1632,plain,
( sQ1_spl
| ~ sQ7_spl
| ~ element(sK9_skl,powerset(sK8_skl)) ),
inference(resolution,[status(thm)],[f1631,f1223]) ).
fof(f1637,plain,
( sQ1_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f84]) ).
fof(f1638,plain,
( sQ1_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f1637]) ).
fof(f1847,definition,
! [X0] :
( sQ21_spl
<=> in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1848,plain,
! [X0] :
( ~ sQ21_spl
| in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0) ),
inference(component_clause,[status(thm)],[f1847]) ).
fof(f1852,plain,
! [X0] :
( sQ2_spl
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0)
| ~ element(X0,powerset(sK8_skl)) ),
inference(resolution,[status(thm)],[f373,f58]) ).
fof(f1979,plain,
! [X0,X1] :
( ~ sQ13_spl
| ~ in(sK1_skl(sK3_skl(sK10_skl),X0,sK4_skl),X1)
| sK3_skl(sK10_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f253,f928]) ).
fof(f1980,plain,
! [X0] :
( ~ sQ0_spl
| ~ in(sK1_skl(sK10_skl,X0,sK4_skl),sK9_skl)
| sK10_skl = sK4_skl ),
inference(resolution,[status(thm)],[f253,f256]) ).
fof(f1990,definition,
( sQ22_spl
<=> sK3_skl(sK10_skl) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1991,plain,
( ~ sQ22_spl
| sK4_skl = sK3_skl(sK10_skl) ),
inference(component_clause,[status(thm)],[f1990]) ).
fof(f1992,plain,
( sQ22_spl
| sK3_skl(sK10_skl) != sK4_skl ),
inference(component_clause,[status(thm)],[f1990]) ).
fof(f1993,definition,
! [X0,X1] :
( sQ23_spl
<=> ~ in(sK1_skl(sK3_skl(sK10_skl),X0,sK4_skl),X1) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1994,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ in(sK1_skl(sK3_skl(sK10_skl),X0,sK4_skl),X1) ),
inference(component_clause,[status(thm)],[f1993]) ).
fof(f1996,plain,
( ~ sQ13_spl
| sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f1979,f1990,f1993,f927]) ).
fof(f2008,definition,
! [X0] :
( sQ26_spl
<=> ~ in(sK1_skl(sK10_skl,X0,sK4_skl),sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f2009,plain,
! [X0] :
( ~ sQ26_spl
| ~ in(sK1_skl(sK10_skl,X0,sK4_skl),sK9_skl) ),
inference(component_clause,[status(thm)],[f2008]) ).
fof(f2011,plain,
( ~ sQ0_spl
| sQ26_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f1980,f678,f2008,f97]) ).
fof(f2017,plain,
( ~ sQ22_spl
| ~ empty(sK4_skl)
| empty(sK10_skl) ),
inference(paramodulation,[status(thm)],[f1991,f62]) ).
fof(f2031,definition,
( sQ30_spl
<=> empty(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f2033,plain,
( sQ30_spl
| ~ empty(sK4_skl) ),
inference(component_clause,[status(thm)],[f2031]) ).
fof(f2034,plain,
( ~ sQ22_spl
| ~ sQ30_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f2017,f1296,f2031,f1990]) ).
fof(f2036,plain,
( ~ sQ12_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f703,f560,f678]) ).
fof(f2058,plain,
( ~ sQ26_spl
| set_difference(sK4_skl,sK9_skl) = sK10_skl
| ~ in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK4_skl)
| ~ in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f2009,f44]) ).
fof(f2062,definition,
( sQ31_spl
<=> in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f2063,plain,
( ~ sQ31_spl
| in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK10_skl) ),
inference(component_clause,[status(thm)],[f2062]) ).
fof(f2064,plain,
( sQ31_spl
| ~ in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK10_skl) ),
inference(component_clause,[status(thm)],[f2062]) ).
fof(f2065,definition,
( sQ32_spl
<=> in(sK1_skl(sK10_skl,sK9_skl,sK4_skl),sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f2068,definition,
( sQ33_spl
<=> set_difference(sK4_skl,sK9_skl) = sK10_skl ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f2069,plain,
( ~ sQ33_spl
| set_difference(sK4_skl,sK9_skl) = sK10_skl ),
inference(component_clause,[status(thm)],[f2068]) ).
fof(f2071,plain,
( ~ sQ26_spl
| sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2058,f2062,f2065,f2068,f2008]) ).
fof(f2072,plain,
( ~ sQ33_spl
| sK4_skl = sK10_skl ),
inference(forward_demodulation,[status(thm)],[f197,f2069]) ).
fof(f2073,plain,
( ~ sQ33_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2072,f680]) ).
fof(f2074,plain,
( ~ sQ33_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f2073]) ).
fof(f2237,plain,
( ~ sQ23_spl
| sK3_skl(sK10_skl) = sK4_skl ),
inference(resolution,[status(thm)],[f1994,f253]) ).
fof(f2248,plain,
( ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f2237,f1990,f1993]) ).
fof(f2252,plain,
! [X0] :
( ~ sQ16_spl
| ~ in(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f1297,f93]) ).
fof(f2253,plain,
( ~ sQ16_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f2252,f560,f1296]) ).
fof(f2255,plain,
( sQ16_spl
| element(sK3_skl(sK10_skl),powerset(sK10_skl)) ),
inference(resolution,[status(thm)],[f1298,f61]) ).
fof(f2285,plain,
( sQ16_spl
| element(subset_complement(sK10_skl,sK3_skl(sK10_skl)),powerset(sK10_skl)) ),
inference(resolution,[status(thm)],[f2255,f50]) ).
fof(f2307,plain,
( sQ31_spl
| sK10_skl = sK4_skl ),
inference(resolution,[status(thm)],[f2064,f253]) ).
fof(f2316,plain,
( sQ31_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f2307,f678,f2062]) ).
fof(f2529,plain,
! [X0,X1] :
( ~ in(sK8_skl,set_difference(X0,X1))
| ~ in(X0,sK10_skl) ),
inference(paramodulation,[status(thm)],[f231,f415]) ).
fof(f2530,plain,
! [X0,X1] :
( ~ in(X0,sK9_skl)
| ~ in(sK8_skl,set_difference(X0,X1)) ),
inference(paramodulation,[status(thm)],[f451,f415]) ).
fof(f2537,plain,
( sQ1_spl
| ~ sQ21_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f265,f1848]) ).
fof(f2566,plain,
( sQ1_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f2537]) ).
fof(f2567,plain,
! [X0,X1] :
( in(sK8_skl,X1)
| ~ in(sK8_skl,X0)
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f2530,f106]) ).
fof(f2573,plain,
( ~ in(sK8_skl,sK9_skl)
| ~ in(sK8_skl,sK9_skl) ),
inference(paramodulation,[status(thm)],[f451,f2530]) ).
fof(f2577,definition,
( sQ45_spl
<=> in(sK8_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f2579,plain,
( sQ45_spl
| ~ in(sK8_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f2577]) ).
fof(f2580,plain,
~ sQ45_spl,
inference(split_clause,[status(thm)],[f2573,f2577]) ).
fof(f2581,definition,
( sQ46_spl
<=> in(sK8_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2585,definition,
! [X0] :
( sQ47_spl
<=> ( ~ in(sK8_skl,X0)
| ~ in(X0,sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f2588,definition,
! [X1] :
( sQ48_spl
<=> in(sK8_skl,X1) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2589,plain,
! [X0] :
( ~ sQ48_spl
| in(sK8_skl,X0) ),
inference(component_clause,[status(thm)],[f2588]) ).
fof(f2591,plain,
( sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f2567,f2585,f2588]) ).
fof(f2596,definition,
( sQ50_spl
<=> in(sK8_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f2598,plain,
( sQ50_spl
| ~ in(sK8_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f2596]) ).
fof(f2630,plain,
! [X0] :
( sQ45_spl
| ~ in(sK8_skl,set_difference(sK9_skl,X0)) ),
inference(resolution,[status(thm)],[f2579,f107]) ).
fof(f2634,plain,
! [X0,X1] :
( sQ45_spl
| ~ in(sK8_skl,set_difference(set_difference(sK9_skl,X0),X1)) ),
inference(resolution,[status(thm)],[f2630,f107]) ).
fof(f2638,plain,
( sQ45_spl
| ~ in(sK8_skl,sK2_skl(powerset(sK9_skl))) ),
inference(paramodulation,[status(thm)],[f861,f2630]) ).
fof(f2662,plain,
! [X0] :
( sQ45_spl
| ~ in(sK8_skl,set_difference(sK2_skl(powerset(sK9_skl)),X0)) ),
inference(resolution,[status(thm)],[f2638,f107]) ).
fof(f2669,plain,
! [X0,X1] :
( sQ45_spl
| in(sK8_skl,X1)
| ~ in(sK8_skl,set_difference(sK9_skl,X0)) ),
inference(resolution,[status(thm)],[f2634,f106]) ).
fof(f2680,definition,
! [X0] :
( sQ51_spl
<=> ~ in(sK8_skl,set_difference(sK9_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2683,plain,
( sQ45_spl
| sQ48_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f2669,f2680,f2588,f2577]) ).
fof(f2716,plain,
! [X0,X1] :
( ~ sQ48_spl
| ~ in(sK8_skl,sK2_skl(powerset(set_difference(X0,X1)))) ),
inference(resolution,[status(thm)],[f2589,f144]) ).
fof(f2723,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2716,f2589]) ).
fof(f2724,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f2723]) ).
fof(f3130,plain,
( sK4_skl = sK6_skl
| sK3_skl(sK6_skl) = subset_complement(sK6_skl,set_difference(sK6_skl,sK3_skl(sK6_skl))) ),
inference(paramodulation,[status(thm)],[f379,f425]) ).
fof(f3131,definition,
( sQ55_spl
<=> sK3_skl(sK6_skl) = subset_complement(sK6_skl,set_difference(sK6_skl,sK3_skl(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f3134,definition,
( sQ56_spl
<=> sK4_skl = sK6_skl ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f3135,plain,
( ~ sQ56_spl
| sK6_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f3134]) ).
fof(f3137,plain,
( sQ56_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f3130,f3131,f3134]) ).
fof(f3149,plain,
( sK6_skl = sK4_skl
| set_difference(sK6_skl,sK3_skl(sK6_skl)) = set_difference(sK6_skl,sK3_skl(sK6_skl)) ),
inference(paramodulation,[status(thm)],[f424,f379]) ).
fof(f3152,definition,
( sQ57_spl
<=> set_difference(sK6_skl,sK3_skl(sK6_skl)) = set_difference(sK6_skl,sK3_skl(sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f3155,plain,
( sQ56_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f3149,f3152,f3134]) ).
fof(f3163,plain,
( sK4_skl = sK6_skl
| element(set_difference(sK6_skl,sK3_skl(sK6_skl)),powerset(sK6_skl)) ),
inference(paramodulation,[status(thm)],[f379,f423]) ).
fof(f3164,plain,
! [X0] :
( X0 = sK4_skl
| sK4_skl = X0
| element(set_difference(X0,sK3_skl(X0)),powerset(X0)) ),
inference(paramodulation,[status(thm)],[f424,f423]) ).
fof(f3165,definition,
( sQ58_spl
<=> element(set_difference(sK6_skl,sK3_skl(sK6_skl)),powerset(sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3168,plain,
( sQ56_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f3163,f3165,f3134]) ).
fof(f3169,plain,
! [X0] :
( sK4_skl = X0
| element(set_difference(X0,sK3_skl(X0)),powerset(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f3164]) ).
fof(f3186,plain,
( ~ sQ56_spl
| empty(sK6_skl) ),
inference(backward_demodulation,[status(thm)],[f3135,f64]) ).
fof(f3192,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3186,f69]) ).
fof(f3193,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f3192]) ).
fof(f3959,plain,
( ~ sQ31_spl
| in(sK0_skl(sK4_skl,sK10_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f2063,f270]) ).
fof(f4015,plain,
! [X0] :
( ~ sQ31_spl
| ~ in(sK10_skl,set_difference(sK0_skl(sK4_skl,sK10_skl),X0)) ),
inference(resolution,[status(thm)],[f3959,f218]) ).
fof(f4263,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2033,f64]) ).
fof(f4264,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f4263]) ).
fof(f4265,plain,
( ~ sQ11_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f1175,f1990,f674]) ).
fof(f4273,plain,
! [X0,X1] :
( in(sK8_skl,X1)
| ~ in(sK8_skl,X0)
| ~ in(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f2529,f106]) ).
fof(f4278,plain,
( ~ in(sK8_skl,sK10_skl)
| ~ in(sK8_skl,sK10_skl) ),
inference(paramodulation,[status(thm)],[f231,f2529]) ).
fof(f4282,plain,
! [X0] :
( ~ in(sK8_skl,sK4_skl)
| ~ in(X0,sK10_skl) ),
inference(paramodulation,[status(thm)],[f300,f2529]) ).
fof(f4283,plain,
( ~ sQ46_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f4282,f560,f2581]) ).
fof(f4285,plain,
~ sQ50_spl,
inference(split_clause,[status(thm)],[f4278,f2596]) ).
fof(f4290,definition,
! [X0] :
( sQ72_spl
<=> ( ~ in(sK8_skl,X0)
| ~ in(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f4293,plain,
( sQ48_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f4273,f4290,f2588]) ).
fof(f4294,plain,
! [X0] :
( sQ50_spl
| ~ in(sK8_skl,set_difference(sK10_skl,X0)) ),
inference(resolution,[status(thm)],[f2598,f107]) ).
fof(f4298,plain,
! [X0,X1] :
( sQ50_spl
| ~ in(sK8_skl,set_difference(set_difference(sK10_skl,X0),X1)) ),
inference(resolution,[status(thm)],[f4294,f107]) ).
fof(f4302,plain,
( sQ50_spl
| ~ in(sK8_skl,sK2_skl(powerset(sK10_skl))) ),
inference(paramodulation,[status(thm)],[f861,f4294]) ).
fof(f4315,plain,
! [X0] :
( sQ50_spl
| ~ in(sK8_skl,set_difference(sK2_skl(powerset(sK10_skl)),X0)) ),
inference(resolution,[status(thm)],[f4302,f107]) ).
fof(f4322,plain,
! [X0,X1] :
( sQ50_spl
| in(sK8_skl,X1)
| ~ in(sK8_skl,set_difference(sK10_skl,X0)) ),
inference(resolution,[status(thm)],[f4298,f106]) ).
fof(f4333,definition,
! [X0] :
( sQ73_spl
<=> ~ in(sK8_skl,set_difference(sK10_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f4336,plain,
( sQ50_spl
| sQ48_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f4322,f4333,f2588,f2596]) ).
fof(f4345,plain,
! [X0] :
( sQ45_spl
| in(sK8_skl,X0)
| ~ in(sK8_skl,sK2_skl(powerset(sK9_skl))) ),
inference(resolution,[status(thm)],[f2662,f106]) ).
fof(f4352,definition,
( sQ74_spl
<=> in(sK8_skl,sK2_skl(powerset(sK9_skl))) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f4355,plain,
( sQ45_spl
| sQ48_spl
| ~ sQ74_spl ),
inference(split_clause,[status(thm)],[f4345,f4352,f2588,f2577]) ).
fof(f4398,plain,
! [X0,X1] :
( ~ in(X1,sK10_skl)
| ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,subset_complement(sK10_skl,sK3_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f232,f443]) ).
fof(f4403,plain,
! [X0,X1] :
( ~ in(X1,sK10_skl)
| ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f232,f230]) ).
fof(f4407,definition,
! [X0] :
( sQ75_spl
<=> ( ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,subset_complement(sK10_skl,sK3_skl(sK10_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f4410,plain,
( sQ7_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f4398,f4407,f560]) ).
fof(f4411,definition,
! [X0] :
( sQ76_spl
<=> ( ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,sK3_skl(sK10_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f4414,plain,
( sQ7_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f4403,f4411,f560]) ).
fof(f4514,plain,
! [X0] :
( ~ sQ31_spl
| in(sK10_skl,X0)
| ~ in(sK10_skl,sK0_skl(sK4_skl,sK10_skl)) ),
inference(resolution,[status(thm)],[f4015,f106]) ).
fof(f4521,definition,
( sQ78_spl
<=> in(sK10_skl,sK0_skl(sK4_skl,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f4524,definition,
! [X0] :
( sQ79_spl
<=> in(sK10_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f4527,plain,
( ~ sQ31_spl
| sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f4514,f4521,f4524,f2062]) ).
fof(f4542,definition,
( sQ82_spl
<=> set_difference(sK4_skl,sK9_skl) = sK3_skl(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f4543,plain,
( ~ sQ82_spl
| set_difference(sK4_skl,sK9_skl) = sK3_skl(sK10_skl) ),
inference(component_clause,[status(thm)],[f4542]) ).
fof(f4546,plain,
( ~ sQ82_spl
| sK4_skl = sK3_skl(sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f197,f4543]) ).
fof(f4547,plain,
( ~ sQ82_spl
| sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4546,f1992]) ).
fof(f4548,plain,
( ~ sQ82_spl
| sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f4547]) ).
fof(f4559,plain,
! [X0] :
( sQ50_spl
| in(sK8_skl,X0)
| ~ in(sK8_skl,sK2_skl(powerset(sK10_skl))) ),
inference(resolution,[status(thm)],[f4315,f106]) ).
fof(f4566,definition,
( sQ83_spl
<=> in(sK8_skl,sK2_skl(powerset(sK10_skl))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f4569,plain,
( sQ50_spl
| sQ48_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f4559,f4566,f2588,f2596]) ).
fof(f4597,plain,
( sQ16_spl
| sK10_skl = sK4_skl
| element(set_difference(sK10_skl,sK3_skl(sK10_skl)),powerset(sK10_skl)) ),
inference(paramodulation,[status(thm)],[f1059,f2285]) ).
fof(f4598,definition,
( sQ84_spl
<=> element(set_difference(sK10_skl,sK3_skl(sK10_skl)),powerset(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f4601,plain,
( sQ16_spl
| sQ12_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f4597,f4598,f678,f1296]) ).
fof(f4837,plain,
! [X0] :
( ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,set_difference(sK10_skl,sK3_skl(sK10_skl)))
| sK4_skl = sK10_skl ),
inference(resolution,[status(thm)],[f3169,f232]) ).
fof(f4858,definition,
! [X0] :
( sQ92_spl
<=> ( ~ in(X0,set_difference(sK8_skl,sK10_skl))
| ~ in(X0,set_difference(sK10_skl,sK3_skl(sK10_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f4861,plain,
( sQ92_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f4837,f678,f4858]) ).
fof(f4960,plain,
! [X0] :
( sQ1_spl
| ~ sQ0_spl
| in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),X0)
| ~ in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f534,f106]) ).
fof(f4967,plain,
( sQ1_spl
| ~ sQ0_spl
| sQ21_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f4960,f374,f1847,f97,f100]) ).
fof(f5492,plain,
( sQ1_spl
| in(sK0_skl(set_difference(sK8_skl,sK10_skl),sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f242,f36]) ).
fof(f5684,plain,
subset_complement(sK8_skl,set_difference(sK8_skl,sK10_skl)) = set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)),
inference(resolution,[status(thm)],[f129,f48]) ).
fof(f6567,plain,
set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK10_skl,
inference(forward_demodulation,[status(thm)],[f123,f5684]) ).
fof(f8297,plain,
! [X0,X1] :
( ~ in(X1,sK9_skl)
| ~ in(X1,set_difference(sK8_skl,sK9_skl))
| ~ in(X0,set_difference(sK8_skl,sK9_skl))
| ~ in(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f1442,f208]) ).
fof(f8302,definition,
! [X0] :
( sQ213_spl
<=> ( ~ in(X0,set_difference(sK8_skl,sK9_skl))
| ~ in(X0,sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f8305,plain,
sQ213_spl,
inference(split_clause,[status(thm)],[f8297,f8302]) ).
fof(f8324,plain,
! [X0] :
( ~ sQ31_spl
| sK4_skl = sK10_skl
| in(sK0_skl(set_difference(X0,sK10_skl),sK10_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f1181,f2063]) ).
fof(f8335,definition,
! [X0] :
( sQ214_spl
<=> in(sK0_skl(set_difference(X0,sK10_skl),sK10_skl),sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f8338,plain,
( ~ sQ31_spl
| sQ12_spl
| sQ214_spl ),
inference(split_clause,[status(thm)],[f8324,f8335,f678,f2062]) ).
fof(f8422,plain,
! [X0] :
( ~ sQ31_spl
| ~ in(sK0_skl(set_difference(X0,sK10_skl),sK10_skl),set_difference(X0,sK10_skl))
| sK10_skl = sK4_skl ),
inference(resolution,[status(thm)],[f1183,f2063]) ).
fof(f8435,definition,
! [X0] :
( sQ219_spl
<=> ~ in(sK0_skl(set_difference(X0,sK10_skl),sK10_skl),set_difference(X0,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f8438,plain,
( ~ sQ31_spl
| sQ219_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f8422,f678,f8435,f2062]) ).
fof(f8628,plain,
! [X0] :
( set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK4_skl
| ~ in(sK1_skl(sK10_skl,X0,sK4_skl),set_difference(sK8_skl,sK10_skl)) ),
inference(paramodulation,[status(thm)],[f6567,f1180]) ).
fof(f8643,definition,
! [X0] :
( sQ230_spl
<=> ~ in(sK1_skl(sK10_skl,X0,sK4_skl),set_difference(sK8_skl,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f8646,definition,
( sQ231_spl
<=> set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f8647,plain,
( ~ sQ231_spl
| set_difference(sK8_skl,set_difference(sK8_skl,sK10_skl)) = sK4_skl ),
inference(component_clause,[status(thm)],[f8646]) ).
fof(f8649,plain,
( sQ231_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f8628,f8643,f8646]) ).
fof(f8661,plain,
( ~ sQ231_spl
| sK10_skl = sK4_skl ),
inference(forward_demodulation,[status(thm)],[f6567,f8647]) ).
fof(f8662,plain,
( ~ sQ231_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8661,f680]) ).
fof(f8663,plain,
( ~ sQ231_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f8662]) ).
fof(f9743,definition,
( sQ271_spl
<=> in(sK9_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f9744,plain,
( ~ sQ271_spl
| in(sK9_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f9743]) ).
fof(f10162,plain,
( ~ sQ271_spl
| ~ in(sK9_skl,sK9_skl) ),
inference(resolution,[status(thm)],[f9744,f30]) ).
fof(f10164,plain,
~ sQ271_spl,
inference(split_clause,[status(thm)],[f10162,f9743]) ).
fof(f10281,plain,
( sQ1_spl
| sQ2_spl
| ~ element(sK9_skl,powerset(sK8_skl)) ),
inference(resolution,[status(thm)],[f1852,f5492]) ).
fof(f10286,plain,
( sQ1_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10281,f84]) ).
fof(f10287,plain,
( sQ1_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f10286]) ).
fof(f10288,plain,
$false,
inference(sat_refutation,[status(thm)],[f103,f104,f241,f377,f681,f1638,f1996,f2011,f2034,f2036,f2071,f2074,f2248,f2253,f2316,f2566,f2580,f2591,f2683,f2724,f3137,f3155,f3168,f3193,f4264,f4265,f4283,f4285,f4293,f4336,f4355,f4410,f4414,f4527,f4548,f4569,f4601,f4861,f4967,f8305,f8338,f8438,f8649,f8663,f10164,f10287]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU170+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n019.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 05:54:35 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.13/0.57 % Drodi V4.1.1
% 61.81/8.91 % Refutation found
% 61.81/8.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 61.81/8.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 61.81/8.97 % Elapsed time: 8.395061 seconds
% 61.81/8.97 % CPU time: 66.343201 seconds
% 61.81/8.97 % Total memory used: 478.166 MB
% 61.81/8.97 % Net memory used: 406.313 MB
%------------------------------------------------------------------------------