%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU239+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:51 PM UTC 2026
% Result : Theorem 3.88s 1.00s
% Output : CNFRefutation 2.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 144
% Syntax : Number of formulae : 611 ( 93 unt; 96 def)
% Number of atoms : 1950 ( 293 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 2165 ( 826 ~; 921 |; 244 &)
% ( 142 <=>; 31 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 112 ( 110 usr; 96 prp; 0-4 aty)
% Number of functors : 50 ( 50 usr; 9 con; 0-4 aty)
% Number of variables : 782 ( 713 !; 69 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] :
( empty(A)
=> function(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( empty(A)
=> relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] :
( ( function(A)
& empty(A)
& relation(A) )
=> ( one_to_one(A)
& function(A)
& relation(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( ( epsilon_connected(A)
& epsilon_transitive(A) )
=> ordinal(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( empty(A)
=> ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,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/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( relation(C)
=> ( C = relation_dom_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),A)
& in(D,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( D = apply(A,E)
& in(E,B)
& in(E,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B] :
( relation(B)
=> ! [C] :
( relation(C)
=> ( C = relation_rng_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),B)
& in(E,A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(apply(A,D),B)
& in(D,relation_dom(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A] :
( relation(A)
=> ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] : succ(A) = set_union2(A,singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( relation(A)
<=> ! [B] :
~ ( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
( relation(A)
=> ! [B] :
( is_reflexive_in(A,B)
<=> ! [C] :
( in(C,B)
=> in(ordered_pair(C,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( in(B,A)
=> subset(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [A] :
( epsilon_connected(A)
<=> ! [B,C] :
~ ( ~ in(C,B)
& B != C
& ~ in(B,C)
& in(C,A)
& in(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [A] :
( relation(A)
=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A] :
( relation(A)
=> ( reflexive(A)
<=> is_reflexive_in(A,relation_field(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,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/sandbox/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [A] :
( ordinal(A)
=> ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [A,B] : set_union2(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,conjecture,
! [A] :
( relation(A)
=> ( reflexive(A)
<=> ! [B] :
( in(B,relation_field(A))
=> in(ordered_pair(B,B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,negated_conjecture,
~ ! [A] :
( relation(A)
=> ( reflexive(A)
<=> ! [B] :
( in(B,relation_field(A))
=> in(ordered_pair(B,B),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f127]) ).
fof(f129,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,axiom,
? [A] :
( relation(A)
& empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,lemma,
powerset(empty_set) = singleton(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,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/sandbox/benchmark/theBenchmark.p') ).
fof(f210,lemma,
! [A] :
( ! [B] :
( in(B,A)
=> ( subset(B,A)
& ordinal(B) ) )
=> ordinal(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f225,lemma,
! [A,B,C] :
~ ( in(C,A)
& in(B,C)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f243,axiom,
! [A] : set_difference(empty_set,A) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f253,lemma,
( relation_rng(empty_set) = empty_set
& relation_dom(empty_set) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f262,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,lemma,
! [A] :
( relation_rng(identity_relation(A)) = A
& relation_dom(identity_relation(A)) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,lemma,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f285,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f286,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f289,plain,
! [A] :
( function(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f290,plain,
! [X0] :
( function(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f289]) ).
fof(f294,plain,
! [A] :
( relation(A)
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f295,plain,
! [X0] :
( relation(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [A] :
( ( one_to_one(A)
& function(A)
& relation(A) )
| ~ function(A)
| ~ empty(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f299,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f296]) ).
fof(f300,plain,
! [A] :
( ordinal(A)
| ~ epsilon_connected(A)
| ~ epsilon_transitive(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f301,plain,
! [X0] :
( ordinal(X0)
| ~ epsilon_connected(X0)
| ~ epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f302,plain,
! [A] :
( ( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) )
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f303,plain,
! [X0] :
( epsilon_transitive(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f304,plain,
! [X0] :
( epsilon_connected(X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f307,plain,
! [X0,X1] : set_union2(X0,X1) = set_union2(X1,X0),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f311,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)],[f13]) ).
fof(f312,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)],[f311]) ).
fof(f313,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)],[f312]) ).
fof(f314,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))],[f313]) ).
fof(f319,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X1)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f320,plain,
! [X0,X1] :
( sK0_skl(X1,X0) = sK1_skl(X1,X0)
| in(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f326,plain,
! [A] :
( ! [B,C] :
( ( C = relation_dom_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),A)
& in(D,B) ) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f327,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D,E] :
( ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_dom_restriction(A,B) )
& ( ! [D,E] :
( ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f326]) ).
fof(f328,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ? [D,E] :
( ( ( in(ordered_pair(D,E),A)
& in(D,B) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_dom_restriction(A,B) )
& ! [B] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f327]) ).
fof(f329,plain,
! [A] :
( ! [C] :
( ( ! [B] :
( ( ( ( in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A)
& in(sK2_skl(B,C,A),B) )
| in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C) )
& ( ~ in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),A)
| ~ in(sK2_skl(B,C,A),B)
| ~ in(ordered_pair(sK2_skl(B,C,A),sK3_skl(B,C,A)),C) ) )
| C = relation_dom_restriction(A,B) )
& ! [B] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),A)
| ~ in(D,B)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),A)
& in(D,B) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_dom_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(D,sK2_skl(B,C,A)),skolemize(E,sK3_skl(B,C,A))],[f328]) ).
fof(f334,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),X2)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f335,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X1)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f336,plain,
! [A] :
( ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( D = apply(A,E)
& in(E,B)
& in(E,relation_dom(A)) ) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f337,definition,
! [A,B,D,E] :
( sP0_prd(E,D,B,A)
<=> ( D = apply(A,E)
& in(E,B)
& in(E,relation_dom(A)) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f338,plain,
! [A] :
( ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] : sP0_prd(E,D,B,A) ) )
| ~ function(A)
| ~ relation(A) ),
inference(formula_renaming,[status(thm)],[f336,f337]) ).
fof(f339,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] : sP0_prd(E,D,B,A)
| in(D,C) )
& ( ! [E] : ~ sP0_prd(E,D,B,A)
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ( ! [D] :
( ( ! [E] : ~ sP0_prd(E,D,B,A)
| in(D,C) )
& ( ? [E] : sP0_prd(E,D,B,A)
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f338]) ).
fof(f340,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] : sP0_prd(E,D,B,A)
| in(D,C) )
& ( ! [E] : ~ sP0_prd(E,D,B,A)
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] : ~ sP0_prd(E,D,B,A)
| in(D,C) )
& ! [D] :
( ? [E] : sP0_prd(E,D,B,A)
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f339]) ).
fof(f341,plain,
! [A] :
( ( ! [B,C] :
( ( ( sP0_prd(sK6_skl(C,B,A),sK5_skl(C,B,A),B,A)
| in(sK5_skl(C,B,A),C) )
& ( ! [E] : ~ sP0_prd(E,sK5_skl(C,B,A),B,A)
| ~ in(sK5_skl(C,B,A),C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] : ~ sP0_prd(E,D,B,A)
| in(D,C) )
& ! [D] :
( sP0_prd(sK4_skl(D,C,B,A),D,B,A)
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(E,sK4_skl(D,C,B,A)),skolemize(D,sK5_skl(C,B,A)),skolemize(E,sK6_skl(C,B,A))],[f340]) ).
fof(f342,plain,
! [X0,X1,X2,X3] :
( sP0_prd(sK4_skl(X3,X1,X2,X0),X3,X2,X0)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f341]) ).
fof(f346,plain,
! [A,B] :
( ! [C] :
( ( C = relation_rng_restriction(A,B)
<=> ! [D,E] :
( in(ordered_pair(D,E),C)
<=> ( in(ordered_pair(D,E),B)
& in(E,A) ) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f347,plain,
! [A,B] :
( ! [C] :
( ( ( ? [D,E] :
( ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_rng_restriction(A,B) )
& ( ! [D,E] :
( ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(NNF_transformation,[status(thm)],[f346]) ).
fof(f348,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ? [D,E] :
( ( ( in(ordered_pair(D,E),B)
& in(E,A) )
| in(ordered_pair(D,E),C) )
& ( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| ~ in(ordered_pair(D,E),C) ) )
| C = relation_rng_restriction(A,B) )
& ! [A] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(miniscoping,[status(thm)],[f347]) ).
fof(f349,plain,
! [B] :
( ! [C] :
( ( ! [A] :
( ( ( ( in(ordered_pair(sK7_skl(A,C,B),sK8_skl(A,C,B)),B)
& in(sK8_skl(A,C,B),A) )
| in(ordered_pair(sK7_skl(A,C,B),sK8_skl(A,C,B)),C) )
& ( ~ in(ordered_pair(sK7_skl(A,C,B),sK8_skl(A,C,B)),B)
| ~ in(sK8_skl(A,C,B),A)
| ~ in(ordered_pair(sK7_skl(A,C,B),sK8_skl(A,C,B)),C) ) )
| C = relation_rng_restriction(A,B) )
& ! [A] :
( ( ! [D,E] :
( ~ in(ordered_pair(D,E),B)
| ~ in(E,A)
| in(ordered_pair(D,E),C) )
& ! [D,E] :
( ( in(ordered_pair(D,E),B)
& in(E,A) )
| ~ in(ordered_pair(D,E),C) ) )
| C != relation_rng_restriction(A,B) ) )
| ~ relation(C) )
| ~ relation(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(D,sK7_skl(A,C,B)),skolemize(E,sK8_skl(A,C,B))],[f348]) ).
fof(f354,plain,
! [X0,X1,X2] :
( in(sK8_skl(X2,X1,X0),X2)
| in(ordered_pair(sK7_skl(X2,X1,X0),sK8_skl(X2,X1,X0)),X1)
| X1 = relation_rng_restriction(X2,X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f355,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK7_skl(X2,X1,X0),sK8_skl(X2,X1,X0)),X0)
| in(ordered_pair(sK7_skl(X2,X1,X0),sK8_skl(X2,X1,X0)),X1)
| X1 = relation_rng_restriction(X2,X0)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f349]) ).
fof(f356,plain,
! [A] :
( ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(apply(A,D),B)
& in(D,relation_dom(A)) ) ) )
| ~ function(A)
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f357,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| in(D,C) )
& ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f356]) ).
fof(f358,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| in(D,C) )
& ( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ! [D] :
( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f357]) ).
fof(f359,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(apply(A,sK9_skl(C,B,A)),B)
& in(sK9_skl(C,B,A),relation_dom(A)) )
| in(sK9_skl(C,B,A),C) )
& ( ~ in(apply(A,sK9_skl(C,B,A)),B)
| ~ in(sK9_skl(C,B,A),relation_dom(A))
| ~ in(sK9_skl(C,B,A),C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ~ in(apply(A,D),B)
| ~ in(D,relation_dom(A))
| in(D,C) )
& ! [D] :
( ( in(apply(A,D),B)
& in(D,relation_dom(A)) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(D,sK9_skl(C,B,A))],[f358]) ).
fof(f360,plain,
! [X0,X1,X2,X3] :
( in(X3,relation_dom(X0))
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f361,plain,
! [X0,X1,X2,X3] :
( in(apply(X0,X3),X2)
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f364,plain,
! [X0,X1,X2] :
( in(sK9_skl(X1,X2,X0),relation_dom(X0))
| in(sK9_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f366,plain,
! [A] :
( ! [B,C] :
( C = relation_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f367,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f366]) ).
fof(f368,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(E,D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f367]) ).
fof(f369,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK12_skl(C,B,A),B)
& in(ordered_pair(sK12_skl(C,B,A),sK11_skl(C,B,A)),A) )
| in(sK11_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,sK11_skl(C,B,A)),A) )
| ~ in(sK11_skl(C,B,A),C) ) )
| C = relation_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(E,D),A) )
| in(D,C) )
& ! [D] :
( ( in(sK10_skl(D,C,B,A),B)
& in(ordered_pair(sK10_skl(D,C,B,A),D),A) )
| ~ in(D,C) ) )
| C != relation_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(E,sK10_skl(D,C,B,A)),skolemize(D,sK11_skl(C,B,A)),skolemize(E,sK12_skl(C,B,A))],[f368]) ).
fof(f370,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(sK10_skl(X3,X1,X2,X0),X3),X0)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f371,plain,
! [X0,X1,X2,X3] :
( in(sK10_skl(X3,X1,X2,X0),X2)
| ~ in(X3,X1)
| X1 != relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f374,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK12_skl(X1,X2,X0),sK11_skl(X1,X2,X0)),X0)
| in(sK11_skl(X1,X2,X0),X1)
| X1 = relation_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f376,plain,
! [A] :
( ! [B,C] :
( C = relation_inverse_image(A,B)
<=> ! [D] :
( in(D,C)
<=> ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) ) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f377,plain,
! [A] :
( ! [B,C] :
( ( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ( ! [D] :
( ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
! [A] :
( ( ! [B,C] :
( ? [D] :
( ( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| in(D,C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ? [E] :
( in(E,B)
& in(ordered_pair(D,E),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f377]) ).
fof(f379,plain,
! [A] :
( ( ! [B,C] :
( ( ( ( in(sK15_skl(C,B,A),B)
& in(ordered_pair(sK14_skl(C,B,A),sK15_skl(C,B,A)),A) )
| in(sK14_skl(C,B,A),C) )
& ( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(sK14_skl(C,B,A),E),A) )
| ~ in(sK14_skl(C,B,A),C) ) )
| C = relation_inverse_image(A,B) )
& ! [B,C] :
( ( ! [D] :
( ! [E] :
( ~ in(E,B)
| ~ in(ordered_pair(D,E),A) )
| in(D,C) )
& ! [D] :
( ( in(sK13_skl(D,C,B,A),B)
& in(ordered_pair(D,sK13_skl(D,C,B,A)),A) )
| ~ in(D,C) ) )
| C != relation_inverse_image(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(E,sK13_skl(D,C,B,A)),skolemize(D,sK14_skl(C,B,A)),skolemize(E,sK15_skl(C,B,A))],[f378]) ).
fof(f380,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X3,sK13_skl(X3,X1,X2,X0)),X0)
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f381,plain,
! [X0,X1,X2,X3] :
( in(sK13_skl(X3,X1,X2,X0),X2)
| ~ in(X3,X1)
| X1 != relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f384,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK14_skl(X1,X2,X0),sK15_skl(X1,X2,X0)),X0)
| in(sK14_skl(X1,X2,X0),X1)
| X1 = relation_inverse_image(X0,X2)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f379]) ).
fof(f396,plain,
! [X0] : succ(X0) = set_union2(X0,singleton(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f397,plain,
! [A] :
( relation(A)
<=> ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f398,plain,
! [A] :
( ( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(NNF_transformation,[status(thm)],[f397]) ).
fof(f399,plain,
( ! [A] :
( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ! [A] :
( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(miniscoping,[status(thm)],[f398]) ).
fof(f400,plain,
( ! [A] :
( ( ! [C,D] : sK19_skl(A) != ordered_pair(C,D)
& in(sK19_skl(A),A) )
| relation(A) )
& ! [A] :
( ! [B] :
( B = ordered_pair(sK17_skl(B,A),sK18_skl(B,A))
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(C,sK17_skl(B,A)),skolemize(D,sK18_skl(B,A)),skolemize(B,sK19_skl(A))],[f399]) ).
fof(f402,plain,
! [X0] :
( in(sK19_skl(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f404,plain,
! [A] :
( ! [B] :
( is_reflexive_in(A,B)
<=> ! [C] :
( in(ordered_pair(C,C),A)
| ~ in(C,B) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f405,plain,
! [A] :
( ! [B] :
( ( ? [C] :
( ~ in(ordered_pair(C,C),A)
& in(C,B) )
| is_reflexive_in(A,B) )
& ( ! [C] :
( in(ordered_pair(C,C),A)
| ~ in(C,B) )
| ~ is_reflexive_in(A,B) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f404]) ).
fof(f406,plain,
! [A] :
( ( ! [B] :
( ? [C] :
( ~ in(ordered_pair(C,C),A)
& in(C,B) )
| is_reflexive_in(A,B) )
& ! [B] :
( ! [C] :
( in(ordered_pair(C,C),A)
| ~ in(C,B) )
| ~ is_reflexive_in(A,B) ) )
| ~ relation(A) ),
inference(miniscoping,[status(thm)],[f405]) ).
fof(f407,plain,
! [A] :
( ( ! [B] :
( ( ~ in(ordered_pair(sK20_skl(B,A),sK20_skl(B,A)),A)
& in(sK20_skl(B,A),B) )
| is_reflexive_in(A,B) )
& ! [B] :
( ! [C] :
( in(ordered_pair(C,C),A)
| ~ in(C,B) )
| ~ is_reflexive_in(A,B) ) )
| ~ relation(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(C,sK20_skl(B,A))],[f406]) ).
fof(f408,plain,
! [X0,X1,X2] :
( in(ordered_pair(X2,X2),X0)
| ~ in(X2,X1)
| ~ is_reflexive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f409,plain,
! [X0,X1] :
( in(sK20_skl(X1,X0),X1)
| is_reflexive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f410,plain,
! [X0,X1] :
( ~ in(ordered_pair(sK20_skl(X1,X0),sK20_skl(X1,X0)),X0)
| is_reflexive_in(X0,X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f423,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)],[f26]) ).
fof(f424,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)],[f423]) ).
fof(f425,plain,
( ! [A,B] :
( ( ( sK24_skl(B,A) = A
| in(sK24_skl(B,A),B) )
& ( sK24_skl(B,A) != A
| ~ in(sK24_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,[sK24_skl]),skolemize(C,sK24_skl(B,A))],[f424]) ).
fof(f426,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f425]) ).
fof(f430,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f27]) ).
fof(f431,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f430]) ).
fof(f432,plain,
( ! [A] :
( in(sK25_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(B,sK25_skl(A))],[f431]) ).
fof(f433,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f434,plain,
! [X0] :
( in(sK25_skl(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f442,plain,
! [A] :
( epsilon_transitive(A)
<=> ! [B] :
( subset(B,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f443,plain,
! [A] :
( ( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(NNF_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
( ! [A] :
( ? [B] :
( ~ subset(B,A)
& in(B,A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(miniscoping,[status(thm)],[f443]) ).
fof(f445,plain,
( ! [A] :
( ( ~ subset(sK27_skl(A),A)
& in(sK27_skl(A),A) )
| epsilon_transitive(A) )
& ! [A] :
( ! [B] :
( subset(B,A)
| ~ in(B,A) )
| ~ epsilon_transitive(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(B,sK27_skl(A))],[f444]) ).
fof(f447,plain,
! [X0] :
( in(sK27_skl(X0),X0)
| epsilon_transitive(X0) ),
inference(cnf_transformation,[status(thm)],[f445]) ).
fof(f491,plain,
! [A] :
( epsilon_connected(A)
<=> ! [B,C] :
( in(C,B)
| B = C
| in(B,C)
| ~ in(C,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f492,plain,
! [A] :
( ( ? [B,C] :
( ~ in(C,B)
& B != C
& ~ in(B,C)
& in(C,A)
& in(B,A) )
| epsilon_connected(A) )
& ( ! [B,C] :
( in(C,B)
| B = C
| in(B,C)
| ~ in(C,A)
| ~ in(B,A) )
| ~ epsilon_connected(A) ) ),
inference(NNF_transformation,[status(thm)],[f491]) ).
fof(f493,plain,
( ! [A] :
( ? [B,C] :
( ~ in(C,B)
& B != C
& ~ in(B,C)
& in(C,A)
& in(B,A) )
| epsilon_connected(A) )
& ! [A] :
( ! [B,C] :
( in(C,B)
| B = C
| in(B,C)
| ~ in(C,A)
| ~ in(B,A) )
| ~ epsilon_connected(A) ) ),
inference(miniscoping,[status(thm)],[f492]) ).
fof(f494,plain,
( ! [A] :
( ( ~ in(sK38_skl(A),sK37_skl(A))
& sK37_skl(A) != sK38_skl(A)
& ~ in(sK37_skl(A),sK38_skl(A))
& in(sK38_skl(A),A)
& in(sK37_skl(A),A) )
| epsilon_connected(A) )
& ! [A] :
( ! [B,C] :
( in(C,B)
| B = C
| in(B,C)
| ~ in(C,A)
| ~ in(B,A) )
| ~ epsilon_connected(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl]),skolemize(B,sK37_skl(A)),skolemize(C,sK38_skl(A))],[f493]) ).
fof(f497,plain,
! [X0] :
( in(sK38_skl(X0),X0)
| epsilon_connected(X0) ),
inference(cnf_transformation,[status(thm)],[f494]) ).
fof(f587,plain,
! [A] :
( relation_field(A) = set_union2(relation_dom(A),relation_rng(A))
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f588,plain,
! [X0] :
( relation_field(X0) = set_union2(relation_dom(X0),relation_rng(X0))
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f634,plain,
! [A] :
( ( reflexive(A)
<=> is_reflexive_in(A,relation_field(A)) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f635,plain,
! [A] :
( ( ( ~ is_reflexive_in(A,relation_field(A))
| reflexive(A) )
& ( is_reflexive_in(A,relation_field(A))
| ~ reflexive(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f634]) ).
fof(f636,plain,
! [X0] :
( is_reflexive_in(X0,relation_field(X0))
| ~ reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f637,plain,
! [X0] :
( ~ is_reflexive_in(X0,relation_field(X0))
| reflexive(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f635]) ).
fof(f650,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f671,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f672,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f692,plain,
function(empty_set),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f695,plain,
epsilon_transitive(empty_set),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f696,plain,
epsilon_connected(empty_set),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f707,plain,
! [A] :
( ( ordinal(succ(A))
& epsilon_connected(succ(A))
& epsilon_transitive(succ(A))
& ~ empty(succ(A)) )
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f709,plain,
! [X0] :
( epsilon_transitive(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f710,plain,
! [X0] :
( epsilon_connected(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f711,plain,
! [X0] :
( ordinal(succ(X0))
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f707]) ).
fof(f743,plain,
! [A] : set_union2(A,A) = A,
inference(miniscoping,[status(thm)],[f121]) ).
fof(f744,plain,
! [X0] : set_union2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f743]) ).
fof(f755,plain,
? [A] :
( ( reflexive(A)
<~> ! [B] :
( in(ordered_pair(B,B),A)
| ~ in(B,relation_field(A)) ) )
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f128]) ).
fof(f756,plain,
? [A] :
( ( ? [B] :
( ~ in(ordered_pair(B,B),A)
& in(B,relation_field(A)) )
| ~ reflexive(A) )
& ( ! [B] :
( in(ordered_pair(B,B),A)
| ~ in(B,relation_field(A)) )
| reflexive(A) )
& relation(A) ),
inference(NNF_transformation,[status(thm)],[f755]) ).
fof(f757,plain,
( ( ( ~ in(ordered_pair(sK67_skl,sK67_skl),sK66_skl)
& in(sK67_skl,relation_field(sK66_skl)) )
| ~ reflexive(sK66_skl) )
& ( ! [B] :
( in(ordered_pair(B,B),sK66_skl)
| ~ in(B,relation_field(sK66_skl)) )
| reflexive(sK66_skl) )
& relation(sK66_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66_skl,sK67_skl]),skolemize(A,sK66_skl),skolemize(B,sK67_skl)],[f756]) ).
fof(f758,plain,
relation(sK66_skl),
inference(cnf_transformation,[status(thm)],[f757]) ).
fof(f759,plain,
! [X0] :
( in(ordered_pair(X0,X0),sK66_skl)
| ~ in(X0,relation_field(sK66_skl))
| reflexive(sK66_skl) ),
inference(cnf_transformation,[status(thm)],[f757]) ).
fof(f760,plain,
( in(sK67_skl,relation_field(sK66_skl))
| ~ reflexive(sK66_skl) ),
inference(cnf_transformation,[status(thm)],[f757]) ).
fof(f761,plain,
( ~ in(ordered_pair(sK67_skl,sK67_skl),sK66_skl)
| ~ reflexive(sK66_skl) ),
inference(cnf_transformation,[status(thm)],[f757]) ).
fof(f762,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f807,plain,
( ordinal(sK70_skl)
& epsilon_connected(sK70_skl)
& epsilon_transitive(sK70_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70_skl]),skolemize(A,sK70_skl)],[f143]) ).
fof(f808,plain,
epsilon_transitive(sK70_skl),
inference(cnf_transformation,[status(thm)],[f807]) ).
fof(f809,plain,
epsilon_connected(sK70_skl),
inference(cnf_transformation,[status(thm)],[f807]) ).
fof(f811,plain,
( relation(sK71_skl)
& empty(sK71_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71_skl]),skolemize(A,sK71_skl)],[f144]) ).
fof(f812,plain,
empty(sK71_skl),
inference(cnf_transformation,[status(thm)],[f811]) ).
fof(f818,plain,
empty(sK73_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73_skl]),skolemize(A,sK73_skl)],[f146]) ).
fof(f819,plain,
empty(sK73_skl),
inference(cnf_transformation,[status(thm)],[f818]) ).
fof(f820,plain,
( function(sK74_skl)
& empty(sK74_skl)
& relation(sK74_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74_skl]),skolemize(A,sK74_skl)],[f147]) ).
fof(f822,plain,
empty(sK74_skl),
inference(cnf_transformation,[status(thm)],[f820]) ).
fof(f823,plain,
function(sK74_skl),
inference(cnf_transformation,[status(thm)],[f820]) ).
fof(f824,plain,
( ordinal(sK75_skl)
& epsilon_connected(sK75_skl)
& epsilon_transitive(sK75_skl)
& empty(sK75_skl)
& one_to_one(sK75_skl)
& function(sK75_skl)
& relation(sK75_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75_skl]),skolemize(A,sK75_skl)],[f148]) ).
fof(f825,plain,
relation(sK75_skl),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f826,plain,
function(sK75_skl),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f828,plain,
empty(sK75_skl),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f829,plain,
epsilon_transitive(sK75_skl),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f830,plain,
epsilon_connected(sK75_skl),
inference(cnf_transformation,[status(thm)],[f824]) ).
fof(f844,plain,
( ordinal(sK80_skl)
& epsilon_connected(sK80_skl)
& epsilon_transitive(sK80_skl)
& ~ empty(sK80_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80_skl]),skolemize(A,sK80_skl)],[f153]) ).
fof(f846,plain,
epsilon_transitive(sK80_skl),
inference(cnf_transformation,[status(thm)],[f844]) ).
fof(f847,plain,
epsilon_connected(sK80_skl),
inference(cnf_transformation,[status(thm)],[f844]) ).
fof(f965,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f966,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f191]) ).
fof(f967,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f966]) ).
fof(f971,plain,
powerset(empty_set) = singleton(empty_set),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f1013,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f1014,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)],[f209]) ).
fof(f1015,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)],[f1014]) ).
fof(f1016,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1015]) ).
fof(f1017,plain,
! [X0,X1,X2] :
( in(X2,relation_field(X0))
| ~ in(ordered_pair(X1,X2),X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1015]) ).
fof(f1018,plain,
! [A] :
( ordinal(A)
| ? [B] :
( ( ~ subset(B,A)
| ~ ordinal(B) )
& in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f210]) ).
fof(f1019,plain,
! [A] :
( ordinal(A)
| ( ( ~ subset(sK87_skl(A),A)
| ~ ordinal(sK87_skl(A)) )
& in(sK87_skl(A),A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87_skl]),skolemize(B,sK87_skl(A))],[f1018]) ).
fof(f1020,plain,
! [X0] :
( ordinal(X0)
| in(sK87_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f1019]) ).
fof(f1072,plain,
! [A,B,C] :
( ~ in(C,A)
| ~ in(B,C)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f225]) ).
fof(f1073,plain,
! [A,C] :
( ~ in(C,A)
| ! [B] :
( ~ in(B,C)
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f1072]) ).
fof(f1074,plain,
! [X0,X1,X2] :
( ~ in(X2,X0)
| ~ in(X1,X2)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1073]) ).
fof(f1123,plain,
! [X0] : set_difference(empty_set,X0) = empty_set,
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f1163,plain,
relation_dom(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f1164,plain,
relation_rng(empty_set) = empty_set,
inference(cnf_transformation,[status(thm)],[f253]) ).
fof(f1192,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f262]) ).
fof(f1193,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f1192]) ).
fof(f1199,plain,
( ! [A] : relation_rng(identity_relation(A)) = A
& ! [A] : relation_dom(identity_relation(A)) = A ),
inference(miniscoping,[status(thm)],[f265]) ).
fof(f1200,plain,
! [X0] : relation_dom(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f1199]) ).
fof(f1201,plain,
! [X0] : relation_rng(identity_relation(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f1199]) ).
fof(f1220,plain,
! [A,B] :
( ( set_difference(A,B) != A
| disjoint(A,B) )
& ( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f271]) ).
fof(f1221,plain,
( ! [A,B] :
( set_difference(A,B) != A
| disjoint(A,B) )
& ! [A,B] :
( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(miniscoping,[status(thm)],[f1220]) ).
fof(f1223,plain,
! [X0,X1] :
( set_difference(X0,X1) != X0
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
fof(f1295,definition,
( sQ0_spl
<=> reflexive(sK66_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1298,definition,
! [X0] :
( sQ1_spl
<=> ( in(ordered_pair(X0,X0),sK66_skl)
| ~ in(X0,relation_field(sK66_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1299,plain,
! [X0] :
( ~ sQ1_spl
| in(ordered_pair(X0,X0),sK66_skl)
| ~ in(X0,relation_field(sK66_skl)) ),
inference(component_clause,[status(thm)],[f1298]) ).
fof(f1301,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f759,f1295,f1298]) ).
fof(f1302,definition,
( sQ2_spl
<=> in(sK67_skl,relation_field(sK66_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( ~ sQ2_spl
| in(sK67_skl,relation_field(sK66_skl)) ),
inference(component_clause,[status(thm)],[f1302]) ).
fof(f1305,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f760,f1295,f1302]) ).
fof(f1306,definition,
( sQ3_spl
<=> in(ordered_pair(sK67_skl,sK67_skl),sK66_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1308,plain,
( sQ3_spl
| ~ in(ordered_pair(sK67_skl,sK67_skl),sK66_skl) ),
inference(component_clause,[status(thm)],[f1306]) ).
fof(f1309,plain,
( ~ sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f761,f1295,f1306]) ).
fof(f1325,plain,
! [X0,X1,X2] :
( sP0_prd(sK4_skl(X1,relation_image(X0,X2),X2,X0),X1,X2,X0)
| ~ in(X1,relation_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f342]) ).
fof(f1330,plain,
! [X0,X1,X2] :
( in(X1,relation_dom(X0))
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f360]) ).
fof(f1331,plain,
! [X0,X1,X2] :
( in(apply(X0,X1),X2)
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ function(X0)
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f361]) ).
fof(f1333,plain,
! [X0,X1,X2] :
( in(ordered_pair(sK10_skl(X1,relation_image(X0,X2),X2,X0),X1),X0)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f370]) ).
fof(f1334,plain,
! [X0,X1,X2] :
( in(sK10_skl(X1,relation_image(X0,X2),X2,X0),X2)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f371]) ).
fof(f1336,plain,
! [X0,X1,X2] :
( in(ordered_pair(X1,sK13_skl(X1,relation_inverse_image(X0,X2),X2,X0)),X0)
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f380]) ).
fof(f1337,plain,
! [X0,X1,X2] :
( in(sK13_skl(X1,relation_inverse_image(X0,X2),X2,X0),X2)
| ~ in(X1,relation_inverse_image(X0,X2))
| ~ relation(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f381]) ).
fof(f1346,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f426]) ).
fof(f1348,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f433]) ).
fof(f1419,definition,
( sQ6_spl
<=> relation(sK66_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1421,plain,
( sQ6_spl
| ~ relation(sK66_skl) ),
inference(component_clause,[status(thm)],[f1419]) ).
fof(f1434,plain,
function(sK71_skl),
inference(resolution,[status(thm)],[f812,f290]) ).
fof(f1435,plain,
function(sK73_skl),
inference(resolution,[status(thm)],[f819,f290]) ).
fof(f1439,plain,
! [X0] :
( one_to_one(X0)
| ~ function(X0)
| ~ empty(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f299,f295]) ).
fof(f1440,plain,
( one_to_one(sK73_skl)
| ~ function(sK73_skl) ),
inference(resolution,[status(thm)],[f1439,f819]) ).
fof(f1441,plain,
( one_to_one(sK71_skl)
| ~ function(sK71_skl) ),
inference(resolution,[status(thm)],[f1439,f812]) ).
fof(f1442,plain,
( one_to_one(empty_set)
| ~ function(empty_set) ),
inference(resolution,[status(thm)],[f1439,f671]) ).
fof(f1443,definition,
( sQ8_spl
<=> function(sK73_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1445,plain,
( sQ8_spl
| ~ function(sK73_skl) ),
inference(component_clause,[status(thm)],[f1443]) ).
fof(f1446,definition,
( sQ9_spl
<=> one_to_one(sK73_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1449,plain,
( sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1440,f1443,f1446]) ).
fof(f1450,definition,
( sQ10_spl
<=> function(sK71_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1452,plain,
( sQ10_spl
| ~ function(sK71_skl) ),
inference(component_clause,[status(thm)],[f1450]) ).
fof(f1453,definition,
( sQ11_spl
<=> one_to_one(sK71_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1456,plain,
( sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f1441,f1450,f1453]) ).
fof(f1457,definition,
( sQ12_spl
<=> function(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
( sQ12_spl
| ~ function(empty_set) ),
inference(component_clause,[status(thm)],[f1457]) ).
fof(f1460,definition,
( sQ13_spl
<=> one_to_one(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1463,plain,
( sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1442,f1457,f1460]) ).
fof(f1464,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1459,f692]) ).
fof(f1465,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1464]) ).
fof(f1466,plain,
( one_to_one(sK74_skl)
| ~ function(sK74_skl) ),
inference(resolution,[status(thm)],[f822,f1439]) ).
fof(f1469,definition,
( sQ14_spl
<=> function(sK74_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1471,plain,
( sQ14_spl
| ~ function(sK74_skl) ),
inference(component_clause,[status(thm)],[f1469]) ).
fof(f1472,definition,
( sQ15_spl
<=> one_to_one(sK74_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1475,plain,
( sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1466,f1469,f1472]) ).
fof(f1476,plain,
( one_to_one(sK75_skl)
| ~ function(sK75_skl) ),
inference(resolution,[status(thm)],[f828,f1439]) ).
fof(f1479,definition,
( sQ16_spl
<=> function(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1481,plain,
( sQ16_spl
| ~ function(sK75_skl) ),
inference(component_clause,[status(thm)],[f1479]) ).
fof(f1482,definition,
( sQ17_spl
<=> one_to_one(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1485,plain,
( sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1476,f1479,f1482]) ).
fof(f1486,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1481,f826]) ).
fof(f1487,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1486]) ).
fof(f1490,plain,
( ordinal(sK75_skl)
| ~ epsilon_connected(sK75_skl) ),
inference(resolution,[status(thm)],[f301,f829]) ).
fof(f1491,plain,
( ordinal(sK70_skl)
| ~ epsilon_connected(sK70_skl) ),
inference(resolution,[status(thm)],[f301,f808]) ).
fof(f1492,plain,
( ordinal(empty_set)
| ~ epsilon_connected(empty_set) ),
inference(resolution,[status(thm)],[f301,f695]) ).
fof(f1493,definition,
( sQ18_spl
<=> epsilon_connected(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1495,plain,
( sQ18_spl
| ~ epsilon_connected(sK75_skl) ),
inference(component_clause,[status(thm)],[f1493]) ).
fof(f1496,definition,
( sQ19_spl
<=> ordinal(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1499,plain,
( sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1490,f1493,f1496]) ).
fof(f1500,definition,
( sQ20_spl
<=> epsilon_connected(sK70_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1502,plain,
( sQ20_spl
| ~ epsilon_connected(sK70_skl) ),
inference(component_clause,[status(thm)],[f1500]) ).
fof(f1503,definition,
( sQ21_spl
<=> ordinal(sK70_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f1506,plain,
( sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1491,f1500,f1503]) ).
fof(f1507,definition,
( sQ22_spl
<=> epsilon_connected(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1509,plain,
( sQ22_spl
| ~ epsilon_connected(empty_set) ),
inference(component_clause,[status(thm)],[f1507]) ).
fof(f1510,definition,
( sQ23_spl
<=> ordinal(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1492,f1507,f1510]) ).
fof(f1514,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1509,f696]) ).
fof(f1515,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1514]) ).
fof(f1516,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1502,f809]) ).
fof(f1517,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1516]) ).
fof(f1518,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1495,f830]) ).
fof(f1519,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1518]) ).
fof(f1521,plain,
epsilon_transitive(sK74_skl),
inference(resolution,[status(thm)],[f303,f822]) ).
fof(f1522,plain,
epsilon_transitive(sK73_skl),
inference(resolution,[status(thm)],[f303,f819]) ).
fof(f1523,plain,
epsilon_transitive(sK71_skl),
inference(resolution,[status(thm)],[f303,f812]) ).
fof(f1526,plain,
epsilon_connected(sK74_skl),
inference(resolution,[status(thm)],[f304,f822]) ).
fof(f1527,plain,
epsilon_connected(sK73_skl),
inference(resolution,[status(thm)],[f304,f819]) ).
fof(f1528,plain,
epsilon_connected(sK71_skl),
inference(resolution,[status(thm)],[f304,f812]) ).
fof(f1530,plain,
( ordinal(sK80_skl)
| ~ epsilon_connected(sK80_skl) ),
inference(resolution,[status(thm)],[f846,f301]) ).
fof(f1531,definition,
( sQ24_spl
<=> epsilon_connected(sK80_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1533,plain,
( sQ24_spl
| ~ epsilon_connected(sK80_skl) ),
inference(component_clause,[status(thm)],[f1531]) ).
fof(f1534,definition,
( sQ25_spl
<=> ordinal(sK80_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1537,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1530,f1531,f1534]) ).
fof(f1545,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1452,f1434]) ).
fof(f1546,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1545]) ).
fof(f1547,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1445,f1435]) ).
fof(f1548,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1547]) ).
fof(f1557,plain,
! [X0] :
( relation_field(X0) = set_union2(relation_rng(X0),relation_dom(X0))
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f307,f588]) ).
fof(f1559,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1471,f823]) ).
fof(f1560,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f1559]) ).
fof(f1561,plain,
( ordinal(sK74_skl)
| ~ epsilon_connected(sK74_skl) ),
inference(resolution,[status(thm)],[f1521,f301]) ).
fof(f1562,definition,
( sQ26_spl
<=> epsilon_connected(sK74_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1564,plain,
( sQ26_spl
| ~ epsilon_connected(sK74_skl) ),
inference(component_clause,[status(thm)],[f1562]) ).
fof(f1565,definition,
( sQ27_spl
<=> ordinal(sK74_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1568,plain,
( sQ27_spl
| ~ sQ26_spl ),
inference(split_clause,[status(thm)],[f1561,f1562,f1565]) ).
fof(f1569,plain,
( ordinal(sK73_skl)
| ~ epsilon_connected(sK73_skl) ),
inference(resolution,[status(thm)],[f1522,f301]) ).
fof(f1570,definition,
( sQ28_spl
<=> epsilon_connected(sK73_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1572,plain,
( sQ28_spl
| ~ epsilon_connected(sK73_skl) ),
inference(component_clause,[status(thm)],[f1570]) ).
fof(f1573,definition,
( sQ29_spl
<=> ordinal(sK73_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1576,plain,
( sQ29_spl
| ~ sQ28_spl ),
inference(split_clause,[status(thm)],[f1569,f1570,f1573]) ).
fof(f1577,plain,
( ordinal(sK71_skl)
| ~ epsilon_connected(sK71_skl) ),
inference(resolution,[status(thm)],[f1523,f301]) ).
fof(f1578,definition,
( sQ30_spl
<=> epsilon_connected(sK71_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1580,plain,
( sQ30_spl
| ~ epsilon_connected(sK71_skl) ),
inference(component_clause,[status(thm)],[f1578]) ).
fof(f1581,definition,
( sQ31_spl
<=> ordinal(sK71_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1584,plain,
( sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f1577,f1578,f1581]) ).
fof(f1585,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1533,f847]) ).
fof(f1586,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1585]) ).
fof(f1597,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1564,f1526]) ).
fof(f1598,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1597]) ).
fof(f1599,plain,
( sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1572,f1527]) ).
fof(f1600,plain,
sQ28_spl,
inference(contradiction_clause,[status(thm)],[f1599]) ).
fof(f1601,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1580,f1528]) ).
fof(f1602,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1601]) ).
fof(f1631,plain,
! [X0,X1] :
( in(sK1_skl(X1,X0),relation_field(X0))
| ~ relation(X0)
| in(sK0_skl(X1,X0),X1)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f319,f1017]) ).
fof(f1632,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),relation_field(X0))
| ~ relation(X0)
| in(sK0_skl(X1,X0),X1)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f319,f1016]) ).
fof(f1633,plain,
! [X0] :
( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f319,f1348]) ).
fof(f1637,plain,
! [X0,X1] :
( in(sK1_skl(X1,X0),relation_field(X0))
| in(sK0_skl(X1,X0),X1)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1631]) ).
fof(f1638,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),relation_field(X0))
| in(sK0_skl(X1,X0),X1)
| X0 = identity_relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1632]) ).
fof(f1639,definition,
( sQ32_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f1641,plain,
( sQ32_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f1639]) ).
fof(f1642,definition,
! [X0] :
( sQ33_spl
<=> ( in(sK0_skl(X0,empty_set),X0)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1645,plain,
( sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1633,f1639,f1642]) ).
fof(f1646,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1641,f672]) ).
fof(f1647,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1646]) ).
fof(f1650,plain,
! [X0] :
( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0)
| ~ relation(empty_set) ),
inference(resolution,[status(thm)],[f320,f1348]) ).
fof(f1656,definition,
! [X0] :
( sQ34_spl
<=> ( sK0_skl(X0,empty_set) = sK1_skl(X0,empty_set)
| empty_set = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1659,plain,
( sQ34_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1650,f1639,f1656]) ).
fof(f1715,plain,
! [X0] : set_union2(empty_set,X0) = X0,
inference(paramodulation,[status(thm)],[f307,f965]) ).
fof(f1720,plain,
( relation_field(empty_set) = set_union2(relation_rng(empty_set),empty_set)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1163,f1557]) ).
fof(f1721,plain,
( relation_field(empty_set) = set_union2(empty_set,relation_rng(empty_set))
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1163,f588]) ).
fof(f1722,definition,
( sQ35_spl
<=> relation_field(empty_set) = set_union2(relation_rng(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f1723,plain,
( ~ sQ35_spl
| relation_field(empty_set) = set_union2(relation_rng(empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f1722]) ).
fof(f1725,plain,
( sQ35_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1720,f1639,f1722]) ).
fof(f1726,definition,
( sQ36_spl
<=> relation_field(empty_set) = set_union2(empty_set,relation_rng(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1729,plain,
( sQ36_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1721,f1639,f1726]) ).
fof(f1730,plain,
( ~ sQ35_spl
| relation_field(empty_set) = relation_rng(empty_set) ),
inference(forward_demodulation,[status(thm)],[f965,f1723]) ).
fof(f1731,plain,
( relation_field(empty_set) = set_union2(empty_set,relation_dom(empty_set))
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1164,f1557]) ).
fof(f1732,plain,
( relation_field(empty_set) = set_union2(relation_dom(empty_set),empty_set)
| ~ relation(empty_set) ),
inference(paramodulation,[status(thm)],[f1164,f588]) ).
fof(f1733,definition,
( sQ37_spl
<=> relation_field(empty_set) = set_union2(empty_set,relation_dom(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1734,plain,
( ~ sQ37_spl
| relation_field(empty_set) = set_union2(empty_set,relation_dom(empty_set)) ),
inference(component_clause,[status(thm)],[f1733]) ).
fof(f1736,plain,
( sQ37_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1731,f1639,f1733]) ).
fof(f1737,definition,
( sQ38_spl
<=> relation_field(empty_set) = set_union2(relation_dom(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1740,plain,
( sQ38_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f1732,f1639,f1737]) ).
fof(f1741,plain,
( ~ sQ37_spl
| relation_field(empty_set) = set_union2(empty_set,empty_set) ),
inference(forward_demodulation,[status(thm)],[f1163,f1734]) ).
fof(f1742,plain,
( ~ sQ37_spl
| relation_field(empty_set) = empty_set ),
inference(forward_demodulation,[status(thm)],[f965,f1741]) ).
fof(f1746,plain,
sK75_skl = empty_set,
inference(resolution,[status(thm)],[f1193,f828]) ).
fof(f1753,plain,
relation_dom(empty_set) = sK75_skl,
inference(backward_demodulation,[status(thm)],[f1746,f1163]) ).
fof(f1757,plain,
! [X0] : subset(sK75_skl,X0),
inference(backward_demodulation,[status(thm)],[f1746,f1013]) ).
fof(f1758,plain,
! [X0] : singleton(X0) != sK75_skl,
inference(backward_demodulation,[status(thm)],[f1746,f762]) ).
fof(f1759,plain,
! [X0] : ~ in(X0,sK75_skl),
inference(backward_demodulation,[status(thm)],[f1746,f1348]) ).
fof(f1769,plain,
relation_dom(sK75_skl) = sK75_skl,
inference(forward_demodulation,[status(thm)],[f1746,f1753]) ).
fof(f1791,plain,
( ~ sQ37_spl
| relation_field(sK75_skl) = empty_set ),
inference(forward_demodulation,[status(thm)],[f1746,f1742]) ).
fof(f1792,plain,
( ~ sQ37_spl
| relation_field(sK75_skl) = sK75_skl ),
inference(forward_demodulation,[status(thm)],[f1746,f1791]) ).
fof(f1793,plain,
! [X0] :
( ~ sQ37_spl
| in(sK0_skl(X0,sK75_skl),sK75_skl)
| in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1792,f1638]) ).
fof(f1794,plain,
! [X0] :
( ~ sQ37_spl
| in(sK1_skl(X0,sK75_skl),sK75_skl)
| in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1792,f1637]) ).
fof(f1795,plain,
( ~ sQ37_spl
| ~ is_reflexive_in(sK75_skl,sK75_skl)
| reflexive(sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1792,f637]) ).
fof(f1797,definition,
( sQ39_spl
<=> relation(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1799,plain,
( sQ39_spl
| ~ relation(sK75_skl) ),
inference(component_clause,[status(thm)],[f1797]) ).
fof(f1800,definition,
! [X0] :
( sQ40_spl
<=> ( in(sK0_skl(X0,sK75_skl),sK75_skl)
| in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1803,plain,
( ~ sQ37_spl
| sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1793,f1797,f1800,f1733]) ).
fof(f1804,definition,
! [X0] :
( sQ41_spl
<=> ( in(sK1_skl(X0,sK75_skl),sK75_skl)
| in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1807,plain,
( ~ sQ37_spl
| sQ41_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1794,f1797,f1804,f1733]) ).
fof(f1808,definition,
( sQ42_spl
<=> reflexive(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1811,definition,
( sQ43_spl
<=> is_reflexive_in(sK75_skl,sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1813,plain,
( sQ43_spl
| ~ is_reflexive_in(sK75_skl,sK75_skl) ),
inference(component_clause,[status(thm)],[f1811]) ).
fof(f1814,plain,
( ~ sQ37_spl
| ~ sQ43_spl
| sQ42_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1795,f1797,f1808,f1811,f1733]) ).
fof(f1816,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1799,f825]) ).
fof(f1817,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f1816]) ).
fof(f1820,plain,
( ~ sQ35_spl
| relation_field(sK75_skl) = relation_rng(empty_set) ),
inference(forward_demodulation,[status(thm)],[f1746,f1730]) ).
fof(f1821,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| sK75_skl = relation_rng(empty_set) ),
inference(forward_demodulation,[status(thm)],[f1792,f1820]) ).
fof(f1822,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| sK75_skl = relation_rng(sK75_skl) ),
inference(forward_demodulation,[status(thm)],[f1746,f1821]) ).
fof(f1823,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| relation_field(sK75_skl) = set_union2(sK75_skl,relation_dom(sK75_skl))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1822,f1557]) ).
fof(f1824,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| relation_field(sK75_skl) = set_union2(relation_dom(sK75_skl),sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1822,f588]) ).
fof(f1825,definition,
( sQ44_spl
<=> relation_field(sK75_skl) = set_union2(sK75_skl,relation_dom(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1828,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| sQ44_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1823,f1797,f1825,f1733,f1722]) ).
fof(f1829,definition,
( sQ45_spl
<=> relation_field(sK75_skl) = set_union2(relation_dom(sK75_skl),sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
( ~ sQ35_spl
| ~ sQ37_spl
| sQ45_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1824,f1797,f1829,f1733,f1722]) ).
fof(f1868,plain,
! [X0] :
( sK0_skl(X0,sK75_skl) = sK1_skl(X0,sK75_skl)
| sK75_skl = identity_relation(X0)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f1759,f320]) ).
fof(f1869,plain,
! [X0] :
( in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f1759,f319]) ).
fof(f1870,definition,
! [X0] :
( sQ46_spl
<=> ( sK0_skl(X0,sK75_skl) = sK1_skl(X0,sK75_skl)
| sK75_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1873,plain,
( sQ46_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1868,f1797,f1870]) ).
fof(f1874,definition,
! [X0] :
( sQ47_spl
<=> ( in(sK0_skl(X0,sK75_skl),X0)
| sK75_skl = identity_relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1877,plain,
( sQ47_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1869,f1797,f1874]) ).
fof(f1882,plain,
! [X0] :
( relation_field(identity_relation(X0)) = set_union2(X0,relation_dom(identity_relation(X0)))
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f1201,f1557]) ).
fof(f1884,plain,
! [X0] :
( relation_field(identity_relation(X0)) = set_union2(X0,X0)
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f1200,f1882]) ).
fof(f1885,plain,
! [X0] :
( relation_field(identity_relation(X0)) = X0
| ~ relation(identity_relation(X0)) ),
inference(forward_demodulation,[status(thm)],[f744,f1884]) ).
fof(f1886,plain,
! [X0] : relation_field(identity_relation(X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f1885,f650]) ).
fof(f1902,plain,
! [X0] : set_union2(sK75_skl,X0) = X0,
inference(forward_demodulation,[status(thm)],[f1746,f1715]) ).
fof(f1924,plain,
! [X0,X1,X2] :
( in(sK3_skl(X2,X1,X0),relation_field(X1))
| ~ relation(X1)
| in(sK2_skl(X2,X1,X0),X2)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f334,f1017]) ).
fof(f1925,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),relation_field(X1))
| ~ relation(X1)
| in(sK2_skl(X2,X1,X0),X2)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f334,f1016]) ).
fof(f1926,plain,
! [X0,X1] :
( in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f334,f1759]) ).
fof(f1934,plain,
! [X0,X1,X2] :
( in(sK3_skl(X2,X1,X0),relation_field(X1))
| in(sK2_skl(X2,X1,X0),X2)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1924]) ).
fof(f1935,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),relation_field(X1))
| in(sK2_skl(X2,X1,X0),X2)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1925]) ).
fof(f1936,definition,
! [X0,X1] :
( sQ48_spl
<=> ( in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f1939,plain,
( ~ sQ39_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1926,f1936,f1797]) ).
fof(f1954,plain,
! [X0] :
( ~ is_reflexive_in(identity_relation(X0),X0)
| reflexive(identity_relation(X0))
| ~ relation(identity_relation(X0)) ),
inference(paramodulation,[status(thm)],[f1886,f637]) ).
fof(f1968,plain,
! [X0] :
( ~ is_reflexive_in(identity_relation(X0),X0)
| reflexive(identity_relation(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1954,f650]) ).
fof(f1985,plain,
( relation_field(sK75_skl) = set_union2(relation_rng(sK75_skl),sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1769,f1557]) ).
fof(f1986,plain,
( relation_field(sK75_skl) = set_union2(sK75_skl,relation_rng(sK75_skl))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1769,f588]) ).
fof(f1987,definition,
( sQ49_spl
<=> relation_field(sK75_skl) = set_union2(relation_rng(sK75_skl),sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1990,plain,
( sQ49_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1985,f1797,f1987]) ).
fof(f1991,definition,
( sQ50_spl
<=> relation_field(sK75_skl) = set_union2(sK75_skl,relation_rng(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1994,plain,
( sQ50_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f1986,f1797,f1991]) ).
fof(f2030,plain,
! [X0,X1,X2] :
( in(sK3_skl(X2,X1,X0),relation_field(X1))
| ~ relation(X1)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f335,f1017]) ).
fof(f2031,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),relation_field(X1))
| ~ relation(X1)
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f335,f1016]) ).
fof(f2032,plain,
! [X0,X1] :
( in(ordered_pair(sK2_skl(X1,sK75_skl,X0),sK3_skl(X1,sK75_skl,X0)),X0)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f335,f1759]) ).
fof(f2041,plain,
! [X0,X1,X2] :
( in(sK3_skl(X2,X1,X0),relation_field(X1))
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2030]) ).
fof(f2042,plain,
! [X0,X1,X2] :
( in(sK2_skl(X2,X1,X0),relation_field(X1))
| in(ordered_pair(sK2_skl(X2,X1,X0),sK3_skl(X2,X1,X0)),X0)
| X1 = relation_dom_restriction(X0,X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2031]) ).
fof(f2043,definition,
! [X0,X1] :
( sQ51_spl
<=> ( in(ordered_pair(sK2_skl(X1,sK75_skl,X0),sK3_skl(X1,sK75_skl,X0)),X0)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f2046,plain,
( ~ sQ39_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f2032,f2043,f1797]) ).
fof(f2100,plain,
! [X0] : set_difference(sK75_skl,X0) = empty_set,
inference(forward_demodulation,[status(thm)],[f1746,f1123]) ).
fof(f2101,plain,
! [X0] : set_difference(sK75_skl,X0) = sK75_skl,
inference(forward_demodulation,[status(thm)],[f1746,f2100]) ).
fof(f2319,definition,
( sQ52_spl
<=> empty(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f2321,plain,
( sQ52_spl
| ~ empty(sK75_skl) ),
inference(component_clause,[status(thm)],[f2319]) ).
fof(f2326,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2321,f828]) ).
fof(f2327,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f2326]) ).
fof(f2350,plain,
! [X0,X1] :
( in(sK8_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_rng_restriction(X1,X0)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f354,f1759]) ).
fof(f2364,definition,
! [X0,X1] :
( sQ53_spl
<=> ( in(sK8_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_rng_restriction(X1,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f2367,plain,
( ~ sQ39_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f2350,f2364,f1797]) ).
fof(f2377,plain,
! [X0,X1] :
( in(ordered_pair(sK7_skl(X1,sK75_skl,X0),sK8_skl(X1,sK75_skl,X0)),X0)
| sK75_skl = relation_rng_restriction(X1,X0)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f355,f1759]) ).
fof(f2391,definition,
! [X0,X1] :
( sQ54_spl
<=> ( in(ordered_pair(sK7_skl(X1,sK75_skl,X0),sK8_skl(X1,sK75_skl,X0)),X0)
| sK75_skl = relation_rng_restriction(X1,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2394,plain,
( ~ sQ39_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f2377,f2391,f1797]) ).
fof(f2550,plain,
powerset(sK75_skl) = singleton(empty_set),
inference(forward_demodulation,[status(thm)],[f1746,f971]) ).
fof(f2551,plain,
powerset(sK75_skl) = singleton(sK75_skl),
inference(forward_demodulation,[status(thm)],[f1746,f2550]) ).
fof(f2558,plain,
powerset(sK75_skl) != sK75_skl,
inference(paramodulation,[status(thm)],[f2551,f1758]) ).
fof(f2753,definition,
( sQ55_spl
<=> sK75_skl = sK75_skl ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f2768,definition,
( sQ56_spl
<=> epsilon_transitive(sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f2777,plain,
! [X0,X1] :
( in(sK9_skl(X0,X1,sK75_skl),sK75_skl)
| in(sK9_skl(X0,X1,sK75_skl),X0)
| X0 = relation_inverse_image(sK75_skl,X1)
| ~ function(sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f1769,f364]) ).
fof(f2779,definition,
! [X0,X1] :
( sQ57_spl
<=> ( in(sK9_skl(X0,X1,sK75_skl),sK75_skl)
| in(sK9_skl(X0,X1,sK75_skl),X0)
| X0 = relation_inverse_image(sK75_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f2782,plain,
( sQ57_spl
| ~ sQ16_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f2777,f1797,f1479,f2779]) ).
fof(f2807,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ relation(X0)
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f1333,f1017]) ).
fof(f2812,plain,
! [X0,X1] :
( ~ in(X0,relation_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f1333,f1759]) ).
fof(f2827,plain,
! [X0,X1,X2] :
( in(X1,relation_field(X0))
| ~ in(X1,relation_image(X0,X2))
| ~ relation(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2807]) ).
fof(f2829,definition,
! [X0,X1] :
( sQ58_spl
<=> ~ in(X0,relation_image(sK75_skl,X1)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f2830,plain,
! [X0,X1] :
( ~ sQ58_spl
| ~ in(X0,relation_image(sK75_skl,X1)) ),
inference(component_clause,[status(thm)],[f2829]) ).
fof(f2832,plain,
( sQ58_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f2812,f1797,f2829]) ).
fof(f3010,plain,
! [X0,X1] :
( ~ sQ37_spl
| in(sK3_skl(X1,sK75_skl,X0),sK75_skl)
| in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f1792,f1934]) ).
fof(f3012,definition,
! [X0,X1] :
( sQ59_spl
<=> ( in(sK3_skl(X1,sK75_skl,X0),sK75_skl)
| in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f3015,plain,
( ~ sQ37_spl
| ~ sQ39_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f3010,f3012,f1797,f1733]) ).
fof(f3023,plain,
! [X0,X1] :
( ~ sQ37_spl
| in(sK2_skl(X1,sK75_skl,X0),sK75_skl)
| in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(sK75_skl)
| ~ relation(X0) ),
inference(paramodulation,[status(thm)],[f1792,f1935]) ).
fof(f3025,definition,
! [X0,X1] :
( sQ60_spl
<=> ( in(sK2_skl(X1,sK75_skl,X0),sK75_skl)
| in(sK2_skl(X1,sK75_skl,X0),X1)
| sK75_skl = relation_dom_restriction(X0,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f3028,plain,
( ~ sQ37_spl
| ~ sQ39_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f3023,f3025,f1797,f1733]) ).
fof(f3052,plain,
! [X0,X1] :
( in(sK11_skl(X0,X1,sK75_skl),X0)
| X0 = relation_image(sK75_skl,X1)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f374,f1759]) ).
fof(f3069,definition,
! [X0,X1] :
( sQ61_spl
<=> ( in(sK11_skl(X0,X1,sK75_skl),X0)
| X0 = relation_image(sK75_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f3072,plain,
( sQ61_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3052,f1797,f3069]) ).
fof(f3100,plain,
! [X0,X1] :
( ~ in(X0,relation_inverse_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f1336,f1759]) ).
fof(f3118,definition,
! [X0,X1] :
( sQ62_spl
<=> ~ in(X0,relation_inverse_image(sK75_skl,X1)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f3119,plain,
! [X0,X1] :
( ~ sQ62_spl
| ~ in(X0,relation_inverse_image(sK75_skl,X1)) ),
inference(component_clause,[status(thm)],[f3118]) ).
fof(f3121,plain,
( sQ62_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3100,f1797,f3118]) ).
fof(f3195,plain,
succ(sK75_skl) = singleton(sK75_skl),
inference(paramodulation,[status(thm)],[f1902,f396]) ).
fof(f3200,plain,
succ(sK75_skl) = powerset(sK75_skl),
inference(forward_demodulation,[status(thm)],[f2551,f3195]) ).
fof(f3206,plain,
( ordinal(powerset(sK75_skl))
| ~ ordinal(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3200,f711]) ).
fof(f3207,plain,
( epsilon_connected(powerset(sK75_skl))
| ~ ordinal(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3200,f710]) ).
fof(f3208,plain,
( epsilon_transitive(powerset(sK75_skl))
| ~ ordinal(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3200,f709]) ).
fof(f3219,definition,
( sQ63_spl
<=> ordinal(powerset(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f3222,plain,
( sQ63_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3206,f1496,f3219]) ).
fof(f3223,definition,
( sQ64_spl
<=> epsilon_connected(powerset(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3226,plain,
( sQ64_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3207,f1496,f3223]) ).
fof(f3227,definition,
( sQ65_spl
<=> epsilon_transitive(powerset(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f3230,plain,
( sQ65_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f3208,f1496,f3227]) ).
fof(f3378,plain,
! [X0] :
( in(sK25_skl(X0),X0)
| X0 = sK75_skl ),
inference(forward_demodulation,[status(thm)],[f1746,f434]) ).
fof(f3380,plain,
! [X0] :
( ~ sQ58_spl
| relation_image(sK75_skl,X0) = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f2830]) ).
fof(f3382,plain,
! [X0] :
( ~ sQ62_spl
| relation_inverse_image(sK75_skl,X0) = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f3119]) ).
fof(f3386,plain,
! [X0] :
( sK25_skl(singleton(X0)) = X0
| singleton(X0) = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f1346]) ).
fof(f3392,plain,
! [X0] :
( element(sK25_skl(X0),X0)
| X0 = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f967]) ).
fof(f3394,plain,
! [X0,X1] :
( ~ in(X1,sK25_skl(X0))
| ~ in(X0,X1)
| X0 = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f1074]) ).
fof(f3396,plain,
! [X0] :
( ~ in(X0,sK25_skl(X0))
| X0 = sK75_skl ),
inference(resolution,[status(thm)],[f3378,f286]) ).
fof(f3397,plain,
! [X0] : sK25_skl(singleton(X0)) = X0,
inference(forward_subsumption_resolution,[status(thm)],[f3386,f1758]) ).
fof(f3398,plain,
sK25_skl(powerset(sK75_skl)) = sK75_skl,
inference(paramodulation,[status(thm)],[f2551,f3397]) ).
fof(f3402,plain,
! [X0] :
( ~ sQ58_spl
| in(X0,relation_field(sK75_skl))
| ~ in(X0,sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3380,f2827]) ).
fof(f3403,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(sK10_skl(X0,sK75_skl,X1,sK75_skl),X1)
| ~ in(X0,relation_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3380,f1334]) ).
fof(f3405,plain,
! [X0,X1] :
( ~ sQ58_spl
| in(ordered_pair(sK10_skl(X0,sK75_skl,X1,sK75_skl),X0),sK75_skl)
| ~ in(X0,relation_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3380,f1333]) ).
fof(f3406,plain,
! [X0,X1] :
( ~ sQ58_spl
| sP0_prd(sK4_skl(X0,sK75_skl,X1,sK75_skl),X0,X1,sK75_skl)
| ~ in(X0,relation_image(sK75_skl,X1))
| ~ function(sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3380,f1325]) ).
fof(f3407,definition,
! [X0] :
( sQ66_spl
<=> ( in(X0,relation_field(sK75_skl))
| ~ in(X0,sK75_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f3410,plain,
( ~ sQ58_spl
| sQ66_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3402,f1797,f3407,f2829]) ).
fof(f3411,definition,
! [X0,X1] :
( sQ67_spl
<=> ( in(sK10_skl(X0,sK75_skl,X1,sK75_skl),X1)
| ~ in(X0,relation_image(sK75_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f3414,plain,
( ~ sQ58_spl
| sQ67_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3403,f1797,f3411,f2829]) ).
fof(f3419,definition,
! [X0,X1] :
( sQ69_spl
<=> ( in(ordered_pair(sK10_skl(X0,sK75_skl,X1,sK75_skl),X0),sK75_skl)
| ~ in(X0,relation_image(sK75_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f3422,plain,
( ~ sQ58_spl
| sQ69_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3405,f1797,f3419,f2829]) ).
fof(f3423,definition,
! [X0,X1] :
( sQ70_spl
<=> ( sP0_prd(sK4_skl(X0,sK75_skl,X1,sK75_skl),X0,X1,sK75_skl)
| ~ in(X0,relation_image(sK75_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3426,plain,
( ~ sQ58_spl
| sQ70_spl
| ~ sQ16_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3406,f1797,f1479,f3423,f2829]) ).
fof(f3433,plain,
! [X0,X1] :
( ~ sQ62_spl
| in(sK13_skl(X0,sK75_skl,X1,sK75_skl),X1)
| ~ in(X0,relation_inverse_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3382,f1337]) ).
fof(f3435,plain,
! [X0,X1] :
( ~ sQ62_spl
| in(ordered_pair(X0,sK13_skl(X0,sK75_skl,X1,sK75_skl)),sK75_skl)
| ~ in(X0,relation_inverse_image(sK75_skl,X1))
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3382,f1336]) ).
fof(f3436,plain,
! [X0,X1] :
( ~ sQ62_spl
| in(apply(sK75_skl,X0),X1)
| ~ in(X0,sK75_skl)
| ~ function(sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3382,f1331]) ).
fof(f3437,plain,
! [X0] :
( ~ sQ62_spl
| in(X0,relation_dom(sK75_skl))
| ~ in(X0,sK75_skl)
| ~ function(sK75_skl)
| ~ relation(sK75_skl) ),
inference(paramodulation,[status(thm)],[f3382,f1330]) ).
fof(f3438,definition,
! [X0,X1] :
( sQ71_spl
<=> ( in(sK13_skl(X0,sK75_skl,X1,sK75_skl),X1)
| ~ in(X0,relation_inverse_image(sK75_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f3441,plain,
( ~ sQ62_spl
| sQ71_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3433,f1797,f3438,f3118]) ).
fof(f3443,definition,
! [X0,X1] :
( sQ72_spl
<=> ( in(ordered_pair(X0,sK13_skl(X0,sK75_skl,X1,sK75_skl)),sK75_skl)
| ~ in(X0,relation_inverse_image(sK75_skl,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f3446,plain,
( ~ sQ62_spl
| sQ72_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3435,f1797,f3443,f3118]) ).
fof(f3447,definition,
! [X0,X1] :
( sQ73_spl
<=> ( in(apply(sK75_skl,X0),X1)
| ~ in(X0,sK75_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f3450,plain,
( ~ sQ62_spl
| sQ73_spl
| ~ sQ16_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3436,f1797,f1479,f3447,f3118]) ).
fof(f3451,definition,
! [X0] :
( sQ74_spl
<=> ( in(X0,relation_dom(sK75_skl))
| ~ in(X0,sK75_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f3454,plain,
( ~ sQ62_spl
| sQ74_spl
| ~ sQ16_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3437,f1797,f1479,f3451,f3118]) ).
fof(f3457,plain,
( in(sK75_skl,powerset(sK75_skl))
| powerset(sK75_skl) = sK75_skl ),
inference(paramodulation,[status(thm)],[f3398,f3378]) ).
fof(f3458,definition,
( sQ75_spl
<=> powerset(sK75_skl) = sK75_skl ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f3459,plain,
( ~ sQ75_spl
| powerset(sK75_skl) = sK75_skl ),
inference(component_clause,[status(thm)],[f3458]) ).
fof(f3461,definition,
( sQ76_spl
<=> in(sK75_skl,powerset(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f3464,plain,
( sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f3457,f3458,f3461]) ).
fof(f3465,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3459,f2558]) ).
fof(f3466,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f3465]) ).
fof(f3578,plain,
! [X0,X1] :
( in(sK14_skl(X0,X1,sK75_skl),X0)
| X0 = relation_inverse_image(sK75_skl,X1)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f384,f1759]) ).
fof(f3592,definition,
! [X0,X1] :
( sQ78_spl
<=> ( in(sK14_skl(X0,X1,sK75_skl),X0)
| X0 = relation_inverse_image(sK75_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f3595,plain,
( sQ78_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3578,f1797,f3592]) ).
fof(f3679,plain,
( ~ in(powerset(sK75_skl),sK75_skl)
| powerset(sK75_skl) = sK75_skl ),
inference(paramodulation,[status(thm)],[f3398,f3396]) ).
fof(f3681,definition,
( sQ79_spl
<=> in(powerset(sK75_skl),sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f3684,plain,
( ~ sQ79_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f3679,f3458,f3681]) ).
fof(f3705,plain,
! [X0] :
( ~ in(X0,sK75_skl)
| ~ in(powerset(sK75_skl),X0)
| powerset(sK75_skl) = sK75_skl ),
inference(paramodulation,[status(thm)],[f3398,f3394]) ).
fof(f3707,definition,
! [X0] :
( sQ80_spl
<=> ( ~ in(X0,sK75_skl)
| ~ in(powerset(sK75_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f3710,plain,
( sQ80_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f3705,f3458,f3707]) ).
fof(f3808,definition,
! [X0] :
( sQ81_spl
<=> ~ subset(sK75_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f3809,plain,
! [X0] :
( ~ sQ81_spl
| ~ subset(sK75_skl,X0) ),
inference(component_clause,[status(thm)],[f3808]) ).
fof(f3812,plain,
( ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3809,f1757]) ).
fof(f3813,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f3812]) ).
fof(f3836,definition,
! [X0] :
( sQ82_spl
<=> ~ disjoint(sK75_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f3837,plain,
! [X0] :
( ~ sQ82_spl
| ~ disjoint(sK75_skl,X0) ),
inference(component_clause,[status(thm)],[f3836]) ).
fof(f3840,plain,
! [X0] : disjoint(sK75_skl,X0),
inference(resolution,[status(thm)],[f1223,f2101]) ).
fof(f3843,plain,
! [X0] :
( sK75_skl != sK75_skl
| disjoint(sK75_skl,X0) ),
inference(paramodulation,[status(thm)],[f2101,f1223]) ).
fof(f3845,plain,
( ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3840,f3837]) ).
fof(f3846,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f3845]) ).
fof(f3847,definition,
! [X0] :
( sQ83_spl
<=> disjoint(sK75_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f3850,plain,
( ~ sQ55_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f3843,f3847,f2753]) ).
fof(f4031,plain,
! [X0,X1] :
( in(sK3_skl(X1,X0,sK75_skl),relation_field(X0))
| X0 = relation_dom_restriction(sK75_skl,X1)
| ~ relation(X0)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f2041,f1759]) ).
fof(f4046,definition,
! [X0,X1] :
( sQ84_spl
<=> ( in(sK3_skl(X1,X0,sK75_skl),relation_field(X0))
| X0 = relation_dom_restriction(sK75_skl,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f4049,plain,
( sQ84_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f4031,f1797,f4046]) ).
fof(f4116,plain,
( element(sK75_skl,powerset(sK75_skl))
| powerset(sK75_skl) = sK75_skl ),
inference(paramodulation,[status(thm)],[f3398,f3392]) ).
fof(f4118,definition,
( sQ85_spl
<=> element(sK75_skl,powerset(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f4121,plain,
( sQ85_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f4116,f3458,f4118]) ).
fof(f4129,plain,
! [X0] :
( sQ3_spl
| ~ in(sK67_skl,X0)
| ~ is_reflexive_in(sK66_skl,X0)
| ~ relation(sK66_skl) ),
inference(resolution,[status(thm)],[f408,f1308]) ).
fof(f4155,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ is_reflexive_in(sK75_skl,X0)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f408,f1759]) ).
fof(f4174,definition,
! [X0] :
( sQ86_spl
<=> ( ~ in(sK67_skl,X0)
| ~ is_reflexive_in(sK66_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f4175,plain,
! [X0] :
( ~ sQ86_spl
| ~ in(sK67_skl,X0)
| ~ is_reflexive_in(sK66_skl,X0) ),
inference(component_clause,[status(thm)],[f4174]) ).
fof(f4177,plain,
( sQ3_spl
| sQ86_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4129,f1419,f4174,f1306]) ).
fof(f4184,definition,
! [X0,X1] :
( sQ87_spl
<=> ( ~ in(X1,X0)
| ~ is_reflexive_in(sK75_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f4185,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ in(X1,X0)
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(component_clause,[status(thm)],[f4184]) ).
fof(f4187,plain,
( sQ87_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f4155,f1797,f4184]) ).
fof(f4190,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1421,f758]) ).
fof(f4191,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f4190]) ).
fof(f4192,plain,
( ~ sQ2_spl
| ~ sQ86_spl
| ~ is_reflexive_in(sK66_skl,relation_field(sK66_skl)) ),
inference(resolution,[status(thm)],[f4175,f1303]) ).
fof(f4212,plain,
( ~ sQ2_spl
| ~ sQ86_spl
| ~ reflexive(sK66_skl)
| ~ relation(sK66_skl) ),
inference(resolution,[status(thm)],[f4192,f636]) ).
fof(f4213,plain,
( ~ sQ2_spl
| ~ sQ86_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4212,f1419,f1295,f4174,f1302]) ).
fof(f4244,definition,
! [X0] :
( sQ92_spl
<=> ~ in(X0,relation_field(sK66_skl)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f4245,plain,
! [X0] :
( ~ sQ92_spl
| ~ in(X0,relation_field(sK66_skl)) ),
inference(component_clause,[status(thm)],[f4244]) ).
fof(f4260,plain,
( ~ sQ92_spl
| relation_field(sK66_skl) = sK75_skl ),
inference(resolution,[status(thm)],[f4245,f3378]) ).
fof(f4363,plain,
( ~ sQ92_spl
| ~ is_reflexive_in(sK66_skl,sK75_skl)
| reflexive(sK66_skl)
| ~ relation(sK66_skl) ),
inference(paramodulation,[status(thm)],[f4260,f637]) ).
fof(f4381,definition,
( sQ116_spl
<=> is_reflexive_in(sK66_skl,sK75_skl) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f4383,plain,
( sQ116_spl
| ~ is_reflexive_in(sK66_skl,sK75_skl) ),
inference(component_clause,[status(thm)],[f4381]) ).
fof(f4384,plain,
( ~ sQ92_spl
| ~ sQ116_spl
| sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4363,f1419,f1295,f4381,f4244]) ).
fof(f4442,plain,
! [X0,X1] :
( in(sK2_skl(X1,X0,sK75_skl),relation_field(X0))
| X0 = relation_dom_restriction(sK75_skl,X1)
| ~ relation(X0)
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f2042,f1759]) ).
fof(f4458,definition,
! [X0,X1] :
( sQ117_spl
<=> ( in(sK2_skl(X1,X0,sK75_skl),relation_field(X0))
| X0 = relation_dom_restriction(sK75_skl,X1)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f4461,plain,
( sQ117_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f4442,f1797,f4458]) ).
fof(f4516,plain,
! [X0] :
( is_reflexive_in(X0,sK75_skl)
| ~ relation(X0) ),
inference(resolution,[status(thm)],[f409,f1759]) ).
fof(f4626,definition,
( sQ119_spl
<=> ordinal(relation_field(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f4633,definition,
( sQ120_spl
<=> epsilon_connected(relation_field(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f4640,definition,
( sQ121_spl
<=> epsilon_transitive(relation_field(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f4647,definition,
( sQ122_spl
<=> relation_field(sK75_skl) = sK75_skl ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f4653,definition,
( sQ123_spl
<=> relation(relation_field(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f4667,plain,
( sQ116_spl
| ~ relation(sK66_skl) ),
inference(resolution,[status(thm)],[f4516,f4383]) ).
fof(f4668,plain,
( reflexive(identity_relation(sK75_skl))
| ~ relation(identity_relation(sK75_skl)) ),
inference(resolution,[status(thm)],[f4516,f1968]) ).
fof(f4674,plain,
( sQ116_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f4667,f1419,f4381]) ).
fof(f4675,definition,
( sQ124_spl
<=> relation(identity_relation(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f4677,plain,
( sQ124_spl
| ~ relation(identity_relation(sK75_skl)) ),
inference(component_clause,[status(thm)],[f4675]) ).
fof(f4678,definition,
( sQ125_spl
<=> reflexive(identity_relation(sK75_skl)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f4681,plain,
( sQ125_spl
| ~ sQ124_spl ),
inference(split_clause,[status(thm)],[f4668,f4675,f4678]) ).
fof(f4682,plain,
( sQ124_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4677,f650]) ).
fof(f4683,plain,
sQ124_spl,
inference(contradiction_clause,[status(thm)],[f4682]) ).
fof(f4685,plain,
! [X0] :
( ~ sQ87_spl
| ordinal(X0)
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(resolution,[status(thm)],[f4185,f1020]) ).
fof(f4687,plain,
! [X0] :
( ~ sQ87_spl
| epsilon_connected(X0)
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(resolution,[status(thm)],[f4185,f497]) ).
fof(f4689,plain,
! [X0] :
( ~ sQ87_spl
| epsilon_transitive(X0)
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(resolution,[status(thm)],[f4185,f447]) ).
fof(f4690,plain,
! [X0] :
( ~ sQ87_spl
| X0 = sK75_skl
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(resolution,[status(thm)],[f4185,f3378]) ).
fof(f4692,plain,
! [X0] :
( ~ sQ87_spl
| relation(X0)
| ~ is_reflexive_in(sK75_skl,X0) ),
inference(resolution,[status(thm)],[f4185,f402]) ).
fof(f4739,plain,
( ~ sQ87_spl
| ~ reflexive(sK75_skl)
| ~ relation(sK75_skl)
| ordinal(relation_field(sK75_skl)) ),
inference(resolution,[status(thm)],[f4685,f636]) ).
fof(f4741,plain,
( ~ sQ87_spl
| ~ sQ42_spl
| ~ sQ39_spl
| sQ119_spl ),
inference(split_clause,[status(thm)],[f4739,f4626,f1797,f1808,f4184]) ).
fof(f4742,plain,
( sQ43_spl
| ~ relation(sK75_skl) ),
inference(resolution,[status(thm)],[f1813,f4516]) ).
fof(f4743,plain,
( sQ43_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f4742,f1797,f1811]) ).
fof(f4791,plain,
! [X0] :
( ~ sQ1_spl
| is_reflexive_in(sK66_skl,X0)
| ~ relation(sK66_skl)
| ~ in(sK20_skl(X0,sK66_skl),relation_field(sK66_skl)) ),
inference(resolution,[status(thm)],[f1299,f410]) ).
fof(f4805,definition,
! [X0] :
( sQ129_spl
<=> ( is_reflexive_in(sK66_skl,X0)
| ~ in(sK20_skl(X0,sK66_skl),relation_field(sK66_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f4806,plain,
! [X0] :
( ~ sQ129_spl
| is_reflexive_in(sK66_skl,X0)
| ~ in(sK20_skl(X0,sK66_skl),relation_field(sK66_skl)) ),
inference(component_clause,[status(thm)],[f4805]) ).
fof(f4808,plain,
( ~ sQ1_spl
| ~ sQ6_spl
| sQ129_spl ),
inference(split_clause,[status(thm)],[f4791,f4805,f1419,f1298]) ).
fof(f4973,plain,
( ~ sQ87_spl
| ~ reflexive(sK75_skl)
| ~ relation(sK75_skl)
| epsilon_connected(relation_field(sK75_skl)) ),
inference(resolution,[status(thm)],[f4687,f636]) ).
fof(f4975,plain,
( ~ sQ87_spl
| ~ sQ42_spl
| ~ sQ39_spl
| sQ120_spl ),
inference(split_clause,[status(thm)],[f4973,f4633,f1797,f1808,f4184]) ).
fof(f4977,plain,
( ~ sQ87_spl
| ~ relation(sK75_skl)
| epsilon_transitive(sK75_skl) ),
inference(resolution,[status(thm)],[f4689,f4516]) ).
fof(f4978,plain,
( ~ sQ87_spl
| ~ reflexive(sK75_skl)
| ~ relation(sK75_skl)
| epsilon_transitive(relation_field(sK75_skl)) ),
inference(resolution,[status(thm)],[f4689,f636]) ).
fof(f4979,plain,
( ~ sQ87_spl
| ~ sQ39_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f4977,f2768,f1797,f4184]) ).
fof(f4980,plain,
( ~ sQ87_spl
| ~ sQ42_spl
| ~ sQ39_spl
| sQ121_spl ),
inference(split_clause,[status(thm)],[f4978,f4640,f1797,f1808,f4184]) ).
fof(f4982,plain,
( ~ sQ87_spl
| ~ relation(sK75_skl)
| sK75_skl = sK75_skl ),
inference(resolution,[status(thm)],[f4690,f4516]) ).
fof(f4983,plain,
( ~ sQ87_spl
| ~ reflexive(sK75_skl)
| ~ relation(sK75_skl)
| relation_field(sK75_skl) = sK75_skl ),
inference(resolution,[status(thm)],[f4690,f636]) ).
fof(f4984,plain,
( ~ sQ87_spl
| ~ sQ39_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f4982,f2753,f1797,f4184]) ).
fof(f4985,plain,
( ~ sQ87_spl
| ~ sQ42_spl
| ~ sQ39_spl
| sQ122_spl ),
inference(split_clause,[status(thm)],[f4983,f4647,f1797,f1808,f4184]) ).
fof(f4988,plain,
( ~ sQ87_spl
| ~ reflexive(sK75_skl)
| ~ relation(sK75_skl)
| relation(relation_field(sK75_skl)) ),
inference(resolution,[status(thm)],[f4692,f636]) ).
fof(f4990,plain,
( ~ sQ87_spl
| ~ sQ42_spl
| ~ sQ39_spl
| sQ123_spl ),
inference(split_clause,[status(thm)],[f4988,f4653,f1797,f1808,f4184]) ).
fof(f5141,plain,
( ~ sQ129_spl
| is_reflexive_in(sK66_skl,relation_field(sK66_skl))
| ~ relation(sK66_skl)
| is_reflexive_in(sK66_skl,relation_field(sK66_skl)) ),
inference(resolution,[status(thm)],[f4806,f409]) ).
fof(f5142,definition,
( sQ131_spl
<=> is_reflexive_in(sK66_skl,relation_field(sK66_skl)) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f5143,plain,
( ~ sQ131_spl
| is_reflexive_in(sK66_skl,relation_field(sK66_skl)) ),
inference(component_clause,[status(thm)],[f5142]) ).
fof(f5145,plain,
( ~ sQ129_spl
| ~ sQ6_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f5141,f5142,f1419,f4805]) ).
fof(f5146,plain,
( ~ sQ131_spl
| reflexive(sK66_skl)
| ~ relation(sK66_skl) ),
inference(resolution,[status(thm)],[f5143,f637]) ).
fof(f5147,plain,
( ~ sQ131_spl
| sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f5146,f1419,f1295,f5142]) ).
fof(f5148,plain,
$false,
inference(sat_refutation,[status(thm)],[f1301,f1305,f1309,f1449,f1456,f1463,f1465,f1475,f1485,f1487,f1499,f1506,f1513,f1515,f1517,f1519,f1537,f1546,f1548,f1560,f1568,f1576,f1584,f1586,f1598,f1600,f1602,f1645,f1647,f1659,f1725,f1729,f1736,f1740,f1803,f1807,f1814,f1817,f1828,f1832,f1873,f1877,f1939,f1990,f1994,f2046,f2327,f2367,f2394,f2782,f2832,f3015,f3028,f3072,f3121,f3222,f3226,f3230,f3410,f3414,f3422,f3426,f3441,f3446,f3450,f3454,f3464,f3466,f3595,f3684,f3710,f3813,f3846,f3850,f4049,f4121,f4177,f4187,f4191,f4213,f4384,f4461,f4674,f4681,f4683,f4741,f4743,f4808,f4975,f4979,f4980,f4984,f4985,f4990,f5145,f5147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU239+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:05:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 3.88/1.00 % Refutation found
% 3.88/1.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.88/1.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.38/1.02 % Elapsed time: 0.639568 seconds
% 2.38/1.02 % CPU time: 4.730383 seconds
% 2.38/1.02 % Total memory used: 178.292 MB
% 2.38/1.02 % Net memory used: 169.852 MB
%------------------------------------------------------------------------------