%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:20:21 PM UTC 2026
% Result : Theorem 0.13s 0.50s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 88
% Syntax : Number of formulae : 412 ( 47 unt; 61 def)
% Number of atoms : 1149 ( 44 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1201 ( 464 ~; 546 |; 92 &)
% ( 69 <=>; 28 =>; 0 <=; 2 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 80 ( 78 usr; 62 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-2 aty)
% Number of variables : 291 ( 274 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A] :
( empty(A)
=> finite(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] :
( finite(A)
=> ! [B] :
( element(B,powerset(A))
=> finite(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( rel_str(A)
=> ( ( reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( ~ v1_yellow_3(A)
& ~ empty_carrier(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( upper_relstr_subset(B,A)
<=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& in(C,B) )
=> in(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] :
( rel_str(A)
=> element(join_on_relstr(A,B),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( rel_str(A)
=> element(bottom_of_relstr(A),the_carrier(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( rel_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A,B] : subset(A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
<=> in(C,B) )
=> A = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> related(A,bottom_of_relstr(A),B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A,B] :
( element(B,powerset(A))
=> ( proper_element(B,powerset(A))
<=> B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ ! [A] :
( ( rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
=> ( proper_element(B,powerset(the_carrier(A)))
<=> ~ in(bottom_of_relstr(A),B) ) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f47,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f48,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [A] :
( finite(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0] :
( finite(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f53,plain,
! [A] :
( ! [B] :
( finite(B)
| ~ element(B,powerset(A)) )
| ~ finite(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f54,plain,
! [X0,X1] :
( finite(X1)
| ~ element(X1,powerset(X0))
| ~ finite(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f57,plain,
! [A] :
( ( ~ v1_yellow_3(A)
& ~ empty_carrier(A) )
| ~ reflexive_relstr(A)
| empty_carrier(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f59,plain,
! [X0] :
( ~ v1_yellow_3(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f62,plain,
! [A] :
( ! [B] :
( ( upper_relstr_subset(B,A)
<=> ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f63,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ~ in(D,B)
& related(A,C,D)
& in(C,B)
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [A] :
( ! [B] :
( ( ( ( ~ in(sK1_skl(B,A),B)
& related(A,sK0_skl(B,A),sK1_skl(B,A))
& in(sK0_skl(B,A),B)
& element(sK1_skl(B,A),the_carrier(A))
& element(sK0_skl(B,A),the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f63]) ).
fof(f65,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( element(sK0_skl(X1,X0),the_carrier(X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [X0,X1] :
( element(sK1_skl(X1,X0),the_carrier(X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f69,plain,
! [X0,X1] :
( related(X0,sK0_skl(X1,X0),sK1_skl(X1,X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f70,plain,
! [X0,X1] :
( ~ in(sK1_skl(X1,X0),X1)
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f71,plain,
! [A,B] :
( element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f72,plain,
! [A] :
( ! [B] : element(join_on_relstr(A,B),the_carrier(A))
| ~ rel_str(A) ),
inference(miniscoping,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
! [A] :
( element(bottom_of_relstr(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f75,plain,
! [X0] :
( element(bottom_of_relstr(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [A] :
( one_sorted_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f77,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f82,plain,
! [A] : element(sK4_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f19]) ).
fof(f83,plain,
! [X0] : element(sK4_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f86,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f87,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f97,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f98,plain,
! [A] :
( ( ~ empty(sK7_skl(A))
& element(sK7_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f97]) ).
fof(f99,plain,
! [X0] :
( element(sK7_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0] :
( ~ empty(sK7_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
empty(sK8_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f26]) ).
fof(f102,plain,
empty(sK8_skl),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [A] :
( empty(sK9_skl(A))
& element(sK9_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(B,sK9_skl(A))],[f27]) ).
fof(f104,plain,
! [X0] : element(sK9_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X0] : empty(sK9_skl(X0)),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f108,plain,
! [A] :
( ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f109,plain,
! [A] :
( ( finite(sK11_skl(A))
& ~ empty(sK11_skl(A))
& element(sK11_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(B,sK11_skl(A))],[f108]) ).
fof(f110,plain,
! [X0] :
( element(sK11_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0] :
( ~ empty(sK11_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f116,plain,
! [A] :
( ? [B] :
( finite(B)
& ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f117,plain,
! [A] :
( ( finite(sK13_skl(A))
& ~ empty(sK13_skl(A))
& element(sK13_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f116]) ).
fof(f118,plain,
! [X0] :
( element(sK13_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [X0] :
( ~ empty(sK13_skl(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f125,plain,
! [A] : subset(A,A),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f126,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f128,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f130,plain,
! [X0,X1] :
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
! [A,B] :
( A = B
| ? [C] :
( in(C,A)
<~> in(C,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f132,plain,
! [A,B] :
( A = B
| ? [C] :
( ( ~ in(C,B)
| ~ in(C,A) )
& ( in(C,B)
| in(C,A) ) ) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [A,B] :
( A = B
| ( ( ~ in(sK15_skl(B,A),B)
| ~ in(sK15_skl(B,A),A) )
& ( in(sK15_skl(B,A),B)
| in(sK15_skl(B,A),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(C,sK15_skl(B,A))],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( X1 = X0
| in(sK15_skl(X0,X1),X0)
| in(sK15_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( X1 = X0
| ~ in(sK15_skl(X0,X1),X0)
| ~ in(sK15_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f136,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f137,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f139,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
! [A] :
( ! [B] :
( related(A,bottom_of_relstr(A),B)
| ~ element(B,the_carrier(A)) )
| ~ rel_str(A)
| ~ lower_bounded_relstr(A)
| ~ antisymmetric_relstr(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f141,plain,
! [X0,X1] :
( related(X0,bottom_of_relstr(X0),X1)
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ lower_bounded_relstr(X0)
| ~ antisymmetric_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f142,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f143,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f146,plain,
! [C] :
( ~ empty(C)
| ! [B] :
( ~ element(B,powerset(C))
| ! [A] : ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f147,plain,
! [X0,X1,X2] :
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [A,B] :
( ( proper_element(B,powerset(A))
<=> B != A )
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f149,plain,
! [A,B] :
( ( ( B = A
| proper_element(B,powerset(A)) )
& ( B != A
| ~ proper_element(B,powerset(A)) ) )
| ~ element(B,powerset(A)) ),
inference(NNF_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0,X1] :
( X0 != X1
| ~ proper_element(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( X0 = X1
| proper_element(X0,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f157,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f158,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
? [A] :
( ? [B] :
( ( proper_element(B,powerset(the_carrier(A)))
<~> ~ in(bottom_of_relstr(A),B) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f161,plain,
? [A] :
( ? [B] :
( ( in(bottom_of_relstr(A),B)
| ~ proper_element(B,powerset(the_carrier(A))) )
& ( ~ in(bottom_of_relstr(A),B)
| proper_element(B,powerset(the_carrier(A))) )
& element(B,powerset(the_carrier(A)))
& upper_relstr_subset(B,A)
& filtered_subset(B,A)
& ~ empty(B) )
& rel_str(A)
& lower_bounded_relstr(A)
& antisymmetric_relstr(A)
& transitive_relstr(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
( ( in(bottom_of_relstr(sK16_skl),sK17_skl)
| ~ proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) )
& ( ~ in(bottom_of_relstr(sK16_skl),sK17_skl)
| proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) )
& element(sK17_skl,powerset(the_carrier(sK16_skl)))
& upper_relstr_subset(sK17_skl,sK16_skl)
& filtered_subset(sK17_skl,sK16_skl)
& ~ empty(sK17_skl)
& rel_str(sK16_skl)
& lower_bounded_relstr(sK16_skl)
& antisymmetric_relstr(sK16_skl)
& transitive_relstr(sK16_skl)
& reflexive_relstr(sK16_skl)
& ~ empty_carrier(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl)],[f161]) ).
fof(f163,plain,
~ empty_carrier(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
reflexive_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f165,plain,
transitive_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f166,plain,
antisymmetric_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f167,plain,
lower_bounded_relstr(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f168,plain,
rel_str(sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f169,plain,
~ empty(sK17_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f171,plain,
upper_relstr_subset(sK17_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f172,plain,
element(sK17_skl,powerset(the_carrier(sK16_skl))),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f173,plain,
( ~ in(bottom_of_relstr(sK16_skl),sK17_skl)
| proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f174,plain,
( in(bottom_of_relstr(sK16_skl),sK17_skl)
| ~ proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f175,definition,
( sQ0_spl
<=> proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ0_spl
| proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,definition,
( sQ1_spl
<=> in(bottom_of_relstr(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( ~ sQ1_spl
| in(bottom_of_relstr(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f173,f175,f178]) ).
fof(f182,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f174,f175,f178]) ).
fof(f183,plain,
! [X0] :
( ~ proper_element(X0,powerset(X0))
| ~ element(X0,powerset(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f150]) ).
fof(f184,plain,
! [X0] :
( ~ rel_str(X0)
| in(bottom_of_relstr(X0),the_carrier(X0))
| empty(the_carrier(X0)) ),
inference(resolution,[status(thm)],[f130,f75]) ).
fof(f185,plain,
( in(sK17_skl,powerset(the_carrier(sK16_skl)))
| empty(powerset(the_carrier(sK16_skl))) ),
inference(resolution,[status(thm)],[f130,f172]) ).
fof(f186,definition,
( sQ2_spl
<=> empty(powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f187,plain,
( ~ sQ2_spl
| empty(powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f186]) ).
fof(f189,definition,
( sQ3_spl
<=> in(sK17_skl,powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f185,f186,f189]) ).
fof(f193,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f187,f86]) ).
fof(f194,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f193]) ).
fof(f195,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f87,f159]) ).
fof(f199,plain,
finite(sK8_skl),
inference(resolution,[status(thm)],[f50,f102]) ).
fof(f202,plain,
one_sorted_str(sK16_skl),
inference(resolution,[status(thm)],[f77,f168]) ).
fof(f215,definition,
( sQ6_spl
<=> empty(sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( ~ sQ6_spl
| empty(sK17_skl) ),
inference(component_clause,[status(thm)],[f215]) ).
fof(f222,plain,
! [X0] : sK9_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f195,f105]) ).
fof(f223,plain,
sK8_skl = empty_set,
inference(resolution,[status(thm)],[f195,f102]) ).
fof(f230,plain,
! [X0] : sK9_skl(X0) = sK8_skl,
inference(forward_demodulation,[status(thm)],[f223,f222]) ).
fof(f233,plain,
! [X0] :
( ~ empty(the_carrier(sK16_skl))
| ~ in(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f147,f172]) ).
fof(f234,definition,
! [X0] :
( sQ7_spl
<=> ~ in(X0,sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f235,plain,
! [X0] :
( ~ sQ7_spl
| ~ in(X0,sK17_skl) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f237,definition,
( sQ8_spl
<=> empty(the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f239,plain,
( sQ8_spl
| ~ empty(the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f237]) ).
fof(f240,plain,
( ~ sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f233,f234,f237]) ).
fof(f241,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f179,f235]) ).
fof(f242,plain,
( ~ sQ1_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f241]) ).
fof(f243,plain,
! [X0] :
( element(X0,the_carrier(sK16_skl))
| ~ in(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f144,f172]) ).
fof(f244,plain,
( sK17_skl = the_carrier(sK16_skl)
| proper_element(sK17_skl,powerset(the_carrier(sK16_skl))) ),
inference(resolution,[status(thm)],[f151,f172]) ).
fof(f245,definition,
( sQ9_spl
<=> sK17_skl = the_carrier(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f246,plain,
( ~ sQ9_spl
| sK17_skl = the_carrier(sK16_skl) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,plain,
( sQ9_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f244,f175,f245]) ).
fof(f253,plain,
! [X0] :
( in(sK4_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f83,f130]) ).
fof(f255,plain,
! [X0] : element(sK8_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f230,f104]) ).
fof(f256,plain,
! [X0] :
( sK8_skl = X0
| proper_element(sK8_skl,powerset(X0)) ),
inference(resolution,[status(thm)],[f255,f151]) ).
fof(f258,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,sK8_skl) ),
inference(resolution,[status(thm)],[f255,f147]) ).
fof(f259,plain,
! [X0] :
( finite(sK8_skl)
| ~ finite(X0) ),
inference(resolution,[status(thm)],[f255,f54]) ).
fof(f261,definition,
! [X0] :
( sQ10_spl
<=> ~ in(X0,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f262,plain,
! [X0] :
( ~ sQ10_spl
| ~ in(X0,sK8_skl) ),
inference(component_clause,[status(thm)],[f261]) ).
fof(f264,definition,
! [X1] :
( sQ11_spl
<=> ~ empty(X1) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f265,plain,
! [X0] :
( ~ sQ11_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f264]) ).
fof(f267,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f258,f261,f264]) ).
fof(f268,definition,
! [X0] :
( sQ12_spl
<=> ~ finite(X0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f269,plain,
! [X0] :
( ~ sQ12_spl
| ~ finite(X0) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f271,definition,
( sQ13_spl
<=> finite(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f259,f268,f271]) ).
fof(f277,plain,
( ~ sQ12_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f199,f269]) ).
fof(f279,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f277]) ).
fof(f286,plain,
( ~ v1_yellow_3(sK16_skl)
| empty_carrier(sK16_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f59,f164]) ).
fof(f287,definition,
( sQ14_spl
<=> rel_str(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f289,plain,
( sQ14_spl
| ~ rel_str(sK16_skl) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,definition,
( sQ15_spl
<=> empty_carrier(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( ~ sQ15_spl
| empty_carrier(sK16_skl) ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f293,definition,
( sQ16_spl
<=> v1_yellow_3(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( ~ sQ16_spl
| sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f286,f287,f290,f293]) ).
fof(f298,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f65,f144]) ).
fof(f301,plain,
! [X0,X1] :
( in(X0,sK17_skl)
| ~ related(sK16_skl,X1,X0)
| ~ in(X1,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl))
| ~ upper_relstr_subset(sK17_skl,sK16_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f298,f172]) ).
fof(f302,definition,
( sQ17_spl
<=> upper_relstr_subset(sK17_skl,sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f304,plain,
( sQ17_spl
| ~ upper_relstr_subset(sK17_skl,sK16_skl) ),
inference(component_clause,[status(thm)],[f302]) ).
fof(f305,definition,
! [X0,X1] :
( sQ18_spl
<=> ( in(X0,sK17_skl)
| ~ related(sK16_skl,X1,X0)
| ~ in(X1,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f306,plain,
! [X0,X1] :
( ~ sQ18_spl
| in(X0,sK17_skl)
| ~ related(sK16_skl,X1,X0)
| ~ in(X1,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f305]) ).
fof(f308,plain,
( sQ18_spl
| ~ sQ17_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f301,f287,f302,f305]) ).
fof(f309,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f289,f168]) ).
fof(f310,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f309]) ).
fof(f311,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f291,f163]) ).
fof(f312,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f311]) ).
fof(f313,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f304,f171]) ).
fof(f314,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f313]) ).
fof(f318,plain,
! [X0] :
( in(X0,the_carrier(sK16_skl))
| empty(the_carrier(sK16_skl))
| ~ in(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f243,f130]) ).
fof(f319,definition,
! [X0] :
( sQ19_spl
<=> ( in(X0,the_carrier(sK16_skl))
| ~ in(X0,sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f320,plain,
! [X0] :
( ~ sQ19_spl
| in(X0,the_carrier(sK16_skl))
| ~ in(X0,sK17_skl) ),
inference(component_clause,[status(thm)],[f319]) ).
fof(f322,plain,
( sQ8_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f318,f319,f237]) ).
fof(f324,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(the_carrier(sK16_skl),X0)
| ~ in(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f320,f48]) ).
fof(f327,plain,
! [X0] :
( ~ sQ18_spl
| ~ element(X0,the_carrier(sK16_skl))
| ~ rel_str(sK16_skl)
| ~ lower_bounded_relstr(sK16_skl)
| ~ antisymmetric_relstr(sK16_skl)
| empty_carrier(sK16_skl)
| in(X0,sK17_skl)
| ~ in(bottom_of_relstr(sK16_skl),sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f306,f141]) ).
fof(f328,definition,
! [X0] :
( sQ20_spl
<=> ( ~ element(X0,the_carrier(sK16_skl))
| in(X0,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f329,plain,
! [X0] :
( ~ sQ20_spl
| ~ element(X0,the_carrier(sK16_skl))
| in(X0,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f328]) ).
fof(f331,definition,
( sQ21_spl
<=> antisymmetric_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f333,plain,
( sQ21_spl
| ~ antisymmetric_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,definition,
( sQ22_spl
<=> lower_bounded_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( sQ22_spl
| ~ lower_bounded_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f337,plain,
( ~ sQ18_spl
| ~ sQ14_spl
| ~ sQ22_spl
| ~ sQ21_spl
| sQ15_spl
| ~ sQ1_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f327,f328,f178,f290,f331,f334,f287,f305]) ).
fof(f340,plain,
( ~ sQ9_spl
| element(sK17_skl,powerset(sK17_skl)) ),
inference(backward_demodulation,[status(thm)],[f246,f172]) ).
fof(f342,plain,
( ~ sQ9_spl
| element(bottom_of_relstr(sK16_skl),sK17_skl)
| ~ rel_str(sK16_skl) ),
inference(paramodulation,[status(thm)],[f246,f75]) ).
fof(f347,definition,
( sQ24_spl
<=> element(bottom_of_relstr(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ24_spl
| element(bottom_of_relstr(sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,plain,
( ~ sQ9_spl
| sQ24_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f342,f287,f347,f245]) ).
fof(f367,definition,
( sQ27_spl
<=> empty(powerset(sK17_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( ~ sQ27_spl
| empty(powerset(sK17_skl)) ),
inference(component_clause,[status(thm)],[f367]) ).
fof(f374,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f86]) ).
fof(f375,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f374]) ).
fof(f376,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f336,f167]) ).
fof(f377,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f376]) ).
fof(f378,plain,
! [X0] :
( ~ sQ20_spl
| in(X0,sK17_skl)
| ~ element(X0,the_carrier(sK16_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f329]) ).
fof(f407,plain,
( ~ element(sK8_skl,powerset(sK8_skl))
| sK8_skl = sK8_skl ),
inference(resolution,[status(thm)],[f256,f183]) ).
fof(f408,definition,
( sQ29_spl
<=> sK8_skl = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f411,definition,
( sQ30_spl
<=> element(sK8_skl,powerset(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( sQ30_spl
| ~ element(sK8_skl,powerset(sK8_skl)) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,plain,
( ~ sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f407,f408,f411]) ).
fof(f425,plain,
! [X0,X1] :
( element(X1,X0)
| ~ in(X1,sK7_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f99,f144]) ).
fof(f442,plain,
( ~ sQ19_spl
| ~ in(the_carrier(sK16_skl),sK17_skl)
| ~ in(the_carrier(sK16_skl),sK17_skl) ),
inference(resolution,[status(thm)],[f320,f324]) ).
fof(f447,definition,
( sQ32_spl
<=> in(the_carrier(sK16_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ19_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f442,f447,f319]) ).
fof(f454,plain,
! [X0] :
( ~ sQ20_spl
| upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| ~ rel_str(sK16_skl)
| in(sK1_skl(X0,sK16_skl),sK17_skl) ),
inference(resolution,[status(thm)],[f378,f67]) ).
fof(f455,plain,
! [X0] :
( ~ sQ20_spl
| upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| ~ rel_str(sK16_skl)
| in(sK0_skl(X0,sK16_skl),sK17_skl) ),
inference(resolution,[status(thm)],[f378,f66]) ).
fof(f456,plain,
( ~ sQ20_spl
| in(sK4_skl(the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f378,f83]) ).
fof(f457,plain,
( ~ sQ20_spl
| ~ rel_str(sK16_skl)
| in(bottom_of_relstr(sK16_skl),sK17_skl) ),
inference(resolution,[status(thm)],[f378,f75]) ).
fof(f459,definition,
! [X0] :
( sQ33_spl
<=> ( upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| in(sK1_skl(X0,sK16_skl),sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f460,plain,
! [X0] :
( ~ sQ33_spl
| upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| in(sK1_skl(X0,sK16_skl),sK17_skl) ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,plain,
( ~ sQ20_spl
| ~ sQ14_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f454,f459,f287,f328]) ).
fof(f463,definition,
! [X0] :
( sQ34_spl
<=> ( upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| in(sK0_skl(X0,sK16_skl),sK17_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ20_spl
| ~ sQ14_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f455,f463,f287,f328]) ).
fof(f467,plain,
( ~ sQ20_spl
| ~ sQ14_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f457,f178,f287,f328]) ).
fof(f468,plain,
( ~ sQ20_spl
| element(sK4_skl(the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f456,f128]) ).
fof(f471,plain,
( ~ sQ20_spl
| in(sK4_skl(the_carrier(sK16_skl)),sK17_skl)
| empty(sK17_skl) ),
inference(resolution,[status(thm)],[f468,f130]) ).
fof(f472,definition,
( sQ35_spl
<=> in(sK4_skl(the_carrier(sK16_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( ~ sQ20_spl
| sQ35_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f471,f215,f472,f328]) ).
fof(f498,plain,
! [X0,X1] :
( element(X1,X0)
| ~ in(X1,sK11_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f110,f144]) ).
fof(f507,plain,
! [X0,X1] :
( element(X1,X0)
| ~ in(X1,sK13_skl(X0))
| empty(X0) ),
inference(resolution,[status(thm)],[f118,f144]) ).
fof(f518,plain,
! [X0] :
( ~ sQ20_spl
| in(join_on_relstr(sK16_skl,X0),sK17_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f73,f378]) ).
fof(f520,definition,
! [X0] :
( sQ36_spl
<=> in(join_on_relstr(sK16_skl,X0),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( ~ sQ20_spl
| sQ36_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f518,f287,f520,f328]) ).
fof(f548,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(sK1_skl(the_carrier(sK16_skl),X0),sK17_skl)
| upper_relstr_subset(the_carrier(sK16_skl),X0)
| ~ element(the_carrier(sK16_skl),powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f70,f320]) ).
fof(f569,plain,
! [X0] :
( ~ sQ33_spl
| ~ subset(X0,the_carrier(sK16_skl))
| upper_relstr_subset(X0,sK16_skl)
| in(sK1_skl(X0,sK16_skl),sK17_skl) ),
inference(resolution,[status(thm)],[f460,f139]) ).
fof(f576,definition,
( sQ39_spl
<=> reflexive_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f578,plain,
( sQ39_spl
| ~ reflexive_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f579,definition,
( sQ40_spl
<=> transitive_relstr(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ40_spl
| ~ transitive_relstr(sK16_skl) ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f622,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f581,f165]) ).
fof(f623,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f622]) ).
fof(f624,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f164]) ).
fof(f625,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f624]) ).
fof(f672,plain,
! [X0] :
( empty(sK7_skl(X0))
| element(sK4_skl(sK7_skl(X0)),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f425,f253]) ).
fof(f673,plain,
! [X0] :
( element(sK4_skl(sK7_skl(X0)),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f100]) ).
fof(f674,plain,
( ~ sQ20_spl
| in(sK4_skl(sK7_skl(the_carrier(sK16_skl))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f673,f378]) ).
fof(f684,plain,
! [X0] :
( in(sK4_skl(sK7_skl(X0)),X0)
| empty(X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f673,f130]) ).
fof(f685,definition,
( sQ58_spl
<=> in(sK4_skl(sK7_skl(the_carrier(sK16_skl))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( ~ sQ20_spl
| sQ58_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f674,f237,f685,f328]) ).
fof(f707,plain,
! [X0] :
( in(sK4_skl(sK7_skl(X0)),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f684]) ).
fof(f708,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f166]) ).
fof(f709,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f708]) ).
fof(f737,plain,
! [X0] :
( element(sK4_skl(sK7_skl(sK7_skl(X0))),X0)
| empty(X0)
| empty(sK7_skl(X0)) ),
inference(resolution,[status(thm)],[f707,f425]) ).
fof(f744,plain,
! [X0] :
( element(sK4_skl(sK7_skl(sK7_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f100]) ).
fof(f781,plain,
! [X0] :
( empty(sK11_skl(X0))
| element(sK4_skl(sK7_skl(sK11_skl(X0))),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f498,f707]) ).
fof(f782,plain,
! [X0] :
( empty(sK11_skl(X0))
| element(sK4_skl(sK11_skl(X0)),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f498,f253]) ).
fof(f783,plain,
! [X0] :
( element(sK4_skl(sK7_skl(sK11_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f111]) ).
fof(f784,plain,
! [X0] :
( element(sK4_skl(sK11_skl(X0)),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f111]) ).
fof(f785,plain,
( ~ sQ20_spl
| in(sK4_skl(sK11_skl(the_carrier(sK16_skl))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f784,f378]) ).
fof(f793,plain,
! [X0] :
( in(sK4_skl(sK11_skl(X0)),X0)
| empty(X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f784,f130]) ).
fof(f794,definition,
( sQ63_spl
<=> in(sK4_skl(sK11_skl(the_carrier(sK16_skl))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f797,plain,
( ~ sQ20_spl
| sQ63_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f785,f237,f794,f328]) ).
fof(f805,plain,
! [X0] :
( in(sK4_skl(sK11_skl(X0)),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f793]) ).
fof(f810,plain,
! [X0] :
( element(sK4_skl(sK11_skl(sK11_skl(X0))),X0)
| empty(X0)
| empty(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f805,f498]) ).
fof(f811,plain,
! [X0] :
( element(sK4_skl(sK11_skl(sK7_skl(X0))),X0)
| empty(X0)
| empty(sK7_skl(X0)) ),
inference(resolution,[status(thm)],[f805,f425]) ).
fof(f818,plain,
! [X0] :
( element(sK4_skl(sK11_skl(sK11_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f810,f111]) ).
fof(f819,plain,
! [X0] :
( element(sK4_skl(sK11_skl(sK7_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f811,f100]) ).
fof(f825,plain,
! [X0] :
( empty(sK13_skl(X0))
| element(sK4_skl(sK11_skl(sK13_skl(X0))),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f507,f805]) ).
fof(f826,plain,
! [X0] :
( empty(sK13_skl(X0))
| element(sK4_skl(sK7_skl(sK13_skl(X0))),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f507,f707]) ).
fof(f827,plain,
! [X0] :
( empty(sK13_skl(X0))
| element(sK4_skl(sK13_skl(X0)),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f507,f253]) ).
fof(f828,plain,
! [X0] :
( element(sK4_skl(sK11_skl(sK13_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f119]) ).
fof(f829,plain,
! [X0] :
( element(sK4_skl(sK7_skl(sK13_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f826,f119]) ).
fof(f830,plain,
! [X0] :
( element(sK4_skl(sK13_skl(X0)),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f827,f119]) ).
fof(f831,plain,
( ~ sQ20_spl
| in(sK4_skl(sK13_skl(the_carrier(sK16_skl))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f830,f378]) ).
fof(f839,plain,
! [X0] :
( in(sK4_skl(sK13_skl(X0)),X0)
| empty(X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f830,f130]) ).
fof(f840,definition,
( sQ64_spl
<=> in(sK4_skl(sK13_skl(the_carrier(sK16_skl))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f843,plain,
( ~ sQ20_spl
| sQ64_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f831,f237,f840,f328]) ).
fof(f851,plain,
! [X0] :
( in(sK4_skl(sK13_skl(X0)),X0)
| empty(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f839]) ).
fof(f861,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK13_skl(X0))),X0)
| empty(X0)
| empty(sK13_skl(X0)) ),
inference(resolution,[status(thm)],[f851,f507]) ).
fof(f862,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK11_skl(X0))),X0)
| empty(X0)
| empty(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f851,f498]) ).
fof(f863,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK7_skl(X0))),X0)
| empty(X0)
| empty(sK7_skl(X0)) ),
inference(resolution,[status(thm)],[f851,f425]) ).
fof(f870,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK13_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f861,f119]) ).
fof(f871,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK11_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f862,f111]) ).
fof(f872,plain,
! [X0] :
( element(sK4_skl(sK13_skl(sK7_skl(X0))),X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f863,f100]) ).
fof(f891,plain,
! [X0] :
( ~ sQ10_spl
| sK8_skl = X0
| in(sK15_skl(X0,sK8_skl),X0) ),
inference(resolution,[status(thm)],[f134,f262]) ).
fof(f892,plain,
! [X0,X1] :
( element(sK15_skl(X0,X1),X1)
| X1 = X0
| in(sK15_skl(X0,X1),X0) ),
inference(resolution,[status(thm)],[f134,f128]) ).
fof(f896,plain,
! [X0] :
( ~ sQ19_spl
| ~ in(sK15_skl(X0,the_carrier(sK16_skl)),sK17_skl)
| the_carrier(sK16_skl) = X0
| ~ in(sK15_skl(X0,the_carrier(sK16_skl)),X0) ),
inference(resolution,[status(thm)],[f135,f320]) ).
fof(f919,plain,
! [X0] :
( ~ sQ10_spl
| element(sK15_skl(X0,sK8_skl),X0)
| sK8_skl = X0 ),
inference(resolution,[status(thm)],[f891,f128]) ).
fof(f960,plain,
( ~ sQ11_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f102,f265]) ).
fof(f961,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f960]) ).
fof(f1039,plain,
( ~ sQ19_spl
| ~ sQ33_spl
| upper_relstr_subset(the_carrier(sK16_skl),sK16_skl)
| ~ element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl)))
| ~ rel_str(sK16_skl)
| ~ subset(the_carrier(sK16_skl),the_carrier(sK16_skl))
| upper_relstr_subset(the_carrier(sK16_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f569,f548]) ).
fof(f1044,definition,
( sQ67_spl
<=> upper_relstr_subset(the_carrier(sK16_skl),sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f1047,definition,
( sQ68_spl
<=> subset(the_carrier(sK16_skl),the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( sQ68_spl
| ~ subset(the_carrier(sK16_skl),the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f1047]) ).
fof(f1050,definition,
( sQ69_spl
<=> element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( ~ sQ69_spl
| element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f1050]) ).
fof(f1052,plain,
( sQ69_spl
| ~ element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f1050]) ).
fof(f1053,plain,
( ~ sQ19_spl
| ~ sQ33_spl
| ~ sQ69_spl
| ~ sQ14_spl
| ~ sQ68_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f1039,f1044,f1047,f287,f1050,f459,f319]) ).
fof(f1065,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f169]) ).
fof(f1066,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1065]) ).
fof(f1209,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| in(sK15_skl(the_carrier(sK16_skl),sK8_skl),sK17_skl)
| sK8_skl = the_carrier(sK16_skl) ),
inference(resolution,[status(thm)],[f919,f378]) ).
fof(f1218,definition,
( sQ74_spl
<=> sK8_skl = the_carrier(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1219,plain,
( ~ sQ74_spl
| sK8_skl = the_carrier(sK16_skl) ),
inference(component_clause,[status(thm)],[f1218]) ).
fof(f1221,definition,
( sQ75_spl
<=> in(sK15_skl(the_carrier(sK16_skl),sK8_skl),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1224,plain,
( ~ sQ20_spl
| ~ sQ10_spl
| sQ75_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f1209,f1218,f1221,f261,f328]) ).
fof(f1230,plain,
( sQ8_spl
| ~ sQ74_spl
| ~ empty(sK8_skl) ),
inference(backward_demodulation,[status(thm)],[f1219,f239]) ).
fof(f1280,plain,
( sQ8_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1230,f102]) ).
fof(f1281,plain,
( sQ8_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f1280]) ).
fof(f1362,plain,
( sQ69_spl
| ~ subset(the_carrier(sK16_skl),the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f1052,f139]) ).
fof(f1363,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1362,f126]) ).
fof(f1364,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f1363]) ).
fof(f1424,plain,
! [X0,X1] :
( ~ sQ69_spl
| in(X0,the_carrier(sK16_skl))
| ~ related(sK16_skl,X1,X0)
| ~ in(X1,the_carrier(sK16_skl))
| ~ element(X0,the_carrier(sK16_skl))
| ~ upper_relstr_subset(the_carrier(sK16_skl),sK16_skl)
| ~ rel_str(sK16_skl) ),
inference(resolution,[status(thm)],[f1051,f298]) ).
fof(f1425,plain,
! [X0] :
( ~ sQ69_spl
| ~ empty(the_carrier(sK16_skl))
| ~ in(X0,the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f1051,f147]) ).
fof(f1428,plain,
( ~ sQ69_spl
| the_carrier(sK16_skl) = the_carrier(sK16_skl)
| proper_element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(resolution,[status(thm)],[f1051,f151]) ).
fof(f1430,plain,
( ~ sQ69_spl
| in(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl)))
| empty(powerset(the_carrier(sK16_skl))) ),
inference(resolution,[status(thm)],[f1051,f130]) ).
fof(f1435,definition,
! [X0,X1] :
( sQ78_spl
<=> ( in(X0,the_carrier(sK16_skl))
| ~ related(sK16_skl,X1,X0)
| ~ in(X1,the_carrier(sK16_skl))
| ~ element(X0,the_carrier(sK16_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1438,plain,
( ~ sQ69_spl
| sQ78_spl
| ~ sQ67_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1424,f287,f1044,f1435,f1050]) ).
fof(f1439,definition,
! [X0] :
( sQ79_spl
<=> ~ in(X0,the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1440,plain,
! [X0] :
( ~ sQ79_spl
| ~ in(X0,the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f1439]) ).
fof(f1442,plain,
( ~ sQ69_spl
| ~ sQ8_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1425,f1439,f237,f1050]) ).
fof(f1444,definition,
( sQ80_spl
<=> proper_element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1445,plain,
( ~ sQ80_spl
| proper_element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f1444]) ).
fof(f1447,definition,
( sQ81_spl
<=> the_carrier(sK16_skl) = the_carrier(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( ~ sQ69_spl
| sQ81_spl
| sQ80_spl ),
inference(split_clause,[status(thm)],[f1428,f1444,f1447,f1050]) ).
fof(f1451,definition,
( sQ82_spl
<=> in(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( ~ sQ82_spl
| in(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(component_clause,[status(thm)],[f1451]) ).
fof(f1454,plain,
( ~ sQ69_spl
| sQ82_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1430,f186,f1451,f1050]) ).
fof(f1461,plain,
( ~ sQ80_spl
| ~ element(the_carrier(sK16_skl),powerset(the_carrier(sK16_skl))) ),
inference(resolution,[status(thm)],[f1445,f183]) ).
fof(f1462,plain,
( ~ sQ80_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1461,f1050,f1444]) ).
fof(f1466,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1049,f126]) ).
fof(f1467,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1466]) ).
fof(f1476,plain,
( ~ sQ20_spl
| in(sK4_skl(sK7_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f744,f378]) ).
fof(f1485,definition,
( sQ83_spl
<=> in(sK4_skl(sK7_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1488,plain,
( ~ sQ20_spl
| sQ83_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1476,f237,f1485,f328]) ).
fof(f1501,plain,
( ~ sQ20_spl
| in(sK4_skl(sK7_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f783,f378]) ).
fof(f1510,definition,
( sQ84_spl
<=> in(sK4_skl(sK7_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( ~ sQ20_spl
| sQ84_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1501,f237,f1510,f328]) ).
fof(f1590,definition,
( sQ88_spl
<=> sK8_skl = powerset(the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1591,plain,
( ~ sQ88_spl
| sK8_skl = powerset(the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f1590]) ).
fof(f1603,definition,
( sQ91_spl
<=> one_sorted_str(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1605,plain,
( sQ91_spl
| ~ one_sorted_str(sK16_skl) ),
inference(component_clause,[status(thm)],[f1603]) ).
fof(f1639,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1605,f202]) ).
fof(f1640,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f1639]) ).
fof(f1645,plain,
( ~ sQ82_spl
| ~ sQ88_spl
| in(the_carrier(sK16_skl),sK8_skl) ),
inference(backward_demodulation,[status(thm)],[f1591,f1452]) ).
fof(f1709,plain,
( ~ sQ82_spl
| ~ sQ88_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1645,f262]) ).
fof(f1710,plain,
( ~ sQ82_spl
| ~ sQ88_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f1709]) ).
fof(f1769,plain,
( ~ sQ20_spl
| in(sK4_skl(sK11_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f818,f378]) ).
fof(f1778,definition,
( sQ100_spl
<=> in(sK4_skl(sK11_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1781,plain,
( ~ sQ20_spl
| sQ100_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1769,f237,f1778,f328]) ).
fof(f1794,plain,
( ~ sQ20_spl
| in(sK4_skl(sK11_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f819,f378]) ).
fof(f1803,definition,
( sQ101_spl
<=> in(sK4_skl(sK11_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1806,plain,
( ~ sQ20_spl
| sQ101_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1794,f237,f1803,f328]) ).
fof(f1819,plain,
( ~ sQ20_spl
| in(sK4_skl(sK11_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f828,f378]) ).
fof(f1828,definition,
( sQ102_spl
<=> in(sK4_skl(sK11_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
( ~ sQ20_spl
| sQ102_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1819,f237,f1828,f328]) ).
fof(f1844,plain,
( ~ sQ20_spl
| in(sK4_skl(sK7_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f829,f378]) ).
fof(f1853,definition,
( sQ103_spl
<=> in(sK4_skl(sK7_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1856,plain,
( ~ sQ20_spl
| sQ103_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1844,f237,f1853,f328]) ).
fof(f1989,plain,
( ~ sQ20_spl
| in(sK4_skl(sK13_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f870,f378]) ).
fof(f1999,definition,
( sQ119_spl
<=> in(sK4_skl(sK13_skl(sK13_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f2002,plain,
( ~ sQ20_spl
| sQ119_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1989,f237,f1999,f328]) ).
fof(f2030,plain,
( ~ sQ20_spl
| in(sK4_skl(sK13_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f871,f378]) ).
fof(f2040,definition,
( sQ122_spl
<=> in(sK4_skl(sK13_skl(sK11_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f2043,plain,
( ~ sQ20_spl
| sQ122_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2030,f237,f2040,f328]) ).
fof(f2063,plain,
( ~ sQ20_spl
| in(sK4_skl(sK13_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f872,f378]) ).
fof(f2073,definition,
( sQ125_spl
<=> in(sK4_skl(sK13_skl(sK7_skl(the_carrier(sK16_skl)))),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f2076,plain,
( ~ sQ20_spl
| sQ125_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2063,f237,f2073,f328]) ).
fof(f2145,definition,
( sQ128_spl
<=> in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f2147,plain,
( sQ128_spl
| ~ in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl) ),
inference(component_clause,[status(thm)],[f2145]) ).
fof(f2425,plain,
( ~ sQ19_spl
| the_carrier(sK16_skl) = sK17_skl
| ~ in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)
| element(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl))
| the_carrier(sK16_skl) = sK17_skl ),
inference(resolution,[status(thm)],[f892,f896]) ).
fof(f2434,plain,
! [X0] :
( ~ sQ10_spl
| element(sK15_skl(sK8_skl,X0),X0)
| X0 = sK8_skl ),
inference(resolution,[status(thm)],[f892,f262]) ).
fof(f2446,definition,
( sQ129_spl
<=> element(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f2447,plain,
( ~ sQ129_spl
| element(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f2446]) ).
fof(f2449,plain,
( ~ sQ19_spl
| ~ sQ128_spl
| sQ129_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f2425,f245,f2446,f2145,f319]) ).
fof(f2450,plain,
( sQ128_spl
| element(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl))
| the_carrier(sK16_skl) = sK17_skl ),
inference(resolution,[status(thm)],[f2147,f892]) ).
fof(f2452,plain,
( sQ128_spl
| sQ129_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f2450,f245,f2446,f2145]) ).
fof(f2454,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f255]) ).
fof(f2455,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f2454]) ).
fof(f2457,plain,
( ~ sQ10_spl
| ~ sQ79_spl
| sK8_skl = the_carrier(sK16_skl) ),
inference(resolution,[status(thm)],[f1440,f891]) ).
fof(f2478,plain,
( ~ sQ10_spl
| ~ sQ79_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f2457,f1218,f1439,f261]) ).
fof(f2797,plain,
( ~ sQ24_spl
| in(bottom_of_relstr(sK16_skl),sK17_skl)
| empty(sK17_skl) ),
inference(resolution,[status(thm)],[f348,f130]) ).
fof(f2798,plain,
( ~ sQ24_spl
| sQ1_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2797,f215,f178,f347]) ).
fof(f2842,plain,
! [X0] :
( ~ sQ18_spl
| upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| ~ rel_str(sK16_skl)
| in(sK1_skl(X0,sK16_skl),sK17_skl)
| ~ in(sK0_skl(X0,sK16_skl),sK17_skl)
| ~ element(sK1_skl(X0,sK16_skl),the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f306,f69]) ).
fof(f2844,definition,
! [X0] :
( sQ162_spl
<=> ( upper_relstr_subset(X0,sK16_skl)
| ~ element(X0,powerset(the_carrier(sK16_skl)))
| in(sK1_skl(X0,sK16_skl),sK17_skl)
| ~ in(sK0_skl(X0,sK16_skl),sK17_skl)
| ~ element(sK1_skl(X0,sK16_skl),the_carrier(sK16_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f2847,plain,
( ~ sQ18_spl
| ~ sQ14_spl
| sQ162_spl ),
inference(split_clause,[status(thm)],[f2842,f2844,f287,f305]) ).
fof(f2951,plain,
( ~ sQ10_spl
| ~ sQ20_spl
| the_carrier(sK16_skl) = sK8_skl
| in(sK15_skl(sK8_skl,the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f378,f2434]) ).
fof(f2973,definition,
( sQ163_spl
<=> in(sK15_skl(sK8_skl,the_carrier(sK16_skl)),sK17_skl) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f2976,plain,
( ~ sQ10_spl
| ~ sQ20_spl
| sQ74_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f2951,f2973,f1218,f328,f261]) ).
fof(f3059,plain,
( ~ sQ20_spl
| ~ sQ129_spl
| in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f2447,f378]) ).
fof(f3060,plain,
( ~ sQ129_spl
| in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl))
| empty(the_carrier(sK16_skl)) ),
inference(resolution,[status(thm)],[f2447,f130]) ).
fof(f3061,definition,
( sQ164_spl
<=> in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl)) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f3062,plain,
( ~ sQ164_spl
| in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl)) ),
inference(component_clause,[status(thm)],[f3061]) ).
fof(f3064,plain,
( ~ sQ129_spl
| sQ164_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f3060,f237,f3061,f2446]) ).
fof(f3066,plain,
( ~ sQ20_spl
| ~ sQ129_spl
| element(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f3059,f128]) ).
fof(f3068,plain,
( ~ sQ20_spl
| ~ sQ129_spl
| in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)
| empty(sK17_skl) ),
inference(resolution,[status(thm)],[f3066,f130]) ).
fof(f3069,plain,
( ~ sQ20_spl
| ~ sQ129_spl
| sQ128_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f3068,f215,f2145,f2446,f328]) ).
fof(f3130,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| proper_element(sK17_skl,powerset(sK17_skl)) ),
inference(backward_demodulation,[status(thm)],[f246,f176]) ).
fof(f3133,plain,
( ~ sQ9_spl
| ~ rel_str(sK16_skl)
| in(bottom_of_relstr(sK16_skl),sK17_skl)
| empty(the_carrier(sK16_skl)) ),
inference(paramodulation,[status(thm)],[f246,f184]) ).
fof(f3173,plain,
( ~ sQ9_spl
| ~ sQ14_spl
| sQ1_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f3133,f237,f178,f287,f245]) ).
fof(f3220,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ element(sK17_skl,powerset(sK17_skl)) ),
inference(resolution,[status(thm)],[f3130,f183]) ).
fof(f3221,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3220,f340]) ).
fof(f3222,plain,
( ~ sQ0_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f3221]) ).
fof(f3370,plain,
( ~ sQ164_spl
| the_carrier(sK16_skl) = sK17_skl
| ~ in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl) ),
inference(resolution,[status(thm)],[f3062,f135]) ).
fof(f3374,plain,
( ~ sQ164_spl
| sQ9_spl
| ~ sQ128_spl ),
inference(split_clause,[status(thm)],[f3370,f2145,f245,f3061]) ).
fof(f3375,plain,
$false,
inference(sat_refutation,[status(thm)],[f181,f182,f192,f194,f240,f242,f248,f267,f274,f279,f296,f308,f310,f312,f314,f322,f337,f350,f375,f377,f414,f450,f462,f466,f467,f475,f523,f623,f625,f688,f709,f797,f843,f961,f1053,f1066,f1224,f1281,f1364,f1438,f1442,f1450,f1454,f1462,f1467,f1488,f1513,f1640,f1710,f1781,f1806,f1831,f1856,f2002,f2043,f2076,f2449,f2452,f2455,f2478,f2798,f2847,f2976,f3064,f3069,f3173,f3222,f3374]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:13:26 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.13/0.50 % Refutation found
% 0.13/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.54 % Elapsed time: 0.173159 seconds
% 0.13/0.54 % CPU time: 1.109181 seconds
% 0.13/0.54 % Total memory used: 96.687 MB
% 0.13/0.54 % Net memory used: 95.568 MB
%------------------------------------------------------------------------------