%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU271+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:58 PM UTC 2026
% Result : Theorem 139.77s 18.14s
% Output : CNFRefutation 139.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 161
% Syntax : Number of formulae : 732 ( 208 unt; 105 def)
% Number of atoms : 1763 ( 237 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 1695 ( 664 ~; 656 |; 213 &)
% ( 136 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 121 ( 119 usr; 106 prp; 0-2 aty)
% Number of functors : 49 ( 49 usr; 11 con; 0-3 aty)
% Number of variables : 542 ( 497 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( relation(B)
=> ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] : succ(A) = set_union2(A,singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A,B] :
( ( A = empty_set
=> ( B = set_meet(A)
<=> B = empty_set ) )
& ( A != empty_set
=> ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(D,A)
=> in(C,D) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A,B] :
( relation(B)
=> ( B = inclusion_relation(A)
<=> ( ! [C,D] :
( ( in(D,A)
& in(C,A) )
=> ( in(ordered_pair(C,D),B)
<=> subset(C,D) ) )
& relation_field(B) = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( ( in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
=> C = D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( relation(A)
=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A] : relation(inclusion_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,axiom,
! [A,B] :
( relation(B)
=> relation(relation_rng_restriction(A,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [A] :
( function(identity_relation(A))
& relation(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f151,axiom,
! [A,B] : set_union2(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,lemma,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,lemma,
! [A] :
( relation(A)
=> ( antisymmetric(A)
<=> ! [B,C] :
( ( in(ordered_pair(C,B),A)
& in(ordered_pair(B,C),A) )
=> B = C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f182,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f185,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f187,axiom,
? [A] :
( relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f188,axiom,
? [A] :
( function(A)
& relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f200,lemma,
! [A] : in(A,succ(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f210,lemma,
! [A,B] :
( subset(A,B)
=> set_union2(A,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f211,lemma,
! [A] :
? [B] :
( ! [C] :
~ ( ~ in(C,B)
& ~ are_equipotent(C,B)
& subset(C,B) )
& ! [C] :
( in(C,B)
=> in(powerset(C),B) )
& ! [C,D] :
( ( subset(D,C)
& in(C,B) )
=> in(D,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,lemma,
! [A,B] : subset(set_intersection2(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f233,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f236,lemma,
powerset(empty_set) = singleton(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f255,lemma,
! [A,B] :
( subset(A,B)
=> set_intersection2(A,B) = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f260,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f261,lemma,
! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(B,relation_field(C))
& in(A,relation_field(C)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f279,axiom,
! [A] : set_difference(A,empty_set) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f284,lemma,
! [A] :
( subset(A,empty_set)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f314,conjecture,
! [A] : antisymmetric(inclusion_relation(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f315,negated_conjecture,
~ ! [A] : antisymmetric(inclusion_relation(A)),
inference(negated_conjecture,[status(cth)],[f314]) ).
fof(f316,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,lemma,
! [A] : unordered_pair(A,A) = singleton(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f325,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f334,lemma,
! [A,B] : subset(A,set_union2(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f337,lemma,
! [A,B] :
( relation(B)
=> subset(relation_dom_restriction(B,A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f348,axiom,
! [A] :
? [B] :
( ! [C] :
~ ( ~ in(C,B)
& ~ are_equipotent(C,B)
& subset(C,B) )
& ! [C] :
~ ( ! [D] :
~ ( ! [E] :
( subset(E,C)
=> in(E,D) )
& in(D,B) )
& in(C,B) )
& ! [C,D] :
( ( subset(D,C)
& in(C,B) )
=> in(D,B) )
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f375,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f376,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f379,plain,
! [A,B] :
( ( B = identity_relation(A)
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( C = D
& in(C,A) ) ) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f380,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ( ! [C,D] :
( ( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f379]) ).
fof(f381,plain,
! [B] :
( ( ! [A] :
( ? [C,D] :
( ( ( C = D
& in(C,A) )
| in(ordered_pair(C,D),B) )
& ( C != D
| ~ in(C,A)
| ~ in(ordered_pair(C,D),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f380]) ).
fof(f382,plain,
! [B] :
( ( ! [A] :
( ( ( ( sK0_skl(A,B) = sK1_skl(A,B)
& in(sK0_skl(A,B),A) )
| in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) )
& ( sK0_skl(A,B) != sK1_skl(A,B)
| ~ in(sK0_skl(A,B),A)
| ~ in(ordered_pair(sK0_skl(A,B),sK1_skl(A,B)),B) ) )
| B = identity_relation(A) )
& ! [A] :
( ( ! [C,D] :
( C != D
| ~ in(C,A)
| in(ordered_pair(C,D),B) )
& ! [C,D] :
( ( C = D
& in(C,A) )
| ~ in(ordered_pair(C,D),B) ) )
| B != identity_relation(A) ) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(A,B)),skolemize(D,sK1_skl(A,B))],[f381]) ).
fof(f385,plain,
! [X0,X1,X2,X3] :
( X2 != X3
| ~ in(X2,X1)
| in(ordered_pair(X2,X3),X0)
| X0 != identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f389,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f15]) ).
fof(f390,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f389]) ).
fof(f391,plain,
! [X0,X1] :
( subset(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f393,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f424,plain,
! [A] :
( ( antisymmetric(A)
<=> is_antisymmetric_in(A,relation_field(A)) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f425,plain,
! [A] :
( ( ( ~ is_antisymmetric_in(A,relation_field(A))
| antisymmetric(A) )
& ( is_antisymmetric_in(A,relation_field(A))
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f424]) ).
fof(f427,plain,
! [X0] :
( ~ is_antisymmetric_in(X0,relation_field(X0))
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f425]) ).
fof(f483,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f502,plain,
! [A,B] :
( ( ( B = set_meet(A)
<=> B = empty_set )
| A != empty_set )
& ( ( B = set_meet(A)
<=> ! [C] :
( in(C,B)
<=> ! [D] :
( in(C,D)
| ~ in(D,A) ) ) )
| A = empty_set ) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f503,plain,
! [A,B] :
( ( ( ( B != empty_set
| B = set_meet(A) )
& ( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ( ( ( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ( ! [C] :
( ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(NNF_transformation,[status(thm)],[f502]) ).
fof(f504,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ? [C] :
( ( ! [D] :
( in(C,D)
| ~ in(D,A) )
| in(C,B) )
& ( ? [D] :
( ~ in(C,D)
& in(D,A) )
| ~ in(C,B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ? [D] :
( ~ in(C,D)
& in(D,A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(miniscoping,[status(thm)],[f503]) ).
fof(f505,plain,
( ! [A] :
( ( ! [B] :
( B != empty_set
| B = set_meet(A) )
& ! [B] :
( B = empty_set
| B != set_meet(A) ) )
| A != empty_set )
& ! [A] :
( ( ! [B] :
( ( ( ! [D] :
( in(sK24_skl(B,A),D)
| ~ in(D,A) )
| in(sK24_skl(B,A),B) )
& ( ( ~ in(sK24_skl(B,A),sK25_skl(B,A))
& in(sK25_skl(B,A),A) )
| ~ in(sK24_skl(B,A),B) ) )
| B = set_meet(A) )
& ! [B] :
( ( ! [C] :
( ( ~ in(C,sK23_skl(C,B,A))
& in(sK23_skl(C,B,A),A) )
| in(C,B) )
& ! [C] :
( ! [D] :
( in(C,D)
| ~ in(D,A) )
| ~ in(C,B) ) )
| B != set_meet(A) ) )
| A = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl]),skolemize(D,sK23_skl(C,B,A)),skolemize(C,sK24_skl(B,A)),skolemize(D,sK25_skl(B,A))],[f504]) ).
fof(f512,plain,
! [X0,X1] :
( X1 = empty_set
| X1 != set_meet(X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f505]) ).
fof(f514,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f515,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f514]) ).
fof(f516,plain,
( ! [A,B] :
( ( ( sK26_skl(B,A) = A
| in(sK26_skl(B,A),B) )
& ( sK26_skl(B,A) != A
| ~ in(sK26_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(C,sK26_skl(B,A))],[f515]) ).
fof(f518,plain,
! [X0,X1,X2] :
( X2 != X1
| in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f531,plain,
! [A,B] :
( ( B = inclusion_relation(A)
<=> ( ! [C,D] :
( ( in(ordered_pair(C,D),B)
<=> subset(C,D) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A ) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f532,plain,
! [A,B] :
( ( ( ? [C,D] :
( ( subset(C,D)
| in(ordered_pair(C,D),B) )
& ( ~ subset(C,D)
| ~ in(ordered_pair(C,D),B) )
& in(D,A)
& in(C,A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_relation(A) ) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f531]) ).
fof(f533,plain,
! [B] :
( ( ! [A] :
( ? [C,D] :
( ( subset(C,D)
| in(ordered_pair(C,D),B) )
& ( ~ subset(C,D)
| ~ in(ordered_pair(C,D),B) )
& in(D,A)
& in(C,A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ! [A] :
( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_relation(A) ) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f532]) ).
fof(f534,plain,
! [B] :
( ( ! [A] :
( ( ( subset(sK28_skl(A,B),sK29_skl(A,B))
| in(ordered_pair(sK28_skl(A,B),sK29_skl(A,B)),B) )
& ( ~ subset(sK28_skl(A,B),sK29_skl(A,B))
| ~ in(ordered_pair(sK28_skl(A,B),sK29_skl(A,B)),B) )
& in(sK29_skl(A,B),A)
& in(sK28_skl(A,B),A) )
| relation_field(B) != A
| B = inclusion_relation(A) )
& ! [A] :
( ( ! [C,D] :
( ( ( ~ subset(C,D)
| in(ordered_pair(C,D),B) )
& ( subset(C,D)
| ~ in(ordered_pair(C,D),B) ) )
| ~ in(D,A)
| ~ in(C,A) )
& relation_field(B) = A )
| B != inclusion_relation(A) ) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(C,sK28_skl(A,B)),skolemize(D,sK29_skl(A,B))],[f533]) ).
fof(f535,plain,
! [X0,X1] :
( relation_field(X0) = X1
| X0 != inclusion_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f534]) ).
fof(f536,plain,
! [X0,X1,X2,X3] :
( subset(X2,X3)
| ~ in(ordered_pair(X2,X3),X0)
| ~ in(X3,X1)
| ~ in(X2,X1)
| X0 != inclusion_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f534]) ).
fof(f537,plain,
! [X0,X1,X2,X3] :
( ~ subset(X2,X3)
| in(ordered_pair(X2,X3),X0)
| ~ in(X3,X1)
| ~ in(X2,X1)
| X0 != inclusion_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f534]) ).
fof(f542,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f543,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f542]) ).
fof(f544,plain,
( ! [A] :
( in(sK30_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(B,sK30_skl(A))],[f543]) ).
fof(f545,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f544]) ).
fof(f547,plain,
! [A,B] :
( ( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ( ! [C] :
( ( ~ subset(C,A)
| in(C,B) )
& ( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(NNF_transformation,[status(thm)],[f36]) ).
fof(f548,plain,
( ! [A,B] :
( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(miniscoping,[status(thm)],[f547]) ).
fof(f549,plain,
( ! [A,B] :
( ( ( subset(sK31_skl(B,A),A)
| in(sK31_skl(B,A),B) )
& ( ~ subset(sK31_skl(B,A),A)
| ~ in(sK31_skl(B,A),B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl]),skolemize(C,sK31_skl(B,A))],[f548]) ).
fof(f550,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f549]) ).
fof(f551,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f549]) ).
fof(f576,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f577,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f576]) ).
fof(f578,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f577]) ).
fof(f579,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f578]) ).
fof(f581,plain,
! [X0,X1] :
( empty(X1)
| ~ element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f578]) ).
fof(f679,plain,
! [A] :
( ! [B] :
( is_antisymmetric_in(A,B)
<=> ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f680,plain,
! [A] :
( ! [B] :
( ( ? [C,D] :
( C != D
& in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
| is_antisymmetric_in(A,B) )
& ( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f679]) ).
fof(f681,plain,
! [A] :
( ( ! [B] :
( ? [C,D] :
( C != D
& in(ordered_pair(D,C),A)
& in(ordered_pair(C,D),A)
& in(D,B)
& in(C,B) )
| is_antisymmetric_in(A,B) )
& ! [B] :
( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f680]) ).
fof(f682,plain,
! [A] :
( ( ! [B] :
( ( sK57_skl(B,A) != sK58_skl(B,A)
& in(ordered_pair(sK58_skl(B,A),sK57_skl(B,A)),A)
& in(ordered_pair(sK57_skl(B,A),sK58_skl(B,A)),A)
& in(sK58_skl(B,A),B)
& in(sK57_skl(B,A),B) )
| is_antisymmetric_in(A,B) )
& ! [B] :
( ! [C,D] :
( C = D
| ~ in(ordered_pair(D,C),A)
| ~ in(ordered_pair(C,D),A)
| ~ in(D,B)
| ~ in(C,B) )
| ~ is_antisymmetric_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl,sK58_skl]),skolemize(C,sK57_skl(B,A)),skolemize(D,sK58_skl(B,A))],[f681]) ).
fof(f684,plain,
! [X0,X1] :
( in(sK57_skl(X1,X0),X1)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f686,plain,
! [X0,X1] :
( in(ordered_pair(sK57_skl(X1,X0),sK58_skl(X1,X0)),X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f687,plain,
! [X0,X1] :
( in(ordered_pair(sK58_skl(X1,X0),sK57_skl(X1,X0)),X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f688,plain,
! [X0,X1] :
( sK57_skl(X1,X0) != sK58_skl(X1,X0)
| is_antisymmetric_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f682]) ).
fof(f736,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f750,plain,
! [A] :
( relation_field(A) = set_union2(relation_dom(A),relation_rng(A))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f751,plain,
! [X0] :
( relation_field(X0) = set_union2(relation_dom(X0),relation_rng(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f750]) ).
fof(f837,plain,
! [X0] : relation(inclusion_relation(X0)),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f857,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f867,plain,
! [A,B] :
( relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f113]) ).
fof(f868,plain,
! [B] :
( ! [A] : relation(relation_rng_restriction(A,B))
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f867]) ).
fof(f869,plain,
! [X0,X1] :
( relation(relation_rng_restriction(X1,X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f868]) ).
fof(f874,plain,
! [A] : element(sK86_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK86_skl]),skolemize(B,sK86_skl(A))],[f119]) ).
fof(f875,plain,
! [X0] : element(sK86_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f874]) ).
fof(f884,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f885,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f897,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f899,plain,
! [X0,X1] : ~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f900,plain,
( ! [A] : function(identity_relation(A))
& ! [A] : relation(identity_relation(A)) ),
inference(miniscoping,[status(thm)],[f131]) ).
fof(f902,plain,
! [X0] : function(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f900]) ).
fof(f905,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f906,plain,
one_to_one(empty_set),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f913,plain,
! [X0] : ~ empty(singleton(X0)),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f960,plain,
! [A] : set_union2(A,A) = A,
inference(miniscoping,[status(thm)],[f151]) ).
fof(f961,plain,
! [X0] : set_union2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f960]) ).
fof(f978,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f996,plain,
! [A,B] :
( ( ~ in(A,B)
| subset(singleton(A),B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(NNF_transformation,[status(thm)],[f164]) ).
fof(f997,plain,
( ! [A,B] :
( ~ in(A,B)
| subset(singleton(A),B) )
& ! [A,B] :
( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(miniscoping,[status(thm)],[f996]) ).
fof(f998,plain,
! [X0,X1] :
( in(X0,X1)
| ~ subset(singleton(X0),X1) ),
inference(cnf_transformation,[status(thm)],[f997]) ).
fof(f1006,plain,
! [A] :
( ( antisymmetric(A)
<=> ! [B,C] :
( B = C
| ~ in(ordered_pair(C,B),A)
| ~ in(ordered_pair(B,C),A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f167]) ).
fof(f1007,plain,
! [A] :
( ( ( ? [B,C] :
( B != C
& in(ordered_pair(C,B),A)
& in(ordered_pair(B,C),A) )
| antisymmetric(A) )
& ( ! [B,C] :
( B = C
| ~ in(ordered_pair(C,B),A)
| ~ in(ordered_pair(B,C),A) )
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f1006]) ).
fof(f1008,plain,
! [A] :
( ( ( ( sK92_skl(A) != sK93_skl(A)
& in(ordered_pair(sK93_skl(A),sK92_skl(A)),A)
& in(ordered_pair(sK92_skl(A),sK93_skl(A)),A) )
| antisymmetric(A) )
& ( ! [B,C] :
( B = C
| ~ in(ordered_pair(C,B),A)
| ~ in(ordered_pair(B,C),A) )
| ~ antisymmetric(A) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92_skl,sK93_skl]),skolemize(B,sK92_skl(A)),skolemize(C,sK93_skl(A))],[f1007]) ).
fof(f1009,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X2,X1),X0)
| ~ in(ordered_pair(X1,X2),X0)
| ~ antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1008]) ).
fof(f1010,plain,
! [X0] :
( in(ordered_pair(sK92_skl(X0),sK93_skl(X0)),X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1008]) ).
fof(f1011,plain,
! [X0] :
( in(ordered_pair(sK93_skl(X0),sK92_skl(X0)),X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1008]) ).
fof(f1012,plain,
! [X0] :
( sK92_skl(X0) != sK93_skl(X0)
| antisymmetric(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1008]) ).
fof(f1047,plain,
( function(sK97_skl)
& relation(sK97_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK97_skl]),skolemize(A,sK97_skl)],[f175]) ).
fof(f1049,plain,
function(sK97_skl),
inference(cnf_transformation,[status(thm)],[f1047]) ).
fof(f1050,plain,
( ordinal(sK98_skl)
& epsilon_connected(sK98_skl)
& epsilon_transitive(sK98_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK98_skl]),skolemize(A,sK98_skl)],[f176]) ).
fof(f1053,plain,
ordinal(sK98_skl),
inference(cnf_transformation,[status(thm)],[f1050]) ).
fof(f1063,plain,
( function(sK102_skl)
& empty(sK102_skl)
& relation(sK102_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK102_skl]),skolemize(A,sK102_skl)],[f180]) ).
fof(f1065,plain,
empty(sK102_skl),
inference(cnf_transformation,[status(thm)],[f1063]) ).
fof(f1067,plain,
( ordinal(sK103_skl)
& epsilon_connected(sK103_skl)
& epsilon_transitive(sK103_skl)
& empty(sK103_skl)
& one_to_one(sK103_skl)
& function(sK103_skl)
& relation(sK103_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103_skl]),skolemize(A,sK103_skl)],[f181]) ).
fof(f1071,plain,
empty(sK103_skl),
inference(cnf_transformation,[status(thm)],[f1067]) ).
fof(f1075,plain,
( relation(sK104_skl)
& ~ empty(sK104_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK104_skl]),skolemize(A,sK104_skl)],[f182]) ).
fof(f1076,plain,
~ empty(sK104_skl),
inference(cnf_transformation,[status(thm)],[f1075]) ).
fof(f1077,plain,
relation(sK104_skl),
inference(cnf_transformation,[status(thm)],[f1075]) ).
fof(f1083,plain,
( one_to_one(sK107_skl)
& function(sK107_skl)
& relation(sK107_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107_skl]),skolemize(A,sK107_skl)],[f185]) ).
fof(f1085,plain,
function(sK107_skl),
inference(cnf_transformation,[status(thm)],[f1083]) ).
fof(f1086,plain,
one_to_one(sK107_skl),
inference(cnf_transformation,[status(thm)],[f1083]) ).
fof(f1087,plain,
( ordinal(sK108_skl)
& epsilon_connected(sK108_skl)
& epsilon_transitive(sK108_skl)
& ~ empty(sK108_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK108_skl]),skolemize(A,sK108_skl)],[f186]) ).
fof(f1088,plain,
~ empty(sK108_skl),
inference(cnf_transformation,[status(thm)],[f1087]) ).
fof(f1091,plain,
ordinal(sK108_skl),
inference(cnf_transformation,[status(thm)],[f1087]) ).
fof(f1092,plain,
( relation_empty_yielding(sK109_skl)
& relation(sK109_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109_skl]),skolemize(A,sK109_skl)],[f187]) ).
fof(f1093,plain,
relation(sK109_skl),
inference(cnf_transformation,[status(thm)],[f1092]) ).
fof(f1095,plain,
( function(sK110_skl)
& relation_empty_yielding(sK110_skl)
& relation(sK110_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110_skl]),skolemize(A,sK110_skl)],[f188]) ).
fof(f1098,plain,
function(sK110_skl),
inference(cnf_transformation,[status(thm)],[f1095]) ).
fof(f1129,plain,
! [X0] : in(X0,succ(X0)),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f1160,plain,
! [A,B] :
( set_union2(A,B) = B
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f210]) ).
fof(f1161,plain,
! [X0,X1] :
( set_union2(X0,X1) = X1
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1160]) ).
fof(f1162,plain,
! [A] :
? [B] :
( ! [C] :
( in(C,B)
| are_equipotent(C,B)
| ~ subset(C,B) )
& ! [C] :
( in(powerset(C),B)
| ~ in(C,B) )
& ! [C,D] :
( in(D,B)
| ~ subset(D,C)
| ~ in(C,B) )
& in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f211]) ).
fof(f1163,plain,
! [A] :
? [B] :
( ! [C] :
( in(C,B)
| are_equipotent(C,B)
| ~ subset(C,B) )
& ! [C] :
( in(powerset(C),B)
| ~ in(C,B) )
& ! [D] :
( in(D,B)
| ! [C] :
( ~ subset(D,C)
| ~ in(C,B) ) )
& in(A,B) ),
inference(miniscoping,[status(thm)],[f1162]) ).
fof(f1164,plain,
! [A] :
( ! [C] :
( in(C,sK111_skl(A))
| are_equipotent(C,sK111_skl(A))
| ~ subset(C,sK111_skl(A)) )
& ! [C] :
( in(powerset(C),sK111_skl(A))
| ~ in(C,sK111_skl(A)) )
& ! [D] :
( in(D,sK111_skl(A))
| ! [C] :
( ~ subset(D,C)
| ~ in(C,sK111_skl(A)) ) )
& in(A,sK111_skl(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK111_skl]),skolemize(B,sK111_skl(A))],[f1163]) ).
fof(f1165,plain,
! [X0] : in(X0,sK111_skl(X0)),
inference(cnf_transformation,[status(thm)],[f1164]) ).
fof(f1231,plain,
! [X0,X1] : subset(set_intersection2(X0,X1),X0),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f1241,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f1247,plain,
powerset(empty_set) = singleton(empty_set),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f1310,plain,
! [A,B] :
( set_intersection2(A,B) = A
| ~ subset(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f255]) ).
fof(f1311,plain,
! [X0,X1] :
( set_intersection2(X0,X1) = X0
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1310]) ).
fof(f1321,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f1322,plain,
! [A,B,C] :
( ( in(B,relation_field(C))
& in(A,relation_field(C)) )
| ~ in(ordered_pair(A,B),C)
| ~ relation(C) ),
inference(pre_NNF_transformation,[status(thm)],[f261]) ).
fof(f1323,plain,
! [C] :
( ! [A,B] :
( ( in(B,relation_field(C))
& in(A,relation_field(C)) )
| ~ in(ordered_pair(A,B),C) )
| ~ relation(C) ),
inference(miniscoping,[status(thm)],[f1322]) ).
fof(f1324,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1323]) ).
fof(f1325,plain,
! [X0,X1,X2] :
( in(X2,relation_field(X0))
| ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1323]) ).
fof(f1388,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f1403,plain,
! [A] :
( A = empty_set
| ~ subset(A,empty_set) ),
inference(pre_NNF_transformation,[status(thm)],[f284]) ).
fof(f1404,plain,
! [X0] :
( X0 = empty_set
| ~ subset(X0,empty_set) ),
inference(cnf_transformation,[status(thm)],[f1403]) ).
fof(f1497,plain,
? [A] : ~ antisymmetric(inclusion_relation(A)),
inference(pre_NNF_transformation,[status(thm)],[f315]) ).
fof(f1498,plain,
~ antisymmetric(inclusion_relation(sK132_skl)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132_skl]),skolemize(A,sK132_skl)],[f1497]) ).
fof(f1499,plain,
~ antisymmetric(inclusion_relation(sK132_skl)),
inference(cnf_transformation,[status(thm)],[f1498]) ).
fof(f1500,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f1501,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f316]) ).
fof(f1528,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f1529,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f325]) ).
fof(f1530,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1529]) ).
fof(f1559,plain,
! [X0,X1] : subset(X0,set_union2(X0,X1)),
inference(cnf_transformation,[status(thm)],[f334]) ).
fof(f1570,plain,
! [A,B] :
( subset(relation_dom_restriction(B,A),B)
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f337]) ).
fof(f1571,plain,
! [B] :
( ! [A] : subset(relation_dom_restriction(B,A),B)
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f1570]) ).
fof(f1572,plain,
! [X0,X1] :
( subset(relation_dom_restriction(X0,X1),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1571]) ).
fof(f1603,plain,
! [A] :
? [B] :
( ! [C] :
( in(C,B)
| are_equipotent(C,B)
| ~ subset(C,B) )
& ! [C] :
( ? [D] :
( ! [E] :
( in(E,D)
| ~ subset(E,C) )
& in(D,B) )
| ~ in(C,B) )
& ! [C,D] :
( in(D,B)
| ~ subset(D,C)
| ~ in(C,B) )
& in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f348]) ).
fof(f1604,plain,
! [A] :
? [B] :
( ! [C] :
( in(C,B)
| are_equipotent(C,B)
| ~ subset(C,B) )
& ! [C] :
( ? [D] :
( ! [E] :
( in(E,D)
| ~ subset(E,C) )
& in(D,B) )
| ~ in(C,B) )
& ! [D] :
( in(D,B)
| ! [C] :
( ~ subset(D,C)
| ~ in(C,B) ) )
& in(A,B) ),
inference(miniscoping,[status(thm)],[f1603]) ).
fof(f1605,plain,
! [A] :
( ! [C] :
( in(C,sK135_skl(A))
| are_equipotent(C,sK135_skl(A))
| ~ subset(C,sK135_skl(A)) )
& ! [C] :
( ( ! [E] :
( in(E,sK136_skl(C,A))
| ~ subset(E,C) )
& in(sK136_skl(C,A),sK135_skl(A)) )
| ~ in(C,sK135_skl(A)) )
& ! [D] :
( in(D,sK135_skl(A))
| ! [C] :
( ~ subset(D,C)
| ~ in(C,sK135_skl(A)) ) )
& in(A,sK135_skl(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK135_skl,sK136_skl]),skolemize(B,sK135_skl(A)),skolemize(D,sK136_skl(C,A))],[f1604]) ).
fof(f1606,plain,
! [X0] : in(X0,sK135_skl(X0)),
inference(cnf_transformation,[status(thm)],[f1605]) ).
fof(f1654,plain,
! [X0,X1] :
( ~ in(X1,X0)
| in(ordered_pair(X1,X1),identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f385]) ).
fof(f1655,plain,
! [X0] : subset(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f391]) ).
fof(f1682,plain,
set_meet(empty_set) = empty_set,
inference(destructive_equality_resolution,[status(thm)],[f512]) ).
fof(f1685,plain,
! [X0] : in(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f518]) ).
fof(f1689,plain,
! [X0] :
( relation_field(inclusion_relation(X0)) = X0
| ~ relation(inclusion_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f535]) ).
fof(f1690,plain,
! [X0,X1,X2] :
( subset(X1,X2)
| ~ in(ordered_pair(X1,X2),inclusion_relation(X0))
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ relation(inclusion_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f536]) ).
fof(f1691,plain,
! [X0,X1,X2] :
( ~ subset(X1,X2)
| in(ordered_pair(X1,X2),inclusion_relation(X0))
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ relation(inclusion_relation(X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f537]) ).
fof(f1696,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f545]) ).
fof(f1697,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f550]) ).
fof(f1698,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f551]) ).
fof(f1761,plain,
! [X0] : relation_field(inclusion_relation(X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f1689,f837]) ).
fof(f1762,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ in(ordered_pair(X0,X2),inclusion_relation(X1))
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1690,f837]) ).
fof(f1763,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| in(ordered_pair(X0,X2),inclusion_relation(X1))
| ~ in(X2,X1)
| ~ in(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1691,f837]) ).
fof(f1764,plain,
! [X0,X1] :
( in(ordered_pair(X0,X0),inclusion_relation(X1))
| ~ in(X0,X1)
| ~ in(X0,X1) ),
inference(resolution,[status(thm)],[f1655,f1763]) ).
fof(f1765,plain,
! [X0,X1] :
( in(ordered_pair(X0,X0),inclusion_relation(X1))
| ~ in(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1764]) ).
fof(f1789,definition,
( sQ7_spl
<=> relation(sK102_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1791,plain,
( sQ7_spl
| ~ relation(sK102_skl) ),
inference(component_clause,[status(thm)],[f1789]) ).
fof(f1797,definition,
( sQ9_spl
<=> relation(sK103_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1799,plain,
( sQ9_spl
| ~ relation(sK103_skl) ),
inference(component_clause,[status(thm)],[f1797]) ).
fof(f1831,plain,
! [X0,X1] :
( ~ in(X0,X1)
| in(ordered_pair(X0,X0),identity_relation(X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1654,f857]) ).
fof(f2001,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f375,f1241]) ).
fof(f2007,plain,
sK103_skl = empty_set,
inference(resolution,[status(thm)],[f1530,f1071]) ).
fof(f2008,plain,
sK102_skl = empty_set,
inference(resolution,[status(thm)],[f1530,f1065]) ).
fof(f2295,plain,
! [X0,X1] : subset(X0,set_union2(X1,X0)),
inference(paramodulation,[status(thm)],[f375,f1559]) ).
fof(f2303,plain,
! [X0] :
( ~ is_antisymmetric_in(inclusion_relation(X0),X0)
| antisymmetric(inclusion_relation(X0))
| ~ relation(inclusion_relation(X0)) ),
inference(paramodulation,[status(thm)],[f1761,f427]) ).
fof(f2304,plain,
! [X0] :
( ~ is_antisymmetric_in(inclusion_relation(X0),X0)
| antisymmetric(inclusion_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2303,f837]) ).
fof(f2332,definition,
( sQ28_spl
<=> relation(inclusion_relation(succ(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f2334,plain,
( sQ28_spl
| ~ relation(inclusion_relation(succ(empty_set))) ),
inference(component_clause,[status(thm)],[f2332]) ).
fof(f2895,plain,
powerset(empty_set) != empty_set,
inference(paramodulation,[status(thm)],[f1247,f978]) ).
fof(f3167,plain,
succ(empty_set) = singleton(empty_set),
inference(paramodulation,[status(thm)],[f2001,f483]) ).
fof(f3174,plain,
! [X0] : subset(X0,succ(X0)),
inference(paramodulation,[status(thm)],[f483,f1559]) ).
fof(f3177,plain,
succ(empty_set) = powerset(empty_set),
inference(forward_demodulation,[status(thm)],[f1247,f3167]) ).
fof(f3954,definition,
! [X0] :
( sQ90_spl
<=> ( in(sK23_skl(X0,empty_set,empty_set),empty_set)
| in(X0,set_meet(empty_set)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f3955,plain,
! [X0] :
( ~ sQ90_spl
| in(sK23_skl(X0,empty_set,empty_set),empty_set)
| in(X0,set_meet(empty_set)) ),
inference(component_clause,[status(thm)],[f3954]) ).
fof(f3958,plain,
! [X0] :
( ~ sQ90_spl
| in(sK23_skl(X0,empty_set,empty_set),empty_set)
| in(X0,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1682,f3955]) ).
fof(f3959,plain,
! [X0] :
( ~ sQ90_spl
| in(sK23_skl(X0,empty_set,empty_set),empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f3958,f1696]) ).
fof(f4671,plain,
! [X0,X1] : set_intersection2(X0,set_union2(X0,X1)) = X0,
inference(resolution,[status(thm)],[f1311,f1559]) ).
fof(f5006,plain,
! [X0,X1] : set_intersection2(set_union2(X0,X1),X0) = X0,
inference(paramodulation,[status(thm)],[f376,f4671]) ).
fof(f5403,plain,
! [X0,X1] : in(set_intersection2(X0,X1),powerset(X0)),
inference(resolution,[status(thm)],[f1698,f1231]) ).
fof(f5952,plain,
! [X0] :
( in(sK86_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f579,f875]) ).
fof(f5955,plain,
! [X0] :
( empty(X0)
| ~ element(X0,empty_set) ),
inference(resolution,[status(thm)],[f581,f884]) ).
fof(f6017,plain,
empty(sK86_skl(empty_set)),
inference(resolution,[status(thm)],[f5955,f875]) ).
fof(f6031,plain,
sK86_skl(empty_set) = empty_set,
inference(resolution,[status(thm)],[f6017,f1530]) ).
fof(f6684,plain,
! [X0] :
( subset(sK86_skl(powerset(X0)),X0)
| empty(powerset(X0)) ),
inference(resolution,[status(thm)],[f5952,f1697]) ).
fof(f6704,plain,
! [X0] : subset(sK86_skl(powerset(X0)),X0),
inference(forward_subsumption_resolution,[status(thm)],[f6684,f897]) ).
fof(f6934,plain,
! [X0] : set_union2(sK86_skl(powerset(X0)),X0) = X0,
inference(resolution,[status(thm)],[f6704,f1161]) ).
fof(f7869,plain,
! [X0] : set_union2(X0,sK86_skl(powerset(X0))) = X0,
inference(paramodulation,[status(thm)],[f375,f6934]) ).
fof(f9964,plain,
! [X0] : in(X0,succ(singleton(X0))),
inference(resolution,[status(thm)],[f998,f3174]) ).
fof(f9982,plain,
in(empty_set,succ(powerset(empty_set))),
inference(paramodulation,[status(thm)],[f1247,f9964]) ).
fof(f10549,plain,
! [X0] :
( antisymmetric(inclusion_relation(X0))
| in(sK57_skl(X0,inclusion_relation(X0)),X0)
| ~ relation(inclusion_relation(X0)) ),
inference(resolution,[status(thm)],[f684,f2304]) ).
fof(f10552,plain,
! [X0] :
( antisymmetric(inclusion_relation(X0))
| in(sK57_skl(X0,inclusion_relation(X0)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10549,f837]) ).
fof(f10595,plain,
in(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK132_skl),
inference(resolution,[status(thm)],[f10552,f1499]) ).
fof(f10638,plain,
in(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),identity_relation(sK132_skl)),
inference(resolution,[status(thm)],[f10595,f1831]) ).
fof(f10639,plain,
in(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)),
inference(resolution,[status(thm)],[f10595,f1765]) ).
fof(f11186,plain,
in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(identity_relation(sK132_skl))),
inference(resolution,[status(thm)],[f10638,f1831]) ).
fof(f11187,plain,
in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(identity_relation(sK132_skl))),
inference(resolution,[status(thm)],[f10638,f1765]) ).
fof(f11210,plain,
in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(inclusion_relation(sK132_skl))),
inference(resolution,[status(thm)],[f10639,f1831]) ).
fof(f11211,plain,
in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(inclusion_relation(sK132_skl))),
inference(resolution,[status(thm)],[f10639,f1765]) ).
fof(f11221,definition,
( sQ183_spl
<=> relation(inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f11223,plain,
( sQ183_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f11221]) ).
fof(f11224,definition,
( sQ184_spl
<=> antisymmetric(inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f11235,plain,
( sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11223,f837]) ).
fof(f11236,plain,
sQ183_spl,
inference(contradiction_clause,[status(thm)],[f11235]) ).
fof(f12482,definition,
( sQ227_spl
<=> is_antisymmetric_in(inclusion_relation(sK132_skl),sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f12483,plain,
( ~ sQ227_spl
| is_antisymmetric_in(inclusion_relation(sK132_skl),sK132_skl) ),
inference(component_clause,[status(thm)],[f12482]) ).
fof(f12484,plain,
( sQ227_spl
| ~ is_antisymmetric_in(inclusion_relation(sK132_skl),sK132_skl) ),
inference(component_clause,[status(thm)],[f12482]) ).
fof(f12498,plain,
( ~ sQ227_spl
| antisymmetric(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f12483,f2304]) ).
fof(f12500,plain,
( ~ sQ227_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12498,f1499]) ).
fof(f12501,plain,
~ sQ227_spl,
inference(contradiction_clause,[status(thm)],[f12500]) ).
fof(f12502,plain,
( sQ227_spl
| in(ordered_pair(sK58_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f12484,f687]) ).
fof(f12503,plain,
( sQ227_spl
| in(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK58_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f12484,f686]) ).
fof(f12506,definition,
( sQ228_spl
<=> in(ordered_pair(sK58_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition]) ).
fof(f12507,plain,
( ~ sQ228_spl
| in(ordered_pair(sK58_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f12506]) ).
fof(f12509,plain,
( sQ227_spl
| sQ228_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f12502,f11221,f12506,f12482]) ).
fof(f12510,definition,
( sQ229_spl
<=> in(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK58_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f12513,plain,
( sQ227_spl
| sQ229_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f12503,f11221,f12510,f12482]) ).
fof(f12612,definition,
( sQ242_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f12614,plain,
( sQ242_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f12612]) ).
fof(f12624,plain,
( sQ242_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12614,f905]) ).
fof(f12625,plain,
sQ242_spl,
inference(contradiction_clause,[status(thm)],[f12624]) ).
fof(f12747,plain,
! [X0] : subset(relation_dom_restriction(empty_set,X0),empty_set),
inference(resolution,[status(thm)],[f1572,f885]) ).
fof(f12997,plain,
! [X0] : relation_dom_restriction(empty_set,X0) = empty_set,
inference(resolution,[status(thm)],[f12747,f1404]) ).
fof(f13418,definition,
! [X0] :
( sQ257_spl
<=> ~ in(X0,powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition]) ).
fof(f13419,plain,
! [X0] :
( ~ sQ257_spl
| ~ in(X0,powerset(empty_set)) ),
inference(component_clause,[status(thm)],[f13418]) ).
fof(f13476,plain,
( ~ sQ257_spl
| $false ),
inference(resolution,[status(thm)],[f13419,f5403]) ).
fof(f13505,plain,
~ sQ257_spl,
inference(contradiction_clause,[status(thm)],[f13476]) ).
fof(f13517,definition,
( sQ268_spl
<=> succ(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ268_spl])],[split_symbol_definition]) ).
fof(f13518,plain,
( ~ sQ268_spl
| succ(empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f13517]) ).
fof(f13524,plain,
( ~ sQ268_spl
| powerset(empty_set) = empty_set ),
inference(forward_demodulation,[status(thm)],[f3177,f13518]) ).
fof(f13525,plain,
( ~ sQ268_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13524,f2895]) ).
fof(f13526,plain,
~ sQ268_spl,
inference(contradiction_clause,[status(thm)],[f13525]) ).
fof(f13539,plain,
! [X0] : ordered_pair(X0,X0) = unordered_pair(singleton(X0),singleton(X0)),
inference(paramodulation,[status(thm)],[f1528,f736]) ).
fof(f13574,plain,
! [X0] : ordered_pair(X0,X0) = singleton(singleton(X0)),
inference(forward_demodulation,[status(thm)],[f1528,f13539]) ).
fof(f13998,plain,
! [X0] : ordered_pair(X0,X0) != empty_set,
inference(paramodulation,[status(thm)],[f13574,f978]) ).
fof(f14184,plain,
relation_field(empty_set) = set_union2(relation_dom(empty_set),relation_rng(empty_set)),
inference(resolution,[status(thm)],[f751,f885]) ).
fof(f14185,plain,
! [X0] : relation_field(inclusion_relation(X0)) = set_union2(relation_dom(inclusion_relation(X0)),relation_rng(inclusion_relation(X0))),
inference(resolution,[status(thm)],[f751,f837]) ).
fof(f14192,plain,
relation_field(empty_set) = set_union2(empty_set,relation_rng(empty_set)),
inference(forward_demodulation,[status(thm)],[f1500,f14184]) ).
fof(f14193,plain,
relation_field(empty_set) = relation_rng(empty_set),
inference(forward_demodulation,[status(thm)],[f2001,f14192]) ).
fof(f14194,plain,
relation_field(empty_set) = empty_set,
inference(forward_demodulation,[status(thm)],[f1501,f14193]) ).
fof(f14195,plain,
! [X0] : X0 = set_union2(relation_dom(inclusion_relation(X0)),relation_rng(inclusion_relation(X0))),
inference(forward_demodulation,[status(thm)],[f1761,f14185]) ).
fof(f14312,plain,
! [X0] : subset(relation_rng(inclusion_relation(X0)),X0),
inference(paramodulation,[status(thm)],[f14195,f2295]) ).
fof(f14313,plain,
! [X0] : subset(relation_dom(inclusion_relation(X0)),X0),
inference(paramodulation,[status(thm)],[f14195,f1559]) ).
fof(f14448,definition,
( sQ271_spl
<=> in(ordered_pair(sK28_skl(relation_field(empty_set),empty_set),sK29_skl(relation_field(empty_set),empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f14449,plain,
( ~ sQ271_spl
| in(ordered_pair(sK28_skl(relation_field(empty_set),empty_set),sK29_skl(relation_field(empty_set),empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f14448]) ).
fof(f14477,definition,
( sQ278_spl
<=> in(sK29_skl(relation_field(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition]) ).
fof(f14478,plain,
( ~ sQ278_spl
| in(sK29_skl(relation_field(empty_set),empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f14477]) ).
fof(f14481,definition,
( sQ279_spl
<=> in(sK29_skl(empty_set,empty_set),relation_field(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f14482,plain,
( ~ sQ279_spl
| in(sK29_skl(empty_set,empty_set),relation_field(empty_set)) ),
inference(component_clause,[status(thm)],[f14481]) ).
fof(f14485,definition,
( sQ280_spl
<=> in(sK28_skl(relation_field(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f14486,plain,
( ~ sQ280_spl
| in(sK28_skl(relation_field(empty_set),empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f14485]) ).
fof(f14489,definition,
( sQ281_spl
<=> in(sK28_skl(empty_set,empty_set),relation_field(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition]) ).
fof(f14490,plain,
( ~ sQ281_spl
| in(sK28_skl(empty_set,empty_set),relation_field(empty_set)) ),
inference(component_clause,[status(thm)],[f14489]) ).
fof(f14513,plain,
( ~ sQ281_spl
| in(sK28_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f14490]) ).
fof(f14514,plain,
( ~ sQ281_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14513,f1696]) ).
fof(f14515,plain,
~ sQ281_spl,
inference(contradiction_clause,[status(thm)],[f14514]) ).
fof(f14516,plain,
( ~ sQ280_spl
| in(sK28_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f14486]) ).
fof(f14517,plain,
( ~ sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14516,f1696]) ).
fof(f14518,plain,
~ sQ280_spl,
inference(contradiction_clause,[status(thm)],[f14517]) ).
fof(f14519,plain,
( ~ sQ279_spl
| in(sK29_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f14482]) ).
fof(f14520,plain,
( ~ sQ279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14519,f1696]) ).
fof(f14521,plain,
~ sQ279_spl,
inference(contradiction_clause,[status(thm)],[f14520]) ).
fof(f14522,plain,
( ~ sQ278_spl
| in(sK29_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f14478]) ).
fof(f14523,plain,
( ~ sQ278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14522,f1696]) ).
fof(f14524,plain,
~ sQ278_spl,
inference(contradiction_clause,[status(thm)],[f14523]) ).
fof(f14897,definition,
( sQ304_spl
<=> in(ordered_pair(sK86_skl(empty_set),sK86_skl(empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition]) ).
fof(f14898,plain,
( ~ sQ304_spl
| in(ordered_pair(sK86_skl(empty_set),sK86_skl(empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f14897]) ).
fof(f14926,definition,
( sQ307_spl
<=> in(ordered_pair(empty_set,sK30_skl(empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition]) ).
fof(f14927,plain,
( ~ sQ307_spl
| in(ordered_pair(empty_set,sK30_skl(empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f14926]) ).
fof(f14944,definition,
( sQ309_spl
<=> in(ordered_pair(sK30_skl(empty_set),sK30_skl(empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition]) ).
fof(f14945,plain,
( ~ sQ309_spl
| in(ordered_pair(sK30_skl(empty_set),sK30_skl(empty_set)),empty_set) ),
inference(component_clause,[status(thm)],[f14944]) ).
fof(f15100,plain,
( ~ sQ309_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14945,f1696]) ).
fof(f15101,plain,
~ sQ309_spl,
inference(contradiction_clause,[status(thm)],[f15100]) ).
fof(f15102,plain,
( ~ sQ307_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14927,f1696]) ).
fof(f15103,plain,
~ sQ307_spl,
inference(contradiction_clause,[status(thm)],[f15102]) ).
fof(f15104,plain,
( ~ sQ304_spl
| in(ordered_pair(empty_set,sK86_skl(empty_set)),empty_set) ),
inference(forward_demodulation,[status(thm)],[f6031,f14898]) ).
fof(f15105,plain,
( ~ sQ304_spl
| in(ordered_pair(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f6031,f15104]) ).
fof(f15106,plain,
( ~ sQ304_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15105,f1696]) ).
fof(f15107,plain,
~ sQ304_spl,
inference(contradiction_clause,[status(thm)],[f15106]) ).
fof(f15340,definition,
( sQ326_spl
<=> relation(identity_relation(identity_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition]) ).
fof(f15342,plain,
( sQ326_spl
| ~ relation(identity_relation(identity_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f15340]) ).
fof(f15346,definition,
( sQ328_spl
<=> in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(identity_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f15348,plain,
( sQ328_spl
| ~ in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(identity_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f15346]) ).
fof(f15353,plain,
( sQ328_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15348,f11186]) ).
fof(f15354,plain,
sQ328_spl,
inference(contradiction_clause,[status(thm)],[f15353]) ).
fof(f15355,plain,
( sQ326_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15342,f857]) ).
fof(f15356,plain,
sQ326_spl,
inference(contradiction_clause,[status(thm)],[f15355]) ).
fof(f15405,plain,
! [X0] : set_union2(relation_rng(inclusion_relation(X0)),X0) = X0,
inference(resolution,[status(thm)],[f14312,f1161]) ).
fof(f15479,plain,
! [X0] : set_union2(relation_dom(inclusion_relation(X0)),X0) = X0,
inference(resolution,[status(thm)],[f14313,f1161]) ).
fof(f15708,plain,
! [X0] : set_union2(X0,relation_rng(inclusion_relation(X0))) = X0,
inference(paramodulation,[status(thm)],[f375,f15405]) ).
fof(f15824,plain,
! [X0] : set_union2(X0,relation_dom(inclusion_relation(X0))) = X0,
inference(paramodulation,[status(thm)],[f375,f15479]) ).
fof(f16199,definition,
( sQ362_spl
<=> relation(inclusion_relation(identity_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ362_spl])],[split_symbol_definition]) ).
fof(f16201,plain,
( sQ362_spl
| ~ relation(inclusion_relation(identity_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f16199]) ).
fof(f16205,definition,
( sQ364_spl
<=> in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(identity_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition]) ).
fof(f16207,plain,
( sQ364_spl
| ~ in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(identity_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f16205]) ).
fof(f16209,plain,
( sQ364_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16207,f11187]) ).
fof(f16210,plain,
sQ364_spl,
inference(contradiction_clause,[status(thm)],[f16209]) ).
fof(f16211,plain,
( sQ362_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16201,f837]) ).
fof(f16212,plain,
sQ362_spl,
inference(contradiction_clause,[status(thm)],[f16211]) ).
fof(f16758,definition,
( sQ390_spl
<=> powerset(empty_set) = powerset(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f16760,plain,
( sQ390_spl
| powerset(empty_set) != powerset(empty_set) ),
inference(component_clause,[status(thm)],[f16758]) ).
fof(f16762,plain,
( sQ390_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16760]) ).
fof(f16763,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f16762]) ).
fof(f17218,definition,
( sQ420_spl
<=> ordinal(sK108_skl) ),
introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition]) ).
fof(f17220,plain,
( sQ420_spl
| ~ ordinal(sK108_skl) ),
inference(component_clause,[status(thm)],[f17218]) ).
fof(f17234,plain,
( sQ420_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17220,f1091]) ).
fof(f17235,plain,
sQ420_spl,
inference(contradiction_clause,[status(thm)],[f17234]) ).
fof(f17374,definition,
( sQ429_spl
<=> ordinal(sK98_skl) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f17376,plain,
( sQ429_spl
| ~ ordinal(sK98_skl) ),
inference(component_clause,[status(thm)],[f17374]) ).
fof(f17390,plain,
( sQ429_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17376,f1053]) ).
fof(f17391,plain,
sQ429_spl,
inference(contradiction_clause,[status(thm)],[f17390]) ).
fof(f17397,definition,
( sQ433_spl
<=> function(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition]) ).
fof(f17399,plain,
( sQ433_spl
| ~ function(sK107_skl) ),
inference(component_clause,[status(thm)],[f17397]) ).
fof(f17415,plain,
( sQ433_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17399,f1085]) ).
fof(f17416,plain,
sQ433_spl,
inference(contradiction_clause,[status(thm)],[f17415]) ).
fof(f17430,definition,
( sQ436_spl
<=> relation(identity_relation(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f17432,plain,
( sQ436_spl
| ~ relation(identity_relation(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f17430]) ).
fof(f17436,definition,
( sQ438_spl
<=> in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition]) ).
fof(f17438,plain,
( sQ438_spl
| ~ in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),identity_relation(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f17436]) ).
fof(f17440,plain,
( sQ438_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17438,f11210]) ).
fof(f17441,plain,
sQ438_spl,
inference(contradiction_clause,[status(thm)],[f17440]) ).
fof(f17442,plain,
( sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17432,f857]) ).
fof(f17443,plain,
sQ436_spl,
inference(contradiction_clause,[status(thm)],[f17442]) ).
fof(f17632,definition,
! [X0] :
( sQ439_spl
<=> set_difference(X0,empty_set) != X0 ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f17633,plain,
! [X0] :
( ~ sQ439_spl
| set_difference(X0,empty_set) != X0 ),
inference(component_clause,[status(thm)],[f17632]) ).
fof(f17636,plain,
! [X0] :
( ~ sQ439_spl
| X0 != X0 ),
inference(forward_demodulation,[status(thm)],[f1388,f17633]) ).
fof(f17637,plain,
( ~ sQ439_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17636]) ).
fof(f17638,plain,
~ sQ439_spl,
inference(contradiction_clause,[status(thm)],[f17637]) ).
fof(f17714,definition,
( sQ440_spl
<=> relation(inclusion_relation(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition]) ).
fof(f17716,plain,
( sQ440_spl
| ~ relation(inclusion_relation(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f17714]) ).
fof(f17720,definition,
( sQ442_spl
<=> in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f17722,plain,
( sQ442_spl
| ~ in(ordered_pair(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl))),ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))),inclusion_relation(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f17720]) ).
fof(f17724,plain,
( sQ442_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17722,f11211]) ).
fof(f17725,plain,
sQ442_spl,
inference(contradiction_clause,[status(thm)],[f17724]) ).
fof(f17726,plain,
( sQ440_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17716,f837]) ).
fof(f17727,plain,
sQ440_spl,
inference(contradiction_clause,[status(thm)],[f17726]) ).
fof(f18628,plain,
( sQ28_spl
| ~ relation(inclusion_relation(powerset(empty_set))) ),
inference(forward_demodulation,[status(thm)],[f3177,f2334]) ).
fof(f18629,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18628,f837]) ).
fof(f18630,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f18629]) ).
fof(f18633,plain,
( sQ9_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f2007,f1799]) ).
fof(f18634,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18633,f885]) ).
fof(f18635,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f18634]) ).
fof(f18636,plain,
( sQ7_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f2008,f1791]) ).
fof(f18637,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18636,f885]) ).
fof(f18638,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f18637]) ).
fof(f18639,plain,
( ~ sQ271_spl
| in(ordered_pair(sK28_skl(empty_set,empty_set),sK29_skl(relation_field(empty_set),empty_set)),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f14449]) ).
fof(f18640,plain,
( ~ sQ271_spl
| in(ordered_pair(sK28_skl(empty_set,empty_set),sK29_skl(empty_set,empty_set)),empty_set) ),
inference(forward_demodulation,[status(thm)],[f14194,f18639]) ).
fof(f18641,plain,
( ~ sQ271_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f18640,f1696]) ).
fof(f18642,plain,
~ sQ271_spl,
inference(contradiction_clause,[status(thm)],[f18641]) ).
fof(f19297,definition,
( sQ476_spl
<=> one_to_one(sK107_skl) ),
introduced(definition,[new_symbols(definition,[sQ476_spl])],[split_symbol_definition]) ).
fof(f19299,plain,
( sQ476_spl
| ~ one_to_one(sK107_skl) ),
inference(component_clause,[status(thm)],[f19297]) ).
fof(f19311,definition,
( sQ480_spl
<=> one_to_one(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition]) ).
fof(f19313,plain,
( sQ480_spl
| ~ one_to_one(empty_set) ),
inference(component_clause,[status(thm)],[f19311]) ).
fof(f19318,plain,
( sQ480_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19313,f906]) ).
fof(f19319,plain,
sQ480_spl,
inference(contradiction_clause,[status(thm)],[f19318]) ).
fof(f19320,plain,
( sQ476_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19299,f1086]) ).
fof(f19321,plain,
sQ476_spl,
inference(contradiction_clause,[status(thm)],[f19320]) ).
fof(f19442,definition,
( sQ485_spl
<=> function(sK97_skl) ),
introduced(definition,[new_symbols(definition,[sQ485_spl])],[split_symbol_definition]) ).
fof(f19444,plain,
( sQ485_spl
| ~ function(sK97_skl) ),
inference(component_clause,[status(thm)],[f19442]) ).
fof(f19461,plain,
( sQ485_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19444,f1049]) ).
fof(f19462,plain,
sQ485_spl,
inference(contradiction_clause,[status(thm)],[f19461]) ).
fof(f19468,definition,
( sQ490_spl
<=> function(sK110_skl) ),
introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition]) ).
fof(f19470,plain,
( sQ490_spl
| ~ function(sK110_skl) ),
inference(component_clause,[status(thm)],[f19468]) ).
fof(f19487,plain,
( sQ490_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19470,f1098]) ).
fof(f19488,plain,
sQ490_spl,
inference(contradiction_clause,[status(thm)],[f19487]) ).
fof(f19562,definition,
( sQ504_spl
<=> powerset(empty_set) = relation_rng(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ504_spl])],[split_symbol_definition]) ).
fof(f19563,plain,
( ~ sQ504_spl
| powerset(empty_set) = relation_rng(empty_set) ),
inference(component_clause,[status(thm)],[f19562]) ).
fof(f19569,plain,
( ~ sQ504_spl
| powerset(empty_set) = empty_set ),
inference(forward_demodulation,[status(thm)],[f1501,f19563]) ).
fof(f19570,plain,
( ~ sQ504_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19569,f2895]) ).
fof(f19571,plain,
~ sQ504_spl,
inference(contradiction_clause,[status(thm)],[f19570]) ).
fof(f20108,plain,
( ~ sQ228_spl
| sK57_skl(sK132_skl,inclusion_relation(sK132_skl)) = sK58_skl(sK132_skl,inclusion_relation(sK132_skl))
| ~ in(ordered_pair(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)),sK58_skl(sK132_skl,inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))
| ~ antisymmetric(inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f12507,f1009]) ).
fof(f20118,definition,
( sQ566_spl
<=> sK57_skl(sK132_skl,inclusion_relation(sK132_skl)) = sK58_skl(sK132_skl,inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f20119,plain,
( ~ sQ566_spl
| sK57_skl(sK132_skl,inclusion_relation(sK132_skl)) = sK58_skl(sK132_skl,inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f20118]) ).
fof(f20121,plain,
( ~ sQ228_spl
| sQ566_spl
| ~ sQ229_spl
| ~ sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f20108,f11221,f11224,f12510,f20118,f12506]) ).
fof(f20712,plain,
( ~ sQ566_spl
| is_antisymmetric_in(inclusion_relation(sK132_skl),sK132_skl)
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f20119,f688]) ).
fof(f20719,plain,
( ~ sQ566_spl
| sQ227_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f20712,f11221,f12482,f20118]) ).
fof(f22364,definition,
! [X0,X1] :
( sQ654_spl
<=> ( ~ relation(inclusion_relation(X1))
| ~ relation(relation_rng_restriction(X0,inclusion_relation(X1))) ) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f22365,plain,
! [X0,X1] :
( ~ sQ654_spl
| ~ relation(inclusion_relation(X1))
| ~ relation(relation_rng_restriction(X0,inclusion_relation(X1))) ),
inference(component_clause,[status(thm)],[f22364]) ).
fof(f24572,definition,
( sQ723_spl
<=> in(sK132_skl,singleton(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ723_spl])],[split_symbol_definition]) ).
fof(f24574,plain,
( sQ723_spl
| ~ in(sK132_skl,singleton(sK132_skl)) ),
inference(component_clause,[status(thm)],[f24572]) ).
fof(f24579,definition,
( sQ725_spl
<=> in(sK132_skl,succ(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition]) ).
fof(f24581,plain,
( sQ725_spl
| ~ in(sK132_skl,succ(sK132_skl)) ),
inference(component_clause,[status(thm)],[f24579]) ).
fof(f24586,definition,
( sQ727_spl
<=> in(sK132_skl,sK111_skl(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ727_spl])],[split_symbol_definition]) ).
fof(f24588,plain,
( sQ727_spl
| ~ in(sK132_skl,sK111_skl(sK132_skl)) ),
inference(component_clause,[status(thm)],[f24586]) ).
fof(f24593,definition,
( sQ729_spl
<=> in(sK132_skl,sK135_skl(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ729_spl])],[split_symbol_definition]) ).
fof(f24595,plain,
( sQ729_spl
| ~ in(sK132_skl,sK135_skl(sK132_skl)) ),
inference(component_clause,[status(thm)],[f24593]) ).
fof(f24628,definition,
( sQ735_spl
<=> empty(singleton(sK58_skl(sK132_skl,inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ735_spl])],[split_symbol_definition]) ).
fof(f24629,plain,
( ~ sQ735_spl
| empty(singleton(sK58_skl(sK132_skl,inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f24628]) ).
fof(f24667,plain,
( ~ sQ735_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24629,f913]) ).
fof(f24668,plain,
~ sQ735_spl,
inference(contradiction_clause,[status(thm)],[f24667]) ).
fof(f24669,plain,
( sQ729_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24595,f1606]) ).
fof(f24670,plain,
sQ729_spl,
inference(contradiction_clause,[status(thm)],[f24669]) ).
fof(f24671,plain,
( sQ727_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24588,f1165]) ).
fof(f24672,plain,
sQ727_spl,
inference(contradiction_clause,[status(thm)],[f24671]) ).
fof(f24673,plain,
( sQ725_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24581,f1129]) ).
fof(f24674,plain,
sQ725_spl,
inference(contradiction_clause,[status(thm)],[f24673]) ).
fof(f24675,plain,
( sQ723_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24574,f1685]) ).
fof(f24676,plain,
sQ723_spl,
inference(contradiction_clause,[status(thm)],[f24675]) ).
fof(f24811,definition,
( sQ752_spl
<=> empty(singleton(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ752_spl])],[split_symbol_definition]) ).
fof(f24812,plain,
( ~ sQ752_spl
| empty(singleton(sK57_skl(sK132_skl,inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f24811]) ).
fof(f26201,plain,
( in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f1010,f1499]) ).
fof(f26239,definition,
( sQ850_spl
<=> in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ850_spl])],[split_symbol_definition]) ).
fof(f26240,plain,
( ~ sQ850_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f26239]) ).
fof(f26242,plain,
( sQ850_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f26201,f11221,f26239]) ).
fof(f26260,plain,
( ~ sQ850_spl
| subset(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl)))
| ~ in(sK93_skl(inclusion_relation(sK132_skl)),sK132_skl)
| ~ in(sK92_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(resolution,[status(thm)],[f26240,f1762]) ).
fof(f26268,definition,
( sQ851_spl
<=> in(sK92_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ851_spl])],[split_symbol_definition]) ).
fof(f26270,plain,
( sQ851_spl
| ~ in(sK92_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(component_clause,[status(thm)],[f26268]) ).
fof(f26271,definition,
( sQ852_spl
<=> in(sK93_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ852_spl])],[split_symbol_definition]) ).
fof(f26273,plain,
( sQ852_spl
| ~ in(sK93_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(component_clause,[status(thm)],[f26271]) ).
fof(f26274,definition,
( sQ853_spl
<=> subset(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ853_spl])],[split_symbol_definition]) ).
fof(f26275,plain,
( ~ sQ853_spl
| subset(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f26274]) ).
fof(f26277,plain,
( ~ sQ850_spl
| sQ853_spl
| ~ sQ852_spl
| ~ sQ851_spl ),
inference(split_clause,[status(thm)],[f26260,f26268,f26271,f26274,f26239]) ).
fof(f26278,definition,
( sQ854_spl
<=> in(ordered_pair(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ854_spl])],[split_symbol_definition]) ).
fof(f26279,plain,
( ~ sQ854_spl
| in(ordered_pair(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f26278]) ).
fof(f26281,definition,
( sQ855_spl
<=> sK93_skl(inclusion_relation(sK132_skl)) = sK92_skl(inclusion_relation(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ855_spl])],[split_symbol_definition]) ).
fof(f26282,plain,
( ~ sQ855_spl
| sK93_skl(inclusion_relation(sK132_skl)) = sK92_skl(inclusion_relation(sK132_skl)) ),
inference(component_clause,[status(thm)],[f26281]) ).
fof(f26332,plain,
( in(ordered_pair(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f1011,f1499]) ).
fof(f26362,plain,
( sQ854_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f26332,f11221,f26278]) ).
fof(f26406,plain,
( ~ sQ752_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24812,f913]) ).
fof(f26407,plain,
~ sQ752_spl,
inference(contradiction_clause,[status(thm)],[f26406]) ).
fof(f26463,plain,
! [X0] :
( ~ sQ654_spl
| ~ relation(inclusion_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f22365,f869]) ).
fof(f26769,plain,
( ~ sQ654_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f26463,f837]) ).
fof(f26770,plain,
~ sQ654_spl,
inference(contradiction_clause,[status(thm)],[f26769]) ).
fof(f27040,definition,
( sQ903_spl
<=> in(empty_set,succ(powerset(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ903_spl])],[split_symbol_definition]) ).
fof(f27042,plain,
( sQ903_spl
| ~ in(empty_set,succ(powerset(empty_set))) ),
inference(component_clause,[status(thm)],[f27040]) ).
fof(f27055,plain,
( sQ903_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27042,f9982]) ).
fof(f27056,plain,
sQ903_spl,
inference(contradiction_clause,[status(thm)],[f27055]) ).
fof(f27144,definition,
( sQ907_spl
<=> in(inclusion_relation(sK132_skl),singleton(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ907_spl])],[split_symbol_definition]) ).
fof(f27146,plain,
( sQ907_spl
| ~ in(inclusion_relation(sK132_skl),singleton(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f27144]) ).
fof(f27151,definition,
( sQ909_spl
<=> in(inclusion_relation(sK132_skl),succ(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ909_spl])],[split_symbol_definition]) ).
fof(f27153,plain,
( sQ909_spl
| ~ in(inclusion_relation(sK132_skl),succ(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f27151]) ).
fof(f27158,definition,
( sQ911_spl
<=> in(inclusion_relation(sK132_skl),sK111_skl(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ911_spl])],[split_symbol_definition]) ).
fof(f27160,plain,
( sQ911_spl
| ~ in(inclusion_relation(sK132_skl),sK111_skl(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f27158]) ).
fof(f27165,definition,
( sQ913_spl
<=> in(inclusion_relation(sK132_skl),sK135_skl(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ913_spl])],[split_symbol_definition]) ).
fof(f27167,plain,
( sQ913_spl
| ~ in(inclusion_relation(sK132_skl),sK135_skl(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f27165]) ).
fof(f27186,definition,
( sQ915_spl
<=> empty(singleton(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ915_spl])],[split_symbol_definition]) ).
fof(f27187,plain,
( ~ sQ915_spl
| empty(singleton(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))))) ),
inference(component_clause,[status(thm)],[f27186]) ).
fof(f27225,plain,
( sQ907_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27146,f1685]) ).
fof(f27226,plain,
sQ907_spl,
inference(contradiction_clause,[status(thm)],[f27225]) ).
fof(f27227,plain,
( sQ909_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27153,f1129]) ).
fof(f27228,plain,
sQ909_spl,
inference(contradiction_clause,[status(thm)],[f27227]) ).
fof(f27229,plain,
( sQ911_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27160,f1165]) ).
fof(f27230,plain,
sQ911_spl,
inference(contradiction_clause,[status(thm)],[f27229]) ).
fof(f27231,plain,
( sQ913_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27167,f1606]) ).
fof(f27232,plain,
sQ913_spl,
inference(contradiction_clause,[status(thm)],[f27231]) ).
fof(f27233,plain,
( ~ sQ915_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27187,f913]) ).
fof(f27234,plain,
~ sQ915_spl,
inference(contradiction_clause,[status(thm)],[f27233]) ).
fof(f27306,definition,
! [X0] :
( sQ926_spl
<=> empty_set = singleton(X0) ),
introduced(definition,[new_symbols(definition,[sQ926_spl])],[split_symbol_definition]) ).
fof(f27307,plain,
! [X0] :
( ~ sQ926_spl
| empty_set = singleton(X0) ),
inference(component_clause,[status(thm)],[f27306]) ).
fof(f27311,plain,
( ~ sQ926_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27307,f978]) ).
fof(f27312,plain,
~ sQ926_spl,
inference(contradiction_clause,[status(thm)],[f27311]) ).
fof(f27826,definition,
( sQ937_spl
<=> relation(relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ937_spl])],[split_symbol_definition]) ).
fof(f27828,plain,
( sQ937_spl
| ~ relation(relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f27826]) ).
fof(f27830,plain,
( sQ937_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f27828]) ).
fof(f27831,plain,
( sQ937_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27830,f885]) ).
fof(f27832,plain,
sQ937_spl,
inference(contradiction_clause,[status(thm)],[f27831]) ).
fof(f27835,definition,
( sQ938_spl
<=> relation(relation_rng(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ938_spl])],[split_symbol_definition]) ).
fof(f27837,plain,
( sQ938_spl
| ~ relation(relation_rng(empty_set)) ),
inference(component_clause,[status(thm)],[f27835]) ).
fof(f27839,plain,
( sQ938_spl
| ~ relation(empty_set) ),
inference(forward_demodulation,[status(thm)],[f1501,f27837]) ).
fof(f27840,plain,
( sQ938_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f27839,f885]) ).
fof(f27841,plain,
sQ938_spl,
inference(contradiction_clause,[status(thm)],[f27840]) ).
fof(f28082,plain,
( ~ sQ853_spl
| ~ subset(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))
| sK93_skl(inclusion_relation(sK132_skl)) = sK92_skl(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f26275,f393]) ).
fof(f28083,definition,
( sQ947_spl
<=> subset(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition]) ).
fof(f28086,plain,
( ~ sQ853_spl
| ~ sQ947_spl
| sQ855_spl ),
inference(split_clause,[status(thm)],[f28082,f26281,f28083,f26274]) ).
fof(f28200,plain,
( ~ sQ854_spl
| subset(sK93_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))
| ~ in(sK92_skl(inclusion_relation(sK132_skl)),sK132_skl)
| ~ in(sK93_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(resolution,[status(thm)],[f26279,f1762]) ).
fof(f28203,plain,
( ~ sQ854_spl
| sQ947_spl
| ~ sQ851_spl
| ~ sQ852_spl ),
inference(split_clause,[status(thm)],[f28200,f26271,f26268,f28083,f26278]) ).
fof(f28207,plain,
( ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3959,f1696]) ).
fof(f28208,plain,
~ sQ90_spl,
inference(contradiction_clause,[status(thm)],[f28207]) ).
fof(f28931,definition,
( sQ969_spl
<=> in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),relation_dom(relation_dom_restriction(empty_set,inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ969_spl])],[split_symbol_definition]) ).
fof(f28932,plain,
( ~ sQ969_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),relation_dom(relation_dom_restriction(empty_set,inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f28931]) ).
fof(f28938,plain,
( ~ sQ969_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f12997,f28932]) ).
fof(f28939,plain,
( ~ sQ969_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK93_skl(inclusion_relation(sK132_skl))),empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f28938]) ).
fof(f28940,plain,
( ~ sQ969_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28939,f1696]) ).
fof(f28941,plain,
~ sQ969_spl,
inference(contradiction_clause,[status(thm)],[f28940]) ).
fof(f29212,definition,
( sQ973_spl
<=> subset(empty_set,relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ973_spl])],[split_symbol_definition]) ).
fof(f29214,plain,
( sQ973_spl
| ~ subset(empty_set,relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f29212]) ).
fof(f29220,plain,
( sQ973_spl
| ~ subset(empty_set,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f29214]) ).
fof(f29221,plain,
( sQ973_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29220,f1321]) ).
fof(f29222,plain,
sQ973_spl,
inference(contradiction_clause,[status(thm)],[f29221]) ).
fof(f29559,definition,
( sQ993_spl
<=> relation(set_union2(relation_rng(inclusion_relation(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ993_spl])],[split_symbol_definition]) ).
fof(f29561,plain,
( sQ993_spl
| ~ relation(set_union2(relation_rng(inclusion_relation(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f29559]) ).
fof(f29566,definition,
( sQ995_spl
<=> relation(set_union2(relation_dom(inclusion_relation(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ995_spl])],[split_symbol_definition]) ).
fof(f29568,plain,
( sQ995_spl
| ~ relation(set_union2(relation_dom(inclusion_relation(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f29566]) ).
fof(f29573,definition,
( sQ997_spl
<=> relation(set_union2(sK86_skl(powerset(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ997_spl])],[split_symbol_definition]) ).
fof(f29575,plain,
( sQ997_spl
| ~ relation(set_union2(sK86_skl(powerset(inclusion_relation(sK132_skl))),inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f29573]) ).
fof(f29609,definition,
( sQ1007_spl
<=> relation(set_union2(empty_set,inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1007_spl])],[split_symbol_definition]) ).
fof(f29611,plain,
( sQ1007_spl
| ~ relation(set_union2(empty_set,inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f29609]) ).
fof(f29616,definition,
( sQ1009_spl
<=> relation(set_union2(inclusion_relation(sK132_skl),inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1009_spl])],[split_symbol_definition]) ).
fof(f29618,plain,
( sQ1009_spl
| ~ relation(set_union2(inclusion_relation(sK132_skl),inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f29616]) ).
fof(f29626,plain,
( sQ1009_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f961,f29618]) ).
fof(f29627,plain,
( sQ1009_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29626,f837]) ).
fof(f29628,plain,
sQ1009_spl,
inference(contradiction_clause,[status(thm)],[f29627]) ).
fof(f29632,plain,
( sQ1007_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f2001,f29611]) ).
fof(f29633,plain,
( sQ1007_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29632,f837]) ).
fof(f29634,plain,
sQ1007_spl,
inference(contradiction_clause,[status(thm)],[f29633]) ).
fof(f29651,plain,
( sQ997_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f6934,f29575]) ).
fof(f29652,plain,
( sQ997_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29651,f837]) ).
fof(f29653,plain,
sQ997_spl,
inference(contradiction_clause,[status(thm)],[f29652]) ).
fof(f29657,plain,
( sQ995_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f15479,f29568]) ).
fof(f29658,plain,
( sQ995_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29657,f837]) ).
fof(f29659,plain,
sQ995_spl,
inference(contradiction_clause,[status(thm)],[f29658]) ).
fof(f29663,plain,
( sQ993_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f15405,f29561]) ).
fof(f29664,plain,
( sQ993_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29663,f837]) ).
fof(f29665,plain,
sQ993_spl,
inference(contradiction_clause,[status(thm)],[f29664]) ).
fof(f30185,definition,
( sQ1029_spl
<=> relation(set_union2(inclusion_relation(sK132_skl),relation_dom(inclusion_relation(inclusion_relation(sK132_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ1029_spl])],[split_symbol_definition]) ).
fof(f30187,plain,
( sQ1029_spl
| ~ relation(set_union2(inclusion_relation(sK132_skl),relation_dom(inclusion_relation(inclusion_relation(sK132_skl))))) ),
inference(component_clause,[status(thm)],[f30185]) ).
fof(f30192,definition,
( sQ1031_spl
<=> relation(set_union2(inclusion_relation(sK132_skl),relation_rng(inclusion_relation(inclusion_relation(sK132_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ1031_spl])],[split_symbol_definition]) ).
fof(f30194,plain,
( sQ1031_spl
| ~ relation(set_union2(inclusion_relation(sK132_skl),relation_rng(inclusion_relation(inclusion_relation(sK132_skl))))) ),
inference(component_clause,[status(thm)],[f30192]) ).
fof(f30199,definition,
( sQ1033_spl
<=> relation(set_union2(inclusion_relation(sK132_skl),sK86_skl(powerset(inclusion_relation(sK132_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ1033_spl])],[split_symbol_definition]) ).
fof(f30201,plain,
( sQ1033_spl
| ~ relation(set_union2(inclusion_relation(sK132_skl),sK86_skl(powerset(inclusion_relation(sK132_skl))))) ),
inference(component_clause,[status(thm)],[f30199]) ).
fof(f30232,definition,
( sQ1042_spl
<=> relation(set_union2(inclusion_relation(sK132_skl),empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1042_spl])],[split_symbol_definition]) ).
fof(f30234,plain,
( sQ1042_spl
| ~ relation(set_union2(inclusion_relation(sK132_skl),empty_set)) ),
inference(component_clause,[status(thm)],[f30232]) ).
fof(f30241,plain,
( sQ1042_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f1241,f30234]) ).
fof(f30242,plain,
( sQ1042_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30241,f837]) ).
fof(f30243,plain,
sQ1042_spl,
inference(contradiction_clause,[status(thm)],[f30242]) ).
fof(f30258,plain,
( sQ1033_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f7869,f30201]) ).
fof(f30259,plain,
( sQ1033_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30258,f837]) ).
fof(f30260,plain,
sQ1033_spl,
inference(contradiction_clause,[status(thm)],[f30259]) ).
fof(f30262,plain,
( sQ1031_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f15708,f30194]) ).
fof(f30263,plain,
( sQ1031_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30262,f837]) ).
fof(f30264,plain,
sQ1031_spl,
inference(contradiction_clause,[status(thm)],[f30263]) ).
fof(f30266,plain,
( sQ1029_spl
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(forward_demodulation,[status(thm)],[f15824,f30187]) ).
fof(f30267,plain,
( sQ1029_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30266,f837]) ).
fof(f30268,plain,
sQ1029_spl,
inference(contradiction_clause,[status(thm)],[f30267]) ).
fof(f30900,definition,
( sQ1091_spl
<=> empty(singleton(sK21_skl(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1091_spl])],[split_symbol_definition]) ).
fof(f30901,plain,
( ~ sQ1091_spl
| empty(singleton(sK21_skl(sK132_skl))) ),
inference(component_clause,[status(thm)],[f30900]) ).
fof(f30905,plain,
( ~ sQ1091_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30901,f913]) ).
fof(f30906,plain,
~ sQ1091_spl,
inference(contradiction_clause,[status(thm)],[f30905]) ).
fof(f32524,plain,
( ~ sQ850_spl
| in(sK92_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl)))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f1324,f26240]) ).
fof(f32566,definition,
( sQ1189_spl
<=> in(sK92_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1189_spl])],[split_symbol_definition]) ).
fof(f32567,plain,
( ~ sQ1189_spl
| in(sK92_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f32566]) ).
fof(f32569,plain,
( ~ sQ850_spl
| sQ1189_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f32524,f11221,f32566,f26239]) ).
fof(f32586,plain,
( ~ sQ1189_spl
| in(sK92_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(forward_demodulation,[status(thm)],[f1761,f32567]) ).
fof(f32587,plain,
( ~ sQ850_spl
| in(sK93_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl)))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f1325,f26240]) ).
fof(f32629,definition,
( sQ1190_spl
<=> in(sK93_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1190_spl])],[split_symbol_definition]) ).
fof(f32630,plain,
( ~ sQ1190_spl
| in(sK93_skl(inclusion_relation(sK132_skl)),relation_field(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f32629]) ).
fof(f32632,plain,
( ~ sQ850_spl
| sQ1190_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f32587,f11221,f32629,f26239]) ).
fof(f32667,plain,
( ~ sQ1190_spl
| in(sK93_skl(inclusion_relation(sK132_skl)),sK132_skl) ),
inference(forward_demodulation,[status(thm)],[f1761,f32630]) ).
fof(f32796,plain,
( ~ sQ1189_spl
| sQ851_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32586,f26270]) ).
fof(f32797,plain,
( ~ sQ1189_spl
| sQ851_spl ),
inference(contradiction_clause,[status(thm)],[f32796]) ).
fof(f32798,plain,
( ~ sQ1190_spl
| sQ852_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32667,f26273]) ).
fof(f32799,plain,
( ~ sQ1190_spl
| sQ852_spl ),
inference(contradiction_clause,[status(thm)],[f32798]) ).
fof(f33374,definition,
! [X0] :
( sQ1214_spl
<=> ~ relation(set_intersection2(sK109_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ1214_spl])],[split_symbol_definition]) ).
fof(f33375,plain,
! [X0] :
( ~ sQ1214_spl
| ~ relation(set_intersection2(sK109_skl,X0)) ),
inference(component_clause,[status(thm)],[f33374]) ).
fof(f33378,definition,
! [X0] :
( sQ1215_spl
<=> ~ relation(set_intersection2(X0,sK109_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1215_spl])],[split_symbol_definition]) ).
fof(f33379,plain,
! [X0] :
( ~ sQ1215_spl
| ~ relation(set_intersection2(X0,sK109_skl)) ),
inference(component_clause,[status(thm)],[f33378]) ).
fof(f33382,definition,
! [X0] :
( sQ1216_spl
<=> ~ relation(set_difference(sK109_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ1216_spl])],[split_symbol_definition]) ).
fof(f33383,plain,
! [X0] :
( ~ sQ1216_spl
| ~ relation(set_difference(sK109_skl,X0)) ),
inference(component_clause,[status(thm)],[f33382]) ).
fof(f33394,plain,
( ~ sQ1216_spl
| ~ relation(sK109_skl) ),
inference(paramodulation,[status(thm)],[f1388,f33383]) ).
fof(f33399,plain,
( ~ sQ1216_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33394,f1093]) ).
fof(f33400,plain,
~ sQ1216_spl,
inference(contradiction_clause,[status(thm)],[f33399]) ).
fof(f33401,plain,
( ~ sQ1215_spl
| ~ relation(sK109_skl) ),
inference(paramodulation,[status(thm)],[f5006,f33379]) ).
fof(f33408,plain,
( ~ sQ1215_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33401,f1093]) ).
fof(f33409,plain,
~ sQ1215_spl,
inference(contradiction_clause,[status(thm)],[f33408]) ).
fof(f33410,plain,
( ~ sQ1214_spl
| ~ relation(sK109_skl) ),
inference(paramodulation,[status(thm)],[f4671,f33375]) ).
fof(f33417,plain,
( ~ sQ1214_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33410,f1093]) ).
fof(f33418,plain,
~ sQ1214_spl,
inference(contradiction_clause,[status(thm)],[f33417]) ).
fof(f33446,definition,
( sQ1219_spl
<=> in(sK121_skl(empty_set,empty_set),relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1219_spl])],[split_symbol_definition]) ).
fof(f33447,plain,
( ~ sQ1219_spl
| in(sK121_skl(empty_set,empty_set),relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f33446]) ).
fof(f33454,definition,
( sQ1220_spl
<=> in(sK121_skl(relation_dom(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1220_spl])],[split_symbol_definition]) ).
fof(f33455,plain,
( ~ sQ1220_spl
| in(sK121_skl(relation_dom(empty_set),empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f33454]) ).
fof(f33459,plain,
( ~ sQ1220_spl
| in(sK121_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f33455]) ).
fof(f33460,plain,
( ~ sQ1220_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33459,f1696]) ).
fof(f33461,plain,
~ sQ1220_spl,
inference(contradiction_clause,[status(thm)],[f33460]) ).
fof(f33462,plain,
( ~ sQ1219_spl
| in(sK121_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f33447]) ).
fof(f33463,plain,
( ~ sQ1219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f33462,f1696]) ).
fof(f33464,plain,
~ sQ1219_spl,
inference(contradiction_clause,[status(thm)],[f33463]) ).
fof(f34187,definition,
! [X0] :
( sQ1276_spl
<=> ~ relation(set_intersection2(sK104_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ1276_spl])],[split_symbol_definition]) ).
fof(f34188,plain,
! [X0] :
( ~ sQ1276_spl
| ~ relation(set_intersection2(sK104_skl,X0)) ),
inference(component_clause,[status(thm)],[f34187]) ).
fof(f34191,definition,
! [X0] :
( sQ1277_spl
<=> ~ relation(set_intersection2(X0,sK104_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1277_spl])],[split_symbol_definition]) ).
fof(f34192,plain,
! [X0] :
( ~ sQ1277_spl
| ~ relation(set_intersection2(X0,sK104_skl)) ),
inference(component_clause,[status(thm)],[f34191]) ).
fof(f34195,definition,
! [X0] :
( sQ1278_spl
<=> ~ relation(set_difference(sK104_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ1278_spl])],[split_symbol_definition]) ).
fof(f34196,plain,
! [X0] :
( ~ sQ1278_spl
| ~ relation(set_difference(sK104_skl,X0)) ),
inference(component_clause,[status(thm)],[f34195]) ).
fof(f34207,plain,
( ~ sQ1278_spl
| ~ relation(sK104_skl) ),
inference(paramodulation,[status(thm)],[f1388,f34196]) ).
fof(f34212,plain,
( ~ sQ1278_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34207,f1077]) ).
fof(f34213,plain,
~ sQ1278_spl,
inference(contradiction_clause,[status(thm)],[f34212]) ).
fof(f34320,plain,
( ~ sQ1277_spl
| ~ relation(sK104_skl) ),
inference(paramodulation,[status(thm)],[f5006,f34192]) ).
fof(f34327,plain,
( ~ sQ1277_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34320,f1077]) ).
fof(f34328,plain,
~ sQ1277_spl,
inference(contradiction_clause,[status(thm)],[f34327]) ).
fof(f34329,plain,
( ~ sQ1276_spl
| ~ relation(sK104_skl) ),
inference(paramodulation,[status(thm)],[f4671,f34188]) ).
fof(f34336,plain,
( ~ sQ1276_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f34329,f1077]) ).
fof(f34337,plain,
~ sQ1276_spl,
inference(contradiction_clause,[status(thm)],[f34336]) ).
fof(f35467,definition,
! [X0] :
( sQ1316_spl
<=> ~ relation(inclusion_relation(X0)) ),
introduced(definition,[new_symbols(definition,[sQ1316_spl])],[split_symbol_definition]) ).
fof(f35468,plain,
! [X0] :
( ~ sQ1316_spl
| ~ relation(inclusion_relation(X0)) ),
inference(component_clause,[status(thm)],[f35467]) ).
fof(f35499,plain,
( ~ sQ1316_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35468,f837]) ).
fof(f35500,plain,
~ sQ1316_spl,
inference(contradiction_clause,[status(thm)],[f35499]) ).
fof(f35797,definition,
! [X0] :
( sQ1354_spl
<=> ~ relation(identity_relation(X0)) ),
introduced(definition,[new_symbols(definition,[sQ1354_spl])],[split_symbol_definition]) ).
fof(f35798,plain,
! [X0] :
( ~ sQ1354_spl
| ~ relation(identity_relation(X0)) ),
inference(component_clause,[status(thm)],[f35797]) ).
fof(f35831,plain,
( ~ sQ1354_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f35798,f857]) ).
fof(f35832,plain,
~ sQ1354_spl,
inference(contradiction_clause,[status(thm)],[f35831]) ).
fof(f36401,definition,
( sQ1397_spl
<=> subset(empty_set,sK67_skl(empty_set,empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1397_spl])],[split_symbol_definition]) ).
fof(f36403,plain,
( sQ1397_spl
| ~ subset(empty_set,sK67_skl(empty_set,empty_set)) ),
inference(component_clause,[status(thm)],[f36401]) ).
fof(f36405,plain,
( sQ1397_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36403,f1321]) ).
fof(f36406,plain,
sQ1397_spl,
inference(contradiction_clause,[status(thm)],[f36405]) ).
fof(f36539,definition,
( sQ1399_spl
<=> subset(empty_set,sK21_skl(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1399_spl])],[split_symbol_definition]) ).
fof(f36541,plain,
( sQ1399_spl
| ~ subset(empty_set,sK21_skl(empty_set)) ),
inference(component_clause,[status(thm)],[f36539]) ).
fof(f36543,plain,
( sQ1399_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f36541,f1321]) ).
fof(f36544,plain,
sQ1399_spl,
inference(contradiction_clause,[status(thm)],[f36543]) ).
fof(f37191,definition,
( sQ1409_spl
<=> subset(empty_set,sK30_skl(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1409_spl])],[split_symbol_definition]) ).
fof(f37193,plain,
( sQ1409_spl
| ~ subset(empty_set,sK30_skl(empty_set)) ),
inference(component_clause,[status(thm)],[f37191]) ).
fof(f37195,plain,
( sQ1409_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37193,f1321]) ).
fof(f37196,plain,
sQ1409_spl,
inference(contradiction_clause,[status(thm)],[f37195]) ).
fof(f37291,definition,
( sQ1423_spl
<=> subset(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1423_spl])],[split_symbol_definition]) ).
fof(f37293,plain,
( sQ1423_spl
| ~ subset(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f37291]) ).
fof(f37297,plain,
( sQ1423_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37293,f1655]) ).
fof(f37298,plain,
sQ1423_spl,
inference(contradiction_clause,[status(thm)],[f37297]) ).
fof(f37462,definition,
( sQ1434_spl
<=> empty(singleton(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ1434_spl])],[split_symbol_definition]) ).
fof(f37463,plain,
( ~ sQ1434_spl
| empty(singleton(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))))) ),
inference(component_clause,[status(thm)],[f37462]) ).
fof(f37467,plain,
( ~ sQ1434_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37463,f913]) ).
fof(f37468,plain,
~ sQ1434_spl,
inference(contradiction_clause,[status(thm)],[f37467]) ).
fof(f37873,definition,
( sQ1450_spl
<=> in(sK129_skl(empty_set,empty_set),relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ1450_spl])],[split_symbol_definition]) ).
fof(f37874,plain,
( ~ sQ1450_spl
| in(sK129_skl(empty_set,empty_set),relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f37873]) ).
fof(f37974,definition,
( sQ1455_spl
<=> sK108_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1455_spl])],[split_symbol_definition]) ).
fof(f37975,plain,
( ~ sQ1455_spl
| sK108_skl = empty_set ),
inference(component_clause,[status(thm)],[f37974]) ).
fof(f37985,definition,
( sQ1458_spl
<=> empty(sK108_skl) ),
introduced(definition,[new_symbols(definition,[sQ1458_spl])],[split_symbol_definition]) ).
fof(f37986,plain,
( ~ sQ1458_spl
| empty(sK108_skl) ),
inference(component_clause,[status(thm)],[f37985]) ).
fof(f38003,plain,
( ~ sQ1455_spl
| ~ empty(empty_set) ),
inference(backward_demodulation,[status(thm)],[f37975,f1088]) ).
fof(f38009,plain,
( ~ sQ1455_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38003,f884]) ).
fof(f38010,plain,
~ sQ1455_spl,
inference(contradiction_clause,[status(thm)],[f38009]) ).
fof(f38052,definition,
( sQ1466_spl
<=> relation(inclusion_relation(succ(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ1466_spl])],[split_symbol_definition]) ).
fof(f38054,plain,
( sQ1466_spl
| ~ relation(inclusion_relation(succ(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
inference(component_clause,[status(thm)],[f38052]) ).
fof(f38062,definition,
( sQ1469_spl
<=> relation(inclusion_relation(sK111_skl(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ1469_spl])],[split_symbol_definition]) ).
fof(f38064,plain,
( sQ1469_spl
| ~ relation(inclusion_relation(sK111_skl(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
inference(component_clause,[status(thm)],[f38062]) ).
fof(f38072,definition,
( sQ1472_spl
<=> relation(inclusion_relation(sK135_skl(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ1472_spl])],[split_symbol_definition]) ).
fof(f38074,plain,
( sQ1472_spl
| ~ relation(inclusion_relation(sK135_skl(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
inference(component_clause,[status(thm)],[f38072]) ).
fof(f38082,definition,
( sQ1475_spl
<=> relation(inclusion_relation(powerset(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ1475_spl])],[split_symbol_definition]) ).
fof(f38084,plain,
( sQ1475_spl
| ~ relation(inclusion_relation(powerset(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))))) ),
inference(component_clause,[status(thm)],[f38082]) ).
fof(f38108,definition,
( sQ1482_spl
<=> in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),relation_dom(relation_dom_restriction(empty_set,inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1482_spl])],[split_symbol_definition]) ).
fof(f38109,plain,
( ~ sQ1482_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),relation_dom(relation_dom_restriction(empty_set,inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f38108]) ).
fof(f38113,plain,
( ~ sQ1482_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),relation_dom(empty_set)) ),
inference(forward_demodulation,[status(thm)],[f12997,f38109]) ).
fof(f38114,plain,
( ~ sQ1482_spl
| in(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))),empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f38113]) ).
fof(f38115,plain,
( ~ sQ1482_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38114,f1696]) ).
fof(f38116,plain,
~ sQ1482_spl,
inference(contradiction_clause,[status(thm)],[f38115]) ).
fof(f38117,plain,
( sQ1475_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38084,f837]) ).
fof(f38118,plain,
sQ1475_spl,
inference(contradiction_clause,[status(thm)],[f38117]) ).
fof(f38119,plain,
( sQ1472_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38074,f837]) ).
fof(f38120,plain,
sQ1472_spl,
inference(contradiction_clause,[status(thm)],[f38119]) ).
fof(f38121,plain,
( sQ1469_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38064,f837]) ).
fof(f38122,plain,
sQ1469_spl,
inference(contradiction_clause,[status(thm)],[f38121]) ).
fof(f38198,plain,
( sQ1466_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f38054,f837]) ).
fof(f38199,plain,
sQ1466_spl,
inference(contradiction_clause,[status(thm)],[f38198]) ).
fof(f38212,plain,
( ~ sQ1458_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f37986,f1088]) ).
fof(f38213,plain,
~ sQ1458_spl,
inference(contradiction_clause,[status(thm)],[f38212]) ).
fof(f39239,definition,
( sQ1560_spl
<=> sK104_skl = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1560_spl])],[split_symbol_definition]) ).
fof(f39240,plain,
( ~ sQ1560_spl
| sK104_skl = empty_set ),
inference(component_clause,[status(thm)],[f39239]) ).
fof(f39652,plain,
( ~ sQ1560_spl
| ~ empty(empty_set) ),
inference(backward_demodulation,[status(thm)],[f39240,f1076]) ).
fof(f39666,plain,
( ~ sQ1560_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f39652,f884]) ).
fof(f39667,plain,
~ sQ1560_spl,
inference(contradiction_clause,[status(thm)],[f39666]) ).
fof(f40576,plain,
( ~ sQ1450_spl
| in(sK129_skl(empty_set,empty_set),empty_set) ),
inference(forward_demodulation,[status(thm)],[f1500,f37874]) ).
fof(f40577,plain,
( ~ sQ1450_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f40576,f1696]) ).
fof(f40578,plain,
~ sQ1450_spl,
inference(contradiction_clause,[status(thm)],[f40577]) ).
fof(f41532,definition,
( sQ1672_spl
<=> empty(powerset(sK132_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1672_spl])],[split_symbol_definition]) ).
fof(f41533,plain,
( ~ sQ1672_spl
| empty(powerset(sK132_skl)) ),
inference(component_clause,[status(thm)],[f41532]) ).
fof(f41543,plain,
( ~ sQ1672_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f41533,f897]) ).
fof(f41544,plain,
~ sQ1672_spl,
inference(contradiction_clause,[status(thm)],[f41543]) ).
fof(f42015,definition,
( sQ1728_spl
<=> in(sK121_skl(relation_dom(inclusion_relation(sK132_skl)),inclusion_relation(sK132_skl)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ1728_spl])],[split_symbol_definition]) ).
fof(f42016,plain,
( ~ sQ1728_spl
| in(sK121_skl(relation_dom(inclusion_relation(sK132_skl)),inclusion_relation(sK132_skl)),empty_set) ),
inference(component_clause,[status(thm)],[f42015]) ).
fof(f42054,plain,
( ~ sQ1728_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42016,f1696]) ).
fof(f42055,plain,
~ sQ1728_spl,
inference(contradiction_clause,[status(thm)],[f42054]) ).
fof(f42365,definition,
( sQ1758_spl
<=> function(identity_relation(inclusion_relation(sK132_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1758_spl])],[split_symbol_definition]) ).
fof(f42367,plain,
( sQ1758_spl
| ~ function(identity_relation(inclusion_relation(sK132_skl))) ),
inference(component_clause,[status(thm)],[f42365]) ).
fof(f42382,plain,
( sQ1758_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42367,f902]) ).
fof(f42383,plain,
sQ1758_spl,
inference(contradiction_clause,[status(thm)],[f42382]) ).
fof(f42926,definition,
( sQ1783_spl
<=> ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1783_spl])],[split_symbol_definition]) ).
fof(f42927,plain,
( ~ sQ1783_spl
| ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl))) = empty_set ),
inference(component_clause,[status(thm)],[f42926]) ).
fof(f42937,definition,
( sQ1786_spl
<=> empty(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ1786_spl])],[split_symbol_definition]) ).
fof(f42938,plain,
( ~ sQ1786_spl
| empty(ordered_pair(sK92_skl(inclusion_relation(sK132_skl)),sK92_skl(inclusion_relation(sK132_skl)))) ),
inference(component_clause,[status(thm)],[f42937]) ).
fof(f42956,plain,
( ~ sQ1783_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42927,f13998]) ).
fof(f42957,plain,
~ sQ1783_spl,
inference(contradiction_clause,[status(thm)],[f42956]) ).
fof(f42959,plain,
( ~ sQ1786_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f42938,f899]) ).
fof(f42960,plain,
~ sQ1786_spl,
inference(contradiction_clause,[status(thm)],[f42959]) ).
fof(f46014,plain,
( ~ sQ855_spl
| antisymmetric(inclusion_relation(sK132_skl))
| ~ relation(inclusion_relation(sK132_skl)) ),
inference(resolution,[status(thm)],[f1012,f26282]) ).
fof(f46016,plain,
( ~ sQ855_spl
| sQ184_spl
| ~ sQ183_spl ),
inference(split_clause,[status(thm)],[f46014,f11221,f11224,f26281]) ).
fof(f46018,plain,
$false,
inference(sat_refutation,[status(thm)],[f11236,f12501,f12509,f12513,f12625,f13505,f13526,f14515,f14518,f14521,f14524,f15101,f15103,f15107,f15354,f15356,f16210,f16212,f16763,f17235,f17391,f17416,f17441,f17443,f17638,f17725,f17727,f18630,f18635,f18638,f18642,f19319,f19321,f19462,f19488,f19571,f20121,f20719,f24668,f24670,f24672,f24674,f24676,f26242,f26277,f26362,f26407,f26770,f27056,f27226,f27228,f27230,f27232,f27234,f27312,f27832,f27841,f28086,f28203,f28208,f28941,f29222,f29628,f29634,f29653,f29659,f29665,f30243,f30260,f30264,f30268,f30906,f32569,f32632,f32797,f32799,f33400,f33409,f33418,f33461,f33464,f34213,f34328,f34337,f35500,f35832,f36406,f36544,f37196,f37298,f37468,f38010,f38116,f38118,f38120,f38122,f38199,f38213,f39667,f40578,f41544,f42055,f42383,f42957,f42960,f46016]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU271+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n008.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 06:06:08 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.47 % Drodi V4.1.1
% 139.77/18.14 % Refutation found
% 139.77/18.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 139.77/18.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 17.78/18.22 % Elapsed time: 17.782170 seconds
% 17.78/18.22 % CPU time: 140.485019 seconds
% 17.78/18.22 % Total memory used: 576.464 MB
% 17.78/18.22 % Net memory used: 508.490 MB
%------------------------------------------------------------------------------